PropLogic.SomeExamples
(*
CoMoEx - Some examples for propositional logic
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 Import Classical_Prop.
CoMoEx - Some examples for propositional logic
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 Import Classical_Prop.
In diesem File habe ich versucht, eigene Beispiele zu kreieren. Wahrscheinlich wird insbesondere diese Sammlung mit der Zeit weiter ergänzt.
Dank der folgenden Zeile stehen uns die bereits bewiesenen Gesetze aus Laws.v zur Verfügung:
Man kann z.B. `de_morgan_1` ganz normal aufrufen, wie in der folgenden Section zu sehen ist:
Section how_to_use_Laws.
Variables p1 p2 : Prop.
Check de_morgan_1.
Example how_to_use_Laws_1 : (p1 /\ p2) -> ~(~p1 \/ ~p2).
Proof.
intro A1.
apply de_morgan_1 with (p := p1) (q := p2).
exact A1.
Qed.
Example how_to_use_Laws_2 : ~(~p1 \/ ~p2) -> p1 /\ p2.
Proof.
intro A1.
apply de_morgan_1 with (p := p1) (q := p2).
exact A1.
Qed.
Oftmals braucht man die `with`-Klausel gar nicht, ich wollte sie nur der Vollständigkeit halber erwähnen.
In dieser Section geht es nochmal um einen exzessiven Gebrauch von Konjunktion und Disjunktion. Sollte nicht allzu schwer sein.
Hypothesis A1 : (p1 /\ p2) \/ (p3 /\ p4).
Hypothesis A2 : (p1 /\ p3) \/ (p2 /\ p4).
Theorem T12 : p1 \/ p2.
Proof.
Admitted.
Theorem T13 : p1 \/ p3.
Proof.
Admitted.
Theorem T14 : p1 \/ p4.
Proof.
Admitted.
Theorem T23 : p2 \/ p3.
Proof.
Admitted.
Theorem T24 : p2 \/ p4.
Proof.
Admitted.
Theorem T34 : p3 \/ p4.
Proof.
Admitted.
End se_1.
Section se_2.
Variables p1 p2 p3 p4 : Prop.
Hypothesis A2 : (p1 /\ p3) \/ (p2 /\ p4).
Theorem T12 : p1 \/ p2.
Proof.
Admitted.
Theorem T13 : p1 \/ p3.
Proof.
Admitted.
Theorem T14 : p1 \/ p4.
Proof.
Admitted.
Theorem T23 : p2 \/ p3.
Proof.
Admitted.
Theorem T24 : p2 \/ p4.
Proof.
Admitted.
Theorem T34 : p3 \/ p4.
Proof.
Admitted.
End se_1.
Section se_2.
Variables p1 p2 p3 p4 : Prop.
Und nochmal etwas Konjunktion/Disjunktion, zusammen mit etwas Negation. Das spannendste Theorem ist vermutlich das erste.
Hypothesis A1 : (p1 \/ p2) /\ (~ p1 \/ ~p2).
Theorem se_2_1 : (p1 /\ ~p2) \/ (~p1 /\ p2).
Proof.
Admitted.
Theorem se_2_2 : ~ (p1 /\ p2).
Proof.
Admitted.
Theorem se_2_3 : ~ (~ p1 /\ ~ p2).
Proof.
Admitted.
End se_2.
Section se_3.
Variables p1 p2 p3 p4 p5: Prop.
Theorem se_2_1 : (p1 /\ ~p2) \/ (~p1 /\ p2).
Proof.
Admitted.
Theorem se_2_2 : ~ (p1 /\ p2).
Proof.
Admitted.
Theorem se_2_3 : ~ (~ p1 /\ ~ p2).
Proof.
Admitted.
End se_2.
Section se_3.
Variables p1 p2 p3 p4 p5: Prop.
Der Beweis in dieser Section erfordert einen guten Blick für das Wesentliche sowie ggf. ein bisschen Kreativität. Definitiv schwieriger als die letzten beiden Sections.
Hypothesis A1 : ~ (p1 /\ ~p2).
Hypothesis A2 : p3 -> ~ (p1 /\ p2).
Hypothesis A3 : ~ (p1 -> ~ p3).
Hypothesis A4 : p4 \/ p5.
Hypothesis A5 : p4 -> p3.
Hypothesis A6 : p2 -> p5.
Theorem se_3_1 : p4 /\ p5.
Proof.
Admitted.
End se_3.
Section se_4.
Variables p1 p2 p3 : Prop.
Hypothesis A1 : (p1 -> p2) /\ (p2 -> p3) /\ (p3 -> ~ p1).
Theorem se_4_1 : ~ p1.
Proof.
Admitted.
End se_4.
Section se_5.
Variables p1 p2 : Prop.
Hypothesis A1 : (~ p1 /\ p2) \/ (~p2 /\ p1).
Theorem se_5_1 : ~ (p1 /\ p2).
Proof.
Admitted.
End se_5.
Section se_6.
Variables p1 p2 : Prop.
Hypothesis A1 : (p1 -> (p1 -> p2)) -> ~ p1.
Theorem se_6_1 : ~ (p1 /\ p2).
Proof.
Admitted.
End se_6.
Section se_7.
Variables p1 p2 : Prop.
Theorem se_7_1 : ((p1 -> ~(p1 -> p2)) -> ~(p1 -> p1)) -> p2.
Proof.
Admitted.
End se_7.
Hypothesis A2 : p3 -> ~ (p1 /\ p2).
Hypothesis A3 : ~ (p1 -> ~ p3).
Hypothesis A4 : p4 \/ p5.
Hypothesis A5 : p4 -> p3.
Hypothesis A6 : p2 -> p5.
Theorem se_3_1 : p4 /\ p5.
Proof.
Admitted.
End se_3.
Section se_4.
Variables p1 p2 p3 : Prop.
Hypothesis A1 : (p1 -> p2) /\ (p2 -> p3) /\ (p3 -> ~ p1).
Theorem se_4_1 : ~ p1.
Proof.
Admitted.
End se_4.
Section se_5.
Variables p1 p2 : Prop.
Hypothesis A1 : (~ p1 /\ p2) \/ (~p2 /\ p1).
Theorem se_5_1 : ~ (p1 /\ p2).
Proof.
Admitted.
End se_5.
Section se_6.
Variables p1 p2 : Prop.
Hypothesis A1 : (p1 -> (p1 -> p2)) -> ~ p1.
Theorem se_6_1 : ~ (p1 /\ p2).
Proof.
Admitted.
End se_6.
Section se_7.
Variables p1 p2 : Prop.
Theorem se_7_1 : ((p1 -> ~(p1 -> p2)) -> ~(p1 -> p1)) -> p2.
Proof.
Admitted.
End se_7.