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