Parameter Ens : Type.                (* L'univers des ensembles *)
Parameter someset : Ens.             (* Un habitant de l'univers *)
Parameter elt : Ens -> Ens -> Prop.  (* La relation d'appartenance *)

(*********************************************)
(*   EXERCICE 1 : Axiome d'extensionnalité   *)
(*********************************************)

(* 1. La relation d'inclusion *)

Definition subset (a b : Ens) :=
  forall x : Ens, elt x a -> elt x b.

(* 2. L'inclusion est réflexive et transitive *)

Lemma subset_refl :
  forall x : Ens, subset x x.

Proof.
unfold subset; auto.
Qed.

Lemma subset_trans :
  forall x y z : Ens, subset x y -> subset y z -> subset x z.

Proof.
unfold subset; auto.
Qed.

(*=== Axiome d'extensionnalité ===*)

Axiom extensionality :
  forall (a b : Ens), (forall x, elt x a <-> elt x b) -> a = b.

(* 3. Réciproque de l'axiome d'extensionnalité *)

Lemma converse_extensionality :
  forall (a b : Ens), a = b -> (forall x, elt x a <-> elt x b).

Proof. (* La preuve n'utilise aucun axiome *)
split; rewrite H; auto.
Qed.

(* 4. L'inclusion est anti-symétrique. *)

Lemma subset_asym :
  forall x y : Ens, subset x y -> subset y x -> x = y.

Proof.
unfold subset; intros; apply extensionality; split; auto.
Qed.

(***************************************)
(*   EXERCICE 2 : Axiome de la paire   *)
(***************************************)

Parameter pair : Ens -> Ens -> Ens.

Axiom pair_axiom :
  forall (a b x : Ens), elt x (pair a b) <-> x = a \/ x = b.

(* 1. Compatibilité vis-à-vis de l'égalité. *)

Lemma pair_rewrite :
  forall a a' b b' : Ens,
    a = a' -> b = b' -> pair a b = pair a' b'.

Proof.
assert (forall a a' b b', a = a' -> b = b' -> subset (pair a b) (pair a' b')).
 unfold subset in |- *; intros.
   destruct (pair_axiom a b x).
   destruct (pair_axiom a' b' x).
   apply H5; assert (x = a \/ x = b).
  apply H2; assumption.
  destruct H6.
   left; transitivity a; assumption.
   right; transitivity b; assumption.
 intros; apply subset_asym.
  apply H; assumption.
  apply H; symmetry  in |- *; assumption.
Qed.

(* 2. Égalité de deux paires *)

Lemma pair_equal :
  forall a b c d,
    pair a b = pair c d -> (a = c /\ b = d) \/ (a = d /\ b = c).

Proof.
intros; assert (forall x, x = a \/ x = b <-> x = c \/ x = d).
 intro; apply iff_trans with (elt x (pair a b)).
  apply iff_sym; apply pair_axiom.
  rewrite H; apply pair_axiom.
 assert (a = c \/ a = d).
  destruct (H0 a) as (H1, H2); apply H1; left; reflexivity.
  assert (b = c \/ b = d).
   destruct (H0 b) as (H2, H3); apply H2; right; reflexivity.
   assert (c = a \/ c = b).
    destruct (H0 c) as (H3, H4); apply H4; left; reflexivity.
    assert (d = a \/ d = b).
     destruct (H0 d) as (H4, H5); apply H5; right; reflexivity.
     destruct H1; [ left | right ]; (split; [ assumption | idtac ]).
      destruct H2; [ destruct H4 | assumption ].
       rewrite H4; rewrite H1; assumption.
       symmetry  in |- *; assumption.
      destruct H2; [ assumption | destruct H3 ].
       rewrite H3; rewrite H1; assumption.
       symmetry  in |- *; assumption.
Qed.

(* Le singleton *)

Definition single (a : Ens) := pair a a.

(* 3. Caractérisation des éléments du singleton *)


Lemma single_equiv :
  forall (a x : Ens), elt x (single a) <-> x = a.

Proof.
unfold single in |- *; intros; apply iff_trans with (x = a \/ x = a).
 apply pair_axiom.
 split; [ intro; destruct H; assumption | left; assumption ].
Qed.

(* Un lemme qui servira pour la question suivante *)

Lemma single_equal :
  forall a b, single a = single b -> a = b.

Proof.
intros.
destruct (single_equiv a a) as (H1, H2).
destruct (single_equiv b a) as (H3, H4).
apply H3; rewrite <- H; apply H2; reflexivity.
Qed.

(* 4. Le couple (= la paire ordonnée) *)

Definition couple (a b : Ens) := pair (single a) (pair a b).

Lemma couple_equal :
  forall a b c d, couple a b = couple c d <-> a = c /\ b = d.

Proof.
unfold couple; split; intros.
 destruct (pair_equal (single a) (pair a b) (single c) (pair c d) H).
  destruct H0.
    generalize (single_equal a c H0); clear H0; intro H0.
    destruct (pair_equal a b c d H1); destruct H2.
   split; assumption.
   split; [ assumption | rewrite <- H2; rewrite H0; assumption ].
  destruct H0.
    destruct (pair_equal a a c d H0); destruct H2;
     (split; [ assumption | idtac ]).
   destruct (pair_equal a b c c H1); destruct H4; rewrite <- H3; rewrite H2;
    assumption.
   destruct (pair_equal a b c c H1); destruct H4; rewrite <- H2; rewrite H3;
    assumption.
 destruct H; rewrite H; rewrite H0; reflexivity.
Qed.

(*****************************************)
(*   EXERCICE 3 : Axiome de séparation   *)
(*****************************************)

Parameter separ : Ens -> (Ens -> Prop) -> Ens.

Axiom separ_axiom :
  forall (P : Ens -> Prop),
    forall (a x : Ens), elt x (separ a P) <-> elt x a /\ P x.

(*
  \begin{enumerate}
  \item Définissez l'ensemble vide\ \ \verb|emptyset : Ens|,\ \
    et vérifiez qu'il est vide.\\
    (Indication: il est utile de considérer la constante
    \verb|someset| introduite au début.)
  \item Montrez que tout ensemble vide est égal à \verb|emptyset|.
  \item Montrez qu'il n'existe pas d'ensemble de tous les ensembles.\\
    (Indication: déduire de l'existence d'un tel ensemble
    le paradoxe de Russell.)
*)

Definition emptyset := separ someset (fun _ => False).

(* 1. "emptyset" est un ensemble vide *)

Lemma emptyset_is_empty :
  forall x, ~ elt x emptyset.

Proof.
unfold emptyset in |- *; intros x H.
destruct (separ_axiom (fun _ => False) someset x).
destruct (H0 H); assumption.
Qed.

(* 2. Tout ensemble vide est égal à "emptyset" *)

Lemma empty_is_emptyset :
  forall a, (forall x, ~ elt x a) -> a = emptyset.

Proof.
intros; apply extensionality; split; intros.
 destruct (H x H0).
 destruct (emptyset_is_empty x H0).
Qed.

(* 3. Il n'existe pas d'ensemble de tous les ensembles *)

Lemma no_universal_set :
  ~ (exists U, forall x, elt x U).

Proof.
intro; destruct H as (U, H).
(* On introduit l'ensemble paradoxal de Russell... *)
assert (exists R : Ens, elt R R <-> elt R U /\ ~ elt R R).
(* ... dont on démontre d'abord l'existence ... *)
 exists (separ U (fun x => ~ elt x x)).
   exact (separ_axiom (fun x => ~ elt x x) U (separ U (fun x => ~ elt x x))).
(* ... avant de faire le paradoxe. *)
 destruct H0 as (R, H0); destruct H0; assert (~ elt R R).
  intro; destruct (H0 H2); absurd (elt R R); assumption.
  apply H2; apply H1; split; [ apply H | assumption ].
Qed.

(*****************************************)
(*   EXERCICE 4 : Axiome de la réunion   *)
(*****************************************)

Parameter union : Ens -> Ens.

Axiom union_axiom :
  forall (a x : Ens), elt x (union a) <-> exists y, elt y a /\ elt x y.

(* 1. L'opérateur d'union binaire *)

Definition cup (a b : Ens) := union (pair a b).

Lemma cup_equiv :
  forall (a b x : Ens), elt x (cup a b) <-> elt x a \/ elt x b.

Proof.
unfold cup in |- *; intros.
destruct (union_axiom (pair a b) x); split; intro.
 destruct (H H1) as (y, H2); destruct H2.
   destruct (pair_axiom a b y).
   destruct (H4 H2); rewrite <- H6; [ left | right ]; assumption.
 apply H0; destruct H1; [ exists a | exists b ].
  destruct (pair_axiom a b a).
    split; [ apply H3; left; reflexivity | assumption ].
  destruct (pair_axiom a b b).
    split; [ apply H3; right; reflexivity | assumption ].
Qed.

(***************************************)
(*   EXERCICE 5 : Axiome des parties   *)
(***************************************)

Parameter power : Ens -> Ens.

Axiom power_axiom :
    forall (a x : Ens), elt x (power a) <-> subset x a.

(* 1. Les ensembles vide et plein appartiennent à l'ensemble
      des parties *)

Lemma power_bot :
  forall a : Ens, elt emptyset (power a).

Proof.
intro; destruct (power_axiom a emptyset).
apply H0; unfold subset in |- *; intros.
destruct (emptyset_is_empty x H1).
Qed.

Lemma power_top :
  forall a : Ens, elt a (power a).

Proof.
intro; destruct (power_axiom a a).
apply H0; apply subset_refl.
Qed.

(* 2. L'union est l'inverse à gauche du powerset *)

Lemma union_power :
  forall a : Ens, union (power a) = a.

Proof.
intro; apply extensionality; split; intro.
 destruct (union_axiom (power a) x).
   destruct (H0 H) as (y, H2); destruct H2.
   destruct (power_axiom a y); apply H4; assumption.
 destruct (union_axiom (power a) x).
   apply H1; exists a; split; [ apply power_top | assumption ].
Qed.

(* 3. Pour tout ensemble, il existe un objet en dehors *)

Lemma outside :
  forall a, exists x, ~ elt x a.

Proof.
intro a; exists (power (union a)).
(* On commence par montrer l'existence d'un ensemble U contenant
   l'ensemble de ses parties (on prend U := union a) *)
intro H0; assert (exists U : _, subset (power U) U).
 exists (union a); unfold subset in |- *; intros.
   destruct (union_axiom a x).
   apply H2; exists (power (union a)); split; assumption.
 clear H0 a; destruct H as (U, H).
(* On montre l'existence d'un ensemble R tel que pour tout x on ait:
   elt x R <-> elt x U /\ ~ elt x x (par axiome de séparation) *)
   assert (exists R : _, (forall x, elt x R <-> elt x U /\ ~ elt x x)).
  exists (separ U (fun x => ~ elt x x)).
    exact (separ_axiom (fun x => ~ elt x x) U).
(* Enfin, on formalise le paradoxe de Russell dans U *)
  destruct H0 as (R, H0); destruct (H0 R); assert (~ elt R R).
   intro; destruct (H1 H3); apply H5; assumption.
   apply H3; apply H2; split.
    apply H; destruct (power_axiom U R).
      apply H5; unfold subset in |- *; intros.
      destruct (H0 x); destruct (H7 H6); assumption.
    assumption.
Qed.

(***************************************)
(*   EXERCICE 6 : Axiome de l'infini   *)
(***************************************)

Definition zero := emptyset.
Definition succ (x : Ens) := cup x (single x).

(* 1. Zero est different d'un successeur *)

Lemma zero_succ :
  forall x, zero <> succ x.

Proof.
intros x H; apply (emptyset_is_empty x).
unfold zero in H; rewrite H.
destruct (cup_equiv x (single x) x).
unfold succ in |- *; apply H1.
right; destruct (single_equiv x x).
apply H3; reflexivity.
Qed.

Parameter big : Ens.
Axiom big_axiom : elt zero big /\ forall x, elt x big -> elt (succ x) big.

(* 2. Définition de l'ensemble des entiers naturels *)

Definition Nat (x : Ens) :=
  forall a, elt zero a -> (forall y, elt y a -> elt (succ y) a) -> elt x a.

Definition N := separ big Nat.

(* Stabilité par zero et succ: *)

Lemma N_zero :
  elt zero N.

Proof.
unfold N in |- *; destruct (separ_axiom Nat big zero); apply H0; split.
 destruct big_axiom; assumption.
 unfold Nat in |- *; intros; assumption.
Qed.

Lemma N_succ :
  forall x, elt x N -> elt (succ x) N.

Proof.
unfold N in |- *; intros.
destruct (separ_axiom Nat big x).
destruct (separ_axiom Nat big (succ x)).
apply H3; split.
 destruct big_axiom; apply H5; destruct (H0 H); assumption.
 unfold Nat in |- *; intros; apply H5; destruct (H0 H); apply H7; assumption.
Qed.

(* 3. Le principe de récurrence *)

Lemma N_rec :
  forall P : Ens -> Prop,
    P zero -> (forall x, elt x N -> P x -> P (succ x)) ->
      forall x, elt x N -> P x.

Proof.
intros; destruct (separ_axiom Nat big x).
destruct (H2 H1); assert (elt x (separ N P)).
 apply H5.
  destruct (separ_axiom P N zero).
    apply H7; split; [ exact N_zero | assumption ].
  intros; destruct (separ_axiom P N y).
    destruct (separ_axiom P N (succ y)); apply H10; split.
   apply N_succ; destruct (H7 H6); assumption.
   apply H0; destruct (H7 H6); assumption.
 destruct (separ_axiom P N x); destruct (H7 H6); assumption.
Qed.

(* 4. Injectivité du successeur *)

(* Lemme: les entiers sont des ensembles transitifs *)

Lemma N_trans :
  forall x, elt x N ->
    forall y z, elt z y -> elt y x -> elt z x.

Proof.
intros x H; pattern x in |- *; apply N_rec.
(* Cas de base: *)
 clear H x; intros; destruct (emptyset_is_empty y H0).
(* Cas inductif: *)
 clear H x; intros.
   destruct (cup_equiv x (single x) y) as (H3, _).
   destruct (H3 H2).
  destruct (cup_equiv x (single x) z) as (_, H5).
    unfold succ in |- *; apply H5; left; apply H0 with y; assumption.
  destruct (cup_equiv x (single x) z) as (_, H5).
    unfold succ in |- *; apply H5; left.
    destruct (single_equiv x y) as (H6, _).
    rewrite <- (H6 H4); assumption.
 assumption.
Qed.

(* Lemme: sur N, le prédecesseur est calculé par l'union: *)

Lemma union_succ :
  forall x, elt x N -> union (succ x) = x.

Proof.
intros; apply extensionality; intro z; split; intro.
 destruct (union_axiom (succ x) z) as (H1, _).
   destruct (H1 H0) as (y, H2); destruct H2.
   destruct (cup_equiv x (single x) y) as (H4, _); destruct (H4 H2).
  apply N_trans with y; assumption.
  destruct (single_equiv x y) as (H6, _).
    rewrite <- (H6 H5); assumption.
 destruct (union_axiom (succ x) z) as (_, H1).
   apply H1; exists x; split.
  destruct (cup_equiv x (single x) x) as (_, H2); apply H2; right.
    destruct (single_equiv x x) as (_, H3); apply H3; reflexivity.
  assumption.
Qed.

Lemma succ_inj :
  forall x y, elt x N -> elt y N -> succ x = succ y -> x = y.

Proof.
intros.
rewrite <- (union_succ x H).
rewrite <- (union_succ y H0).
rewrite H1; reflexivity.
Qed.