Wie kann ich `false` und damit die Coq-Hypothese 'd = d + 1' beweisen?

Question

Goal forall (d : nat), d + 1 = d -> False. 
Proof. 
    intros d H. 
Abort.  

Wie kann ich False von H nachweisen? inversion H repliziert es nur.

Answer 1

Hier ist, wie Sie einige hilfreiche Lemmata entdecken einen Widerspruch aus dem Kontext zu tun abzuleiten. Zunächst einmal müssen wir ein Modul importieren sie enthalten, da sonst der Search Befehl nicht in der Lage sein wird, diese Lemmata zu entdecken:

Require Import Coq.Arith.Arith. 

wir prüfen, ob wir genau das Lemma brauchen wir haben (man erinnere sich, dass x <> y ist eine Notation für not (eq x y) und not A steht für A -> False):

Search (?x + _ <> ?x). 

Kein Glück diesmal. Ok, Addition ist kommutativ, lassen Sie uns es auf diese Weise versuchen:

Search (_ + ?x <> ?x). 

Nichts wieder. Aber wir sollten auf jeden Fall etwas wie folgt aus:

Search (S ?x <> ?x). 

Schließlich haben wir das folgende Lemma:

Nat.neq_succ_diag_l: forall n : nat, S n <> n 

, die wir wie so verwenden können:

Require Import Coq.Arith.Arith. 

Goal forall (d : nat), d + 1 = d -> False. 
Proof. 
    intros d H. 
    rewrite Nat.add_comm in H. 
    now apply Nat.neq_succ_diag_l in H. 
Qed. 

Answer 2

Der Beweis erfolgt durch Induktion über d und verwendet:

eq_add_S 
    : forall n m : nat, S n = S m -> n = m 

Basisfall ist 0 = 1 die durch Inversion False führt, dies den Fall abzuschließen. Der induktive Fall Sie haben d + 1 = d -> False als Induktion Hypothese und S d + 1 = S d -> False als Ihr Ziel. Wir wissen das x + 1 = y + 1 -> x + y von eq_add_S, also schreiben wir unser Ziel um und wenden die Induktions-Hypothese an.

vollständiger Beweis:

Goal forall (d : nat), d + 1 = d -> False. 
Proof. 
    induction d. 
    intros. 
    - inversion H. 
    - intros H. 
    erewrite <- eq_add_S in H; eauto. 
Qed.