Library ZFskol
Require Import basic.
Require Export ZFdef.
Require Import Sublogic.
Module Skolem (Z : IZF_R_Ex_sig CoqSublogicThms) <: IZF_R_sig CoqSublogicThms.
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 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 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.
Definition Z2set (x:Z.set) : set.
Defined.
Lemma Z2set_surj : ∀ x, exists y, x == Z2set y.
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 empty_sig : { empty | ∀ x, ~ x ∈ empty }.
Definition empty := proj1_sig empty_sig.
Lemma empty_ax: ∀ x, ~ x ∈ empty.
Lemma pair_sig : ∀ a b,
{ pair | ∀ x, x ∈ pair <-> (x == a \/ x == b) }.
Definition pair a b := proj1_sig (pair_sig a b).
Lemma pair_ax: ∀ a b x, x ∈ pair a b <-> (x == a \/ x == b).
Lemma union_sig: ∀ a,
{ union | ∀ x, x ∈ union <-> (exists2 y, x ∈ y & y ∈ a) }.
Definition union a := proj1_sig (union_sig a).
Lemma union_ax: ∀ a x,
x ∈ union a <-> (exists2 y, x ∈ y & y ∈ a).
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').
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 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'.
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.
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, P x -> P x) ->
(∀ x, (∀ y, y ∈ x -> P y) -> P x) ->
∀ x, P x.
Section Collection.
Hypothesis lst_rk : (Z.set->Prop) -> Z.set -> Prop.
Hypothesis lst_rk_morph : ∀ (P P':Z.set->Prop),
(∀ x x', Z.eq_set x x' -> (P x <-> P' x')) ->
∀ y y', Z.eq_set y y' -> lst_rk P y -> lst_rk P' y'.
Hypothesis lst_incl : ∀ P y, lst_rk P y -> P y.
Hypothesis lst_fun : ∀ P y y', lst_rk P y -> lst_rk P y' -> Z.eq_set y y'.
Hypothesis coll_ax_uniq : ∀ 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') ->
exists B, lst_rk(fun B =>
∀ x, Z.in_set x A ->
(exists y, R x y) ->
exists2 y, Z.in_set y B & R x y) B.
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 Collection.
End Skolem.