Library Ens

Require Import ZFskol.
Require Import Choice. Require Import Sublogic.

Module IZF_R <: IZF_R_Ex_sig CoqSublogicThms.

Definition Ti := Type.

Inductive set_ : Type :=
  sup (X:Ti) (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} :=
  (∀ i, exists j, eq_set (elts x i) (elts y j)) /\
  (∀ j, exists i, eq_set (elts x i) (elts y j)).

Lemma eq_set_refl : ∀ x, eq_set x x.

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

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

Lemma eq_set_def : ∀ x y,
  (∀ i, exists j, eq_set (elts x i) (elts y j)) ->
  (∀ 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).

Definition incl_set x y := ∀ z, in_set z x -> in_set z y.

Lemma eq_elim0 : ∀ x y i,
  eq_set x y ->
  exists j, eq_set (elts x i) (elts y j).

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

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

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

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

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


Lemma Acc_in_set : ∀ x, Acc in_set x.

Lemma wf_rec :
  ∀ P : set -> Type,
  (∀ x, (∀ y, in_set y x -> P y) -> P x) -> ∀ x, P x.

Lemma wf_ax :
  ∀ (P:set->Prop),
  (∀ x, P x -> P x) ->
  (∀ x, (∀ y, in_set y x -> P y) -> P x) -> ∀ x, P x.


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

Lemma empty_ax : ∀ x, ~ in_set x empty.

Definition singl x := sup unit (fun _ => x).

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

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

Lemma pair_morph :
  ∀ a a', eq_set a a' -> ∀ 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 : ∀ a z,
  in_set z (union a) <-> exists2 b, in_set z b & in_set b a.

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

Fixpoint wfrec (F:(set->set)->set->set) (x:set) : set :=
  F (fun y => union (sup {i:idx x|eq_set (elts x i) y}
               (fun i => wfrec F (elts x (proj1_sig i))))) x.
Section FixRec.
Hypothesis F : (set->set)->set->set.
Hypothesis Fext : ∀ x x' f f',
  (∀ y y', in_set y x -> eq_set y y' -> eq_set (f y) (f' y')) ->
  eq_set x x' ->
  eq_set (F f x) (F f' x').

Instance wfrecm : Proper (eq_set==>eq_set) (wfrec F).

Qed.

Lemma wfrec_eqn x :
  eq_set (wfrec F x) (F (wfrec F) x).
End FixRec.

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 : ∀ 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 : ∀ x z,
  in_set z (power x) <->
  (∀ y, in_set y z -> in_set y x).

Lemma power_morph : ∀ 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 : ∀ x, in_set x infinity ->
  in_set (union (pair x (pair x x))) infinity.

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

