How can i proof by absurd with coq?

Question

I am reading Logical Foundations from Software Foundations series and i saw the plus_id_example that is:

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

Proof.
  intros n m.
  intros H.
  rewrite H.
  reflexivity.  Qed.

I could understand the solution, so i tried to solve it using absurd, what i want to do is:

Lets consider by absurd, that n+n <> m+m, so we have 2n <> 2m, n <> m, which is a contradiction since we have n=m as our hypothesis.

How could i write this using Coq tactics?

Answer 1

You can use one of the many contraposition-based lemmas in Coq: you can see them by using, for instance, Search "contra". in Coq.

Using the ssreflect tactic language, a proof based on this idea can be obtained as follows (I'm sure there must be shorter proofs):

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Proof.
  move=> n m.
  apply: contra_eq.
  have twice : forall p, p + p = p * 2.
    move=> p.
    by rewrite -iter_addn_0 /= addn0.
  by rewrite !twice eqn_mul2r.
Qed.