(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch L06 (More Predicate Logic) The material in this file contains coq proofs which can be read and animated with coqide or xemacs+proofgeneral. **) Section l06. Section deMorgan. Variable D : Set. Variables P Q: D -> Prop. Variable R : Prop. Lemma dm1 : (forall x:D,~ P x) -> ~(exists x:D,P x). intros ha he. unfold not in ha. destruct he as [d pd]. eapply ha. apply pd. Qed. Lemma dm2 : ~(exists x:D,P x) -> forall x:D,~ (P x). intros he d hp. apply he. exists d. exact hp. Qed. Lemma dm3 : (exists x:D,~ P x) -> ~ forall x:D,P x. intros he ha. destruct he as [d pd]. apply pd. apply ha. Qed. Require Import Classical. Lemma dm4 : ~ (forall x:D,P x) -> exists x:D,~(P x). intro ha. apply NNPP. intro he. apply ha. intro d. apply NNPP. intro npd. apply he. exists d. exact npd. Qed. End deMorgan. (* Section drinker. Require Import Classical. Variable Pubs People : Set. Variables InPub : People -> Pubs -> Prop. Variables Drinks : People -> Prop. (* In every non-empty pub there is sombeody, if he (or she) drinks then everybody drinks. *) Lemma drink: forall p:Pubs, (exists a:People , InPub a p) -> exists b:People, InPub b p /\ (Drinks b -> forall c:People, InPub c p -> Drinks c). End drinker. *) Section cheat. Variable D : Set. Variables PP QQ: D -> Prop. Variable R : Prop. (* automatisation ? *) Lemma allMon : (forall x:D,PP x) -> (forall y:D, PP y -> QQ y) -> forall z:D,QQ z. auto. Qed. Lemma exOr : (exists x:D,PP x) \/ (exists y:D,QQ y) <-> exists z:D,PP z \/ QQ z. firstorder. Qed. Print exOr. End cheat.