Lemma replf_ax : ∀ x F z,
  (∀ z z', in_set z x ->
   eq_set z z' -> eq_set (F z) (F z')) ->
  (in_set z (replf 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 : ∀ x F z,
  (∀ 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 : ∀ x y F G,
  eq_set x y ->
  (∀ x' y', eq_set (proj1_sig x') (proj1_sig y') ->
   eq_set (F x') (G y')) ->
  eq_set (repl1 x F) (repl1 y G).

Definition ttrepl :=
  ∀ a:set, unique_choice {x|in_set x a} set eq_set.

Lemma ttrepl_axiom : ttrepl.

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

Lemma ttrepl_needed_for_repl :
  ∀ a:set,
  let A := {x|in_set x a} in
  let eqA (x y:A) := eq_set (proj1_sig x) (proj1_sig y) in
  let B := set in
  let eqB := eq_set in
  ∀ (R:A->B->Prop),
  Proper (eqA==>eqB==>iff) R ->
  (∀ x:A, exists y:B, R x y) ->
  (∀ x y y', R x y -> R x y' -> eqB y y') ->
  exists f:A->B, ∀ x:A, R x (f x).

Notation "x ∈ y" := (in_set x y).
Notation "x == y" := (eq_set x y).


Lemma empty_ex: exists empty, ∀ x, ~ x ∈ empty.

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

Lemma union_ex: ∀ a, exists b,
    ∀ x, x ∈ b <-> (exists2 y, x ∈ y & y ∈ a).

Lemma subset_ex : ∀ x P, exists b,
  ∀ z, z ∈ b <->
  (z ∈ x /\ exists2 z', z == z' & P z').

Lemma power_ex: ∀ a, exists b,
     ∀ x, x ∈ b <-> (∀ y, y ∈ x -> y ∈ a).

Lemma repl_ex: ∀ a (R:set->set->Prop),
    (∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
    (∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
    exists b, ∀ x, x ∈ b <-> (exists2 y, y ∈ a & R y x).
Section Collection.

Section FromTTColl.

Lemma ttcoll :
  ∀ (A:Ti) (R:A->set->Prop),
  (∀ x:A, exists y:set, R x y) ->
  exists X:Ti, exists f : X->set,
    ∀ x:A, exists i:X, R x (f i).

Lemma ttcoll' :
  ∀ (A:Ti) R,
  (∀ x:A, exists y:set, R x y) ->
  exists B, ∀ x:A, exists2 y, y ∈ B & R x y.

Lemma coll_ax_ttcoll : ∀ A (R:set->set->Prop),
    (∀ x x' y y', in_set x A ->
     eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
    (∀ x, in_set x A -> exists y, R x y) ->
    exists B, ∀ x, in_set x A -> exists2 y, in_set y B & R x y.

Lemma ttcoll'' : ∀ A (R:set->set->Prop),
  (∀ x x' y y', in_set x A ->
   eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
  (∀ x, x ∈ A -> exists y:set, R x y) ->
  exists f : {x|x∈ A} -> {X:Ti & X->set},
    ∀ x, exists i:projT1 (f x), R (proj1_sig x) (projT2 (f x) i).

End FromTTColl.

Section FromChoice.

Lemma coll_ax_choice : ∀ A (R:set->set->Prop),
    (∀ x x' y y', in_set x A ->
     eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
    (∀ x, in_set x A -> exists y, R x y) ->
    exists B, ∀ x, in_set x A -> exists y, in_set y B /\ R x y.

End FromChoice.

Section FromReplClassic.

Hypothesis EM : ∀ A:Prop, A \/ ~A.

Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))).

Lemma V_morph : ∀ x x', eq_set x x' -> eq_set (V x) (V x').

Lemma V_def : ∀ x z,
  in_set z (V x) <-> exists y, in_set y x /\ incl_set z (V y).

Lemma V_trans : ∀ x y z,
  z ∈ y -> y ∈ V x -> z ∈ V x.

Lemma V_pow : ∀ x, power (V x) == V (singl x).

Lemma V_mono : ∀ x x',
  in_set x x' -> in_set (V x) (V x').

Lemma V_sub : ∀ x y y',
  in_set y (V x) -> incl_set y' y -> in_set y' (V x).

Lemma V_compl : ∀ x z, in_set z (V x) -> in_set (V z) (V x).

Lemma V_intro : ∀ x, incl_set x (V x).

Lemma V_idem : ∀ x, V (V x) == V x.

Lemma rk_induc :
  ∀ P:set->Prop,
  (∀ x, (∀ y, y ∈ V x -> P y) -> P x) ->
  ∀ x, P x.

Lemma V_total : ∀ x y, in_set (V x) (V y) \/ incl_set (V y) (V x).

Definition lst_rk (P:set->Prop) (y:set) :=
  P y /\
  (exists w, y == V w) /\
  (∀ x, (exists w, x == V w) -> P x -> incl_set y (V x)).

Lemma lst_rk_morph :
  ∀ (P P':set->Prop), (∀ x x', x == x' -> (P x <-> P' x')) ->
  ∀ y y', y == y' -> lst_rk P y -> lst_rk P' y'.

Lemma lst_incl : ∀ P y, lst_rk P y -> P y.

Lemma lst_fun : ∀ P y y', lst_rk P y -> lst_rk P y' -> y == y'.

Lemma lst_ex : ∀ (P:set->Prop), (∀ x x', eq_set x x' -> P x -> P x') ->
  (exists x, P (V x)) -> exists y, lst_rk P y.

Lemma coll_ax : ∀ A (R:set->set->Prop),
    (∀ x x' y y', in_set x A ->
     eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
    (∀ x, in_set x A -> exists y, R x y) ->
    exists B, ∀ x, in_set x A -> exists y, in_set y B /\ R x y.

Lemma coll2_ax : ∀ A (R:set->set->Prop) x,
    (∀ x x' y y', in_set x A ->
     eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
    (exists y, R x y) ->
    in_set x A ->
    exists B, exists y, in_set y B /\ R x y.

End FromReplClassic.

End Collection.


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

Lemma set_dec_EM :
  (∀ x y, in_set x y \/ ~ in_set x y) ->
  (∀ P, P \/ ~ P).


Section Choice.

Hypothesis C : ∀ X:Type, X + (X->False).

Lemma impl_choice_ax : ∀ A B, choice A B.

Definition choose (x:set) :=
  match C (idx x) with
  | inl i => elts x i
  | _ => empty
  end.

Lemma choose_ax : ∀ a, (exists x, x ∈ a) -> choose a ∈ a.

Lemma choose_not_morph : ~ ∀ x x', x == x' -> choose x == choose x'.

End Choice.


Section Regularity.

Definition regularity :=
  ∀ a a0, a0 ∈ a ->
  exists2 b, b ∈ a & ~(exists2 c, c ∈ a & c ∈ b).

Lemma regularity_ax (EM:∀ P,P\/~P): regularity.

Lemma regularity_is_classical (reg : regularity) : ∀ P, P \/ ~P.

End Regularity.

End IZF_R.