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

    Exercise 1 (Propositional logic)
    published 1/10/09, deadline 8/10/09, 17:00 electronic submission

    Use
    $ cw submit ex01.v
    on one of the CS servers
    then look for the coursework 220 labelled 'g52mc2 coursework 1' 
    and enter the associated code.

    Multiple submissions are allowed, up to the deadline.

    Fill in the missing proofs. You are only supposed to use the
    tactics introduced in the lectures, e.g.
    cut, exact, assumption, intro(s), apply, split, elim, left, right, case
    Do not use auto or tauto.

**)

Section Ex1.

Variables P Q R : Prop.

(* Simple proofs only using -> 
** use the tactics intro, apply, exact *)

Lemma X : ((P -> P) -> Q) -> Q.
intro H.
apply H.
intro p.
exact p.
Qed.

Lemma MP : P -> (P -> Q) -> Q.
intro p.
intro pq.
apply pq.
exact p.
Qed.

Lemma B : (P -> Q) -> (Q -> R) -> P -> R.
intro pq.
intro qr.
intro p.
apply qr.
apply pq.
exact p.
Qed.

Lemma C : (P -> Q -> R) -> (Q -> P -> R).
intro pqr.
intro q.
intro p.
apply pqr.
exact p.
exact q.

(* simple proofs using -> and /\ 
** use tactics: exact, intro, apply, split, elim *)

Lemma fst : P /\ Q -> P.
intro pq.
elim pq.
intro p.
intro q.
exact p.
Qed.


Lemma snd : P /\ Q -> Q.
intro pq.
elim pq.
intro p.
intro q.
exact q.
Qed.

Lemma andCom : P /\ Q -> Q /\ P.
intro pq.
elim pq.
intro p.
intro q.
split.
exact q.
exact p.
Qed.


Lemma andAssoc : P /\ (Q /\ R) -> (P /\ Q) /\ R.
intros H.
elim H.
intro p.
intro qr.
elim qr.
intro q.
intro r.
split.
  (* P /\ Q *)
  split.
  (* P *)
     exact p.
     exact q.
  exact r.
Qed.

(* Simple proofs only using ->,/\,\/,<->,~
** use the tactics: cut, exact, assumption,
                    intro(s), apply, split, elim, left, right, case *)

Lemma orCom : (P \/ Q) -> (Q \/ P).
intro pq.
case pq.
intro p.
right.
exact p.
intro q.
left.
exact q.
Qed.

Lemma distrOrAndL : P /\ (Q \/ R) <-> P /\ Q \/ P /\ R.
split.
intro pqr.
elim pqr.
intro p.
intro qr.
case qr.
intro q.
left.
split.
exact p.
exact q.
intro r.
right.
split.
exact p.
exact r.
(* <- *)
intro pqpr.
case pqpr.
intro pq.
elim pq.
intro p.
intro q.
split.
exact p.
left.
exact q.
intro pr.
elim pr.
intro p.
intro r.
split.
exact p.
right.
exact r.
Qed.

Lemma monOrL : P \/ Q -> (P -> R) -> R \/ Q.
intro pq.
intro pr.
case pq.
intro p.
left.
apply pr.
exact p.
intro q.
right.
exact q.
Qed.

Lemma negAntiMon : (P -> Q) -> ~Q -> ~P.
intro pq.
intro nq.
intro p.
apply nq.
apply pq.
exact p.
Qed.

Lemma nnpem : ~~(P \/ ~P).
intros pnp.
apply pnp.
right.
intro p.
apply pnp.
left.
exact p.
Qed.