(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    L03 (More Coq)

    This lecture introduces propositional logic using the proof
    assistant Coq.  The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Section l03.

Variables P Q R : Prop.

Lemma one : (P /\ ~P) -> Q.
intro pnp.
destruct pnp as [p np].
cut False.
intro f.
case f.
apply np.
exact p.
Qed.

Lemma C : (P -> Q -> R) -> 
          (Q -> P -> R).
auto.
Qed.

Print C.

Section auto.
Variables P1 P2 P3 P4 P5 P6 : Prop.

Lemma hard : (P1 -> P2) 
     -> (P2 -> P3) -> (P3 -> P4) 
     -> (P4 -> P5) -> (P5 -> P6) 
     -> P1 -> P6.
auto 6.
Qed.

Print hard.

Goal (P1 \/ P1) -> P1.
tauto.
Save p1.

Print p1.

End auto.

(*
Lemma tnd : P \/ ~P.
*)

(*
Lemma nnpp : ~~P -> P.
tauto.
*)

Require Import Coq.Logic.Classical.

Print classic.

Lemma nnpp : ~~P -> P.
cut (P \/ ~P).
intro pnp.
case pnp.
intros p nnp.
exact p.
intros np nnp.
unfold not in np.
unfold not in nnp.
contradict nnp.
exact np.
apply classic.
Qed.