(** Introduction to Formal Reasoning (G52IFR) Thorsten Altenkirch Exercise 2 (Predicate logic) published 17/10/11, deadline 25/10/11, 18:00 electronic submission Use \$ cw submit ex02.v on one of the CS servers then look for the coursework ??? labelled 'g52cfr coursework 1' and enter the associated code. Multiple submissions are allowed, up to the deadline. Try to fill in the missing proofs, using only the basic tactics presented in the first lectures (i.e. exact, intro(s), apply, destruct, left, right, split). Do not use auto or tauto. Do not use any libraries. Note that not all the propositions below are provable! Comment out the ones, which you think are not provable and mark them with the words "not provable", if you are sure. **) Section Relations. Variable People : Set. Variables Male Female : People -> Prop. (* Male x = x is a male Female x = x is a female *) Variable Parent : People -> People -> Prop. (* Parent x y = x is the parent of y *) Variable Married : People -> People -> Prop. (* Married x y = x is married to y *) (** Define the following relations: - Father - Mother - Brother - Sister - Halfbrother - Halfsister - MotherInLaw - FatherInLaw - Aunt - Uncle you are encourange to use auxilliary definitions to avoud having to repeat definitions. As an example we define Father: *) Definition Father (x y : People) := Male x /\ Parent x y. Definition Mother (x y : People) := Female x /\ Parent x y. Definition Sibling (x y : People) := ~ (x = y) /\ forall z : People, Parent z x <-> Parent z y. Definition Sister (x y : People) := Female x /\ Sibling x y. Definition Brother (x y : People) := Male x /\ Sibling x y. Definition HalfSibling (x y : People) := ~ (x = y) /\ exists z : People, Parent z x /\ Parent z y /\ exists z:People, ~ (Parent z x /\ Parent z y). Definition Halfsister (x y : People) := Female x /\ HalfSibling x y. Definition Halfbrother (x y : People) := Male x /\ Sibling x y. Definition Grandparent (x y : People) := exists z:People, Parent x z /\ Parent z y. Definition Grandfather (x y : People) := Male x /\ Grandparent x y. Definition Grandmother (x y : People) := Female x /\ Grandparent x y. Definition ParentInLaw (x y : People) := exists z:People, Parent x z /\ Married z y. Definition MotherInLaw (x y : People) := Female x /\ ParentInLaw x y. Definition FatherInLaw (x y : People) := Male x /\ ParentInLaw x y. Definition SiblingInLaw (x y : People) := exists x':People, Married x x' /\ Sibling x' y. Definition BrotherInLaw (x y : People) := Male x /\ SiblingInLaw x y. Definition SisterInLaw (x y : People) := Female x /\ SiblingInLaw x y. Definition AuntOrUncle (x y : People) := exists z:People, (Sibling x z \/ SiblingInLaw x z) /\ Parent z y. Definition Aunt (x y : People) := Female x /\ AuntOrUncle x y. Definition Uncle (x y : People) := Male x /\ AuntOrUncle x y. End Relations. Section Tautologies. Variable A B : Set. Variable P : A -> Prop. Variables R : A -> B -> Prop. Require Import Coq.Logic.Classical. (* Try to prove the following propositions. If you can't prove a propsoition comment is out. If you are sure that a proposition is not provable in general then add the words *unprovable* in the comment. You can use classical logic, if you need to. If you use classical logic uxsnneccessarily you will loose poins. *) (* Lemma forallexcom : (forall x:A, exists y : B, R x y) -> exists y : B, forall x : A, R x y. unprovable *) Lemma exforallcom : (exists x : A,forall y : B, R x y) -> forall y : B, exists x : A, R x y. intros H y. destruct H as [a r]. exists a. apply r. Qed. Lemma demorgan1 : (~ exists x : A, P x) <-> forall x:A , ~ P x. split. intros H x p. apply H. exists x. exact p. intros H1 H2. destruct H2 as [x p]. assert (H1x : ~ P x). apply H1. apply H1x. exact p. Qed. Lemma demorgan2 : (~ forall x : A, P x) <-> exists x : A, ~ P x. split. intro H. apply NNPP. intro ne. apply H. intro x. apply NNPP. intro np. apply ne. exists x. exact np. intros H1 H2. destruct H1 as [a np]. apply np. apply H2. Qed. Lemma dp : (exists x:A, True) -> exists x:A, P x -> forall x:A, P x. intros ne. destruct (classic (forall x:A,P x)) as [alld | nalld]. destruct ne as [x _]. exists x. intros px y. apply alld. assert (H : exists x:A, ~P x). apply NNPP. intro nne. apply nalld. intro a. apply NNPP. intro np. apply nne. exists a. exact np. destruct H as [tt nd]. exists tt. intros ptt x. assert (ic : False). apply nd. apply ptt. destruct ic. Qed. Lemma transsym : forall x y z : A, x = y -> x = z -> y = z. intros x y z xy xz. rewrite<- xy. exact xz. Qed. Lemma eqneq : forall x y z : A, x = y -> ~ (x = z) -> ~ (y = z). intros x y z xy nxz yz. apply nxz. rewrite xy. exact yz. Qed. Lemma symneq : forall x y : A, ~(x = y) -> ~(y = x). intros x y nxy yx. apply nxy. rewrite yx. reflexivity. (* Lemma transneq : forall x y z : A, ~(x = y) -> ~(y = z) -> ~(x = z). unprovable. *)