(** Introduction to Formal Reasoning (G52IFR) Thorsten Altenkirch Exercise 2 (Predicate logic) published 17/10/11, deadline 1/11/11, 18:00 electronic submission (extended) Use \$ cw submit ex02.v on one of the CS servers then look for the coursework 413 labelled 'g52cfr coursework 2' 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, exists). 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. If you are unsure what these terms mean, check them out on wiktionary (http://en.wiktionary.org/wiki/). In some cases there is a choice, document which alternative you have been using. As an example we define Father: *) Definition Father (x y : People) := Male x /\ Parent x y. 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 proposition comment is out. Use only the basic tactics presented in the lectures (i.e. exact, intro(s), apply, destruct, left, right, split, exists). Don't use any automatc tactics or import any additional libraries. 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 unneccessarily you will loose points. *) Lemma forallexcom : (forall x:A, exists y : B, R x y) -> exists y : B, forall x : A, R x y. Lemma exforallcom : (exists x : A,forall y : B, R x y) -> forall y : B, exists x : A, R x y. Lemma demorgan1 : (~ exists x : A, P x) <-> forall x:A , ~ P x. Lemma demorgan2 : (~ forall x : A, P x) <-> exists x : A, ~ P x. Lemma dp : (exists x:A, True) -> exists x:A, P x -> forall x:A, P x. Lemma transsym : forall x y z : A, x = y -> x = z -> y = z. Lemma eqneq : forall x y z : A, x = y -> ~ (x = z) -> ~ (y = z). Lemma symneq : forall x y : A, ~(x = y) -> ~(y = x). Lemma transneq : forall x y z : A, ~(x = y) -> ~(y = z) -> ~(x = z).