(******************)
(*   EXERCICE 1   *)
(******************)

Definition pred (n : nat) := match n with O => O | S p => p end.
Definition null (n : nat) := match n with O => True | S _ => False end.

(* 1. La fonction successeur est injective *)

Lemma S_injective :
  forall x y : nat, S x = S y -> x = y.

Proof.
intros; change (pred (S x) = pred (S y)); rewrite H; reflexivity.
Qed.

(* 2. Le successeur de quiconque est différent de zéro *)

Lemma S_diff_0 :
  forall x, S x <> 0.

Proof.
intros; intro; change (null (S x)) in |- *; rewrite H; split.
Qed.

(* Le prédicat "Even" et la fonction de test "even" *)

Require Bool.

Definition Even (n : nat) := exists p : nat, n = 2 * p.

Fixpoint even (n : nat) : bool :=
  match n with
  | O   => true
  | S p => Bool.negb (even p)
  end.

(* 3. Test de la fonction "even" *)

Eval compute in (even 7).  (* = false : bool *)
Eval compute in (even 18).  (* = true : bool *)

(* 4. Équivalence: Even x <-> even x = true. *)

(* On commence par prouver la partie directe *)

Lemma Even_even :
  forall x, Even x -> even x = true.

Proof.
unfold Even in |- *; intros.
destruct H as (y, H); rewrite H; clear H x.
induction y.
 reflexivity.
 simpl in IHy; rewrite <- plus_n_O in IHy.
   simpl in |- *; rewrite <- plus_n_O.
   rewrite <- plus_n_Sm; simpl in |- *; rewrite IHy; reflexivity.
Qed.

(* La partie réciproque repose sur un principe d'induction ad hoc,
   qui propage la propriété de 2 en 2, en partant de 0 et 1. *)

Lemma nat_ind2 :
  forall P : nat -> Prop,
    P 0 -> P 1 ->
    (forall n : nat, P n -> P (S (S n))) ->
      forall n : nat, P n.

Proof.
intros; assert (P n /\ P (S n)).
 induction n.
  split; assumption.
  destruct IHn; split.
   assumption.
   apply H1; assumption.
 destruct H2; assumption.
Qed.

(* Un petit lemme qui dit que la négation booléenne est involutive: *)

Lemma negb_invol :
  forall b : bool, Bool.negb (Bool.negb b) = b.

Proof.
intro b; case b; reflexivity.
Qed.

(* La partie réciproque se fait par induction, en utilisant "nat_ind2": *)

Lemma even_Even :
  forall x, even x = true -> Even x.

Proof.
unfold Even in |- *; induction x using nat_ind2; intros.
 exists 0; reflexivity.
 discriminate H.
 simpl in H; rewrite negb_invol in H.
   destruct (IHx H) as (p, H1); exists (S p); simpl in |- *.
   rewrite H1; rewrite <- plus_n_Sm; reflexivity.
Qed.

(* Équivalence: *)

Lemma Even_iff_even :
  forall x, Even x <-> even x = true.

Proof.
split; intros.
 apply Even_even; assumption.
 apply even_Even; assumption.
Qed.

(******************)
(*   EXERCICE 2   *)
(******************)

Parameter T : Set.

