(* des théorèmes réutilisables *) Theorem de_morgan_1 : forall P Q:Prop, ~(P \/ Q) -> ~P /\ ~Q. Proof. Admitted. Check (de_morgan_1 (2=3) (6+6=3*4)). Theorem de_morgan_2 : (forall P, P \/ ~P) -> (forall P Q:Prop, ~(P /\ Q) -> ~P \/~Q). Proof. intros Classic P Q H. elim (Classic P). Admitted. Section Proof_of_Peirce_to_exm. Hypothesis Peirce : (forall P Q:Prop, ((P -> Q) -> P) -> P). Variable P:Prop. Lemma Peirce_to_exm : P \/ ~P. Proof. Admitted. End Proof_of_Peirce_to_exm. Check Peirce_to_exm. Section proof_of_not_for_all. Hypothesis Classic : forall P:Prop, P \/~P. Variable A: Set. Variable P : A-> Prop. Theorem not_for_all : ~(forall a:A, ~ P a) -> exists x:A, P x. Proof. Admitted. End proof_of_not_for_all. Check not_for_all. (* Ensembles *) Section Ensembles_sur_A. Variable A: Set. Definition Ensembles := A -> Prop. Definition Vide : Ensembles := fun a => False. Definition Plein : Ensembles := fun a => True. Definition singleton (a:A) := fun b => b = a. Definition appartient_a (E:Ensembles) a := E a. Definition inclus (E F:Ensembles) := forall a, appartient_a E a -> appartient_a F a. Definition Eq (E F:Ensembles) := inclus E F /\ inclus F E. Definition intersection E F := fun a => appartient_a E a /\ appartient_a F a. Definition complement (E:Ensembles) := fun a => ~ appartient_a E a. Theorem inclusion_inter_1 : forall E F, inclus (intersection E F) E. Proof. Admitted. Theorem inclusion_inter_2 : forall E F, inclus (intersection E F) F. Proof. Admitted. Theorem intersection_inclus : forall E F G , inclus E G -> inclus F G -> inclus (intersection E G) G. Proof. Admitted. Theorem inter_comm : forall E F: Ensembles, Eq (intersection E F) (intersection F E). Proof. Admitted. Lemma singleton_inv : forall a b, appartient_a (singleton b) a -> a = b. Proof. Admitted. Lemma singleton_inv_2 : forall a b, ~appartient_a (singleton b) a -> a <> b. Proof. Admitted. Lemma singleton_inclus_inv : forall a E, inclus (singleton a) E -> appartient_a E a. Proof. Admitted. Lemma singleton_inclus_inv_2 : forall a b, inclus (singleton a) (singleton b) -> a = b. Proof. Admitted. Theorem subset_of_singleton : (forall P:Prop, P \/ ~P) -> forall a E, inclus E (singleton a) -> Eq E Vide \/ Eq E (singleton a). Proof. (* moyennement facile *) Admitted. End Ensembles_sur_A. (* Definition imprédicatives *) Definition Faux := forall P:Prop, P. Definition Vrai := forall P:Prop, P -> P. Definition non (P:Prop) := P -> Faux. Definition et (P Q:Prop) := forall G:Prop, (P -> Q -> G) -> G. Definition ou (P Q : Prop) := forall G:Prop, (P -> G) -> (Q -> G) -> G. Definition Egal (A:Set)(a b: A) := forall (P: A-> Prop), P a -> P b. Lemma Egal_refl : forall (A:Set) a, Egal A a a. Proof. Admitted. Lemma Egal_sym : forall (A:Set)(a b: A), Egal A a b -> Egal A b a. Proof. Admitted.