CoMoEx PropLogic.IntroElim
In diesem File geht es um die Nachbildung der üblichen Fitch-Regeln. Die Beispiele führen also die Einführungs- (Introduction-) und Eliminationsregeln (Elimination) an den einfachsten Beispielen vor. Insbesondere sind die entsprechenden Theoreme nicht dazu gedacht, in den anderen Files verwendet zu werden.
Falsum führt man üblicherweise dadurch ein, dass widersprüchliche Informationen vorhanden sind: Eine Aussage p kommt also negiert und nicht negiert in den Annahmen von.
Hypothesis A1 : p.
Hypothesis A2 : ¬p.
Theorem bot_I : False.
Proof.
Admitted.
End bot_1.
Section bot_2.
Variables p : Prop.
Hingegen kann man aus etwas Falschen Beliebiges herleiten.
Hypothesis A1 : False.
Theorem bot_E : p.
Proof.
Admitted.
End bot_2.
Section neg_1.
Variables p : Prop.
Theorem bot_E : p.
Proof.
Admitted.
End bot_2.
Section neg_1.
Variables p : Prop.
Die Negations-Einführung ist trivial, wenn man die Codierung von "~" mit `unfold ~ _.` aufdeckt. Wie geht man etwas kleinschrittiger vor?
Hypothesis A1 : p → False.
Theorem neg_I : ¬p.
Proof.
Admitted.
End neg_1.
Section neg_2.
Variables p : Prop.
Theorem neg_I : ¬p.
Proof.
Admitted.
End neg_1.
Section neg_2.
Variables p : Prop.
Die Negations-Eliminierungsregel mussten wir erst mittels `Require Import Classical_Prop.` importieren. Dadurch können wir axiomatisch `NNPP` annehmen. Was ist NNPP? -> Siehe `Check NNPP.`.
Hypothesis A1 : ¬ ¬ p.
Theorem neg_E : p.
Proof.
Admitted.
End neg_2.
Section and_1.
Variables p q : Prop.
Theorem neg_E : p.
Proof.
Admitted.
End neg_2.
Section and_1.
Variables p q : Prop.
Um eine Konjunktion zu zeigen, muss man sowohl ihre linke als auch rechte Seite zeigen. Wie bekommt man aus einem Goal zwei Goals?
Hypothesis A1 : p.
Hypothesis A2 : q.
Theorem and_I : p ∧ q.
Proof.
Admitted.
End and_1.
Section and_2.
Variables p q : Prop.
Hypothesis A2 : q.
Theorem and_I : p ∧ q.
Proof.
Admitted.
End and_1.
Section and_2.
Variables p q : Prop.
Wenn p und q gelten, gelten sowohl p als auch q.
Hypothesis A1 : p ∧ q.
Theorem and_E1 : p.
Proof.
Admitted.
Theorem and_E2 : q.
Proof.
Admitted.
End and_2.
Section or_1.
Variables p q : Prop.
Theorem and_E1 : p.
Proof.
Admitted.
Theorem and_E2 : q.
Proof.
Admitted.
End and_2.
Section or_1.
Variables p q : Prop.
Wenn p gilt, gilt ja p oder q.
Hypothesis A1 : p.
Theorem or_I1 : p ∨ q.
Proof.
Admitted.
End or_1.
Section or_2.
Variables p q : Prop.
Theorem or_I1 : p ∨ q.
Proof.
Admitted.
End or_1.
Section or_2.
Variables p q : Prop.
Wenn q gilt, gilt ja p oder q.
Hypothesis A1 : q.
Theorem or_I2 : p ∨ q.
Proof.
Admitted.
End or_2.
Section or_3.
Variables p q r : Prop.
Theorem or_I2 : p ∨ q.
Proof.
Admitted.
End or_2.
Section or_3.
Variables p q r : Prop.
Ok, wir wollen r zeigen und wissen, dass zumindest p oder q gelten. Wenn wir jetzt also sowohl aus p als auch aus q unser Ziel r herleiten können, können wir auch aus "p oder q" r herleiten.
Hypothesis A1 : p → r.
Hypothesis A2 : q → r.
Hypothesis A3 : p ∨ q.
Theorem or_E : r.
Proof.
Admitted.
End or_3.
Section impl_1.
Variables p q : Prop.
Hypothesis A2 : q → r.
Hypothesis A3 : p ∨ q.
Theorem or_E : r.
Proof.
Admitted.
End or_3.
Section impl_1.
Variables p q : Prop.
Ich schätze, dass dies die Stelle in dem File ist, die am meisten trivial wirkt. Ich finde aber, dass dieses Theorem nochmal den Fokus darauf lenkt, dass in Coq kein großer Unterschied zwischen einer Herleitung und einer Implikation vorhanden ist.
Hypothesis A1 : p → q.
Theorem impl_I : p → q.
Proof.
Admitted.
End impl_1.
Section impl_2.
Variables p q : Prop.
Theorem impl_I : p → q.
Proof.
Admitted.
End impl_1.
Section impl_2.
Variables p q : Prop.
Ein bisschen Wissen für Zwischendurch: Dieser Schluss nennt sich "Modus Ponens".
Hypothesis A1 : p → q.
Hypothesis A2 : p.
Theorem impl_E : q.
Proof.
Admitted.
End impl_2.
Section iff_1.
Variables p q : Prop.
Hypothesis A2 : p.
Theorem impl_E : q.
Proof.
Admitted.
End impl_2.
Section iff_1.
Variables p q : Prop.
Um eine Äquivalenz zu beweisen, braucht man meistens zwei Beweise.
Hypothesis A1 : p → q.
Hypothesis A2 : q → p.
Theorem iff_I : p ↔ q.
Proof.
Admitted.
End iff_1.
Section iff_2.
Variables p q : Prop.
Hypothesis A2 : q → p.
Theorem iff_I : p ↔ q.
Proof.
Admitted.
End iff_1.
Section iff_2.
Variables p q : Prop.
Wird schon!
Hypothesis A1 : p ↔ q.
Hypothesis A2 : p.
Theorem iff_E_1 : q.
Proof.
Admitted.
End iff_2.
Section iff_3.
Variables p q : Prop.
Hypothesis A2 : p.
Theorem iff_E_1 : q.
Proof.
Admitted.
End iff_2.
Section iff_3.
Variables p q : Prop.
Wird schon!