Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Require Import Arith Ring Omega. Section LogiquePropositionnelle. Variable P Q R : Prop. (* Ex. 1.1 : Énoncer et prouver quatre des formules. *) (* Ex. 1.2 : Donner des contre-exemples pour les deux autres. *) End LogiquePropositionnelle. Section Quantificateurs. Variable A : Type. Variable P : A -> Prop. Variable Q : Prop. (* Ex. 2.1: Compléter *) (* Ex. 2.2 *) Definition Surj (p : A -> bool) := (* Compléter *) Theorem bpred_surj (p : A -> bool) : Surj p -> exists (x y : A), x <> y. Proof. (* Compléter *) Qed. End Quantificateurs. Section GraphesEtRelations. Variable V : Type. Variable pere : V -> V -> Prop. (* Ex 3.1 *) Axiom pere_unique : (* Compléter *) (* Ex 3.2 *) Inductive ancetre := (* Compléter *) (* Ex 3.3 *) Definition famille x y := (* Compléter *) (* Ex 3.4 *) Lemma lignee : forall x y z, ancetre x y -> ancetre x z -> (ancetre y z \/ ancetre z y). Proof. (* Compléter *) Qed. (* Ex 3.5 *) Definition rel := V -> V -> Prop. (* Compléter définitions auxiliaires *) Definition equivalence rel := (* Compléter *) Lemma famille_eq : equivalence famille. Proof. (* Compléter *) Qed. End GraphesEtRelations. Section Arbres. Inductive arbre := | F : nat -> arbre | N : arbre * nat * arbre -> arbre. (* Ex 4.1 *) Inductive estDans := (* Compléter *) (* Ex 4.2 *) Inductive tas := (* Compléter *) (* Ex 4.3 *) (* Enoncer et prouver *) (* Ex 4.4 *) Lemma racine_min : (* Completer *) Proof. (* Compléter *) Qed. End Arbres.