(******************) (* Exercice 1 *) (******************) (* Question 1: Principe d'identité *) Lemma imp_refl : forall A : Prop, A -> A. Proof. intros; assumption. (* ou: auto. *) Qed. (* Question 2: Le syllogisme Barbara *) Lemma imp_trans : forall A B C : Prop, (A -> B) -> (B -> C) -> A -> C. Proof. intros; apply H0; apply H; assumption. (* ou: auto. *) Qed. (* Question 3: Commutativité du /\ *) Lemma and_commut : forall A B : Prop, A /\ B <-> B /\ A. Proof. intros; split; intro; destruct H; split; assumption. Qed. (* Question 4: Commutativité du \/ *) Lemma or_commut : forall A B : Prop, A \/ B <-> B \/ A. Proof. intros; split; (intro; destruct H; [ right | left ]; assumption). Qed. (* Question 5: Introduction de la double négation *) Lemma not_not_intro : forall A : Prop, A -> ~~A. Proof. intros; intro; apply H0; assumption. Qed. (* Question 6: Raisonnement par contraposition *) Lemma contra : forall A B : Prop, (A -> B) -> ~B -> ~A. Proof. intros; intro; apply H0; apply H; assumption. Qed. (* Question 7: Double négation du tiers exclu *) Lemma not_not_em : forall A : Prop, ~~(A \/ ~A). Proof. intro; intro; apply H; right; intro; apply H; left; assumption. Qed. (* Question 8: Distributivité du /\ par rapport au \/ *) Lemma distr_and_or : forall A B C : Prop, (A \/ B) /\ C <-> (A /\ C) \/ (B /\ C). Proof. intros; split; intro. destruct H; destruct H; [ left | right ]; split; assumption. destruct H; destruct H; split; [ left | idtac | right | idtac ]; assumption. Qed. (* Question 9: Distributivité du \/ par rapport au /\ *) Lemma distr_or_and : forall A B C : Prop, (A /\ B) \/ C <-> (A \/ C) /\ (B \/ C). Proof. intros; split; intro. destruct H. destruct H; split; left; assumption. split; right; assumption. destruct H; destruct H; destruct H0. left; split; assumption. right; assumption. right; assumption. right; assumption. Qed. (******************) (* Exercice 2 *) (******************) Parameter X Y : Set. Parameter A B : X -> Prop. Parameter S : X -> Y -> Prop. (* R dans l'énoncé *) (* Question 1: Échange forall avec /\ *) Lemma forall_and : (forall x : X, A x /\ B x) <-> (forall x : X, A x) /\ (forall x : X, B x). Proof. split; intros. split; intro x; destruct (H x); assumption. destruct H as (H, H0); split; [ apply H | apply H0 ]. Qed. (* Question 2: Échange exists avec \/ *) Lemma exists_or : (exists x : X, A x \/ B x) <-> (exists x : X, A x) \/ (exists x : X, B x). Proof. split; intro. destruct H as (x, H); destruct H; [ left | right ]; exists x; assumption. destruct H; destruct H as (x, H); exists x; [ left | right ]; assumption. Qed. (* La question 3 est mathématiquement impossible. Si jamais vous trouvez un script de preuve qui marche: mail coq-bugs@inria.fr :-) *) (* Question 4: Échange exists/forall (dans ce sens) *) Lemma exists_forall_exch : (exists y : Y, forall x : X, S x y) -> (forall x : X, exists y : Y, S x y). Proof. intro; destruct H as (y, H); intro; exists y; apply H. Qed. (******************) (* Exercice 3 *) (******************) Parameter E : Set. Parameter R : E -> E -> Prop. Axiom refl : forall (x : E), R x x. Axiom trans : forall (x y z : E), R x y -> R y z -> R x z. Axiom antisym : forall (x y : E), R x y -> R y x -> x = y. Definition smallest (x0 : E) := forall (x : E), R x0 x. Definition minimal (x0 : E) := forall (x : E), R x x0 -> x = x0. (* Question 1: Unicité du plus petit élément (s'il existe) *) Lemma smallest_unique : forall (x1 x2 : E), smallest x1 -> smallest x2 -> x1 = x2. Proof. unfold smallest in |- *; intros. apply antisym; [ apply H | apply H0 ]. Qed. (* Question 2: Le plus petit élément (s'il existe) est minimal *) Lemma smallest_minimal : forall (x0 : E), smallest x0 -> minimal x0. Proof. unfold smallest, minimal in |- *; intros. apply antisym; [ assumption | apply H; assumption ]. Qed. (* Question 2: S'il existe un plus petit élément, il n'y a pas d'autre élément minimal que celui-ci. *) Lemma smallest_minimal_eq : forall (x0 x1 : E), smallest x0 -> minimal x1 -> x1 = x0. Proof. unfold smallest, minimal in |- *; intros. symmetry in |- *; apply H0; apply H. Qed. (******************) (* Exercice 4 *) (******************) Axiom not_not_elim : forall A : Prop, ~~A -> A. (* Question 1 *) Lemma em : forall A : Prop, A \/ ~A. Proof. intro; apply not_not_elim; apply not_not_em. Qed. (* Question 2 *) Parameter Personne : Set. Parameter Boit : Personne -> Prop. Parameter Gege : Personne. (* Atteste que le type "Personne" est non vide *) (* Question 3 *) Lemma drinker's_paradox : exists x, Boit x -> forall y, Boit y. Proof. (* Existe-t-il une personne qui ne boit pas? *) destruct (em (exists x, ~ Boit x)). (* Si oui, on prend cette personne pour x. L'implication recherchée devient vraie car son membre gauche est faux. *) destruct H as (x, H); exists x; intros; absurd (Boit x); assumption. (* Si non, on peut prendre n'importe qui; par exemple Gégé. L'implication recherchée devient vraie car son membre droit est vrai, modulo une élimination de double négation. *) exists Gege; intros; apply not_not_elim. intro; apply H; exists y; assumption. Qed.