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.

Require Import ZF ZFrelations ZFnats ZFord ZFfunext.

Section TransfiniteIteration.

(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.

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.

Building a function by transfinite iteration. The domain of the function grows along the iteration process.

Section Recursor.

The maximal ordinal we are allowed to iterate over

Variable ord : set.
Hypothesis oord : isOrd ord.

Let oordlt := fun o olt => isOrd_inv _ o oord olt.

The domain of the function to build (indexed by ordinals):

Variable T : set -> set.

An invariant (e.g. typing)

Variable Q : set -> set -> Prop.

Let Ty o f := isOrd o /\ is_cc_fun (T o) f /\ Q o f.

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).

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).

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.