Section Propositionnel. Variables P Q R : Prop. Theorem un : (P /\ Q) -> R -> (Q /\ R). Proof. (* compléter *) Qed. Theorem uncurry : (P -> Q -> R) <-> (P /\ Q -> R). Proof. (* compléter *) Qed. Theorem contra : (P -> Q) -> (~Q -> ~P). Proof. (* compléter *) Qed. Theorem quatre : (P \/ (Q /\ R)) -> P \/ Q. Proof. (* compléter *) Qed. Theorem circuit : (P <-> (~ P)) -> False. Proof. (* compléter *) Qed. End Propositionnel. Section Quantificateurs. Variable p : nat -> Prop. Theorem fimpe : (forall x:nat, p x) -> exists y:nat, p y. Proof. (* compléter *) Qed. Theorem notexists : (forall x:nat, ~ p x) <-> ~ (exists y:nat, p y). Proof. (* compléter *) Qed. Variable rel : nat -> nat -> Prop. Theorem effe : (exists x, forall y, rel x y) -> (forall y, exists x, rel x y). Proof. (* compléter *) Qed. Definition le (x y:nat) : Prop := exists z:nat, y = x + z. Theorem plus_croissante : forall x y:nat, le x (x+y). Proof. (* compléter *) Qed. Require Import Omega. Theorem le_refl : forall x:nat, le x x. Proof. (* compléter *) Qed. Theorem le_trans : forall (x y z:nat), le x y /\ le y z -> le x z. Proof. (* compléter *) Qed. End Quantificateurs. Section PurPire. Variable habitant : Set. Variable pur : habitant -> Prop. Variable pire : habitant -> Prop. Axiom pur_ou_pire : forall x, pur x \/ pire x. Variable say : habitant -> Prop -> Prop. Axiom ax_pur : forall x P, pur x -> say x P -> P. Axiom ax_pire : forall x P, pire x -> say x P -> ~P. End PurPire. Section Relations. Variable A : Set. Definition RTot (R : A -> A -> Prop) := forall x, exists y, R x y. (* TODO Définir RFun, Inj et Surj *) Definition Inv (R : A -> A -> Prop) x y := R y x. Theorem inj_fun_inv : forall R, Inj R -> RFun (Inv R). Proof. (* compléter *) Qed. Theorem fun_inj_inv : forall R, RFun R -> Inj (Inv R). Proof. (* compléter *) Qed. Theorem tot_surj_inv : forall R, RTot R -> Surj (Inv R). Proof. (* compléter *) Qed. End Relations. Section Fonctions. Variable A : Set. Definition FInj (f : A -> A) := forall x y, f x = f y -> x = y. Definition FSurj (f : A -> A) := (* compléter *). Definition Comp (f : A -> A) (g : A -> A) x := (* compléter *). Theorem comp_inj : forall f g, FInj f -> FInj g -> FInj (Comp f g). Proof. (* compléter *) Qed. Theorem comp_surj : forall f g, FSurj f -> FSurj g -> FSurj (Comp f g). Proof. (* compléter *) Qed. End Fonctions.