Library ZFord
This file defines and develop the basic theory of ordinals in
intuitionistic set theory. We use directed plump ordinals.
Directed set (finite union)
Definition and elementary properties
Definition isDir o := ∀ x y,
x < o -> y < o -> exists2 z, z < o & x ⊆ z /\ y ⊆ z.
Global Instance isDir_morph : Proper (eq_set==>iff) isDir.
Qed.
x < o -> y < o -> exists2 z, z < o & x ⊆ z /\ y ⊆ z.
Global Instance isDir_morph : Proper (eq_set==>iff) isDir.
Qed.
Directed plump ordinals.
Plumpness is the property that
forall ordinal x s.t. z ⊆ y ∈ x, we have z ∈ x
Since the plumpness property is not monotonic (if we have more
ordinals, the plumpness requirement becomes tighter), we could
not separate the directedness property from the plumpness one.
Even if plumpness is not monotonic, it can be defined by recursion
over the rank (since the rank of z is smaller than that of x). So
we go by first defining well-founded sets (cf ZFwf.v), then
well-founded, and finally define plumpness.
Not resorting to higher-order:
Any property could replace directedness
The set of plump ordinals included in ub, given f the sets of plump ordinals
of smaller rank.
Let plump_set f ub :=
subset (power ub)
(fun x =>
(∀ y, y ∈ ub -> y ∈ x -> y ∈ f y) /\
(∀ z y, y ∈ ub -> z ∈ f y -> z ⊆ y -> y ∈ x -> z ∈ x) /\
Q x).
Definition plumps := WFR plump_set.
Let plumps_m :
Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) plump_set.
Qed.
Lemma plump_eqn ub x :
isWf ub ->
(x ∈ plumps ub <->
x ⊆ ub /\
(∀ y, y ∈ ub -> y ∈ x -> y ∈ plumps y) /\
(∀ z y, y ∈ ub -> z ∈ plumps y -> z ⊆ y -> y ∈ x -> z ∈ x) /\
Q x).
Instance plumps_morph : morph1 plumps.
Qed.
Lemma plump_bound : ∀ ub1 ub2 x,
isWf ub1 ->
isWf ub2 ->
x ⊆ ub2 ->
x ∈ plumps ub1 -> x ∈ plumps ub2.
subset (power ub)
(fun x =>
(∀ y, y ∈ ub -> y ∈ x -> y ∈ f y) /\
(∀ z y, y ∈ ub -> z ∈ f y -> z ⊆ y -> y ∈ x -> z ∈ x) /\
Q x).
Definition plumps := WFR plump_set.
Let plumps_m :
Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) plump_set.
Qed.
Lemma plump_eqn ub x :
isWf ub ->
(x ∈ plumps ub <->
x ⊆ ub /\
(∀ y, y ∈ ub -> y ∈ x -> y ∈ plumps y) /\
(∀ z y, y ∈ ub -> z ∈ plumps y -> z ⊆ y -> y ∈ x -> z ∈ x) /\
Q x).
Instance plumps_morph : morph1 plumps.
Qed.
Lemma plump_bound : ∀ ub1 ub2 x,
isWf ub1 ->
isWf ub2 ->
x ⊆ ub2 ->
x ∈ plumps ub1 -> x ∈ plumps ub2.
The class of directed plump ordinals
Definition isOrd x := isWf x /\ x ∈ plumps x.
Lemma isOrd_wf o : isOrd o -> isWf o.
Hint Resolve isOrd_wf.
Lemma isOrd_ext : ∀ x y, x == y -> isOrd x -> isOrd y.
Global Instance isOrd_morph : Proper (eq_set ==> iff) isOrd.
Qed.
Lemma isOrd_inv : ∀ x y,
isOrd x -> y < x -> isOrd y.
Lemma isOrd_plump : ∀ z, isOrd z ->
∀ x y, isOrd x -> x ⊆ y -> y ∈ z -> x ∈ z.
Lemma isOrd_dir : ∀ z, isOrd z -> Q z.
Lemma isOrd_intro : ∀ x,
(∀ a b, isOrd a -> a ⊆ b -> b ∈ x -> a ∈ x) ->
Q x ->
(∀ y, y ∈ x -> isOrd y) ->
isOrd x.
Lemma isOrd_trans : ∀ x y z,
isOrd x -> z < y -> y < x -> z < x.
Lemma isOrd_ind : ∀ x (P:set->Prop),
(∀ y, isOrd y ->
y ⊆ x ->
(∀ z, z < y -> P z) -> P y) ->
isOrd x -> P x.
Lemma isOrd_wf o : isOrd o -> isWf o.
Hint Resolve isOrd_wf.
Lemma isOrd_ext : ∀ x y, x == y -> isOrd x -> isOrd y.
Global Instance isOrd_morph : Proper (eq_set ==> iff) isOrd.
Qed.
Lemma isOrd_inv : ∀ x y,
isOrd x -> y < x -> isOrd y.
Lemma isOrd_plump : ∀ z, isOrd z ->
∀ x y, isOrd x -> x ⊆ y -> y ∈ z -> x ∈ z.
Lemma isOrd_dir : ∀ z, isOrd z -> Q z.
Lemma isOrd_intro : ∀ x,
(∀ a b, isOrd a -> a ⊆ b -> b ∈ x -> a ∈ x) ->
Q x ->
(∀ y, y ∈ x -> isOrd y) ->
isOrd x.
Lemma isOrd_trans : ∀ x y z,
isOrd x -> z < y -> y < x -> z < x.
Lemma isOrd_ind : ∀ x (P:set->Prop),
(∀ y, isOrd y ->
y ⊆ x ->
(∀ z, z < y -> P z) -> P y) ->
isOrd x -> P x.
Alternative definition of ordinals, slightly shorter by using Coq's accessibility
predicate, and the plump property below by well-founded induction.
Module HigherOrder.
Fixpoint plump ub (p:Acc in_set ub) x : Prop :=
(∀ y (q: y ∈ ub), y ∈ x -> plump y (Acc_inv p _ q) y) /\
(∀ z y (q: y ∈ ub), plump y (Acc_inv p _ q) z ->
z ⊆ y -> y ∈ x -> z ∈ x) /\
isDir x.
Lemma plump_morph : ∀ x x' p p' y y',
x == x' -> y == y' -> (plump x p y <-> plump x' p' y').
Lemma plump_bound : ∀ ub1 ub2 p1 p2 x,
x ⊆ ub1 ->
plump ub1 p1 x -> plump ub2 p2 x.
Lemma plump_Acc : ∀ ub p x,
plump ub p x -> x ⊆ ub -> Acc in_set x.
Definition isOrd x :=
{ p:Acc in_set x | plump x p x }.
Lemma isOrd_ext : ∀ x y, x == y -> isOrd x -> isOrd y.
Instance isOrd_morph : Proper (eq_set ==> iff) isOrd.
Qed.
Lemma isOrd_inv : ∀ x y,
isOrd x -> y < x -> isOrd y.
Lemma isOrd_plump : ∀ z, isOrd z ->
∀ x y, isOrd x -> x ⊆ y -> y ∈ z -> x ∈ z.
Lemma isOrd_dir : ∀ z, isOrd z -> isDir z.
Lemma isOrd_intro : ∀ x,
(∀ a b, isOrd a -> a ⊆ b -> b ∈ x -> a ∈ x) ->
isDir x ->
(∀ y, y ∈ x -> isOrd y) ->
isOrd x.
Lemma isOrd_trans : ∀ x y z,
isOrd x -> z < y -> y < x -> z < x.
Lemma isOrd_ind : ∀ x (P:set->Prop),
(∀ y, isOrd y ->
y ⊆ x ->
(∀ z, z < y -> P z) -> P y) ->
isOrd x -> P x.
End HigherOrder.
Fixpoint plump ub (p:Acc in_set ub) x : Prop :=
(∀ y (q: y ∈ ub), y ∈ x -> plump y (Acc_inv p _ q) y) /\
(∀ z y (q: y ∈ ub), plump y (Acc_inv p _ q) z ->
z ⊆ y -> y ∈ x -> z ∈ x) /\
isDir x.
Lemma plump_morph : ∀ x x' p p' y y',
x == x' -> y == y' -> (plump x p y <-> plump x' p' y').
Lemma plump_bound : ∀ ub1 ub2 p1 p2 x,
x ⊆ ub1 ->
plump ub1 p1 x -> plump ub2 p2 x.
Lemma plump_Acc : ∀ ub p x,
plump ub p x -> x ⊆ ub -> Acc in_set x.
Definition isOrd x :=
{ p:Acc in_set x | plump x p x }.
Lemma isOrd_ext : ∀ x y, x == y -> isOrd x -> isOrd y.
Instance isOrd_morph : Proper (eq_set ==> iff) isOrd.
Qed.
Lemma isOrd_inv : ∀ x y,
isOrd x -> y < x -> isOrd y.
Lemma isOrd_plump : ∀ z, isOrd z ->
∀ x y, isOrd x -> x ⊆ y -> y ∈ z -> x ∈ z.
Lemma isOrd_dir : ∀ z, isOrd z -> isDir z.
Lemma isOrd_intro : ∀ x,
(∀ a b, isOrd a -> a ⊆ b -> b ∈ x -> a ∈ x) ->
isDir x ->
(∀ y, y ∈ x -> isOrd y) ->
isOrd x.
Lemma isOrd_trans : ∀ x y z,
isOrd x -> z < y -> y < x -> z < x.
Lemma isOrd_ind : ∀ x (P:set->Prop),
(∀ y, isOrd y ->
y ⊆ x ->
(∀ z, z < y -> P z) -> P y) ->
isOrd x -> P x.
End HigherOrder.
Successor
Definition osucc x := subset (power x) isOrd.
Instance osucc_morph : morph1 osucc.
Qed.
Lemma lt_osucc : ∀ x, isOrd x -> x < osucc x.
Hint Resolve isOrd_zero lt_osucc.
Lemma olts_le : ∀ x y, x < osucc y -> x ⊆ y.
Lemma ole_lts : ∀ x y, isOrd x -> x ⊆ y -> x < osucc y.
Lemma oles_lt : ∀ x y,
isOrd x ->
osucc x ⊆ y ->
x < y.
Lemma le_lt_trans : ∀ x y z, isOrd z -> x < osucc y -> y < z -> x < z.
Lemma ord_lt_le : ∀ o o', isOrd o -> o' ∈ o -> o' ⊆ o.
Hint Resolve ord_lt_le.
Lemma isOrd_succ : ∀ n, isOrd n -> isOrd (osucc n).
Hint Resolve isOrd_succ.
Lemma lt_osucc_compat : ∀ n m, isOrd m -> n < m -> osucc n < osucc m.
Lemma osucc_mono : ∀ n m, isOrd n -> isOrd m -> n ⊆ m -> osucc n ⊆ osucc m.
Lemma lt_osucc_inv : ∀ o o',
isOrd o ->
osucc o < osucc o' ->
o < o'.
Lemma isOrd_eq : ∀ o, isOrd o -> o == sup o osucc.
Instance osucc_morph : morph1 osucc.
Qed.
Lemma lt_osucc : ∀ x, isOrd x -> x < osucc x.
Hint Resolve isOrd_zero lt_osucc.
Lemma olts_le : ∀ x y, x < osucc y -> x ⊆ y.
Lemma ole_lts : ∀ x y, isOrd x -> x ⊆ y -> x < osucc y.
Lemma oles_lt : ∀ x y,
isOrd x ->
osucc x ⊆ y ->
x < y.
Lemma le_lt_trans : ∀ x y z, isOrd z -> x < osucc y -> y < z -> x < z.
Lemma ord_lt_le : ∀ o o', isOrd o -> o' ∈ o -> o' ⊆ o.
Hint Resolve ord_lt_le.
Lemma isOrd_succ : ∀ n, isOrd n -> isOrd (osucc n).
Hint Resolve isOrd_succ.
Lemma lt_osucc_compat : ∀ n m, isOrd m -> n < m -> osucc n < osucc m.
Lemma osucc_mono : ∀ n m, isOrd n -> isOrd m -> n ⊆ m -> osucc n ⊆ osucc m.
Lemma lt_osucc_inv : ∀ o o',
isOrd o ->
osucc o < osucc o' ->
o < o'.
Lemma isOrd_eq : ∀ o, isOrd o -> o == sup o osucc.
Examples: ordinals of rank less than 2
Module Examples.
Definition ord_0 := empty.
Definition ord_1 := osucc ord_0.
Definition ord_2 := osucc ord_1.
Definition ord_0 := empty.
Definition ord_1 := osucc ord_0.
Definition ord_2 := osucc ord_1.
1 = {0}
Lemma ord1 : ∀ x, x ∈ ord_1 <-> x == zero.
Definition ord_rk_1 P := subset ord_1 (fun _ => P).
Lemma rk1_order : ∀ P Q, ord_rk_1 P ⊆ ord_rk_1 Q <-> (P->Q).
Lemma isOrd_rk_1 : ∀ P, isOrd (ord_rk_1 P).
Definition isOrd2 x := exists P:Prop, x == ord_rk_1 P.
Definition ord_rk_1 P := subset ord_1 (fun _ => P).
Lemma rk1_order : ∀ P Q, ord_rk_1 P ⊆ ord_rk_1 Q <-> (P->Q).
Lemma isOrd_rk_1 : ∀ P, isOrd (ord_rk_1 P).
Definition isOrd2 x := exists P:Prop, x == ord_rk_1 P.
2 = {o| 0<=o<=1 } is isomorphic to Prop
Lemma ord2 : ∀ x, x ∈ ord_2 <-> exists P, x == ord_rk_1 P.
Definition ord_rk_2 (P2:Prop->Prop) :=
subset ord_2 (fun x => exists2 P, x == ord_rk_1 P & P2 P).
Definition decr_2 (P2:Prop->Prop) :=
(∀ P Q:Prop, (P -> Q) -> (P2 Q -> P2 P)) /\
(∀ P Q:Prop, P2 P -> P2 Q -> P2 (P\/Q)).
Lemma isOrd_rk_2 : ∀ P2, decr_2 P2 -> isOrd (ord_rk_2 P2).
Definition ord_rk_2 (P2:Prop->Prop) :=
subset ord_2 (fun x => exists2 P, x == ord_rk_1 P & P2 P).
Definition decr_2 (P2:Prop->Prop) :=
(∀ P Q:Prop, (P -> Q) -> (P2 Q -> P2 P)) /\
(∀ P Q:Prop, P2 P -> P2 Q -> P2 (P\/Q)).
Lemma isOrd_rk_2 : ∀ P2, decr_2 P2 -> isOrd (ord_rk_2 P2).
3 is isomorphic to decreasing functions of type Prop->Prop
(and closed by union to ensure directedness)
Increasing sequences
Definition increasing F :=
∀ x y, isOrd x -> isOrd y -> y ⊆ x -> F y ⊆ F x.
Definition increasing_bounded o F :=
∀ x x', x' < o -> x < x' -> F x ⊆ F x'.
Successor ordinals
Limit ordinals
Definition limitOrd o := isOrd o /\ (∀ x, x < o -> lt (osucc x) o).
Lemma limit_is_ord : ∀ o, limitOrd o -> isOrd o.
Hint Resolve limit_is_ord.
Lemma limit_union : ∀ o, limitOrd o -> union o == o.
Lemma limit_union_intro : ∀ o, isOrd o -> union o == o -> limitOrd o.
Lemma discr_lim_succ : ∀ o, limitOrd o -> succOrd o -> False.
Lemma isOrd_inter2 : ∀ x y,
isOrd x -> isOrd y -> isOrd (x ∩ y).
Lemma inter2_succ : ∀ x y,
isOrd x -> isOrd y ->
osucc x ∩ osucc y == osucc (x ∩ y).
Require Import ZFpairs ZFrelations.
Require Import ZFrepl.
Module FirstOrderStyle.
Section TransfiniteRecursion.
Variable F : (set -> set) -> set -> set.
Hypothesis Fm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) F.
Variable ord : set.
Hypothesis Fmorph :
∀ x f f', isOrd x -> x ⊆ ord -> eq_fun x f f' -> F f x == F f' x.
Definition isTR_rel P :=
∀ o y,
couple o y ∈ P ->
exists2 f, (∀ n, n ∈ o -> couple n (cc_app f n) ∈ P) &
y == F (cc_app f) o.
Lemma isTR_rel_fun P P' o y y':
isOrd o ->
o ⊆ ord ->
isTR_rel P ->
isTR_rel P' ->
couple o y ∈ P ->
couple o y' ∈ P' ->
y == y'.
Instance isTR_rel_morph : Proper (eq_set==>iff) isTR_rel.
Qed.
Definition TR_rel o y :=
exists2 P, isTR_rel P & couple o y ∈ P.
Instance TR_rel_morph : Proper (eq_set ==> eq_set ==> iff) TR_rel.
Qed.
Lemma TR_rel_intro x f :
morph1 f ->
isOrd x ->
x ⊆ ord ->
(∀ y, y ∈ x -> TR_rel y (f y)) ->
TR_rel x (F f x).
Lemma TR_rel_ex o :
isOrd o -> o ⊆ ord ->
uchoice_pred (TR_rel o).
Definition TR := uchoice (fun y => TR_rel ord y).
Lemma TR_eqn0 : ∀ o, isOrd o -> o ⊆ ord ->
uchoice (fun y => TR_rel o y) == F (fun o => uchoice (fun y => TR_rel o y)) o.
End TransfiniteRecursion.
Global Instance TR_morph0 : ∀ F, morph1 (TR F).
Qed.
Global Instance TR_morph :
Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) TR.
Qed.
End FirstOrderStyle.
Higher-order style: quantification over relations
Section TransfiniteRecursion.
Variable F : (set -> set) -> set -> set.
Hypothesis Fm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) F.
Variable ord : set.
Hypothesis Fmorph :
∀ x f f', isOrd x -> x ⊆ ord -> eq_fun x f f' -> F f x == F f' x.
Definition TR_rel o y :=
(isOrd o /\ o ⊆ ord) /\
∀ (P:set->set->Prop),
Proper (eq_set ==> eq_set ==> iff) P ->
(∀ o' f, isOrd o' -> o' ⊆ ord -> morph1 f ->
(∀ n, n < o' -> P n (f n)) ->
P o' (F f o')) ->
P o y.
Instance TR_rel_morph : Proper (eq_set ==> eq_set ==> iff) TR_rel.
Qed.
Lemma TR_rel_intro : ∀ x f,
isOrd x ->
x ⊆ ord ->
morph1 f ->
(∀ y, y ∈ x -> TR_rel y (f y)) ->
TR_rel x (F f x).
Lemma TR_rel_inv : ∀ x y,
TR_rel x y ->
exists2 f,
morph1 f /\ (∀ y, y ∈ x -> TR_rel y (f y)) &
y == F f x.
Lemma TR_rel_fun :
∀ x y, TR_rel x y -> ∀ y', TR_rel x y' -> y == y'.
Lemma TR_rel_repl_rel :
∀ x, repl_rel x TR_rel.
Lemma TR_rel_def : ∀ o, isOrd o -> o ⊆ ord -> exists y, TR_rel o y.
Lemma TR_rel_choice_pred : ∀ o, isOrd o -> o ⊆ ord ->
uchoice_pred (fun y => TR_rel o y).
Definition TR := uchoice (fun y => TR_rel ord y).
Lemma TR_eqn0 : ∀ o, isOrd o -> o ⊆ ord ->
uchoice (fun y => TR_rel o y) == F (fun o => uchoice (fun y => TR_rel o y)) o.
End TransfiniteRecursion.
Lemma TR_rel_irrel : ∀ F b1 b2 o y,
o ⊆ b2 ->
TR_rel F b1 o y -> TR_rel F b2 o y.
Instance TR_morph0 : ∀ F, morph1 (TR F).
Qed.
Instance TR_morph :
Proper (((eq_set ==> eq_set) ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) TR.
Qed.
Section TransfiniteRec.
Variable F : (set -> set) -> set -> set.
Hypothesis Fm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) F.
Lemma TR_eqn o :
isOrd o ->
(∀ x f f', isOrd x -> x ⊆ o -> eq_fun x f f' -> F f x == F f' x) ->
TR F o == F (TR F) o.
Lemma TR_ind : ∀ o (P:set->set->Prop),
Proper (eq_set ==> eq_set ==> iff) P ->
isOrd o ->
(∀ x f f', isOrd x -> x ⊆ o -> eq_fun x f f' -> F f x == F f' x) ->
(∀ y, isOrd y -> y ⊆ o ->
(∀ x, x < y -> P x (TR F x)) ->
P y (F (TR F) y)) ->
P o (TR F o).
Lemma TR_typ : ∀ o X,
isOrd o ->
(∀ x f f', isOrd x -> x ⊆ o -> eq_fun x f f' -> F f x == F f' x) ->
morph1 X ->
(∀ y f, morph1 f -> isOrd y -> y ⊆ o ->
(∀ z, z < y -> f z ∈ X z) -> F f y ∈ X y) ->
TR F o ∈ X o.
End TransfiniteRec.
Specialized version where the case of limit ordinals is union
Section TransfiniteIteration.
Variable F : set -> set.
Hypothesis Fmorph : Proper (eq_set ==> eq_set) F.
Let G f o := sup o (fun o' => F (f o')).
Let Gm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) G.
Qed.
Let Gmorph : ∀ o f f', eq_fun o f f' -> G f o == G f' o.
Qed.
Definition TI := TR G.
Instance TI_morph : morph1 TI.
Qed.
Lemma TI_fun_ext : ∀ x, ext_fun x (fun y => F (TI y)).
Hint Resolve TI_fun_ext.
Lemma TI_eq : ∀ o,
isOrd o ->
TI o == sup o (fun o' => F (TI o')).
Lemma TI_intro : ∀ o o' x,
isOrd o ->
lt o' o ->
x ∈ F (TI o') ->
x ∈ TI o.
Lemma TI_elim : ∀ o x,
isOrd o ->
x ∈ TI o ->
exists2 o', o' < o & x ∈ F (TI o').
Lemma TI_initial : TI zero == empty.
Lemma TI_typ : ∀ n X,
(∀ a, a ∈ X -> F a ∈ X) ->
isOrd n ->
(∀ m G, isOrd m -> m ⊆ n ->
ext_fun m G ->
(∀ x, x < m -> G x ∈ X) -> sup m G ∈ X) ->
TI n ∈ X.
End TransfiniteIteration.
Hint Resolve TI_fun_ext.
Variable F : set -> set.
Hypothesis Fmorph : Proper (eq_set ==> eq_set) F.
Let G f o := sup o (fun o' => F (f o')).
Let Gm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) G.
Qed.
Let Gmorph : ∀ o f f', eq_fun o f f' -> G f o == G f' o.
Qed.
Definition TI := TR G.
Instance TI_morph : morph1 TI.
Qed.
Lemma TI_fun_ext : ∀ x, ext_fun x (fun y => F (TI y)).
Hint Resolve TI_fun_ext.
Lemma TI_eq : ∀ o,
isOrd o ->
TI o == sup o (fun o' => F (TI o')).
Lemma TI_intro : ∀ o o' x,
isOrd o ->
lt o' o ->
x ∈ F (TI o') ->
x ∈ TI o.
Lemma TI_elim : ∀ o x,
isOrd o ->
x ∈ TI o ->
exists2 o', o' < o & x ∈ F (TI o').
Lemma TI_initial : TI zero == empty.
Lemma TI_typ : ∀ n X,
(∀ a, a ∈ X -> F a ∈ X) ->
isOrd n ->
(∀ m G, isOrd m -> m ⊆ n ->
ext_fun m G ->
(∀ x, x < m -> G x ∈ X) -> sup m G ∈ X) ->
TI n ∈ X.
End TransfiniteIteration.
Hint Resolve TI_fun_ext.
Definition osup2_rel x y z :=
∀ P,
Proper (eq_set ==> eq_set ==> eq_set ==> iff) P ->
(∀ x y g,
morph2 g ->
(∀ x' y', x' ∈ x -> y' ∈ y -> P x' y' (g x' y')) ->
P x y (x ∪ y ∪ sup x (fun x' => replf y (fun y' => g x' y')))) ->
P x y z.
Instance osup2_relm : Proper (eq_set ==> eq_set ==> eq_set ==> iff) osup2_rel.
Qed.
Lemma osup2_rel_intro : ∀ x y g,
morph2 g ->
(∀ x' y', x' ∈ x -> y' ∈ y -> osup2_rel x' y' (g x' y')) ->
osup2_rel x y (x ∪ y ∪ sup x (fun x' => replf y (fun y' => g x' y'))).
Lemma osup2_rel_elim x y z :
osup2_rel x y z ->
exists2 g, morph2 g &
(∀ x' y', x' ∈ x -> y' ∈ y -> osup2_rel x' y' (g x' y')) /\
z == x ∪ y ∪ sup x (fun x' => replf y (fun y' => g x' y')).
Lemma osup2_rel_unique x y z z' :
osup2_rel x y z ->
osup2_rel x y z' ->
z == z'.
osup2 defined on well-founded sets
Lemma uchoice_pred_osup2 : ∀ x y, isWf x -> uchoice_pred (osup2_rel x y).
Definition osup2 x y := uchoice (osup2_rel x y).
Infix "⊔" := osup2 (at level 50).
Instance osup2_morph : morph2 osup2.
Qed.
Lemma osup2_def : ∀ x y, isWf x ->
x ⊔ y == x ∪ y ∪ sup x (fun x' => replf y (fun y' => x' ⊔ y')).
Lemma osup2_ax : ∀ x y z,
isWf x ->
(z ∈ x ⊔ y <->
z ∈ x \/ z ∈ y \/
exists2 x', x' ∈ x & exists2 y', y' ∈ y & z == x' ⊔ y').
Lemma osup2_incl1 : ∀ x y, isWf x -> x ⊆ x ⊔ y.
Lemma osup2_incl2 : ∀ x y, isWf x -> y ⊆ x ⊔ y.
Lemma osup2_mono x x' y y' :
isWf x' -> x ⊆ x' -> y ⊆ y' ->
x ⊔ y ⊆ x' ⊔ y'.
Lemma isDir_osup2 : ∀ x y, isWf x -> isDir x -> isDir y -> isDir (x ⊔ y).
Lemma osup2_proof : ∀ x, isOrd x -> ∀ y, isOrd y ->
isOrd (x ⊔ y) /\
(∀ z, isOrd z -> z ∩ (x ⊔ y) == z ∩ x ⊔ z ∩ y).
Lemma isOrd_osup2 : ∀ x y,
isOrd x ->
isOrd y ->
isOrd (x ⊔ y).
Lemma osup2_lub : ∀ x y z,
isOrd x -> isOrd y -> isOrd z ->
x ⊆ z -> y ⊆ z -> x ⊔ y ⊆ z.
Lemma osup2_refl x : isOrd x -> x ⊔ x == x.
Lemma osup2_lt x y z : isOrd z -> x ∈ z -> y ∈ z -> x ⊔ y ∈ z.
Lemma isDir_succ : ∀ o,
isOrd o -> isDir (osucc o).
Lemma osup2_sym : ∀ x y, isWf x -> isWf y -> x ⊔ y == y ⊔ x.
Lemma osup2_assoc : ∀ x y z, isOrd x -> isOrd y -> isOrd z ->
x ⊔ (y ⊔ z) == x ⊔ y ⊔ z.
Definition osup2 x y := uchoice (osup2_rel x y).
Infix "⊔" := osup2 (at level 50).
Instance osup2_morph : morph2 osup2.
Qed.
Lemma osup2_def : ∀ x y, isWf x ->
x ⊔ y == x ∪ y ∪ sup x (fun x' => replf y (fun y' => x' ⊔ y')).
Lemma osup2_ax : ∀ x y z,
isWf x ->
(z ∈ x ⊔ y <->
z ∈ x \/ z ∈ y \/
exists2 x', x' ∈ x & exists2 y', y' ∈ y & z == x' ⊔ y').
Lemma osup2_incl1 : ∀ x y, isWf x -> x ⊆ x ⊔ y.
Lemma osup2_incl2 : ∀ x y, isWf x -> y ⊆ x ⊔ y.
Lemma osup2_mono x x' y y' :
isWf x' -> x ⊆ x' -> y ⊆ y' ->
x ⊔ y ⊆ x' ⊔ y'.
Lemma isDir_osup2 : ∀ x y, isWf x -> isDir x -> isDir y -> isDir (x ⊔ y).
Lemma osup2_proof : ∀ x, isOrd x -> ∀ y, isOrd y ->
isOrd (x ⊔ y) /\
(∀ z, isOrd z -> z ∩ (x ⊔ y) == z ∩ x ⊔ z ∩ y).
Lemma isOrd_osup2 : ∀ x y,
isOrd x ->
isOrd y ->
isOrd (x ⊔ y).
Lemma osup2_lub : ∀ x y z,
isOrd x -> isOrd y -> isOrd z ->
x ⊆ z -> y ⊆ z -> x ⊔ y ⊆ z.
Lemma osup2_refl x : isOrd x -> x ⊔ x == x.
Lemma osup2_lt x y z : isOrd z -> x ∈ z -> y ∈ z -> x ⊔ y ∈ z.
Lemma isDir_succ : ∀ o,
isOrd o -> isDir (osucc o).
Lemma osup2_sym : ∀ x y, isWf x -> isWf y -> x ⊔ y == y ⊔ x.
Lemma osup2_assoc : ∀ x y z, isOrd x -> isOrd y -> isOrd z ->
x ⊔ (y ⊔ z) == x ⊔ y ⊔ z.
Section OrdinalUpperBound.
Variable I : set.
Variable f : set -> set.
Hypothesis f_ext : ext_fun I f.
Hypothesis f_ord : ∀ x, x ∈ I -> isOrd (f x).
Lemma isOrd_supf_intro : ∀ n, n ∈ I -> f n ⊆ sup I f.
Lemma isOrd_supf_elim : ∀ x, x < sup I f -> exists2 n, n ∈ I & x < f n.
Hypothesis supf_dir : ∀ x y, x ∈ I -> y ∈ I ->
exists2 z, z ∈ I & f x ⊆ f z /\ f y ⊆ f z.
Lemma isDir_ord_sup : isDir (sup I f).
Lemma isOrd_supf : isOrd (sup I f).
End OrdinalUpperBound.
Require Import ZFrepl.
Section LimOrd.
Variable f : nat -> set.
Variable ford : ∀ n, isOrd (f n).
Variable fmono : ∀ m n, (m <= n)%nat -> f m ⊆ f n.
Let F x := uchoice (fun y => exists2 n, x == nat2set n & f n == y).
Let Fm : morph1 F.
Qed.
Let Fch : ∀ x, x ∈ N ->
uchoice_pred (fun y => exists2 n, x == nat2set n & f n == y).
Qed.
Definition ord_sup := sup N F.
Lemma isOrd_sup_intro : ∀ n, f n ⊆ ord_sup.
Lemma isOrd_sup_elim : ∀ x, x < ord_sup -> exists n, x < f n.
Lemma isOrd_sup : isOrd ord_sup.
Lemma ord_sup_typ X :
(∀ n, f n ∈ X) ->
(∀ g, morph1 g -> (∀ n, n ∈ N -> g n ∈ X) -> sup N g ∈ X) ->
ord_sup ∈ X.
End LimOrd.
Lemma isOrd_union : ∀ x,
(∀ y, y ∈ x -> isOrd y) ->
(∀ a a', a ∈ x -> a' ∈ x -> exists2 b, b ∈ x & a ⊆ b /\ a' ⊆ b) ->
isOrd (union x).
Lemma isOrd_inter : ∀ x,
(∀ y, y ∈ x -> isOrd y) -> isOrd (inter x).
Fixpoint nat2ordset n :=
match n with
| 0 => zero
| S k => osucc (nat2ordset k)
end.
Lemma nat2ordset_typ : ∀ n, isOrd (nat2ordset n).
Hint Resolve nat2ordset_typ.
Ordinal omega
Definition omega := ord_sup nat2ordset.
Lemma isOrd_omega : isOrd omega.
Hint Resolve isOrd_omega.
Lemma zero_omega : lt zero omega.
Hint Resolve zero_omega.
Lemma osucc_omega : ∀ n, lt n omega -> lt (osucc n) omega.
Hint Resolve osucc_omega.
Lemma omega_limit_ord : limitOrd omega.
Hint Resolve omega_limit_ord.
Definition iter_w (f:set->set) o :=
ord_sup(nat_rect(fun _=>set) o (fun _ => f)).
Lemma isOrd_iter_w : ∀ f o,
o ⊆ f o ->
(∀ x y, isOrd x -> isOrd y -> x ⊆ y -> f x ⊆ f y) ->
(∀ x, isOrd x -> isOrd (f x)) ->
isOrd o ->
isOrd (iter_w f o).
Definition plus_w := iter_w osucc.
Section DirOrdinalSup.
Variable I : set.
Variable f : set -> set.
Hypothesis f_ext : ext_fun I f.
Hypothesis f_ord : ∀ x, x ∈ I -> isOrd (f x).
Taking the supremum pairwise
Definition osupf X := sup X (fun x => replf X (fun y => x ⊔ y)).
Definition osupfn n := nat_rect (fun _ => set) (sup I f) (fun _ => osupf) n.
Definition osupfn n := nat_rect (fun _ => set) (sup I f) (fun _ => osupf) n.
Iterating ω times, we get a fixpoint
Definition osup := ord_sup osupfn.
Lemma osupf_def X z : z ∈ osupf X <-> exists2 x, x ∈ X & exists2 y, y ∈ X & z == x ⊔ y.
Lemma osupf_mono X Y :
X ⊆ Y ->
osupf X ⊆ osupf Y.
Lemma osupfn_mono m n : (m <= n)%nat -> osupfn m ⊆ osupfn n.
Lemma osup_intro : ∀ x, x ∈ I -> f x ⊆ osup.
Lemma isOrd_osupfn : ∀ n x, x ∈ osupfn n -> isOrd x.
Lemma isOrd_osup : isOrd osup.
Lemma osup_lub z :
isOrd z ->
(∀ x, x ∈ I -> f x ⊆ z) ->
osup ⊆ z.
Lemma osup_univ U :
(∀ X F, ext_fun X F -> X ∈ U -> (∀ x, x ∈ X -> F x ∈ U) ->
sup X F ∈ U) ->
(∀ X x y, X ∈ U -> isWf x -> x ∈ X -> y ∈ X -> singl (x ⊔ y) ∈ U) ->
N ∈ U ->
I ∈ U ->
(∀ x, x ∈ I -> f x ∈ U) ->
osup ∈ U.
End DirOrdinalSup.
Lemma isOrd_eq_osup : ∀ o, isOrd o -> o == osup o osucc.
Lemma osup_morph : ∀ x x' f f',
x == x' -> eq_fun x f f' -> osup x f == osup x' f'.
Lemma osupf_def X z : z ∈ osupf X <-> exists2 x, x ∈ X & exists2 y, y ∈ X & z == x ⊔ y.
Lemma osupf_mono X Y :
X ⊆ Y ->
osupf X ⊆ osupf Y.
Lemma osupfn_mono m n : (m <= n)%nat -> osupfn m ⊆ osupfn n.
Lemma osup_intro : ∀ x, x ∈ I -> f x ⊆ osup.
Lemma isOrd_osupfn : ∀ n x, x ∈ osupfn n -> isOrd x.
Lemma isOrd_osup : isOrd osup.
Lemma osup_lub z :
isOrd z ->
(∀ x, x ∈ I -> f x ⊆ z) ->
osup ⊆ z.
Lemma osup_univ U :
(∀ X F, ext_fun X F -> X ∈ U -> (∀ x, x ∈ X -> F x ∈ U) ->
sup X F ∈ U) ->
(∀ X x y, X ∈ U -> isWf x -> x ∈ X -> y ∈ X -> singl (x ⊔ y) ∈ U) ->
N ∈ U ->
I ∈ U ->
(∀ x, x ∈ I -> f x ∈ U) ->
osup ∈ U.
End DirOrdinalSup.
Lemma isOrd_eq_osup : ∀ o, isOrd o -> o == osup o osucc.
Lemma osup_morph : ∀ x x' f f',
x == x' -> eq_fun x f f' -> osup x f == osup x' f'.