Library Ens0
In this file, we give an attempt to build a model of IZF
in Coq.
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.