(** Introduction to Formal Reasoning (G52IFR) Nicolai Kraus Tutorial 1 October 09/10, 2012 **) Section FirstTutorial. (** we use the following variables: **) Variable P Q R : Prop. (** first, we repeat the basic commands **) Lemma id : P -> P. intro p. exact p. Qed. Lemma and : P -> Q -> P /\ Q. intros. split. assumption. assumption. Qed. Lemma proj1 : P /\ Q -> P. intro. destruct H. exact H. Qed. Lemma inright : Q -> P \/ Q. intro q. (** Now, we have to choose: do we want to prove the left side or the right side? If we choose incorrectly, we get stuck, so care! **) right. assumption. Qed. Lemma p2nnp : P -> ~~P. unfold not. intros. apply H0. exact H. Qed. Lemma refl : P <-> P. split. exact id. exact id. Qed. (** now, let us do more complicated things **) (** from the lecture **) Lemma incons : ~ (P /\ ~ P). intro pnp. destruct pnp as [p np]. apply np. exact p. Qed. (** Lemma danger : (P /\ R -> Q /\ R) -> P -> Q. Try to solve this lemma. It is not possible. Let us construct a counter example: To make the formula 'danger' false, we need make the 'conditions' true, but the 'conclusion' false. So: Q: false P: true R: false Now: (P /\ R -> Q /\ R) -> P -> Q becomes (true /\ false -> false /\ false) -> true -> false and this is false! So, we cannot prove 'danger'! (Because this interpretation is sound. That means, if we can prove something, it is true for all examples, where we chose a boolean value for each variable.) But care, this does not always work! If you cannot find a counterexample, but also don't manage to prove it, it might still be provable with classical logic! **) (** Lemma again : P \/ Q -> Q. Same again. Try to find the counter example. **) Lemma similar : Q \/ Q -> Q. intro. destruct H. assumption. assumption. Qed. Require Import Coq.Logic.Classical. (** you can use things like assert (cl := classic P) or destruct (classic P) **) (** The only difference to intutionistic logic is that you are always allowed to assume P \/ ~P, if P is any proposition. **) Lemma p2nnp2p : ~~P <-> P. split. intro nnp. (** We can use the following to get an additional assumption: **) assert (c := classic P). (** The following is possible, but useless here: *) assert (d := classic Q). (** We can now use these new assumption like any other assumption. **) destruct c. assumption. (** We can choose to prove something else first. Then, we can use whatever we have proved later. Here, we choose to prove False first: **) assert (f : False). apply nnp. assumption. (** Now, we have f : False as an assumption. Not that False is an 'empty disjunction': A \/ B is true if one of A, B is true (2 possibilities) A is true if A is true (1 possibility) False is true if one of the variables is true. But there is non. (0 possibilities) We can use destruct and we get 0 new subgoals, so that solves the current goal **) destruct f. (** We have done the current goal before: **) exact p2nnp. Qed. Lemma implToOr : (P -> Q) <-> ~P \/ Q. split. intro. (** Is P \/ ~~P or Q \/ ~~Q more useful here? We can destruct it immediately: **) destruct (classic P). right. apply H. assumption. left. assumption. intro. destruct H. intro. (** We could use 'assert False' as before, but there is something quicker. Think of H as a function: **) destruct (H H0). intro. assumption. Qed. (** The lab sessions on Thursday are important as well! **) End FirstTutorial.