Comment mentira d'hypothèses contradictoires évidemment

Question

Supposons que je veux prouver le théorème suivant:

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

Celui-ci est trivial puisque m ne peut pas être à la fois successeur et zéro, comme on le suppose. Cependant je l'ai trouvé assez difficile de le prouver, et je ne sais pas comment faire sans lemme auxiliaire:

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

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

Je suis assez sûr qu'il ya une meilleure façon de le prouver. Quelle est la meilleure façon de le faire?

Answer 1

Vous avez juste besoin de remplacer m dans la première équation:

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

Answer 2

Il y a un moyen très facile de le prouver:

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

La tactique congruence est une procédure de décision pour égalités au sol sur symboles non interprétés. C'est complet pour les symboles non interprétés et pour les constructeurs, donc dans des cas comme celui-ci, cela peut prouver que l'égalité 0 = m est impossible.