(** 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).