(* Second tutorial, October 17/18, 2013 *) Section Tut2. Require Import Coq.Logic.Classical. (* Why classical logic? Why not *only* classical logic? *) Variable Tomorrow_will_rain : Prop. (* how to decide whether classical logic is needed for a concrete lemma? [white board] *) Lemma Classic_Example : Tomorrow_will_rain \/ ~ Tomorrow_will_rain. exact (classic Tomorrow_will_rain). Qed. Lemma Equivalent1 : forall P Q : Prop, (~P \/ Q) -> (P -> Q). intro P'. intro Q'. clear Tomorrow_will_rain. (* not necessary *) intros npq p. destruct npq. exfalso. apply H. exact p. exact H. Qed. Variables P Q R : Prop. Lemma Pierce : ((P -> Q) -> P) -> P. intro pqp. assert (c := classic P). assert (d := classic (P -> P -> Q \/ R)). clear d. (* we don't need that *) destruct c as [p | np]. exact p. apply pqp. intro p. (* we cannot prove this. but we can prove false. *) exfalso. apply np. exact p. Qed. Lemma lemma1 : (~~P \/ Q) -> ~Q -> P. intros nnpq nq. destruct nnpq. apply NNPP. exact H. exfalso. apply nq. exact H. Qed. End Tut2.