How to add to both sides of an equality in Coq

Question

This seems like a really simple question, but I wasn't able to find anything useful.

I have the statement

n - x = n

and would like to prove

(n - x) + x = n + x

I haven't been able to find what theorem allows for this.

Answer 1

You should have a look at the rewrite tactic (and then maybe reflexivity).

EDIT: more info about rewrite:

• You can rewrite H rewrite -> H to rewrite from left to right
• You can rewrite <- H to rewrite from right to left

• You can use the pattern tactic to only select specific instances of the goal to rewrite. For example, to only rewrite the second n, you can perform the following steps

  pattern n at 2. rewrite <- H.

In your case, the solution is much simpler.

Answer 2

Building on @gallais' suggestion on using f_equal. We start in the following state:

n : nat
x : nat
H : n - x = n
============================
 n - x + x = n + x

(1) First variant via "forward" reasoning (where one applies theorems to hypotheses) using the f_equal lemma.

Check f_equal.
f_equal
 : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

It needs the function f, so

apply f_equal with (f := fun t => t + x) in H.

This will give you:

H : n - x + x = n + x

This can be solved via apply H. or exact H. or assumption. or auto. ... or some other way which suits you the most.

(2) Or you can use "backward" reasoning (where one applies theorems to the goal). There is also the f_equal2 lemma:

Check f_equal2.
f_equal2
 : forall (A1 A2 B : Type) (f : A1 -> A2 -> B) 
     (x1 y1 : A1) (x2 y2 : A2),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2

We just apply it to the goal, which results in two trivial subgoals.

apply f_equal2. assumption. reflexivity.

or just

apply f_equal2; trivial.

(3) There is also the more specialized lemma f_equal2_plus:

Check f_equal2_plus.
(*
f_equal2_plus
  : forall x1 y1 x2 y2 : nat,
    x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
*)

Using this lemma we are able to solve the goal with the following one-liner:

apply (f_equal2_plus _ _ _ _ H eq_refl).