(** Tutorial 3 IFR 2013/2014 **) Section Sec1. (* intro, elim for forall, exists - see board *) Variable A : Set. Variable P Q : A -> Prop. (* WARNING! *) (* Lemma AllAndCom : forall x:A, P x /\ Q x <-> forall x:A, P x /\ forall x:A, Q x. (* it is not what it seems to be *) *) (* a formalization exercise *) Variable Pub : Set. Variable Drunk : Pub -> Prop. (* drinker *) (* Lemma drinker : (exists a : Pub, True) -> (exists x : Pub, Drunk x -> forall y : Pub, Drunk y). *) End Sec1. Section Family. Variable People : Set. (** some people **) Variable Ann : People. Variable Kate : People. Variable Peter : People. Variable Child : People -> People -> Prop. (** Child x y = "x is the Child of y" **) (** Ann is not the child of Kate **) Definition one : ~ Child Ann Kate. (** There is someone with exactly one child **) (* suggested by a student in the tutorial *) Definition two : exists p:People, exists c:People, forall d:People, Child d p <-> c=d. (** we could prove in Coq: if Ann has no children, then Kate is not the child of Ann **) (** We can not prove: nobody is the child of herself **) End Family.