PropLogic.Laws

(*
    CoMoEx - Laws
    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/>.
 *)

In diesem File soll es um übliche und (teilweise) bekannte klassische logische Gesetze gehen. Eine weitere Annotierung bleibt hier aktuell aus, da die Gesetze ja eh schon ausgeschrieben sind.

Require Import Classical_Prop.

Triviale Biimplikationen


Section trivial_iff.

  Variable p : Prop.

  Theorem trivial_iff_true : (p <-> True) <-> p.
  Proof.
  Admitted.

  Theorem trivial_iff_false : (p <-> False) <-> ~p.
  Proof.
  Admitted.

End trivial_iff.

Kommutativität


Section comm.
  Variables p q : Prop.

Konjunktion


  Theorem and_comm : (p /\ q) -> (q /\ p).
  Proof.
  Admitted.

Disjunktion


  Theorem or_comm : (p \/ q) -> (q \/ p).
  Proof.
  Admitted.

End comm.

Assoziativität


Section assoc.

  Variables p q r : Prop.

Konjunktion


  Theorem and_assoc : ((p /\ q) /\ r) <-> (p /\ (q /\ r)).
  Proof.
  Admitted.

Disjunktion


  Theorem or_assoc : ((p \/ q) \/ r) <-> (p \/ (q \/ r)).
  Proof.
  Admitted.

End assoc.

Gesetze von De Morgan


Section de_morgan.

  Variables p q : Prop.

  Theorem de_morgan_1 : (p /\ q) <-> ~ (~p \/ ~q).
  Proof.
  Admitted.

  Theorem de_morgan_2 : (p \/ q) <-> ~ (~p /\ ~q).
  Proof.
  Admitted.

End de_morgan.

Weitere Implementierungen von Implikationen


Section implsem.

  Variables p q : Prop.

Konjunktion


  Theorem impl_with_disj : (p -> q) <-> (~p \/ q).
  Proof.
  Admitted.

Disjunktion


  Theorem impl_with_conj : (p -> q) <-> ~(p /\ ~q).
  Proof.
  Admitted.

End implsem.

Distributivität von Konjunktion und Disjunktion


Section distr.

  Variables p q r : Prop.

  Theorem distr_1 : (p /\ q) \/ r <-> (p \/ r) /\ (q \/ r).
  Proof.
  Admitted.

  Theorem distr_2 : (p \/ q) /\ r <-> (p /\ r) \/ (q /\ r).
  Proof.
  Admitted.

End distr.

Typische klassische Gesetze


Section p_not_p.

  Variables p : Prop.

  Theorem p_and_not_p : ~ (p /\ ~p).
  Proof.
  Admitted.

  Theorem excluded_middle : (p \/ ~p).
  Proof.
  Admitted.

End p_not_p.

Idempotenz


Section idem.

  Variables p : Prop.

Konjunktion


  Theorem idem_and : p /\ p <-> p.
  Proof.
  Admitted.

Disjunktion


  Theorem idem_or : p \/ p <-> p.
  Proof.
  Admitted.

End idem.

Absorbtion


Section absorb.

  Variables p q : Prop.

Konjunktion


  Theorem absorb_and : p /\ (p \/ q) <-> p.
  Proof.
  Admitted.

Disjunktion


  Theorem absorb_or : p \/ (p /\ q) <-> p.
  Proof.
  Admitted.

End absorb.

Neutrale Elemente


Section neutr.

  Variables p : Prop.

Konjunktion


  Theorem neutr_and : p /\ True <-> p.
  Proof.
  Admitted.

Disjunktion


  Theorem neutr_or : p \/ False <-> p.
  Proof.
  Admitted.

End neutr.

Kontraposition & Modus Tollens


Section contrapos.

  Variables p q : Prop.

  Theorem contrapos : (p -> q) <-> (~q -> ~p).
  Proof.
  Admitted.

  Corollary mod_tollens : ((p -> q) /\ ~q) -> ~p.
  Proof.
  Admitted.

End contrapos.

Transitivität der Implikation


Section impl_trans.

  Variables p q r : Prop.

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

  Theorem impl_trans : p -> r.
  Proof.
  Admitted.

End impl_trans.

Currying


Section currying.

  Variables p q r : Prop.

  Theorem curry : ((p /\ q) -> r) <-> (p -> q -> r).
  Proof.
  Admitted.

End currying.

Gesetz von Peirce


Section peirce_law.

  Variables p q : Prop.

  Theorem peirce : ((p -> q) -> p) -> p.
  Proof.
  Admitted.

End peirce_law.