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


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

Lemma subset_refl : forall a, subset a a.
Proof.
intros a x ax; exact ax.
Qed.

Lemma subset_trans : forall a b c, 
  subset a b -> subset b c -> subset a c.
Proof.
intros a b c sab sbc x ax.
apply sbc.
apply sab.
assumption.
Qed.

(* La réciproque de l'extensionalité est vraie*)
Lemma subst_ens : forall a b : Ens,
  a = b -> (forall x, elt x a <-> elt x b).
Proof.
intros a b eab x.
rewrite eab.
split; trivial.
Qed.

Lemma antisym2ext : 
(forall a b, subset a b -> subset b a -> a = b) ->
(forall (a b : Ens), (forall x, elt x a <-> elt x b) -> a = b).
Proof.
intros antisym a b eab.
apply antisym; intro x; case (eab x); intros xab xba; assumption.
Qed.


(* On ajoute un axiome : celui d'extensionnalité *)
Axiom extensionality :
  forall (a b : Ens), (forall x, elt x a <-> elt x b) -> a = b.

Lemma subset_antisym : forall a b, subset a b -> subset b a -> a = b.
Proof.
intros a b; unfold subset; intros sab sba.
apply extensionality.
intros x; split; [apply sab | apply sba].
Qed.

(* Avec des paires *)
Parameter pair : Ens -> Ens -> Ens.


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


(* On commence par un lemme, toujours sans rw : *)

Lemma pair_eq_subset : forall a a' b b', 
  a = a' -> b = b' -> subset (pair a b) (pair a' b').
Proof.
intros a a' b b' e e' x exab.
destruct (pair_axiom a b x) as [H1 H2].
assert (H3 := H1 exab); clear H1.
destruct (pair_axiom a' b' x) as [H1' H2'].
apply H2'.
destruct H3.
  left; transitivity a; trivial.
right; transitivity b; trivial.
Qed.

Lemma pair_ext : forall a a' b b', 
  a = a' -> b = b' -> pair a b = pair a' b'.
Proof.
intros a a' b b' e e'.
apply subset_antisym; apply pair_eq_subset; trivial; symmetry; assumption.
Qed.

Lemma pair_destruct : forall a b c d, 
  pair a b = pair c d -> ((a = c) /\ (b = d))\/((a = d)/\(b = c)).
Proof.
intros a b c d ep.
assert (H : forall x, x = a \/ x = b <-> x = c \/ x = d).
  intro x; apply iff_trans with (elt x (pair a b)).
    apply iff_sym; exact (pair_axiom a b x).
  rewrite ep; exact (pair_axiom c d x).
destruct (H a) as [H1 _].
assert (H2 : a = c \/ a = d) by (apply H1; left; trivial).
clear H1.
destruct (H b) as [H1 _].
assert (H3 : b = c \/ b = d) by (apply H1; right; trivial).
clear H1.
destruct (H c) as [_ H1].
assert (H4 : c = a \/ c = b) by (apply H1; left; trivial).
clear H1.
destruct (H d) as [_ H1].
assert (H5 : d = a \/ d = b) by (apply H1; right; trivial).
clear H1.
destruct H2 as [eac | ead]; [left; split; trivial | right; split; trivial].
  destruct H3 as [ebc | ebd]; trivial.
  destruct H5 as [ed|ed]; rewrite ed; trivial.
  rewrite ebc; rewrite eac; trivial.
destruct H3 as [ebc | ebd]; trivial.
destruct H4 as [ec|ec]; rewrite ec; trivial.
rewrite ead; rewrite ebd; trivial.
Qed.


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

Lemma elt_single : forall a x, elt x (single a) <-> x = a.
Proof.
intros a x; apply iff_trans with (x = a \/ x = a).
  unfold single; apply pair_axiom.
split; auto.
intros h; case h; trivial.
Qed.


Lemma single_eq : forall a b, single a = single b -> a = b.
Proof.
intros a b es.
destruct (elt_single a a) as [H1 H2].
destruct (elt_single b a) as [H3 H4].
apply H3; rewrite <- es; apply H2; reflexivity.
Qed.


(* Couples *)  
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.
intros a b c d; split.
  unfold couple; intros e.
  destruct (pair_destruct (single a) (pair a b) (single c) (pair c d) e) as [H|H].
    case H; intros es ep.
    assert (eac : a = c) by (apply single_eq; assumption).
    rewrite eac; split; trivial.
    destruct (pair_destruct a b c d ep) as [H1|H1].
      case H1; trivial.
    case H1; intros ead ebc; rewrite <- ead; rewrite eac; assumption.
  case H; intros e1 e2.
  destruct (pair_destruct a a c d e1) as [H1|H1]; case H1; intros e3 e4; clear H1.
    split; trivial.
  rewrite <- e4; rewrite e3.
    destruct (pair_destruct a b c c e2) as [H2|H2]; case H2; intros _ ebc; trivial.
  split; trivial.
  destruct (pair_destruct a b c c e2) as [H2|H2]; case H2; intros _ ebc; trivial; clear H2.
     rewrite <- e3; rewrite e4; trivial.
  rewrite <- e3; rewrite e4; trivial.
intro e; case e; intros e1 e2; rewrite e1; rewrite e2.
trivial.
Qed.


(* 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.

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


Lemma emptyset_is_empty : forall x, ~ elt x emptyset.
Proof.
unfold emptyset in |- *; intros x H.
destruct (separ_axiom (fun _ => False) someset x) as [H1 _].
destruct (H1 H); assumption.
Qed.


Lemma empty_is_emptyset :
  forall a, (forall x, ~ elt x a) -> a = emptyset.
Proof.
intros.
apply extensionality.
intros x; split; intro hx.
   contradiction (H x).
contradiction (emptyset_is_empty x).
Qed.


Lemma no_universal_set :
  ~ (exists U, forall x, elt x U).
Proof.
intro h; destruct h as [x hx].
pose (russell_ens := separ x (fun t => ~(elt t t))).
destruct (separ_axiom (fun t => ~(elt t t)) x russell_ens) as [h1 h2].
fold russell_ens in h2, h1.
assert (nrr: ~elt russell_ens russell_ens).
  intro rr; destruct (h1 rr)as [rr' nrr]; contradiction nrr.
apply nrr; apply h2; split; trivial.
Qed.

(* 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.

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

Lemma elt_cup : forall a b x, elt x (cup a b) <->  elt x a \/ elt x b.
Proof.
intros a b x; unfold cup.
apply (@iff_trans _ _  (elt x a \/ elt x b) (union_axiom (pair a b) x)).
split; intros h.
  case h; intros y hy; destruct hy as [py yx].
  destruct (pair_axiom a b y) as [h1 h2]; assert (h3 := h1 py).
  case h3; intro hy; rewrite <- hy; [left | right]; assumption.
case h; intro hx; [exists a | exists b]; split; trivial.
  destruct (pair_axiom a b a) as [_ h2]; apply h2; auto.
destruct (pair_axiom a b b) as [_ h2]; apply h2; auto.
Qed.

(* Axiome des parties *)
Parameter power : Ens -> Ens.

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


Lemma emptyset_subset : forall a : Ens, subset emptyset a.
Proof.
unfold subset.
intros a x ex.
assert (nex := emptyset_is_empty x).
absurd (elt x emptyset); trivial.
Qed.


Lemma power_empty : forall a : Ens, elt emptyset (power a).
Proof.
intro a.
destruct (power_axiom a emptyset) as [pa1 pa2].
apply pa2.
apply emptyset_subset.
Qed.

Lemma power_top : forall a : Ens, elt a (power a).
Proof.
intro a.
destruct (power_axiom a a) as [pa1 pa2].
apply pa2.
apply subset_refl.
Qed.

Lemma power_union : forall a : Ens, union (power a) = a.
Proof.
intros a.
apply extensionality; intros x; split; intro h.
  destruct (union_axiom (power a) x) as [ua1 ua2].
  destruct (ua1 h) as [y hy].
  destruct hy as [hy1 hy2].
  destruct (power_axiom a y) as [hy3 hy4].
  apply hy3; trivial.
destruct (union_axiom (power a) x) as [ua1 ua2].
apply ua2.
exists a; split; trivial.
apply power_top.
Qed.

Lemma exists_outside : forall (a : Ens), exists x : Ens, ~ elt x a.
Proof.
intros a.
pose (out := power (union a)).
exists out.
intro h.
(* on montre aue h est inconsistante car alors :*)
pose (u := union a).
(* 1- L'ensemble u contiendrait l'ensemble de ses parties *)
assert (hu : subset (power u) u).
  intros x pux.
  destruct (union_axiom a x) as [pa1 pa2].
  apply pa2. 
  exists (power u); split; trivial.
pose (r := separ u (fun x => ~ elt x x)).
(* 2- Les éléments de l'ensemble r seraient dans u et non dans eux-même*)
assert (hr : forall x, elt x r <-> elt x u /\ ~ elt x x).
  intros x.
  exact (separ_axiom (fun x => ~ elt x x) u x).
(* 3- et on obtient le paradoxe de russel dans u *)
destruct (hr r) as [hr1 hr2].
assert (nrr : ~ elt r r).
  intro rr; destruct (hr1 rr) as [r1 rr2]; absurd (elt r r); trivial.
apply nrr.
apply hr2; split; trivial.
destruct (power_axiom u r) as [h1 h2].
apply hu.
apply h2.
intros x rx.
destruct (hr x) as [hx1 hx2].
destruct (hx1 rx); assumption.
Qed.

(* Axiome de l'infini *)
Definition zero := emptyset.

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

Lemma zero_succ_ne : forall x, zero <> succ x.
Proof.
intros x h; apply (emptyset_is_empty x).
unfold zero in h; rewrite h.
destruct (elt_cup x (single x) x) as [h1 h2].
apply h2.
right; destruct (elt_single x x) as [h3 h4].
apply h4; 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.
destruct (separ_axiom Nat big zero) as [h1 h2]; apply h2; split.
destruct big_axiom as [h3 h4]; assumption.
unfold Nat in |- *; intros; assumption.
Qed.

Lemma N_succ :
  forall x, elt x N -> elt (succ x) N.
Proof.
unfold N in |- *; intros x h.
destruct (separ_axiom Nat big x) as [h1 h2].
destruct (separ_axiom Nat big (succ x)) as [h3 h4].
apply h4; split.
 destruct big_axiom as [h6 h7]; apply h7; destruct (h1 h); assumption.
unfold Nat in |- *; intros h5 h6 h7; apply h7; destruct (h1 h) as [h8 h9]; apply h9; 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 (elt_cup x (single x) y) as (H3, _).
   destruct (H3 H2).
  destruct (elt_cup x (single x) z) as (_, H5).
    unfold succ in |- *; apply H5; left; apply H0 with y; assumption.
  destruct (elt_cup x (single x) z) as (_, H5).
    unfold succ in |- *; apply H5; left.
    destruct (elt_single 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 (elt_cup x (single x) y) as (H4, _); destruct (H4 H2).
  apply N_trans with y; assumption.
  destruct (elt_single x y) as (H6, _).
    rewrite <- (H6 H5); assumption.
 destruct (union_axiom (succ x) z) as (_, H1).
   apply H1; exists x; split.
  destruct (elt_cup x (single x) x) as (_, H2); apply H2; right.
    destruct (elt_single 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.