(** 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 *) (** 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 for any P:Prop *) Variables P Q R : Prop. Lemma dm1 : ~(P \/ Q) <-> ~P /\ ~Q. (* insert your proof here. *) Lemma dm2 : ~(P /\ Q) <-> ~P \/ ~Q. (* insert your proof here. *)