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

    Exercise 2 (More propositional logic, classical reasoning)
    published 8/10/09, deadline 15/10/09, 17:00 electronic submission

    Use
    $ cw submit ex02.v
    on one of the CS servers
    then look for the coursework 221 labelled 'g52mc2 coursework 2' 
    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.
    If you want to use another simple tactic not on the list, please
    check with your tutor.
**)

Section Ex2.

(** 1. **)

(* Explain two proofs from exercise 1 in English. At least one of the proofs should use disjunction
   and one should use conjunction or negation.

   Here is an example:

In Coq:
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.

In English:
To show P \/ Q -> (P -> R) -> R \/ Q we assume 
(1) P \/ Q
(2) P -> R
It remains to show R \/ Q. We analyze 1, there are two cases:
(P holds) Using (2) we know R and hence R \/ Q.
(Q holds) Then we also have R \/ Q.
QED
*)


(* From rxm08u, Robert Miles *)

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.

(*
In English:
To show P \/ Q -> (P -> R) -> R \/ Q we assume (1) P \/ Q
(2) P -> R
It remains to show R \/ Q. We analyze (1), there are two cases:
(P holds) Using (2) we know R and hence R \/ Q.
(Q holds) Then we also have R \/ Q.
QED
*)

(* From wxz09u, Wei Zeng (modified slightly) *)

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

In English:
To show P /\ Q -> Q /\ P we assume (1)P /\ Q It remains to show Q /\ P, we can split to prove two subgoals:
(2) P
(3) Q We eliminate (1), then we can have P and Q, which can discharge both goals.
QED
*)


(** 2 **)

(* you are asked to prove the de Morgan rules.
   You will need to use classical logic at some point.
   However, you get all the points, if you use classical
   reasoning as little as possible.
*)

Require Import Coq.Logic.Classical.
(* asserts the axiom classic : P \/ ~P *)

Variables P Q R : Prop.

Lemma dm1 : ~(P \/ Q) <-> ~P /\ ~Q.
split.
  (* -> *)
  intro pq.
  split.
    (* ~P *)
    intro p.
    apply pq.
    left.
    exact p.
    (* ~Q *)
    intro q.
    apply pq.
    right.
    exact q.
  (* <- *)
  intro pq.
  intro pvq.
  elim pq.
  intros np nq.
  case pvq.
  exact np.
  exact nq.
Qed.

Lemma dm2 : ~(P /\ Q) <-> ~P \/ ~Q.
split.
  (* -> *)
  intro npq.
  case (classic (~ P \/ ~ Q)).
   intro npnq.
   exact npnq.
   intro nnpnq.
   left.
   intro p.
   apply nnpnq.
   right.
   intro q.
   apply npq.
   split.
   exact p.
   exact q.
   (* <- *)
   intros npnq npq.
   elim npq.
   intros p q.
   case npnq.
   intro np.
   apply np.
   exact p.
   intro nq.
   apply nq.
   exact q.
Qed.