Hintergrund
Ich lerne selbst Hilfe, Coq. Bisher habe ich Yves Bertots Coq in Eile gelesen . Mein Ziel ist es nun, einige grundlegende Ergebnisse bezüglich der natürlichen Zahlen zu beweisen, die mit dem sogenannten Divisionsalgorithmus gipfeln. Auf meinem Weg zu diesem Ziel bin ich jedoch auf einige Rückschläge gestoßen. Insbesondere haben sich die beiden folgenden Ergebnisse in Coq als schwieriger zu beweisen erwiesen (Wortspiel beabsichtigt), als ich es mir ursprünglich vorgestellt hatte. Tatsächlich habe ich nach vielen erfolglosen Versuchen versucht, sie von Hand zu beweisen (wie unten gezeigt). Dies hilft mir eindeutig nicht dabei, Coq besser zu handhaben. Deshalb wende ich mich diesem Forum zu. Ich hoffe, dass jemand auf dieser Seite fähig und willens istum mir zu helfen, meine Beweise unten in einen Beweis zu übersetzen, den Coq akzeptiert. Jede Hilfe wird aufrichtig geschätzt!
Satz A.
Für alle Beweis:x < S ( y ) ≤ x < y ≤ I ( N , x , y )
Angenommen, . Daher gibt es ein mit Daher durch (Peano 1b und 3)z ≤ N I ( N , x + S ( z ) , S ( y ) ) I ( N , x + z , y )
Definieren Sie ein Prädikat
Es reicht aus, zu zeigen . Wir beweisen dies durch Induktion auf . Um , nicht ethat, wenn gilt, dann ist nach Peano 1a wahr. Somit ist . Nun beweisen wir : Angenommen, . Aus dieser Definition ergibt sich auch in diesem Fall und damit . Schließlich gibt Peanos fünftes Axiom und durch wir .
Satz B.
Für alle Beweis:
Wenn dann per Definition , und wenn dann per Definition auch . Wenn und dann haben wir durch Transitivität und Reflexivität , was ein Widerspruch ist. Folglich ist nicht mehr als eine der Aussagen wahr.¬ I ( N , x , y ) x > y ¬ I ( N , x , y ) x > y y > x I ( N , x , y )
Wir halten fest und induzieren auf . Wenn , haben wir für alle , was den Basisfall beweist. Nehmen wir als nächstes an, dass der Satz für ; Jetzt wollen wir den Satz für beweisen . Aus der Trichotomie für ergeben sich drei Fälle: und . Wenn , dann eindeutig . Wenn , dann ist (als für alle ). Nehmen wir schließlichx I ( N , 0 , y ) 0 < y ∨ I ( N , 0 , y ) y xDann haben wir nach Satz A oder , und in jedem Fall sind wir fertig.
Die Sätze, die ich beweisen möchte, können wie folgt in Coq ausgedrückt werden.
Lemma less_lem (xy: N): weniger x (succ y) -> oder (weniger xy) (IN xy).
Satz Ntrichotomie: (für alle xy: N oder (weniger xy) (oder (IN xy) (weniger yx))).
Nützliche Ergebnisse
Hier habe ich einige der von mir definierten Ergebnisse gesammelt und bis zu diesem Punkt bewiesen. Dies sind diejenigen, auf die ich mich oben beziehe. * Dies ist der Code, den ich bisher geschrieben habe. Beachten Sie, dass die meisten aus Definitionen bestehen. * *
(* Sigma types *)
Inductive Sigma (A:Set)(B:A -> Set) :Set :=
Spair: forall a:A, forall b : B a,Sigma A B.
Definition E (A:Set)(B:A -> Set)
(C: Sigma A B -> Set)
(c: Sigma A B)
(d: (forall x:A, forall y:B x,
C (Spair A B x y))): C c :=
match c as c0 return (C c0) with
| Spair a b => d a b
end.
(* Binary sum type *)
Inductive sum' (A B:Set):Set :=
inl': A -> sum' A B | inr': B -> sum' A B.
Print sum'_rect.
Definition D (A B : Set)(C: sum' A B -> Set)
(c: sum' A B)
(d: (forall x:A, C (inl' A B x)))
(e: (forall y:B, C (inr' A B y))): C c :=
match c as c0 return C c0 with
| inl' x => d x
| inr' y => e y
end.
(* Three useful finite sets *)
Inductive N_0: Set :=.
Definition R_0
(C:N_0 -> Set)
(c: N_0): C c :=
match c as c0 return (C c0) with
end.
Inductive N_1: Set := zero_1:N_1.
Definition R_1
(C:N_1 -> Set)
(c: N_1)
(d_zero: C zero_1): C c :=
match c as c0 return (C c0) with
| zero_1 => d_zero
end.
Inductive N_2: Set := zero_2:N_2 | one_2:N_2.
Definition R_2
(C:N_2 -> Set)
(c: N_2)
(d_zero: C zero_2)
(d_one: C one_2): C c :=
match c as c0 return (C c0) with
| zero_2 => d_zero
| one_2 => d_one
end.
(* Natural numbers *)
Inductive N:Set :=
zero: N | succ : N -> N.
Print N.
Print N_rect.
Definition R
(C:N -> Set)
(d: C zero)
(e: (forall x:N, C x -> C (succ x))):
(forall n:N, C n) :=
fix F (n: N): C n :=
match n as n0 return (C n0) with
| zero => d
| succ n0 => e n0 (F n0)
end.
(* Boolean to truth-value converter *)
Definition Tr (c:N_2) : Set :=
match c as c0 with
| zero_2 => N_0
| one_2 => N_1
end.
(* Identity type *)
Inductive I (A: Set)(x: A) : A -> Set :=
r : I A x x.
Print I_rect.
Theorem J
(A:Set)
(C: (forall x y:A,
forall z: I A x y, Set))
(d: (forall x:A, C x x (r A x)))
(a:A)(b:A)(c:I A a b): C a b c.
induction c.
apply d.
Defined.
(* functions are extensional wrt
identity types *)
Theorem I_I_extensionality (A B: Set)(f: A -> B):
(forall x y:A, I A x y -> I B (f x) (f y)).
Proof.
intros x y P.
induction P.
apply r.
Defined.
(* addition *)
Definition add (m n:N) : N
:= R (fun z=> N) m (fun x y => succ y) n.
(* multiplication *)
Definition mul (m n:N) : N
:= R (fun z=> N) zero (fun x y => add y m) n.
(* Axioms of Peano verified *)
Theorem P1a: (forall x: N, I N (add x zero) x).
intro x.
(* force use of definitional equality
by applying reflexivity *)
apply r.
Defined.
Theorem P1b: (forall x y: N,
I N (add x (succ y)) (succ (add x y))).
intros.
apply r.
Defined.
Theorem P2a: (forall x: N, I N (mul x zero) zero).
intros.
apply r.
Defined.
Theorem P2b: (forall x y: N,
I N (mul x (succ y)) (add (mul x y) x)).
intros.
apply r.
Defined.
Definition pd (n: N): N :=
R (fun _=> N) zero (fun x y=> x) n.
(* alternatively
Definition pd (x: N): N :=
match x as x0 with
| zero => zero
| succ n0 => n0
end.
*)
Theorem P3: (forall x y:N,
I N (succ x) (succ y) -> I N x y).
intros x y p.
apply (I_I_extensionality N N pd (succ x) (succ y)).
apply p.
Defined.
Definition not (A:Set): Set:= (A -> N_0).
Definition isnonzero (n: N): N_2:=
R (fun _ => N_2) zero_2 (fun x y => one_2) n.
Theorem P4 : (forall x:N,
not (I N (succ x) zero)).
intro x.
intro p.
apply (J N (fun x y z =>
Tr (isnonzero x) -> Tr (isnonzero y))
(fun x => (fun t => t)) (succ x) zero)
.
apply p.
simpl.
apply zero_1.
Defined.
Theorem P5 (P:N -> Set):
P zero -> (forall x:N, P x -> P (succ x))
-> (forall x:N, P x).
intros base step n.
apply R.
apply base.
apply step.
Defined.
(* I(A,-,-) is an equivalence relation *)
Lemma Ireflexive (A:Set): (forall x:A, I A x x).
intro x.
apply r.
Defined.
Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).
intros x y P.
induction P.
apply r.
Defined.
Lemma Itransitive (A:Set):
(forall x y z:A, I A x y -> I A y z -> I A x z).
intros x y z P Q.
induction P.
assumption.
Defined.
Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)).
intros m n H.
induction H.
apply r.
Defined.
Lemma zeroadd: (forall n:N, I N (add zero n) n).
intro n.
induction n.
simpl.
apply r.
apply succ_cong.
auto.
Defined.
Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))).
intros.
induction n.
simpl.
apply r.
simpl.
apply succ_cong.
auto.
Defined.
Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)).
intros n m; elim n.
apply zeroadd.
intros y H; elim (succadd m y).
simpl.
rewrite succadd.
apply succ_cong.
assumption.
Defined.
Lemma associative_add: (forall m n k:N,
I N (add (add m n) k) (add m (add n k))).
intros m n k.
induction k.
simpl.
apply Ireflexive.
simpl.
apply succ_cong.
assumption.
Defined.
Definition or (A B : Set):= sum' A B.
Definition less (m n: N) :=
Sigma N (fun z => I N (add m (succ z)) n).
Lemma less_lem (x y:N) :
less x (succ y) -> or (less x y) (I N x y).
intro.
destruct H.
right.
(* Here is where I'm working right now *)
Defined.
Theorem Ntrichotomy: (forall x y:N,
or (less x y) (or (I N x y) (less y x))).
Antworten:
Coq ist etwas grausamer als Papier-Proofs: Wenn Sie in einem Papier-Proof "und wir sind fertig" oder "klar" schreiben, gibt es oft viel mehr zu tun, um Coq zu überzeugen.
Jetzt habe ich Ihren Code ein wenig aufgeräumt, während ich versucht habe, ihn im gleichen Sinne zu halten. Sie finden es hier .
Mehrere Bemerkungen:
Ich habe eingebaute Datentypen und Definitionen verwendet, bei denen ich dachte, dass dies Ihrer Absicht nicht schaden würde. Beachten Sie, dass
identity
Beweise viel einfacher gewesen wären , wenn ich anstelle der eingebauten "weniger als" -Relation die eingebaute Gleichheit verwendet hätte, da sich viele Ihrer Lemmas in der Datenbank bekannter Theoreme befinden, die bei jedem Aufruf von überprüft werdenIch habe einige Taktiken verwendet, die Sie wahrscheinlich nicht kennen, aber eine "echte" Coq-Superuserin hätte viel mächtigere Taktiken zur Hand und ihre eigenen Taktiken geschrieben, um den Job zu vereinfachen. Ich empfehle CPDT immer als Ort, um zu lernen, wie man Taktiken auf kraftvolle Weise einsetzt.
Ich habe Notationen und Tabulatoren verwendet, um die Lesbarkeit zu verbessern, und integrierte Konstrukte wie Matching und die
induction
Taktik, um das Beweisen und Umfaktieren zu vereinfachen. Insbesondere war Ihre Definition vonless
schwer zu bearbeiten. Sie können sehen, wie ich sie geringfügig von auf das Äquivalent (aber einfacher zu verwenden) geändert habe. diese Art von „Definition Zwicken“ passiert eine Menge in der formalen Beweisen.∃ x , ( x + m ) + 1 = nWährend Sie hier möglicherweise Antworten auf diese Art von Fragen erhalten, empfehle ich Ihnen dringend, Ihre Arbeit beim Coq-Club einzureichen, der mit dem ausdrücklichen Zweck erstellt wurde, diese Art von Fragen zu beantworten.
quelle
Codys Antwort ist ausgezeichnet und erfüllt Ihre Frage nach der Übersetzung Ihres Beweises in Coq. Als Ergänzung dazu wollte ich die gleichen Ergebnisse hinzufügen, aber auf einem anderen Weg nachweisen, hauptsächlich als Illustration einiger Teile von Coq, und um zu demonstrieren, was Sie mit sehr wenig zusätzlicher Arbeit syntaktisch beweisen können. Dies ist jedoch keine Behauptung, dass dies der kürzeste Weg ist - nur ein anderer. Die Beweise enthalten nur ein zusätzliches Hilfs-Lemma und stützen sich nur auf grundlegende Definitionen. Ich führe keine Addition, Multiplikation oder eine ihrer Eigenschaften oder funktionale Extensionalität ein, und die einzigen Peano-Axiome sind eine einfache Form von a <= b -> a + c <= b + c im Helfer-Lemma (nur für c = 1) und strukturelle Induktion, die ohnehin kostenlos mit induktiven Typen geliefert wird.
Wie Cody, wo ich dachte, dass es keinen Unterschied macht, habe ich vordefinierte Typen usw. verwendet, also werde ich vor dem Beweis diese beschreiben:
und
Was jetzt folgt, sind meine Beweise. Wenn Markups nicht im Weg sind, sollten Sie in der Lage sein, diese einfach auszuschneiden und in eine Coq .v-Datei einzufügen, und es wird funktionieren. Ich habe Kommentare eingefügt, um interessante Teile zu notieren, aber sie befinden sich in (* *) Trennzeichen, sodass Sie sie nicht entfernen müssen.
quelle