(** Introduction to Formal Reasoning (G52IFR) Tutorial 1 October 10/11, 2013 **) Section FirstTutorial. Variable P Q R : Prop. (* First, it is important to know all the introduction and elimination rules [white board] *) Lemma exfalso : False -> P. intro. destruct H. Qed. Lemma lemma1 : (P -> False) -> P -> Q. intros np p. assert (f : False). apply np. exact p. destruct f. Qed. (* not provable Lemma lemma2 : P \/ Q -> Q. intro h. destruct h. Lemma example : (P /\ R -> Q /\ R) -> P -> Q. intros. They are both not provable. How could we have seen this before? With a truth table! [white board] However, it does not always work: Lemma cl : ((P -> False) -> False) -> P. *) Lemma l : P -> (P \/ Q). intro. (* disjunction - introduction is a "dangerous" step! *) left. exact H. Qed. (* You can use everything that you have proved before: *) Lemma id : P -> P. intro. exact H. Qed. Lemma idid : P <-> P. split; exact id. (* or - longer: assert (idl := id). exact idl. exact id. *) Qed. End FirstTutorial.