(* 1. Définition de l'égalité de Leibniz *)

Definition EQ (x y : T) := forall P : T -> Prop, P x -> P y.

(* 2. L'égalité de Leibniz est réflexive et transitive *)

Lemma EQ_refl :
  forall x : T, EQ x x.

Proof.
unfold EQ in |- *; intros; assumption.
Qed.

Lemma EQ_trans :
  forall x y z : T, EQ x y -> EQ y z -> EQ x z.

Proof.
unfold EQ in |- *; intros; apply H0; apply H; assumption.
Qed.

(* 3. L'égalité de Leibniz est symétrique *)

Lemma EQ_sym :
  forall x y : T, EQ x y -> EQ y x.

Proof.
intros; unfold EQ in H.
apply H. (* Ici: le système devine que P = fun z : T => EQ z x. *)
apply EQ_refl.
Qed.

Lemma EQ_sym' : (* Une autre preuve, prédicative *)
  forall x y : T, EQ x y -> EQ y x.

Proof.
unfold EQ in |- *; intros x y H P.
apply H; intro; assumption.
Qed.

(* 4. Équivalence des deux égalités *)

Lemma EQ_equiv :
  forall x y : T, EQ x y <-> eq x y.

Proof.
split; intros.
 apply H; reflexivity.
 rewrite H; apply EQ_refl.
Qed.

(******************)
(*   EXERCICE 3   *)
(******************)

(* 1. Définition de la conjonction *)

Definition ET (A B : Prop) := forall X : Prop, (A -> B -> X) -> X.

(* 2. Règles d'introduction et d'élimination: *)

Lemma ET_intro :
  forall A B : Prop, A -> B -> ET A B.

Proof.
unfold ET in |- *; intros.
apply H1; assumption.
Qed.

Lemma ET_elim1 :
  forall A B : Prop, ET A B -> A.

Proof.
unfold ET in |- *; intros.
apply H; intros; assumption.
Qed.

Lemma ET_elim2 :
  forall A B : Prop, ET A B -> B.

Proof.
unfold ET in |- *; intros.
apply H; intros; assumption.
Qed.

(* 3. Équivalence avec la conjonction de Coq: *)

Lemma ET_equiv :
  forall A B : Prop, ET A B <-> A /\ B.

Proof.
split; intros.
 split; [ apply (ET_elim1 A B) | apply (ET_elim2 A B) ]; assumption.
 destruct H; apply ET_intro; assumption.
Qed.

(* 4. Le codage du OU au second ordre: *)

Definition OU (A B : Prop) := forall X : Prop, (A -> X) -> (B -> X) -> X.

Lemma OU_intro1 :
  forall A B : Prop, A -> OU A B.

Proof.
unfold OU in |- *; intros.
apply H0; assumption.
Qed.

Lemma OU_intro2 :
  forall A B : Prop, B -> OU A B.

Proof.
unfold OU in |- *; intros.
apply H1; assumption.
Qed.

Lemma OU_elim :
  forall A B C : Prop, (A -> C) -> (B -> C) -> OU A B -> C.

Proof.
unfold OU in |- *; intros.
apply H1; assumption.
Qed.

Lemma OU_equiv :
  forall A B : Prop, OU A B <-> A \/ B.

Proof.
split; intros.
 apply OU_elim with A B.
  intro; left; assumption.
  intro; right; assumption.
  assumption.
 destruct H; [ apply OU_intro1 | apply OU_intro2 ]; assumption.
Qed.

(* 5. Les connecteurs BOT et TOP: *)

Definition BOT := forall X : Prop, X.

Lemma BOT_elim :
  forall A : Prop, BOT -> A.

Proof.
unfold BOT in |- *; intros; apply H.
Qed.

Lemma BOT_equiv : BOT <-> False.

Proof.
split; intro; [ apply H | destruct H ].
Qed.

Definition TOP := forall X : Prop, X -> X.

Lemma TOP_intro :
  TOP.

Proof.
unfold TOP in |- *; intros; assumption.
Qed.

Lemma TOP_equiv : TOP <-> True.

Proof.
split; intro; [ split | exact TOP_intro ].
Qed.

(******************)
(*   EXERCICE 4   *)
(******************)

(* 1. Définition du quantificateur existentiel *)

Definition EX (P : T -> Prop) :=
  forall X : Prop, (forall x : T, P x -> X) -> X.

(* 2. Introduction et élimination *)

Lemma EX_intro :
  forall P : T -> Prop, forall x : T, P x -> EX P.

Proof.
unfold EX in |- *; intros.
apply H0 with x; assumption.
Qed.

Lemma EX_elim :
  forall P : T -> Prop, forall A : Prop,
    (forall x : T, P x -> A) -> EX P -> A.

Proof.
intros; apply H0; assumption.
Qed.

(* 3. Équivalence de "EX" et "exists" *)

Lemma EX_equiv :
  forall P : T -> Prop, EX P <-> exists x : T, P x.

Proof.
split; intros.
 apply H; intros; exists x; assumption.
 destruct H as (x, H); apply EX_intro with x; assumption.
Qed.

(******************)
(*   EXERCICE 5   *)
(******************)

(* Parameter T : Set. *)
Parameter o : T.
Parameter s : T -> T.

Definition N (x : T) :=
  forall P : T -> Prop, P o -> (forall y, P y -> P (s y)) -> P x.

(* 1. N contient o *)

Lemma N_o :
  N o.

Proof.
unfold N in |- *; intros; assumption.
Qed.

(* 2. N est clos par s *)

Lemma N_s :
  forall x, N x -> N (s x).

Proof.
unfold N in |- *; intros.
apply H1; apply H; assumption.
Qed.

(* 3. Principe de récurrence: *)

Lemma N_rec :
  forall A : T -> Prop,
    A o -> (forall x, N x -> A x -> A (s x)) -> forall x, N x -> A x.

Proof.
intros; assert (N x /\ A x).
 apply H1.
  split; [ exact N_o | assumption ].
  intros; destruct H2; split.
   apply N_s; assumption.
   apply H0; assumption.
 destruct H2; assumption.
Qed.