Library ZFfixrec
Specialized version of transfinite recursion where the case of limit
ordinals is union and the stage ordinal is fed to the step function.
(F o x) produces value for stage o+1 given x the value for stage o
Variable F : set -> set -> set.
Hypothesis Fmorph : morph2 F.
Let G f o := sup o (fun o' => F o' (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.
Hypothesis Fmorph : morph2 F.
Let G f o := sup o (fun o' => F o' (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 of the recursor
Definition REC := TR G.
Instance REC_morph : morph1 REC.
Qed.
Lemma REC_fun_ext : ∀ x, isOrd x -> ext_fun x (fun y => F y (REC y)).
Hint Resolve REC_fun_ext.
Lemma REC_eq : ∀ o,
isOrd o ->
REC o == sup o (fun o' => F o' (REC o')).
Lemma REC_intro : ∀ o o' x,
isOrd o ->
lt o' o ->
x ∈ F o' (REC o') ->
x ∈ REC o.
Lemma REC_elim : ∀ o x,
isOrd o ->
x ∈ REC o ->
exists2 o', lt o' o & x ∈ F o' (REC o').
Lemma REC_mono : increasing REC.
Lemma REC_incl : ∀ o, isOrd o ->
∀ o', lt o' o ->
REC o' ⊆ REC o.
Lemma REC_initial : REC zero == empty.
Lemma REC_typ : ∀ n X,
isOrd n ->
(∀ o a, lt o n -> a ∈ X o -> F o a ∈ X (osucc o)) ->
(∀ m G, isOrd m -> m ⊆ n ->
ext_fun m G ->
(∀ x, lt x m -> G x ∈ X (osucc x)) -> sup m G ∈ X m) ->
REC n ∈ X n.
End TransfiniteIteration.
Hint Resolve REC_fun_ext.
Instance REC_morph : morph1 REC.
Qed.
Lemma REC_fun_ext : ∀ x, isOrd x -> ext_fun x (fun y => F y (REC y)).
Hint Resolve REC_fun_ext.
Lemma REC_eq : ∀ o,
isOrd o ->
REC o == sup o (fun o' => F o' (REC o')).
Lemma REC_intro : ∀ o o' x,
isOrd o ->
lt o' o ->
x ∈ F o' (REC o') ->
x ∈ REC o.
Lemma REC_elim : ∀ o x,
isOrd o ->
x ∈ REC o ->
exists2 o', lt o' o & x ∈ F o' (REC o').
Lemma REC_mono : increasing REC.
Lemma REC_incl : ∀ o, isOrd o ->
∀ o', lt o' o ->
REC o' ⊆ REC o.
Lemma REC_initial : REC zero == empty.
Lemma REC_typ : ∀ n X,
isOrd n ->
(∀ o a, lt o n -> a ∈ X o -> F o a ∈ X (osucc o)) ->
(∀ m G, isOrd m -> m ⊆ n ->
ext_fun m G ->
(∀ x, lt x m -> G x ∈ X (osucc x)) -> sup m G ∈ X m) ->
REC n ∈ X n.
End TransfiniteIteration.
Hint Resolve REC_fun_ext.
Building a function by transfinite iteration. The domain of the
function grows along the iteration process.
The maximal ordinal we are allowed to iterate over
The domain of the function to build (indexed by ordinals):
An invariant (e.g. typing)
The step function
Variable F : set -> set -> set.
Definition stage_irrelevance :=
∀ o o' f g,
o' ⊆ ord ->
o ⊆ o' ->
Ty o f -> Ty o' g ->
fcompat (T o) f g ->
fcompat (T (osucc o)) (F o f) (F o' g).
Definition stage_irrelevance :=
∀ o o' f g,
o' ⊆ ord ->
o ⊆ o' ->
Ty o f -> Ty o' g ->
fcompat (T o) f g ->
fcompat (T (osucc o)) (F o f) (F o' g).
Assumptions
Record recursor := mkRecursor {
rec_dom_m : morph1 T;
rec_dom_cont : ∀ o, isOrd o ->
T o == sup o (fun o' => T (osucc o'));
rec_inv_m : ∀ o o',
isOrd o -> o ⊆ ord -> o == o' ->
∀ f f', fcompat (T o) f f' -> Q o f -> Q o' f';
rec_inv_cont : ∀ o f,
isOrd o ->
o ⊆ ord ->
is_cc_fun (T o) f ->
(∀ o', o' ∈ o -> Q (osucc o') f) ->
Q o f;
rec_body_m : morph2 F;
rec_body_typ : ∀ o f,
isOrd o -> o ⊆ ord ->
is_cc_fun (T o) f -> Q o f ->
is_cc_fun (T (osucc o)) (F o f) /\ Q (osucc o) (F o f);
rec_body_irrel : stage_irrelevance
}.
Hypothesis Hrecursor : recursor.
Let Tm := rec_dom_m Hrecursor.
Let Tcont := rec_dom_cont Hrecursor.
Let Qm := rec_inv_m Hrecursor.
Let Qcont := rec_inv_cont Hrecursor.
Let Fm := rec_body_m Hrecursor.
Let Ftyp := rec_body_typ Hrecursor.
Let Firrel := rec_body_irrel Hrecursor.
Lemma Tmono : ∀ o o', isOrd o -> o' ∈ o ->
T (osucc o') ⊆ T o.
Lemma Ftyp' : ∀ o f, o ⊆ ord -> Ty o f -> Ty (osucc o) (F o f).
Definition fincr o :=
fdirected o (fun z => T (osucc z)) (fun z => F z (REC F z)).
Hint Unfold fincr.
Lemma fincr_cont : ∀ o,
isOrd o ->
(∀ z, z ∈ o -> fincr (osucc z)) ->
fincr o.
Definition inv z := Ty z (REC F z) /\ fincr (osucc z).
Lemma fty_step : ∀ o, isOrd o ->
o ⊆ ord ->
(∀ z, z ∈ o -> Ty z (REC F z)) ->
fincr o ->
Ty o (REC F o).
Lemma finc_ext x z :
isOrd x -> isOrd z ->
x ⊆ ord ->
(∀ w, w ∈ x -> Ty w (REC F w)) ->
fincr x ->
z ⊆ x ->
fcompat (T z) (REC F z) (REC F x).
Lemma finc_ext2 o o' z :
isOrd o -> isOrd o' ->
o ⊆ ord ->
o' ⊆ ord ->
(∀ w, w ∈ o ⊔ o' -> Ty w (REC F w)) ->
fincr (o ⊔ o') ->
z ∈ T o ->
z ∈ T o' ->
cc_app (REC F o) z == cc_app (REC F o') z.
Lemma finc_step : ∀ o,
isOrd o ->
o ⊆ ord ->
(∀ z, z ∈ o -> Ty z (REC F z)) ->
fincr o ->
fincr (osucc o).
rec_dom_m : morph1 T;
rec_dom_cont : ∀ o, isOrd o ->
T o == sup o (fun o' => T (osucc o'));
rec_inv_m : ∀ o o',
isOrd o -> o ⊆ ord -> o == o' ->
∀ f f', fcompat (T o) f f' -> Q o f -> Q o' f';
rec_inv_cont : ∀ o f,
isOrd o ->
o ⊆ ord ->
is_cc_fun (T o) f ->
(∀ o', o' ∈ o -> Q (osucc o') f) ->
Q o f;
rec_body_m : morph2 F;
rec_body_typ : ∀ o f,
isOrd o -> o ⊆ ord ->
is_cc_fun (T o) f -> Q o f ->
is_cc_fun (T (osucc o)) (F o f) /\ Q (osucc o) (F o f);
rec_body_irrel : stage_irrelevance
}.
Hypothesis Hrecursor : recursor.
Let Tm := rec_dom_m Hrecursor.
Let Tcont := rec_dom_cont Hrecursor.
Let Qm := rec_inv_m Hrecursor.
Let Qcont := rec_inv_cont Hrecursor.
Let Fm := rec_body_m Hrecursor.
Let Ftyp := rec_body_typ Hrecursor.
Let Firrel := rec_body_irrel Hrecursor.
Lemma Tmono : ∀ o o', isOrd o -> o' ∈ o ->
T (osucc o') ⊆ T o.
Lemma Ftyp' : ∀ o f, o ⊆ ord -> Ty o f -> Ty (osucc o) (F o f).
Definition fincr o :=
fdirected o (fun z => T (osucc z)) (fun z => F z (REC F z)).
Hint Unfold fincr.
Lemma fincr_cont : ∀ o,
isOrd o ->
(∀ z, z ∈ o -> fincr (osucc z)) ->
fincr o.
Definition inv z := Ty z (REC F z) /\ fincr (osucc z).
Lemma fty_step : ∀ o, isOrd o ->
o ⊆ ord ->
(∀ z, z ∈ o -> Ty z (REC F z)) ->
fincr o ->
Ty o (REC F o).
Lemma finc_ext x z :
isOrd x -> isOrd z ->
x ⊆ ord ->
(∀ w, w ∈ x -> Ty w (REC F w)) ->
fincr x ->
z ⊆ x ->
fcompat (T z) (REC F z) (REC F x).
Lemma finc_ext2 o o' z :
isOrd o -> isOrd o' ->
o ⊆ ord ->
o' ⊆ ord ->
(∀ w, w ∈ o ⊔ o' -> Ty w (REC F w)) ->
fincr (o ⊔ o') ->
z ∈ T o ->
z ∈ T o' ->
cc_app (REC F o) z == cc_app (REC F o') z.
Lemma finc_step : ∀ o,
isOrd o ->
o ⊆ ord ->
(∀ z, z ∈ o -> Ty z (REC F z)) ->
fincr o ->
fincr (osucc o).
Invariant inv holds for any ordinal up to ord.
Lemma REC_inv : ∀ o,
isOrd o -> o ⊆ ord -> inv o.
Lemma REC_step : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
o' ⊆ ord ->
fcompat (T o) (REC F o) (F o' (REC F o')).
Section REC_Eqn.
Lemma REC_wt : is_cc_fun (T ord) (REC F ord) /\ Q ord (REC F ord).
Lemma REC_typing : Q ord (REC F ord).
Lemma REC_ord_irrel o o' x:
isOrd o ->
isOrd o' ->
o ⊆ o' ->
o' ⊆ ord ->
x ∈ T o ->
cc_app (REC F o) x == cc_app (REC F o') x.
Lemma REC_ind : ∀ P x,
Proper (eq_set==>eq_set==>eq_set==>iff) P ->
(∀ o x, isOrd o -> o ⊆ ord ->
x ∈ T o ->
(∀ o' y, lt o' o -> y ∈ T o' -> P o' y (cc_app (REC F ord) y)) ->
P o x (cc_app (F ord (REC F ord)) x)) ->
x ∈ T ord ->
P ord x (cc_app (REC F ord) x).
Lemma REC_ext G :
is_cc_fun (T ord) G ->
(∀ o', o' ∈ ord ->
REC F o' == cc_lam (T o') (cc_app G) ->
fcompat (T (osucc o')) G (F o' (cc_lam (T o') (cc_app G)))) ->
REC F ord == G.
Lemma REC_expand : ∀ x,
x ∈ T ord -> cc_app (REC F ord) x == cc_app (F ord (REC F ord)) x.
Lemma REC_eqn :
REC F ord == cc_lam (T ord) (fun x => cc_app (F ord (REC F ord)) x).
End REC_Eqn.
End Recursor.
isOrd o -> o ⊆ ord -> inv o.
Lemma REC_step : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
o' ⊆ ord ->
fcompat (T o) (REC F o) (F o' (REC F o')).
Section REC_Eqn.
Lemma REC_wt : is_cc_fun (T ord) (REC F ord) /\ Q ord (REC F ord).
Lemma REC_typing : Q ord (REC F ord).
Lemma REC_ord_irrel o o' x:
isOrd o ->
isOrd o' ->
o ⊆ o' ->
o' ⊆ ord ->
x ∈ T o ->
cc_app (REC F o) x == cc_app (REC F o') x.
Lemma REC_ind : ∀ P x,
Proper (eq_set==>eq_set==>eq_set==>iff) P ->
(∀ o x, isOrd o -> o ⊆ ord ->
x ∈ T o ->
(∀ o' y, lt o' o -> y ∈ T o' -> P o' y (cc_app (REC F ord) y)) ->
P o x (cc_app (F ord (REC F ord)) x)) ->
x ∈ T ord ->
P ord x (cc_app (REC F ord) x).
Lemma REC_ext G :
is_cc_fun (T ord) G ->
(∀ o', o' ∈ ord ->
REC F o' == cc_lam (T o') (cc_app G) ->
fcompat (T (osucc o')) G (F o' (cc_lam (T o') (cc_app G)))) ->
REC F ord == G.
Lemma REC_expand : ∀ x,
x ∈ T ord -> cc_app (REC F ord) x == cc_app (F ord (REC F ord)) x.
Lemma REC_eqn :
REC F ord == cc_lam (T ord) (fun x => cc_app (F ord (REC F ord)) x).
End REC_Eqn.
End Recursor.