Require Import Classical_Prop.
Parameters A B C D : Prop.    (* A,B,C,D nutzen wir als propositionale Variablen *)

Lemma const : A -> B -> A.
Proof.
  (* Das Ziel ist aktuell: A -> B -> A *)
  intro a.   (* holt uns 'a : A' in den Kontext *)
  (* Das Ziel ist jetzt: B -> A *)
  intro b.   (* holt uns 'b : B' in den Kontext *)
  (* Das Ziel ist jetzt: A *)
  exact a.   (* wir verwenden 'a' *)
Qed.

Lemma AndElim1 : A /\ B -> A.
Proof.
  (* Ziel: A /\ B -> A *)
  intro ab. (* holt uns 'ab : A /\ B' in den Kontext *)
  (* Ziel: A *)
  destruct ab as [a b].
  (* jetzt haben wir 'a : A' und 'b : B' im Kontext *)
  exact a.
Qed.

Lemma AndElim2 : A /\ B -> B.
Proof.
  intro ab.
  destruct ab as [a b].
  exact b.
Qed.

Lemma AndIntro : A -> B -> A /\ B.
Proof.
  intro a.
  intro b.
  split. (* jetzt haben wir zwei Ziele.. *)
  - exact a. (* Beweis des ersten Ziels *)
  - exact b. (* Beweis des zweiten Ziels *)
Qed.

Lemma ImpElim : A -> (A -> B) -> B.
Proof.
  intro a.
  (* Ziel: (A -> B) -> B *)
  intro a2b.
  (* Ziel: B *)
  apply a2b.
  (* Ziel: A *)
  exact a.
Qed.

(* Wir repräsentieren Herleitbarkeit als Implikation, deshalb
   passiert in 'ImpIntro' nahezu nichts: *)
Lemma ImpIntro : (A -> B) -> (A -> B).
Proof.
  (* Ziel: (A -> B) -> (A -> B) *)
  intro a2b. (* a2b : A -> B *)
  exact a2b.
Qed.

Lemma OrIntro1 : A -> A \/ B.
Proof.
  intro a.
  left.
  exact a.
Qed.

Lemma OrIntro2 : B -> A \/ B.
Proof.
  intro b.
  right.
  exact b.
Qed.

Lemma OrElim : (A -> C) -> (B -> C) -> A \/ B -> C.
Proof.
  intro a2c.
  intro b2c.
  intro aub.
  destruct aub as [a|b].
  * apply a2c.
    exact a.
  * apply b2c.
    exact b.
Qed.

(* Mit den bisherigen Regeln/Taktiken können wir bereits
   Distributivität von \/ und /\ zeigen: *)
Lemma DistOrAnd : A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
Proof.
  intro abc.
  destruct abc as [a bc].
  destruct bc as [b|c].
  * (* Ziel: (A /\ B) \/ (A /\ C) *)
    left.
    (* Ziel: (A /\ B) *)
    split.
    - (* Ziel: A *)
      exact a.
    - (* Ziel: B *)
      exact b.
  * (* Ziel: (A /\ B) \/ (A /\ C) *)
    right.
    (* Ziel: (A /\ C) *)
    split.
    - (* Ziel: A *)
      exact a.
    - (* Ziel: C *)
      exact c.
Qed.

(* Negation ist in Coq direkt als Implikation nach ⊥ kodiert,
   deshalb ist NotIntro genau wie ImpIntro: *)
Lemma NotIntro : (A -> False) -> ~A.
Proof.
  intro a2bot.
  exact a2bot.
Qed.

(* Und entsprechend ist BotIntro einfach Implikationsanwendung *)
Lemma BotIntro : A -> ~A -> False.
Proof.
  intro a.
  intro na. (* na : A -> ⊥ *)
  apply na.
  apply a.
Qed.

Lemma BotElim1 : False -> A.
Proof.
  intro bot. (* bot : ⊥ *)
  contradiction.
Qed.

Lemma BotElim2 : False -> A.
Proof.
  intro bot.
  exfalso.
  exact bot.
Qed.

Lemma ExampleContrapos1 : (A -> B) -> (~B -> ~A).
  (* für die andere Richtung: siehe Übung! *)
Proof.
  intro a2b.
  intro nb.
  intro a.
  apply nb. (* Denn nb: B → ⊥ *)
  apply a2b.
  exact a.
Qed.

Lemma NegationElim : ~~A -> A.
Proof.
  intro nna.
  (* Hier hilft jetzt keine Coq-Taktik weiter,
     sondern wir benötigen das Axiom NNPP.
     (Mehr dazu auf Blatt 05) *)
  apply NNPP.
  exact nna.
Qed.

Lemma ExampleNegationElim : ~(A -> B) -> ~B /\ A.
Proof.
  intro an2b. (* an2b :  A ---/---> B *)
  (* Ziel: ~B /\ A *)
  split.
  - (* Ziel: ~B *)
    intro b.
    (* jetzt haben wir b : B im Kontext, was im
     Widerspruch dazu steht, dass (laut an2b)
     die Implikation von A nach B falsch sein soll: *)
    apply an2b.
    intro a.
    exact b.
  - apply NNPP.
    intro na.
    apply an2b.
    intro a.
    contradiction.
Qed.