How to prove False from obviously contradictory assumptions

Question

Suppose I want to prove following Theorem:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.forall n m : nat, S n = m -> 0 = m -> False

This one is trivial since m cannot be both successor and zero, as assumed. However I found it quite tricky to prove it, and I don't know how to make it without an auxiliary lemma:

Lemma succ_neq_zero_lemma : forall n : nat, O = S n -> False.forall n : nat, 0 = S n -> False
Proof.forall n : nat, 0 = S n -> False intros.n: nat
H: 0 = S n
False inversion H. Qed.

Theorem succ_neq_zero : forall n m : nat, S n = m -> 0 = m -> False.forall n m : nat, S n = m -> 0 = m -> False
Proof.forall n m : nat, S n = m -> 0 = m -> False
  intros.n, m: nat
H: S n = m
H0: 0 = m
False symmetry in H.n, m: nat
H: m = S n
H0: 0 = m
False
  apply (succ_neq_zero_lemma n).n, m: nat
H: m = S n
H0: 0 = m
0 = S n transitivity m.n, m: nat
H: m = S n
H0: 0 = m
0 = m
n, m: nat
H: m = S n
H0: 0 = m
m = S n
  -n, m: nat
H: m = S n
H0: 0 = m
0 = m assumption.
  -n, m: nat
H: m = S n
H0: 0 = m
m = S n assumption.
Qed.

I am pretty sure there is a better way to prove this. What is the best way to do it?

Answer (Arthur Azevedo De Amorim)

You just need to substitute for m in the first equation:

Theorem succ_neq_zero : forall n m : nat, S n = m -> 0 = m -> False.forall n m : nat, S n = m -> 0 = m -> False
Proof.forall n m : nat, S n = m -> 0 = m -> False
  intros n m H1 H2.n, m: nat
H1: S n = m
H2: 0 = m
False rewrite <- H2 in H1.n, m: nat
H1: S n = 0
H2: 0 = m
False inversion H1.
Qed.

A: Or a bit more concise yet still explicit:

Theorem succ_neq_zero : forall n m : nat, S n = m -> 0 = m -> False.forall n m : nat, S n = m -> 0 = m -> False
Proof.forall n m : nat, S n = m -> 0 = m -> False
  intros n m H <-.n: nat
H: S n = 0
False discriminate H.
Qed.

less explicit works too:

Theorem succ_neq_zero : forall n m : nat, S n = m -> 0 = m -> False.forall n m : nat, S n = m -> 0 = m -> False
Proof.forall n m : nat, S n = m -> 0 = m -> False
  intros.n, m: nat
H: S n = m
H0: 0 = m
False subst.n: nat
H0: 0 = S n
False discriminate.
Qed.

Answer (Gilles 'SO- stop being evil')

There's a very easy way to prove it:

Theorem succ_neq_zero : forall n m : nat, S n = m -> 0 = m -> False.forall n m : nat, S n = m -> 0 = m -> False
Proof.forall n m : nat, S n = m -> 0 = m -> False
  congruence.
Qed.

The congruence tactic is a decision procedure for ground equalities on uninterpreted symbols. It's complete for uninterpreted symbols and for constructors, so in cases like this one, it can prove that the equality 0 = m is impossible.

Answer (larsr)

It might be useful to know how congruence works.

To prove that two terms constructed by different constructors are in fact different, just create a function that returns True in one case and False in the other cases, and then use it to prove True = False. I think this is explained in Coq'Art

Example not_congruent : 0 <> 1.0 <> 1
Proof.0 <> 1
  intros C. (* now our goal is 'False' *)C: 0 = 1
False
  pose (fun m => match m with 0 => True | S _ => False end) as f.C: 0 = 1
f:= fun m : nat =>
match m with
| 0 => True
| S _ => False
end: nat -> Prop
False
  assert (Contra: f 1 = f 0) by (rewrite C; reflexivity).C: 0 = 1
f:= fun m : nat =>
match m with
| 0 => True
| S _ => False
end: nat -> Prop
Contra: f 1 = f 0
False
  now replace False with True by Contra.
Qed.