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