(** Introduction to Formal Reasoning (G52IFR) Nuo Li and Nicolai Kraus T02 Predicate Logic **) Section Family. Variable People : Set. (** some people **) Hypothesis Ann : People. Hypothesis Kate : People. Hypothesis Peter : People. (** We have two predicates about the gender **) Variables Male Female : People -> Prop. (** Male x = "x is male" **) Variables Child : People -> People -> Prop. (** Child x y = "x is the Child of y" **) (** Kate is the daughter of Ann **) Hypothesis h1 : Female Kate /\ Child Kate Ann. (** Kate and Peter are (half or full) siblings **) Hypothesis h2 : exists p : People, Child Kate p /\ Child Peter p. (** Kate and Peter are 'full' siblings **) Hypothesis h3 : exists dad : People, exists mum : People, Child Kate dad /\ Child Kate mum /\ Child Peter dad /\ Child Peter mum /\ mum <> dad. (** h2 /\ h2 = h2**) (** mum <> dad is the same as not (mum = dad) **) (** same again! **) Hypothesis h4 : forall p : People, Child Kate p <-> Child Peter p. (** No one is the parent of all the others **) Hypothesis h5 : ~ exists p : People, forall c : People, Child c p. (** There is someone with exactly one child **) Hypothesis h6 : exists p : People, exists c : People, Child c p /\ forall d : People, Child d p -> d = c. End Family. Section Misc. Variable A : Set. Variable P : A -> Prop. Variable Q : Prop. Lemma curry_dependend : (exists x : A, P x) -> Q <-> forall x : A, P x -> Q. split. intro. intros x p. apply H. exists x. assumption. intros p2q p. destruct p as [a pa]. apply (p2q a). exact pa. Qed. (** A x B -> C <=== (un)curry ===> A -> B -> C **) Lemma sym : forall x y : A, x = y -> y = x. intros x y. intro p. rewrite <- p. (** or just without <- **) reflexivity. Qed. (** if there is much time, we can do the following: **) (** the two axioms for classical logic are equivalent: **) Lemma TND_NNPP : (forall P : Prop, P \/ ~P) <-> (forall P : Prop, ~~P -> P). split. intros pnp P0 nnp. destruct (pnp P0) as [p0 | np0]. assumption. destruct (nnp np0). intro nnp2p. intro P0. apply nnp2p. (** what exactly happens here? Try to figure it our! *) intro nTNDp0. apply nTNDp0. right. intro p0. apply nTNDp0. left. exact p0. Qed. Require Import Coq.Logic.Classical. (** with classical logic, we therefore can show "reductio ad absurdum" : **) Lemma reductio_ad_absurdum : (forall P : Prop, ~~P -> P). assert (tnd_nnpp := TND_NNPP). destruct tnd_nnpp as [important notImportant]. apply important. intro. exact (classic P0). Qed. (** but it is in the library anyway... **) Lemma reductio_ad_absurdum2 : (forall P : Prop, ~~P -> P). apply NNPP. Qed. End Misc.