Require Import basic.
Require Export ZFdef.
Require Import EnsEm Sublogic.

Module Skolem (L:SublogicTheory).

Module Z := Ensembles L.
Import L.

Instance Zsetoid: Equivalence Z.eq_set.

Instance Zin_morph : Proper (Z.eq_set ==> Z.eq_set ==> iff) Z.in_set.

Definition set :=
  { f : Z.set -> Prop |
    (#exists u, f u) /\
    (∀ a a', f a -> f a' -> Z.eq_set a a') }.

Lemma set_intro : ∀ (f:Z.set->Prop) (P:set->Prop),
  (#exists u, f u) ->
  (∀ a a', f a -> f a' -> Z.eq_set a a') ->
  (∀ Hex Huniq, P (exist _ f (conj Hex Huniq))) ->
  sig P.

Inductive in_set_ (x y:set) : Prop :=
 InSet
  (_:#exists2 x', proj1_sig x x' &
      exists2 y', proj1_sig y y' & Z.in_set x' y').

Definition in_set := in_set_.

Lemma inset_isL x y : isL (in_set x y).
Global Hint Resolve inset_isL.

Lemma in_set_elim : ∀ x y, in_set x y <->
  #exists2 x', proj1_sig x x' &
   exists2 y', proj1_sig y y' & Z.in_set x' y'.

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

Definition eq_set a b := ∀ x, x ∈ a <-> x ∈ b.

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

Lemma eqset_isL x y : isL (x == y).
Global Hint Resolve eqset_isL.

Lemma eq_set_ax : ∀ a b, a == b <-> (∀ x, x ∈ a <-> x ∈ b).

Instance eq_setoid: Equivalence eq_set.

Lemma In_intro: ∀ x y: set,
  (∀ x' y', proj1_sig x x' -> proj1_sig y y' -> Z.in_set x' y') ->
  x ∈ y.

Lemma In_elim (P:Prop) (x y:set):
  isL P ->
  (∀ x' y', proj1_sig x x' -> proj1_sig y y' -> Z.in_set x' y' -> P) ->
  x ∈ y -> P.

Definition Z2set (x:Z.set) : set.

Defined.

Lemma Eq_proj : ∀ (x:set) x', proj1_sig x x' -> x == Z2set x'.

Lemma inZ_in : ∀ a b, Z.in_set a b -> Z2set a ∈ Z2set b.

Lemma in_inZ : ∀ a b, Z2set a ∈ Z2set b -> Z.in_set a b.

Lemma in_equiv a b : in_set (Z2set a) (Z2set b) <-> Z.in_set a b.

Lemma eq_Zeq : ∀ x y, Z2set x == Z2set y -> Z.eq_set x y.

Lemma Zeq_eq : ∀ x y, Z.eq_set x y -> Z2set x == Z2set y.

Lemma eq_equiv x y : Z2set x == Z2set y <-> Z.eq_set x y.

Instance Z2set_morph : Proper (Z.eq_set ==> eq_set) Z2set.
Qed.

Lemma in_reg : ∀ a a' b, a == a' -> a ∈ b -> a' ∈ b.

Instance in_morph : Proper (eq_set ==> eq_set ==> iff) in_set.

Lemma Z2set_surj : ∀ x, #exists y, x == Z2set y.


Lemma ex2_equiv (P Q:_->Prop) (P' Q':_->Prop) :
  (∀ x x', x == Z2set x' -> (P x <-> P' x')) ->
  (∀ x x', x == Z2set x' -> (Q x <-> Q' x')) ->
  ((#ex2 P Q) <-> (#ex2 P' Q')).

Lemma set_intro' (P:set->Prop) (P':set->Prop) :
  (∀ x, isL (P x)) ->
  Proper (eq_set ==> iff) P ->
  (∀ z, (∀ x, x ∈ z <-> P x) -> P' z) ->
  (#exists z, ∀ x, Z.in_set x z <-> P (Z2set x)) ->
  sig P'.

Lemma empty_sig : { empty | ∀ x, x ∈ empty -> #False }.

Definition empty := proj1_sig empty_sig.
Lemma empty_ax: ∀ x, x ∈ empty -> #False.

Let pair_spec a b x := #(x == a \/ x == b).

Let pair_spec_morph a b :
  Proper (eq_set ==> iff) (pair_spec a b).
Qed.

Lemma pair_sig : ∀ a b,
  { pair | ∀ x, x ∈ pair <-> pair_spec a b x }.

Definition pair a b := proj1_sig (pair_sig a b).
Lemma pair_ax: ∀ a b x, x ∈ pair a b <-> #(x == a \/ x == b).

Let union_spec a x := #exists2 y, x ∈ y & y ∈ a.

Let union_spec_morph a :
  Proper (eq_set==>iff) (union_spec a).
Qed.

Lemma union_sig: ∀ a,
  { union | ∀ x, x ∈ union <-> union_spec a x }.

Definition union a := proj1_sig (union_sig a).
Lemma union_ax: ∀ a x,
  x ∈ union a <-> #exists2 y, x ∈ y & y ∈ a.

Let subset_spec a P x := x ∈ a /\ #exists2 x', x == x' & P x'.

Let subset_spec_morph a P :
  Proper (eq_set ==> iff) (subset_spec a P).

Qed.

Lemma subset_sig: ∀ a P,
  { subset | ∀ x, x ∈ subset <->
             (x ∈ a /\ #exists2 x', x==x' & P x') }.

Definition subset a P := proj1_sig (subset_sig a P).
Lemma subset_ax : ∀ a P x,
    x ∈ subset a P <-> (x ∈ a /\ #exists2 x', x==x' & P x').

Let power_spec a x := ∀ y, y ∈ x -> y ∈ a.

Let power_spec_morph a :
  Proper (eq_set ==> iff) (power_spec a).
Qed.

Lemma power_sig: ∀ a,
  { power | ∀ x, x ∈ power <-> (∀ y, y ∈ x -> y ∈ a) }.

Definition power a := proj1_sig (power_sig a).
Lemma power_ax:
  ∀ a x, x ∈ power a <-> (∀ y, y ∈ x -> y ∈ a).

Definition uchoice_pred (P:set->Prop) :=
  (∀ x x', x == x' -> P x -> P x') /\
  (#exists x, P x) /\
  (∀ x x', P x -> P x' -> x == x').

Definition uchoice (P : set -> Prop) (Hp : uchoice_pred P) : set.

Defined.

Lemma uchoice_ax : ∀ P h x,
  (x ∈ uchoice P h <-> #exists2 z, P z & x ∈ z).

Lemma uchoice_morph_raw : ∀ (P1 P2:set->Prop) h1 h2,
  (∀ x x', x == x' -> (P1 x <-> P2 x')) ->
  uchoice P1 h1 == uchoice P2 h2.

Instance uchoice_pred_morph : Proper ((eq_set ==> iff) ==> iff) uchoice_pred.


Qed.

Lemma uchoice_ext : ∀ (P:set->Prop) h x, (#P x) -> x == uchoice P h.

Lemma uchoice_def : ∀ P h, #P (uchoice P h).

Definition Nat x :=
  ∀ (P:set),
  empty ∈ P ->
  (∀ x, x ∈ P -> union (pair x (pair x x)) ∈ P) ->
  x ∈ P.

Instance Nat_morph : Proper (eq_set ==> iff) Nat.
Qed.

Lemma Nat_S : ∀ x,
  Nat x -> Nat (union (pair x (pair x x))).

Definition infinite_sig :
  { infty | empty ∈ infty /\
      ∀ x, x ∈ infty -> union (pair x (pair x x)) ∈ infty }.












Qed.
Definition infinite := proj1_sig infinite_sig.
Lemma infinity_ax1: empty ∈ infinite.
Lemma infinity_ax2: ∀ x,
  x ∈ infinite -> union (pair x (pair x x)) ∈ infinite.

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

Definition funDom (R:set -> set -> Prop) x :=
  ∀ x' y y', R x y -> R x' y' -> x == x' -> y == y'.
Definition downR (R:set -> set -> Prop) x' y' :=
  exists2 x, x == Z2set x' /\ funDom R x & exists2 y, y == Z2set y' & R x y.

Lemma downR_morph : Proper
  ((eq_set ==> eq_set ==> iff) ==> Z.eq_set ==> Z.eq_set ==> iff) downR.

Lemma downRm : ∀ R x x' y y',
  Z.eq_set x x' ->
  Z.eq_set y y' ->
  downR R x y ->
  downR R x' y'.

Lemma downR_fun : ∀ R x y y',
  downR R x y ->
  downR R x y' ->
  Z.eq_set y y'.

Module Type ExReplacement.
Parameter repl_ex : ∀ a (R:Z.set->Z.set->Prop),
  (∀ x x' y y', Z.in_set x a -> Z.eq_set x x' -> Z.eq_set y y' -> R x y -> R x' y') ->
  (∀ x y y', Z.in_set x a -> R x y -> R x y' -> Z.eq_set y y') ->
  #exists b, ∀ x, Z.in_set x b <-> #exists2 y, Z.in_set y a & R y x.
End ExReplacement.

Module SkolemReplacement (Repl : ExReplacement).

Lemma repl0 : ∀ (a:set) (R:set->set->Prop), set.

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

Lemma repl0_mono :
  Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl0.

Lemma repl_sig :
  { repl |
    Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl /\
    ∀ 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') ->
    ∀ x, x ∈ repl a R <-> #exists2 y, y ∈ a & R y x }.

Definition repl := proj1_sig repl_sig.
Lemma repl_mono :
  Proper (incl_set ==> (eq_set ==> eq_set ==> iff) ==> incl_set) repl.
Lemma repl_ax:
    ∀ 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') ->
    ∀ x, x ∈ repl a R <-> #exists2 y, y ∈ a & R y x.
End SkolemReplacement.

Definition downR' (R:set -> set -> Prop) x' y' :=
  exists2 x, x == Z2set x' & exists2 y, y == Z2set y' & R x y.

Lemma downR'_morph : Proper
  ((eq_set ==> eq_set ==> iff) ==> Z.eq_set ==> Z.eq_set ==> iff) downR'.

Lemma coll_ex : ∀ A (R:set->set->Prop),
    Proper (eq_set ==> eq_set ==> iff) R ->
    #exists B, ∀ x, x ∈ A ->
         (#exists y, R x y) -> #exists2 y, y ∈ B & R x y.

Module ClassicCollection.

Section Classic.

Hypothesis EM : ∀ P, #(P \/ (P -> #False)).

Lemma coll_sig : ∀ A (R:set->set->Prop),
  {coll| Proper (eq_set==>eq_set==>iff) R ->
     ∀ x, x ∈ A ->
     (#exists y, R x y) ->
     (#exists2 y, y ∈ coll & R x y) }.

Definition coll A R := proj1_sig (coll_sig A R).
Lemma coll_ax : ∀ A (R:set->set->Prop),
  Proper (eq_set==>eq_set==>iff) R ->
  ∀ x, x ∈ A -> (#exists y, R x y) ->
  #exists2 y, y ∈ coll A R & R x y.
End Classic.
End ClassicCollection.

End Skolem.

Module IZF_R <: IZF_R_sig CoqSublogicThms.
  Import CoqSublogic.
  Include Skolem CoqSublogicThms.
  Definition intuit : ∀ P:Prop, Tr P -> P := fun P h => h.
  Module Re <: ExReplacement.
    Definition repl_ex := Z.intuit_repl_ax intuit.
  End Re.
  Include SkolemReplacement Re.
End IZF_R.

Let IZFRpack := (IZF_R.repl_mono,IZF_R.repl_ax,IZF_R.wf_ax).
Print Assumptions IZFRpack.

Module IZF_C <: IZF_C_sig CoqSublogicThms := Skolem CoqSublogicThms.
Let IZFCpack := (IZF_C.coll_ex,IZF_C.wf_ax).
Print Assumptions IZFCpack.

Module ZF <: ZF_sig ClassicSublogicThms.
 Include Skolem ClassicSublogicThms.
 Import ClassicSublogicThms.
 Lemma EM : ∀ P, #(P \/ (P -> #False)).
 Definition coll := (ClassicCollection.coll EM).
 Lemma coll_ax : ∀ A R,
    Proper (eq_set==>eq_set==>iff) R ->
    ∀ x, x ∈ A ->
      (#exists y, R x y) -> (#exists2 y, y ∈ coll A R & R x y).
End ZF.

Let ZFpack := ZF.coll_ax.
Print Assumptions ZFpack.