PropLogic.IntroElim

(*
    CoMoEx - IntroElim
    Copyright (C) 2024  Max Ole Elliger

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <https://www.gnu.org/licenses/>.
*)

Require Classical_Prop.

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

Einführung

Section bot_1.

Variables p : Prop.

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 vor.

  Hypothesis A1 : p.
  Hypothesis A2 : ~p.

  Theorem bot_I : False.
  Proof.
  Admitted.

End bot_1.

Eliminierung

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.

Negation

Einführung

Section neg_1.

Variables p : Prop.

Die Negations-Einführung ist trivial, wenn man die Codierung von ~ aufdeckt:

Print "~ _".

Dies geht übrigens in einem Beweis auch direkt mittels unfold "~ _".. Wie geht man etwas kleinschrittiger vor?

  Hypothesis A1 : p -> False.

  Theorem neg_I : ~p.
  Proof.
  Admitted.

End neg_1.

Eliminierung

Section neg_2.

Variables p : Prop.

Für die Negations-Eliminierungsregel benötigen wir klassische Logik:

Import Classical_Prop.

In späteren Files werden wir häufig direkt zu Beginn Require Import Classical_Prop. schreiben. Dadurch können wir axiomatisch NNPP annehmen:

Check NNPP.

Durch den folgenden Befehl können wir sogar die Notwendigkeit von klassischer Logik sichtbar machen!

Print Assumptions NNPP.

Der Beweis unserer Negations-Elimierungsregel ist jetzt nur noch eine Anwendung von NNPP.

  Hypothesis A1 : ~ ~ p.

  Theorem neg_E : p.
  Proof.
  Admitted.

End neg_2.

Konjunktion

Einführung

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.

Eliminierung

Section and_2.

Variables p q : Prop.

Wenn p und q gelten, gelten sowohl p als auch q.

Hypothesis A1 : p /\ q.

Linke Seite

  Theorem and_E1 : p.
  Proof.
  Admitted.

Rechte Seite

  Theorem and_E2 : q.
  Proof.
  Admitted.

End and_2.

Disjunktion

Einführung

Linke Seite

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.

Rechte Seite

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.

Eliminierung

Section or_3.

Variables p q r : Prop.

Ok, wir wollen r zeigen und wissen, dass zumindest p oder q gilt. Wenn wir jetzt also sowohl aus p als auch aus q unser Ziel r herleiten können, können wir auch aus p \/ q r herleiten.

  Hypothesis A1 : p -> r.
  Hypothesis A2 : q -> r.
  Hypothesis A3 : p \/ q.

  Theorem or_E : r.
  Proof.
  Admitted.

End or_3.

Implikation

Einführung

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.

Eliminierung

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.

Biimplikation

Einführung

Section iff_1.

Variables p q : Prop.

Um eine Äquivalenz zu beweisen, braucht man meistens zwei Beweise. Hierzu ein kleiner Tipp:

  Print "<->".

  Hypothesis A1 : p -> q.
  Hypothesis A2 : q -> p.

  Theorem iff_I : p <-> q.
  Proof.
  Admitted.

End iff_1.

Eliminierung

Von Links nach Rechts

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.

Von Rechts nach Links

Section iff_3.

Variables p q : Prop.

Wird schon!

  Hypothesis A1 : p <-> q.
  Hypothesis A2 : q.

  Theorem iff_E_2 : p.
  Proof.
  Admitted.

End iff_3.