Coq proof tactics

Question

I am a beginner at Coq proof system (about 4 days). I've tried hard, but I am not able to prove the following.

forall a b c : nat, S (S (a + b)) = S (S (a + c)) -> b = c.

As far as I know, we need to prove the bijectivity of +, so that we can somehow use f(b) = f(c) -> b = c. How do I do this ?

Answer 1

Using SearchAbout plus or SearchPattern (_ + _ = _ + _ -> _) you could check the available lemmas about +. But if you didn't import the correct modules, that could be useless. What I usually do is that I go look at the online documentation. Here is the documentation for plus and you could have a particular look to plus_reg_l and plus_reg_r.

Answer 2

As pointed out in Vinz's answer, you can find the bijectivity theorem about plus directly in the Coq standard library. You can also prove it directly using primitive tactics and mathematical induction on a as follows.

Theorem plus_l_bij: forall a b c : nat, a + b = a + c -> b = c.
Proof.
induction a as [|a'].
  intros b c H. apply H.
  intros b c H. simpl plus in H. inversion H. apply IHa' in H1. apply H1.
Qed.

After induction a, the base case a = 0 is trivial.

The proof for the second case a = S a', rearranges

S a' + b = S a' + c 

to

S (a' + b) = S (a' + c)

and then removes the constructor S using its bijectivity. Finally, the induction hypothesis can be applied to finish the proof.