(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li

    T02 Predicate Logic

    Read this part carefully in the coursework.

    Assert is allowed in coursework.

**)

Section Family.

(** A few People **)

Inductive People : Set :=
| Ann : People
| John : People
| Peter : People
| Jack : People
| Kate : People
| Andy : People
| Lucy : People.

(** We have two predicates about the gender **)
Variables Male Female : People -> Prop.
(** Male x = "x is male" **)

(* State genders : *)
Hypothesis g1 : Female Ann.
Hypothesis g2 : Male John.
Hypothesis g3 : Male Peter.
Hypothesis g4 : Male Jack.
Hypothesis g5 : Female Kate.
Hypothesis g6 : Male Andy.
Hypothesis g7 : Female Lucy.

(** One of the primitive relation between People **)
Variables Child : People -> People -> Prop.
(** Child x y = "x is the Child of y" **)

Hypothesis c1 : Child Peter Ann.
Hypothesis c2 : Child Jack Ann.
Hypothesis c3 : Child Peter John.
Hypothesis c4 : Child Jack John.
Hypothesis c5 : Child Ann Kate.
Hypothesis c6 : Child Andy Kate.
Hypothesis c7 : Child Lucy Andy.

(** Now in this context Parent is not a primitive relation we can define it by Child **)
Definition Parent (x y : People) := Child y x.

Definition Son (x y : People) := Child x y /\ Male x.

Definition Daughter (x y : People) := Child x y /\ Female x.

Definition Grandchild (x y : People) := exists p : People, Child x p /\ Child p y.

Definition Grandson (x y : People) := Grandchild x y /\ Male x.

Definition Granddaughter  (x y : People) := Grandchild x y /\ Female x.

(** the two people who has at least one parent in common **)

Definition Sibling (x y : People) := exists p : People, Child x p /\ Child y p /\ ~ (x = y).

(** the two people who has only one parent in common **)

Definition half_Sibling (x y : People) := exists a : People, exists b : People, exists c : People,
  Child x a /\ Child y a /\ Child x b /\ Child y c /\ b <> c.

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

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

Definition Nephew (x y : People) := exists p : People, Child x p /\ Sibling p y /\ Male x.

Definition Niece (x y : People) := exists p : People, Child x p /\ Sibling p y /\ Female x.

Definition Cousin (x y : People) := exists a : People, exists b : People, Child x a /\ Child y b /\ Sibling a b.

Lemma aaS : Sibling Andy Ann.
unfold Sibling.
exists Kate.
split.
assumption.
split.
assumption.
intro.
discriminate H.
Qed.

Lemma t1 : Niece Lucy Ann.
unfold Niece.
exists Andy.
split.
assumption.
split.
exact aaS.
exact g7.
Qed.

Lemma t2 : Cousin Jack Lucy.
unfold Cousin.
exists Ann.
exists Andy.
split.
assumption.
split.
assumption.
unfold Sibling.
exists Kate.
split.
assumption.
split.
assumption.
intro.
discriminate H.
Qed.

End Family.


Section T.

Variables A : Set.

Require Import Coq.Logic.Classical.

Lemma RAA : forall P : Prop, ~~ P -> P.
intros.
destruct (classic P).
assumption.
destruct (H H0).
Qed.

(** What is the name of this lemma in library? NNPP **)


Lemma Pierce : forall P Q : Prop,
 ((P -> Q) -> P) -> P.
intros.
apply NNPP.
intro.
apply H0.
apply H.
intro.
destruct (H0 H1).
Qed.

(* You can instantiate Pierces formula by writing
   Pierce R1 R2
   for any two propositions R1 R2, which instantiates to
   ((R1 -> R2) -> R1) -> R1
*)

Lemma sym : forall x y : A, x = y -> y = x.
intros.
rewrite H.
reflexivity.
Qed.

Variables People : Set.

Variables Male : People -> Prop. 

Hypothesis Socrates : People.

Hypothesis ms : Male Socrates. 

Lemma xisMale : forall x : People, Socrates = x -> Male x.
intros.
rewrite <- H.
exact ms.
Qed.

Lemma yisNotSocrates : forall y : People, ~ Male y -> y <> Socrates.
intros.
intro.
apply H.
rewrite H0.
exact ms.
Qed.

End T.