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.
do 3 red; intros.
unfold G.
apply sup_morph; trivial.
red; intros.
apply Fmorph; trivial.
apply H; trivial.
Qed.
Let Gmorph : ∀ o f f', eq_fun o f f' -> G f o == G f' o.
unfold G; intros.
apply sup_morph; auto with *.
red; intros.
apply Fmorph; auto.
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.
do 3 red; intros.
unfold G.
apply sup_morph; trivial.
red; intros.
apply Fmorph; trivial.
apply H; trivial.
Qed.
Let Gmorph : ∀ o f f', eq_fun o f f' -> G f o == G f' o.
unfold G; intros.
apply sup_morph; auto with *.
red; intros.
apply Fmorph; auto.
Qed.
Definition of the recursor
Definition REC := TR G.
Instance REC_morph : morph1 REC.
unfold REC; do 2 red; intros.
apply TR_morph; auto with *.
Qed.
Lemma REC_fun_ext : ∀ x, isOrd x -> ext_fun x (fun y => F y (REC y)).
do 2 red; intros.
apply Fmorph; eauto using isOrd_inv.
apply REC_morph; trivial.
Qed.
Hint Resolve REC_fun_ext.
Lemma REC_eq : ∀ o,
isOrd o ->
REC o == sup o (fun o' => F o' (REC o')).
intros.
unfold REC.
apply TR_eqn; auto.
Qed.
Lemma REC_intro : ∀ o o' x,
isOrd o ->
lt o' o ->
x ∈ F o' (REC o') ->
x ∈ REC o.
intros.
rewrite REC_eq; trivial.
rewrite sup_ax; auto.
exists o'; trivial.
Qed.
Lemma REC_elim : ∀ o x,
isOrd o ->
x ∈ REC o ->
exists2 o', lt o' o & x ∈ F o' (REC o').
intros.
rewrite REC_eq in H0; trivial.
rewrite sup_ax in H0; auto.
Qed.
Lemma REC_mono : increasing REC.
do 2 red; intros.
apply REC_elim in H2; intros; auto with *.
destruct H2.
apply REC_intro with x0; auto with *.
apply H1 in H2; trivial.
Qed.
Lemma REC_incl : ∀ o, isOrd o ->
∀ o', lt o' o ->
REC o' ⊆ REC o.
intros.
apply REC_mono; trivial; auto.
apply isOrd_inv with o; trivial.
Qed.
Lemma REC_initial : REC zero == empty.
apply empty_ext; red; intros.
apply REC_elim in H.
destruct H.
elim empty_ax with (1:=H).
apply isOrd_zero.
Qed.
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.
induction 1 using isOrd_ind; intros.
rewrite REC_eq; trivial.
apply H3 with (G:=fun o => F o (REC o)); intros; auto with *.
apply H2; trivial.
apply H1; intros; trivial.
apply H2; trivial.
apply isOrd_trans with x; trivial.
apply H3; trivial.
rewrite H6.
red; intros.
apply isOrd_trans with x; trivial.
Qed.
End TransfiniteIteration.
Hint Resolve REC_fun_ext.
Existing Instance REC_morph.
Instance REC_morph : morph1 REC.
unfold REC; do 2 red; intros.
apply TR_morph; auto with *.
Qed.
Lemma REC_fun_ext : ∀ x, isOrd x -> ext_fun x (fun y => F y (REC y)).
do 2 red; intros.
apply Fmorph; eauto using isOrd_inv.
apply REC_morph; trivial.
Qed.
Hint Resolve REC_fun_ext.
Lemma REC_eq : ∀ o,
isOrd o ->
REC o == sup o (fun o' => F o' (REC o')).
intros.
unfold REC.
apply TR_eqn; auto.
Qed.
Lemma REC_intro : ∀ o o' x,
isOrd o ->
lt o' o ->
x ∈ F o' (REC o') ->
x ∈ REC o.
intros.
rewrite REC_eq; trivial.
rewrite sup_ax; auto.
exists o'; trivial.
Qed.
Lemma REC_elim : ∀ o x,
isOrd o ->
x ∈ REC o ->
exists2 o', lt o' o & x ∈ F o' (REC o').
intros.
rewrite REC_eq in H0; trivial.
rewrite sup_ax in H0; auto.
Qed.
Lemma REC_mono : increasing REC.
do 2 red; intros.
apply REC_elim in H2; intros; auto with *.
destruct H2.
apply REC_intro with x0; auto with *.
apply H1 in H2; trivial.
Qed.
Lemma REC_incl : ∀ o, isOrd o ->
∀ o', lt o' o ->
REC o' ⊆ REC o.
intros.
apply REC_mono; trivial; auto.
apply isOrd_inv with o; trivial.
Qed.
Lemma REC_initial : REC zero == empty.
apply empty_ext; red; intros.
apply REC_elim in H.
destruct H.
elim empty_ax with (1:=H).
apply isOrd_zero.
Qed.
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.
induction 1 using isOrd_ind; intros.
rewrite REC_eq; trivial.
apply H3 with (G:=fun o => F o (REC o)); intros; auto with *.
apply H2; trivial.
apply H1; intros; trivial.
apply H2; trivial.
apply isOrd_trans with x; trivial.
apply H3; trivial.
rewrite H6.
red; intros.
apply isOrd_trans with x; trivial.
Qed.
End TransfiniteIteration.
Hint Resolve REC_fun_ext.
Existing Instance REC_morph.
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.
red; intros.
rewrite Tcont; trivial.
rewrite sup_ax.
exists o'; trivial.
do 2 red; intros; apply Tm; apply osucc_morph; trivial.
Qed.
Lemma Ftyp' : ∀ o f, o ⊆ ord -> Ty o f -> Ty (osucc o) (F o f).
intros.
destruct H0 as (oo,(ofun,oq)); split; auto.
Qed.
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.
intros o oo incrlt.
do 3 red; intros.
assert (xo : isOrd x) by eauto using isOrd_inv.
assert (yo : isOrd y) by eauto using isOrd_inv.
pose (z:=x ⊔ y).
assert (zo : isOrd z).
apply isOrd_osup2; trivial.
assert (z ∈ o).
apply osup2_lt; trivial.
do 3 red in incrlt.
apply incrlt with z; trivial.
apply isOrd_plump with z; auto.
apply osup2_incl1; auto.
apply lt_osucc; auto.
apply isOrd_plump with z; auto.
apply osup2_incl2; auto.
apply lt_osucc; auto.
Qed.
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).
intros o oo ole tylt incrlt.
assert (is_cc_fun (T o) (REC F o)).
rewrite Tcont; trivial.
rewrite REC_eq; trivial.
apply prd_union; auto; intros.
red; red; intros; apply Tm.
rewrite H0; reflexivity.
apply Ftyp'; auto.
split; trivial.
split; trivial.
apply Qcont; trivial; intros.
assert (isOrd o') by eauto using isOrd_inv.
apply Qm with (osucc o') (F o' (REC F o')); auto with *.
red; intros.
apply isOrd_plump with o'; eauto using isOrd_inv, olts_le.
rewrite REC_eq with (o:=o); trivial.
apply prd_sup with (A:=fun z => T(osucc z)) (F:=fun z => F z (REC F z));
intros; auto.
apply Ftyp'; auto.
apply Ftyp'; auto.
Qed.
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).
intros xo zo zle tylt incrlt inc.
rewrite Tcont; trivial.
rewrite REC_eq with (o:=z); auto.
apply prd_sup_lub; intros; auto with *.
red; red; intros; apply Tm.
rewrite H0; reflexivity.
apply Ftyp'; auto.
red; auto.
rewrite REC_eq with (o:=x); trivial.
apply prd_sup with (A:=fun z => T (osucc z))
(F:=fun z => F z (REC F z)); auto; intros.
apply Ftyp'; auto.
Qed.
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.
transitivity (cc_app (REC F (o ⊔ o')) z).
apply finc_ext; auto with *.
apply isOrd_osup2; trivial.
apply osup2_lub; trivial.
apply osup2_incl1; auto.
symmetry; apply finc_ext; auto with *.
apply isOrd_osup2; trivial.
apply osup2_lub; trivial.
apply osup2_incl2; auto.
Qed.
Lemma finc_step : ∀ o,
isOrd o ->
o ⊆ ord ->
(∀ z, z ∈ o -> Ty z (REC F z)) ->
fincr o ->
fincr (osucc o).
unfold fincr, fdirected; intros o oo ole tylt fo.
red; intros.
assert (xo : isOrd x) by eauto using isOrd_inv.
assert (yo : isOrd y) by eauto using isOrd_inv.
apply olts_le in H.
apply olts_le in H0.
set (z := x ⊔ y).
assert (isOrd z).
apply isOrd_osup2; eauto using isOrd_inv.
assert (z ⊆ o).
apply osup2_lub; auto.
assert (∀ w, isOrd w -> w ⊆ o -> fincr w).
red; red; auto.
rewrite inter2_def in H1; destruct H1.
transitivity (cc_app (F z (REC F z)) x0).
apply Firrel; auto with *.
transitivity o; trivial.
apply osup2_incl1; auto.
apply fty_step; auto.
transitivity o; trivial.
apply fty_step; auto.
transitivity o; trivial.
apply finc_ext; intros; auto.
transitivity o; trivial.
apply osup2_incl1; auto.
symmetry; apply Firrel; auto with *.
transitivity o; trivial.
apply osup2_incl2; auto.
apply fty_step; auto.
transitivity o; trivial.
apply fty_step; auto.
transitivity o; trivial.
apply finc_ext; intros; auto.
transitivity o; trivial.
apply osup2_incl2; auto.
Qed.
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.
red; intros.
rewrite Tcont; trivial.
rewrite sup_ax.
exists o'; trivial.
do 2 red; intros; apply Tm; apply osucc_morph; trivial.
Qed.
Lemma Ftyp' : ∀ o f, o ⊆ ord -> Ty o f -> Ty (osucc o) (F o f).
intros.
destruct H0 as (oo,(ofun,oq)); split; auto.
Qed.
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.
intros o oo incrlt.
do 3 red; intros.
assert (xo : isOrd x) by eauto using isOrd_inv.
assert (yo : isOrd y) by eauto using isOrd_inv.
pose (z:=x ⊔ y).
assert (zo : isOrd z).
apply isOrd_osup2; trivial.
assert (z ∈ o).
apply osup2_lt; trivial.
do 3 red in incrlt.
apply incrlt with z; trivial.
apply isOrd_plump with z; auto.
apply osup2_incl1; auto.
apply lt_osucc; auto.
apply isOrd_plump with z; auto.
apply osup2_incl2; auto.
apply lt_osucc; auto.
Qed.
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).
intros o oo ole tylt incrlt.
assert (is_cc_fun (T o) (REC F o)).
rewrite Tcont; trivial.
rewrite REC_eq; trivial.
apply prd_union; auto; intros.
red; red; intros; apply Tm.
rewrite H0; reflexivity.
apply Ftyp'; auto.
split; trivial.
split; trivial.
apply Qcont; trivial; intros.
assert (isOrd o') by eauto using isOrd_inv.
apply Qm with (osucc o') (F o' (REC F o')); auto with *.
red; intros.
apply isOrd_plump with o'; eauto using isOrd_inv, olts_le.
rewrite REC_eq with (o:=o); trivial.
apply prd_sup with (A:=fun z => T(osucc z)) (F:=fun z => F z (REC F z));
intros; auto.
apply Ftyp'; auto.
apply Ftyp'; auto.
Qed.
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).
intros xo zo zle tylt incrlt inc.
rewrite Tcont; trivial.
rewrite REC_eq with (o:=z); auto.
apply prd_sup_lub; intros; auto with *.
red; red; intros; apply Tm.
rewrite H0; reflexivity.
apply Ftyp'; auto.
red; auto.
rewrite REC_eq with (o:=x); trivial.
apply prd_sup with (A:=fun z => T (osucc z))
(F:=fun z => F z (REC F z)); auto; intros.
apply Ftyp'; auto.
Qed.
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.
transitivity (cc_app (REC F (o ⊔ o')) z).
apply finc_ext; auto with *.
apply isOrd_osup2; trivial.
apply osup2_lub; trivial.
apply osup2_incl1; auto.
symmetry; apply finc_ext; auto with *.
apply isOrd_osup2; trivial.
apply osup2_lub; trivial.
apply osup2_incl2; auto.
Qed.
Lemma finc_step : ∀ o,
isOrd o ->
o ⊆ ord ->
(∀ z, z ∈ o -> Ty z (REC F z)) ->
fincr o ->
fincr (osucc o).
unfold fincr, fdirected; intros o oo ole tylt fo.
red; intros.
assert (xo : isOrd x) by eauto using isOrd_inv.
assert (yo : isOrd y) by eauto using isOrd_inv.
apply olts_le in H.
apply olts_le in H0.
set (z := x ⊔ y).
assert (isOrd z).
apply isOrd_osup2; eauto using isOrd_inv.
assert (z ⊆ o).
apply osup2_lub; auto.
assert (∀ w, isOrd w -> w ⊆ o -> fincr w).
red; red; auto.
rewrite inter2_def in H1; destruct H1.
transitivity (cc_app (F z (REC F z)) x0).
apply Firrel; auto with *.
transitivity o; trivial.
apply osup2_incl1; auto.
apply fty_step; auto.
transitivity o; trivial.
apply fty_step; auto.
transitivity o; trivial.
apply finc_ext; intros; auto.
transitivity o; trivial.
apply osup2_incl1; auto.
symmetry; apply Firrel; auto with *.
transitivity o; trivial.
apply osup2_incl2; auto.
apply fty_step; auto.
transitivity o; trivial.
apply fty_step; auto.
transitivity o; trivial.
apply finc_ext; intros; auto.
transitivity o; trivial.
apply osup2_incl2; auto.
Qed.
Invariant inv holds for any ordinal up to ord.
Lemma REC_inv : ∀ o,
isOrd o -> o ⊆ ord -> inv o.
intros o oo ole.
induction oo using isOrd_ind.
split.
apply fty_step; intros; trivial.
transitivity o; trivial.
apply H0; trivial.
apply fincr_cont; trivial.
apply H0; trivial.
apply finc_step; intros; trivial.
transitivity o; trivial.
apply H0; trivial.
apply fincr_cont; trivial.
apply H0; trivial.
Qed.
Lemma REC_step : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
o' ⊆ ord ->
fcompat (T o) (REC F o) (F o' (REC F o')).
intros.
destruct REC_inv with o'; trivial.
rewrite REC_eq with (o:=o) at 1; trivial.
rewrite Tcont; trivial.
apply prd_sup_lub; intros; auto.
red; red; intros; apply Tm.
rewrite H6; reflexivity.
apply Ftyp'; auto.
apply REC_inv; eauto using isOrd_inv.
red; intros; apply H4.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
red; intros.
apply H4.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
apply lt_osucc; trivial.
rewrite inter2_def; split; trivial.
revert H6; apply Tmono; auto.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
Qed.
Section REC_Eqn.
Lemma REC_wt : is_cc_fun (T ord) (REC F ord) /\ Q ord (REC F ord).
apply REC_inv; auto with *.
Qed.
Lemma REC_typing : Q ord (REC F ord).
apply REC_wt.
Qed.
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.
intros.
apply finc_ext; intros; trivial.
apply REC_inv; eauto using isOrd_inv.
apply fincr_cont; intros; trivial.
apply REC_inv; eauto using isOrd_inv.
Qed.
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).
intros.
revert x H1; apply isOrd_ind with (2:=oord); intros.
rewrite (REC_step y ord H1 oord H2 (fun _ x => x) x); trivial.
apply H0; trivial.
intros.
assert (fcompat (T o') (REC F o') (REC F ord)).
apply finc_ext; auto with *.
eauto using isOrd_inv.
intros.
apply REC_inv; eauto using isOrd_inv.
do 2 red; intros.
apply (REC_inv ord); auto with *.
apply isOrd_trans with ord; auto.
apply isOrd_trans with ord; auto.
rewrite <- (H7 y0); trivial.
auto.
Qed.
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.
intros.
rewrite (cc_eta_eq' _ _ H).
apply fcompat_typ_eq with (T ord); auto.
apply REC_inv; auto with *.
apply is_cc_fun_lam.
do 2 red; intros; apply cc_app_morph; auto with *.
cut ((∀ z, z ∈ ord -> Ty z (cc_lam (T z) (cc_app G))) /\
fcompat (T ord) (cc_lam (T ord) (cc_app G)) (REC F ord)).
destruct 1; red; intros.
symmetry; auto.
apply isOrd_ind with (2:=oord); intros.
assert (QG: ∀ z, z ∈ y -> Ty z (cc_lam (T z) (cc_app G))).
intros.
split;[|split].
apply isOrd_inv with y; trivial.
apply is_cc_fun_lam.
do 2 red; intros; apply cc_app_morph; auto with *.
apply Qm with z (REC F z).
apply isOrd_inv with y; trivial.
red; intros; apply isOrd_trans with z; auto.
apply H2; trivial.
reflexivity.
red; intros; symmetry.
apply H3; trivial.
apply REC_inv; eauto using isOrd_inv.
split; trivial.
red; intros.
rewrite cc_beta_eq; trivial.
2:do 2 red; intros; apply cc_app_morph; auto with *.
rewrite Tcont in H4; trivial.
rewrite sup_ax in H4.
2:do 2 red; intros; apply Tm; apply osucc_morph; trivial.
destruct H4.
assert (tyRx0 : Ty x0 (REC F x0)).
apply REC_inv; eauto using isOrd_inv.
red in H0; rewrite H0 with (o':=x0) (x:=x); auto.
transitivity (cc_app (F y (REC F y)) x).
apply Firrel; auto with *.
apply REC_inv; trivial.
destruct (H3 _ H4) as (_,?).
red; intros.
rewrite (H6 x1 H7).
apply REC_ord_irrel; auto with *.
apply isOrd_inv with y; trivial.
symmetry; apply REC_step; auto with *.
revert H5; apply Tmono; trivial.
destruct tyRx0 as (_,(Rx0fun,_)).
destruct H3 with x0 as (_,?); trivial.
red in H6.
rewrite cc_eta_eq' with (1:=Rx0fun).
apply cc_lam_ext; auto with *.
red; intros; symmetry.
rewrite <- H8; rewrite <- H6 with (1:=H7).
symmetry; apply cc_beta_eq; trivial.
do 2 red; intros; apply cc_app_morph; auto with *.
Qed.
Lemma REC_expand : ∀ x,
x ∈ T ord -> cc_app (REC F ord) x == cc_app (F ord (REC F ord)) x.
apply REC_step; auto with *.
Qed.
Lemma REC_eqn :
REC F ord == cc_lam (T ord) (fun x => cc_app (F ord (REC F ord)) x).
intros.
rewrite (cc_eta_eq' (T ord) (REC F ord)).
2:apply REC_inv; auto with *.
apply cc_lam_ext; auto with *.
red; intros.
rewrite <- H0.
apply REC_expand; trivial.
Qed.
End REC_Eqn.
End Recursor.
isOrd o -> o ⊆ ord -> inv o.
intros o oo ole.
induction oo using isOrd_ind.
split.
apply fty_step; intros; trivial.
transitivity o; trivial.
apply H0; trivial.
apply fincr_cont; trivial.
apply H0; trivial.
apply finc_step; intros; trivial.
transitivity o; trivial.
apply H0; trivial.
apply fincr_cont; trivial.
apply H0; trivial.
Qed.
Lemma REC_step : ∀ o o',
isOrd o ->
isOrd o' ->
o ⊆ o' ->
o' ⊆ ord ->
fcompat (T o) (REC F o) (F o' (REC F o')).
intros.
destruct REC_inv with o'; trivial.
rewrite REC_eq with (o:=o) at 1; trivial.
rewrite Tcont; trivial.
apply prd_sup_lub; intros; auto.
red; red; intros; apply Tm.
rewrite H6; reflexivity.
apply Ftyp'; auto.
apply REC_inv; eauto using isOrd_inv.
red; intros; apply H4.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
red; intros.
apply H4.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
apply lt_osucc; trivial.
rewrite inter2_def; split; trivial.
revert H6; apply Tmono; auto.
apply isOrd_trans with o; auto.
apply ole_lts; auto.
Qed.
Section REC_Eqn.
Lemma REC_wt : is_cc_fun (T ord) (REC F ord) /\ Q ord (REC F ord).
apply REC_inv; auto with *.
Qed.
Lemma REC_typing : Q ord (REC F ord).
apply REC_wt.
Qed.
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.
intros.
apply finc_ext; intros; trivial.
apply REC_inv; eauto using isOrd_inv.
apply fincr_cont; intros; trivial.
apply REC_inv; eauto using isOrd_inv.
Qed.
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).
intros.
revert x H1; apply isOrd_ind with (2:=oord); intros.
rewrite (REC_step y ord H1 oord H2 (fun _ x => x) x); trivial.
apply H0; trivial.
intros.
assert (fcompat (T o') (REC F o') (REC F ord)).
apply finc_ext; auto with *.
eauto using isOrd_inv.
intros.
apply REC_inv; eauto using isOrd_inv.
do 2 red; intros.
apply (REC_inv ord); auto with *.
apply isOrd_trans with ord; auto.
apply isOrd_trans with ord; auto.
rewrite <- (H7 y0); trivial.
auto.
Qed.
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.
intros.
rewrite (cc_eta_eq' _ _ H).
apply fcompat_typ_eq with (T ord); auto.
apply REC_inv; auto with *.
apply is_cc_fun_lam.
do 2 red; intros; apply cc_app_morph; auto with *.
cut ((∀ z, z ∈ ord -> Ty z (cc_lam (T z) (cc_app G))) /\
fcompat (T ord) (cc_lam (T ord) (cc_app G)) (REC F ord)).
destruct 1; red; intros.
symmetry; auto.
apply isOrd_ind with (2:=oord); intros.
assert (QG: ∀ z, z ∈ y -> Ty z (cc_lam (T z) (cc_app G))).
intros.
split;[|split].
apply isOrd_inv with y; trivial.
apply is_cc_fun_lam.
do 2 red; intros; apply cc_app_morph; auto with *.
apply Qm with z (REC F z).
apply isOrd_inv with y; trivial.
red; intros; apply isOrd_trans with z; auto.
apply H2; trivial.
reflexivity.
red; intros; symmetry.
apply H3; trivial.
apply REC_inv; eauto using isOrd_inv.
split; trivial.
red; intros.
rewrite cc_beta_eq; trivial.
2:do 2 red; intros; apply cc_app_morph; auto with *.
rewrite Tcont in H4; trivial.
rewrite sup_ax in H4.
2:do 2 red; intros; apply Tm; apply osucc_morph; trivial.
destruct H4.
assert (tyRx0 : Ty x0 (REC F x0)).
apply REC_inv; eauto using isOrd_inv.
red in H0; rewrite H0 with (o':=x0) (x:=x); auto.
transitivity (cc_app (F y (REC F y)) x).
apply Firrel; auto with *.
apply REC_inv; trivial.
destruct (H3 _ H4) as (_,?).
red; intros.
rewrite (H6 x1 H7).
apply REC_ord_irrel; auto with *.
apply isOrd_inv with y; trivial.
symmetry; apply REC_step; auto with *.
revert H5; apply Tmono; trivial.
destruct tyRx0 as (_,(Rx0fun,_)).
destruct H3 with x0 as (_,?); trivial.
red in H6.
rewrite cc_eta_eq' with (1:=Rx0fun).
apply cc_lam_ext; auto with *.
red; intros; symmetry.
rewrite <- H8; rewrite <- H6 with (1:=H7).
symmetry; apply cc_beta_eq; trivial.
do 2 red; intros; apply cc_app_morph; auto with *.
Qed.
Lemma REC_expand : ∀ x,
x ∈ T ord -> cc_app (REC F ord) x == cc_app (F ord (REC F ord)) x.
apply REC_step; auto with *.
Qed.
Lemma REC_eqn :
REC F ord == cc_lam (T ord) (fun x => cc_app (F ord (REC F ord)) x).
intros.
rewrite (cc_eta_eq' (T ord) (REC F ord)).
2:apply REC_inv; auto with *.
apply cc_lam_ext; auto with *.
red; intros.
rewrite <- H0.
apply REC_expand; trivial.
Qed.
End REC_Eqn.
End Recursor.