(** 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 ex05.v
    on one of the CS servers
    then look for the coursework ??? labelled 'g52mc2 coursework 5' 
    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.
split.
intro H.
destruct H as [HP | HQ].
destruct HP as [d HPd].
exists d.
left.
exact HPd.
destruct HQ as [d HQd].
exists d.
right.
exact HQd. 
intro H.
destruct H as [d HPQ].
destruct HPQ as [HP | HQ].
left.
exists d.
exact HP.
right.
exists d.
exact HQ.
Qed.


Lemma curry : (exists x:D,P x) -> R <-> forall x:D,P x -> R.
split.
intros H d HP.
apply H.
exists d.
exact HP.
intros HPR HP.
destruct HP as [d HPRd].
eapply HPR. (* can be avoided using cut *)
apply HPRd.
Qed.

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
| sophie : People
| edward : People
| anne : People
| andrew : People
| sarah : People
| mark : People
| charles : People 
| diana : People
| william : People
| henry : People.

(* 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 f m x" means m is the mother and f is the father of x" *) 

(* State genders: *)
Hypothesis g01 : Female elizabeth.
Hypothesis g02 : Male philip.
Hypothesis g03 : Female sophie.
Hypothesis g04 : Male edward.
Hypothesis g05 : Female anne.
Hypothesis g06 : Male edward.
Hypothesis g07 : Male andrew.
Hypothesis g08 : Female sarah.
Hypothesis g09 : Male mark.
Hypothesis g10 : Male charles.
Hypothesis g11 : Female diana.
Hypothesis g12 : Male william.
Hypothesis g13 : Male henry.

(* State parenthood *)
Hypothesis p01 : Parents elizabeth philip edward.
Hypothesis p02 : Parents elizabeth philip charles.
Hypothesis p03 : Parents elizabeth philip anne.
Hypothesis p04 : Parents elizabeth philip anne.
Hypothesis p05 : Parents elizabeth philip andrew.
Hypothesis p06 : Parents diana charles william.
Hypothesis p07 : Parents diana charles henry.

(* Define the following derived predicates: *)
Definition Mother (x y : People) : Prop :=
  exists f:People, Parents x f y.

Definition Father (x y : People) : Prop :=
  exists m:People, Parents m x y.

Definition Parent (x y : People) : Prop :=
  Mother x y \/ Father x y.

Definition Sibling (x y : People) : Prop :=
  exists f : People, exists m : People, Parents f m x /\ Parents f m y.

Definition Sister (x y : People) : Prop :=
  Sibling x y /\ Female x.

Definition Brother  (x y : People) : Prop :=
  Sibling x y /\ Male x.

Definition Aunt (x y : People) : Prop :=
  exists z : People, Sister x z /\ Parent z y.

Definition Uncle (x y : People) : Prop :=
  exists z : People, Brother x z /\ Parent z y.

Definition Grandmother (x y : People) : Prop :=
  exists z : People, Mother x z /\ Parent z y.

Definition Grandfather (x y : People) : Prop :=
  exists z : People, Father x z /\ Parent z y.

(* Prove the following facts: *)
Lemma l01 : Mother elizabeth charles.
unfold Mother.
exists philip.
exact p02.
Qed.

Lemma l02 : Uncle edward henry.
unfold Uncle.
exists charles.
split.
unfold Brother.
split.
unfold Sibling.
exists elizabeth.
exists philip.
split.
exact p01.
exact p02.
exact g06.
unfold Parent.
right.
unfold Father.
exists diana.
assumption.
Qed.

Lemma l03 : Grandfather philip william.
unfold Grandfather.
exists charles.
split.
unfold Father.
exists elizabeth.
assumption.
unfold Parent.
right.
unfold Father.
exists diana.
assumption.
Qed.

End royalFamily.