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