(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    Exercise 4
    published 22/10/09, deadline 29/10/09, 17:00 electronic submission

    Use
    $ cw submit ex04.v
    on one of the CS servers
    then look for the coursework 224 labelled 'g52mc2 coursework 4' 
    and enter the associated code.

    Multiple submissions are allowed, up to the deadline.

    Fill in the missing proofs. You are only supposed to use the
    tactics introduced in the lectures, e.g.
    cut, exact, assumption, intro(s), apply, split, elim, left, right, case,
    exists, reflexivity, rewrite(<-), discriminate, destruct, contradict

    If you want to use another simple tactic not on the list, please
    check with your tutor.
**)

Section tautologies.

Variable D : Set.
Variables P Q: D -> Prop.
Variable R : Prop.

(* Prove the following tautologies of predicate logic. *)

Lemma exOr :  (exists x:D,P x) \/ (exists y:D,Q y) 
  <-> exists z:D,P z \/ Q z.
(* insert you proof here. *)


Lemma curry : (exists x:D,P x) -> R <-> forall x:D,P x -> R.
(* insert your proof here. *)

(* Translate one of your proofs into English! *)

End tautologies.

Section royalFamily.

(* We use the example of the British Royal Family to formalize family relationships in Coq.
   Our source is
   http://www.knowledgerush.com/kr/encyclopedia/Kings_of_England_family_tree/ 
   However, we will only consider the tree starting with Elizabth II and Prince Philip. *)

(* First we have to define the set of people inductively. Complete the following definition. *)

Inductive People : Set :=
| elizabeth : People
| philip : People
(* add relevant family members. *)
.

(* We introduce two predicates and one relation. *)
Variables Male Female: People -> Prop.
(* "Male x" means "x is male"
** "Female x" means "x is female. *)

Variable Parents : People -> People -> People -> Prop.
(* "Parents m f x" means m is the mother and f is the father of x" *) 

(* State genders: *)
Hypothesis g01 : Female elizabeth.
(* add hypotheses *)


(* State parenthood *)
(* Example: *)
Hypothesis p01 : Parents elizabeth philip edward.
(* add hypotheses *)

(* Define the following derived predicates: *)

(* Example: *)
Definition Mother (x y : People) : Prop :=
  (* x is the mother of y *)
  exists f:People, Parents x f y.

Definition Father (x y : People) : Prop :=
  (* x is the father of y *)
(* add definition *).

Definition Parent (x y : People) : Prop :=
  (* x is a parent of y *)
(* add definition *).

Definition Sibling (x y : People) : Prop :=
  (* x is a sibling of y *)
(* add definition *).

Definition Sister (x y : People) : Prop :=
  (* x is a sister of y *)
(* add definition *).

Definition Brother  (x y : People) : Prop :=
  (* x is a brother of y *)
(* add definition *).

Definition Aunt (x y : People) : Prop :=
  (* x is an aunt of y *)
(* add definition *).

Definition Uncle (x y : People) : Prop :=
  (* x is an uncle of y *)
(* add definition *).

Definition Grandmother (x y : People) : Prop :=
  (* x is a grandmother of y *)
(* add definition *).

Definition Grandfather (x y : People) : Prop :=
  (* x is a grandfather of y *)
(* add definition *).

(* Prove the following facts: *)

Lemma l01 : Mother elizabeth charles.
(* insert proof here. *)

Lemma l02 : Uncle edward henry.
(* insert proof here. *)

Lemma l03 : Grandfather philip william.
(* insert proof here. *)

End royalFamily.