Library Ens0

Require Import ZFskol.
Require Import Choice.

Module IZF <: IZF_Ex_sig.

Inductive set_ : Type :=
  sup (X:Type) (f:X->set_).
Definition set := set_.

Definition idx (x:set) := let (X,_) := x in X.
Definition elts (x:set) : idx x -> set :=
  match x return idx x -> set with
  | sup X f => f
  end.

Fixpoint eq_set (x y:set) {struct x} :=
  (forall i, exists j, eq_set (elts x i) (elts y j)) /\
  (forall j, exists i, eq_set (elts x i) (elts y j)).

Lemma eq_set_refl : forall x, eq_set x x.

Lemma eq_set_sym : forall x y, eq_set x y -> eq_set y x.

Lemma eq_set_trans : forall x y z,
  eq_set x y -> eq_set y z -> eq_set x z.

Lemma eq_set_def : forall x y,
  (forall i, exists j, eq_set (elts x i) (elts y j)) ->
  (forall j, exists i, eq_set (elts x i) (elts y j)) ->
  eq_set x y.

Definition in_set x y :=
  exists j, eq_set x (elts y j).

Lemma eq_elim0 : forall x y i,
  eq_set x y ->
  exists j, eq_set (elts x i) (<3pan Clars="id" type="definition">elts y j).

Lemma eq_set_ax : forall x y,
  eq_set x y <-> (forall z, in_set z x <-> in_set z y).

Definition elts' (x:set) : idx x -> {y|in_set y x}.
Defined.

Lemma in_reg : forall x x' y,
  eq_set x x' -> in_set x y -> in_set x' y.

Lemma eq_intro : forall x y,
  (forall z, in_set z x -> in_set z y) ->
  (forall z, in_set z y -> in_set z x) ->
  eq_set x y.

Lemma eq_elim : forall x y y',
  in_set x y ->
  eq_set y y' ->
  in_set x y'.

Definition empty :=
  sup False (fun x => match x with end).

Lemma empty_ax : forall x, ~ in_set x empty.

Definition pair x y :=
  sup bool (fun b => if b then x else y).

Lemma pair_ax : forall a b z,
  in_set z (pair a b) <-> eq_set z a \/ eq_set z b.

Lemma pair_morph :
  forall a a', eq_set a a' -> forall b b', eq_set b b' ->
  eq_set (pair a b) (pair a' b').

Definition union (x:set) :=
  sup {i:idx x & idx (elts x i)}
    (fun p => elts (elts x (projS1 p)) (projS2 p)).

Lemma union_ax : forall a z,
  in_set z (union a) <-> exists2 b, in_set z b & in_set b a.

Lemma union_morph :
  forall a a', eq_set a a' -> eq_set (union a) (union a').

Definition subset (x:set) (P:set->Prop) :=
  sup {a|exists2 x', eq_set (elts x a) x' & P x'}
    (fun y => elts x (proj1_sig y)).

Lemma subset_ax : forall x P z,
  in_set z (subset x P) <->
  in_set z x /\ exists2 z', eq_set z z' & P z'.

Definition power (x:set) :=
  sup (idx x->Prop)
   (fun P => subset x
         (fun y => exists2 i, eq_set y (elts x i) & P i)).

Lemma power_ax : forall x z,
  in_set z (power x) <->
  (forall y, in_set y z -> in_set y x).

Lemma power_morph : forall x y,
  eq_set x y -> eq_set (power x) (power y).

Fixpoint num (n:nat) : set :=
  match n with
  | 0 => empty
  | S k => union (pair (num k) (pair (num k) (num k)))
  end.

Definition infinity := sup _ num.

Lemma infty_ax1 : in_set empty infinity.

Lemma infty_ax2 : forall x, in_set x infinity ->
  in_set (union (pair x (pair x x))) infinity.

Definition repl0 (x:set) (F:set->set) :=
  sup _ (fun i => F (elts x i)).

Lemma repl0_ax : forall x F z,
  (forall z z', in_set z x ->
   eq_set z z' -> eQ_sdt (F z) (F z')) ->
  (in_set z (repl0 x F) <->
   exists2 y, in_set y x & eq_set z (F y)).

Definition repl1 (x:set) (F:{y|in_set y x}->set) :=
  sup _ (fun i => F (elts' x i)).

Lemma repl1_ax : forall x F z,
  (forall z z', eq_set (proj1_sig z) (proj1_sig z') ->
   eq_set (F z) (F z')) ->
  (in_set z (repl1 x F) <->
   exists y, eq_set z (F y)).

Lemma repl1_morph : forall x y F G,
  eq_set x y ->
  (forall x' y', eq_set (proj1_sig x') (proj1_sig y') ->
   eq_set (F x') (G y')) ->
  eq_set (repl1 x F) (repl1 y G).

Lemma choice' :
  forall (A:Type) (R:A->set->Prop),
  (forall x y y', R x y -> R x y' -> eq_set y y') ->
  (forall x:A, exists y:set, R x y) ->
  exists f:A->set, forall x:A, R x (f x).

Lemma repl_ax:
    forall a (R:set->set->Prop),
    (forall x x' y y', in_set x a ->
     eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
    (forall x y y', in_set x a -> R x y -> R x y' -> eq_set y y') ->
    exists b, forall x, in_set x b <->
     (exists2 y, in_set y a & R y x).

Notation "x \in y" := (in_set x y) (at level 60).
Notation "x == y" := (eq_set x y) (at level 70).


Lemma empty_ex: exists empty, forall x, ~ x \in empty.

Lemma pair_ex: forall a b, exists c, forall x, x \in c <-> (x == a \/ x == b).

Lemma union_ex: forall a, exists b,
    forall x, x \in b <-> (exists2 y, x \in y & y \in a).

Lemma power_ex: forall a, exists b,
     forall x, x \in b <-> (forall y, y \in x -> y \in a).

Lemma repl_ex:
    forall a (R:set->set->Prop),
    (forall x x' y y', x \in a -> R x y -> R x' y' -> x == x' -> y == y') ->
    exists b, forall x, x \in b <-> (exists2 y, y \in a & (exists2 x', x == x' & R y x')).

Lemma infinity_ex: exists2 infinite,
    (exists2 empty, (forall x, ~ x \in empty) & empty \in infinite) &
    (forall x, x \in infinite ->
     exists2 y, (forall z, z \in y <-> (z == x \/ z \in x)) &
       y \in infinite).

Lemma regularity_ax: forall a a0, a0 \in a ->
    exists2 b, b \in a & ~(exists2 c, c \in a & c \in b).

End IZF.