(* Exercice 1 *)

Lemma identity : forall A : Prop, A -> A.
Proof.
intros A a. 
exact a.
Qed.

Lemma syllogism : forall A B C : Prop, (A -> B) -> (B -> C) -> A -> C.
Proof.
intros A B C ab bc a.
apply bc.
apply ab.
exact a.
Qed.

Lemma and_commutative : forall A B : Prop, (A /\ B) -> (B /\ A).
Proof.
intros A B ab.
destruct ab as (a, b).
split; [exact b | exact a].
Qed.


Lemma or_commutative : forall A B : Prop, (A \/ B) -> (B \/ A).
Proof.
intros A B ab.
destruct ab as [a | b]; [right | left]; assumption.
Qed.

Lemma not_notI : forall A : Prop, A -> ~~ A.
Proof.
intros A a na.
apply na.
assumption.
Qed.

Lemma contraposition : forall A B : Prop, (A -> B) -> (~B -> ~A).
Proof.
intros A B AB nB a.
apply nB; apply AB; exact a.
Qed.

Lemma not_not_em : forall A, ~~ (A \/ ~A).
Proof.
intros A nO; apply nO; right; intro a; apply nO; left.
assumption.
Qed.


Lemma and_or_distr : forall A B C : Prop, (A \/ B) /\ C -> (A /\ C) \/ (B /\ C).
Proof.
intros A B C h1; destruct h1 as (h2, c); destruct h2.
  left; split; assumption.
right; split; assumption.
Qed.

Lemma or_and_distr : forall A B C : Prop, (A /\ B) \/ C -> (A \/ C) /\ (B \/ C).
Proof.
intros A B C h1; destruct h1 as [h2 | c].
  destruct h2 as (a, b); split; left; assumption.
split; right; assumption.
Qed.

(* Exercice 2 *)

Section Exo2.

Variables (X Y : Set)(A B : X -> Prop)(R : X -> Y -> Prop).

Lemma forall_and : (forall x : X, A x /\ B x) <-> (forall x : X, A x)/\(forall x : X, B x).
Proof.
split.
  intro h; split; intro x; destruct (h x); assumption.
intros h x; destruct h as (h1, h2); split; [apply h1 | apply h2].
Qed.

Lemma exists_or : (exists x : X, A x \/ B x) <-> (exists x : X, A x)\/(exists x : X, B x).
Proof.
split; intro h1.
  destruct h1 as (x, hx); destruct hx as [ax | bx]; [left| right]; exists x; assumption.
  destruct h1 as [h|h]; destruct h as (x, hx); 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 :-) *)


Lemma exists_forallC : (exists y : Y, forall x, R x y) ->
  (forall x : X, exists y : Y, R x y).
Proof.
intros h1; destruct h1 as (y, hy); intros x; exists y; apply hy.
Qed. 

End Exo2.

(* Exercice 3 *)

Section Exo3.

Variables (E : Set)(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.

Lemma smallest_unique : forall x y : E, smallest x -> smallest y -> x = y.
Proof.
unfold smallest in |- *; intros x y sx sy.
apply antisym; [apply sx | apply sy].
Qed.

Lemma smallest_is_min : forall x, smallest x -> minimal x.
Proof.
unfold smallest in |- *; unfold minimal in |- *; intros x sx y Ryx.
apply antisym; [assumption|]; apply sx.
Qed.

Lemma smallest_min_unique : forall x : E, smallest x -> 
  forall y, minimal y -> y = x.
Proof.
unfold minimal in |- *; unfold smallest in |- *; intros x sx y my.
symmetry. 
apply my.
apply sx. 
Qed.

End Exo3.

(* Exercice 4 *)
Axiom not_not_elim : forall A, ~~ A -> A.

Lemma em : forall A, A \/ ~ A.
Proof.
intro A.
apply not_not_elim.
apply not_not_em.
Qed.

Parameter Gens : Set.
Parameter Boit : Gens -> Prop.
Parameter Quidam : Gens.  (* Atteste que le type "Gens" est non vide *)

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 Quidam; intros; apply not_not_elim.
   intro; apply H; exists y; assumption.
Qed.