Не равные преемники в Coq

Question

Я пытаюсь доказать следующую лемму в Coq:

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

Это кажется легким, но я не нашел, как закончить доказательство. Может ли кто-нибудь помочь мне, пожалуйста?

спасибо.

Answer 1

Это очень просто (но отрицание делает его немного запутанным).

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

Дело знать, что в Coq, отрицание является функцией, которая предполагает False, поэтому S m <> S n действительно S m = S n -> False. Поэтому вместо того, чтобы доказывать n <> m, мы можем ввести n = m (мы можем либо развернуть not, либо указать intros явно, чтобы сделать это) и вместо этого получить цель False. Но с n = m в контексте мы можем переписать HS: S n <> S m в HS: S n <> S n, которые могут быть обработаны auto или многие другие тактики, такие как apply HS. reflexivity. или congruence. т.д.

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.