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

    Exercise 1 (Propositional logic)
    published 1/10/09, deadline 8/10/08, 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.
Lemma MP : P -> (P -> Q) -> Q.
Lemma B : (P -> Q) -> (Q -> R) -> P -> R.
Lemma C : (P -> Q -> R) -> (Q -> P -> R).

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

Lemma fst : P /\ Q -> P.
Lemma snd : P /\ Q -> Q.
Lemma andCom : P /\ Q -> Q /\ P.
Lemma andAssoc : P /\ (Q /\ R) -> (P /\ Q) /\ R.

(* Simple proofs only using ->,/\,\/,<->,~ *)

Lemma orCom : (P \/ Q) -> (Q \/ P).
Lemma distrOrAndL : P /\ (Q \/ R) <-> P /\ Q \/ P /\ R.
Lemma monOrL : P \/ Q -> (P -> R) -> R \/ Q.
Lemma negAntiMon : (P -> Q) -> ~Q -> ~P.
Lemma nnpem : ~~(P \/ ~P).