Pas égale succesors en Coq

Question

Je suis en train de prouver le lemme suivant en Coq:

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n. 

Il semble facile, mais je ne trouve pas comment finir la preuve. Est-ce que quelqu'un peut m'aider s'il vous plaît?

Merci.

Answer 1

C'est vraiment facile (mais la négation le rend un peu confus).

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n. 
Proof. 
    unfold not.  (*        |- ... -> False *) 
    intros m n H C. (* ..., H : S m = S n -> False |- False *) 
    apply H.   (* ...       |- S m = S n *) 
    (* f_equal gets rid of functions applied on both sides of an equality, 
    this is probably what you didn't find *) 
    (* basically, f_equal turns a goal [f a = f b] into [a = b] *) 
    f_equal.   (* ..., C : m = n    |- m = n *) 
    exact C. 
Qed. 

Answer 2

La chose à savoir est que Coq, une négation est une fonction qui implique False, de sorte que le S m <> S n est vraiment S m = S n -> False. Ainsi, au lieu de prouver n <> m nous pouvons introduire le n = m (nous pouvons soit déplier not ou dire intros explicitement de le faire) et obtenir l'objectif False à la place. Mais avec n = m dans le contexte que nous pouvons réécrire HS: S n <> S m dans HS: S n <> S n, qui peut être manipulé par auto, ou bien d'autres tactiques telles que apply HS. reflexivity. ou congruence. etc.

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n. 

Proof. intros m n HS HC. 
    rewrite HC in HS. auto. 
Qed.