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.

Bimolecular

To clarify/confirm, n - x = n is a hypothesis and (n - x) + x = n + x is the current goal, correct? – Syringomyelia

Yes, that is correct – Bimolecular

You can apply the lemma f_equal. – Quattrocento

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.

Pouf

In that case, how do I rewrite onto only one side of an equation? – Bimolecular

One can also combine pattern n at 2. rewrite <- H. into rewrite <- H at 2. – Molnar

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).

Molnar

Remark that apply f_equal with (f := fun t => t + x). can also be used on the goal. – Umbilicus

Is there a version of f_equal that works for Setoids? – Perplex

@Perplex To be able to prove the analogous lemma, we must have f proper, but to prove f is Proper we need the lemma. Vicious circle :) Btw, there is a tactic called f_equiv, which is a setoid analogue of the f_equal tactic -- can be useful to do "backward reasoning". – Molnar

Answer 3

There is a powerful search engine in Coq using patterns. You can try for example:

Search (_=_ -> _+_=_+_).

Umbilicus