Library ZFind_wnup

Require Import ZF ZFpairs ZFsum ZFnats ZFrelations ZFord ZFfix ZFstable.
Require Import ZFcoc ZFlist.
Require Import ZFfixfun.
Import ZFrepl.

A dependent version of ZFind_w: Arg is the type of indexes This should support non-uniform parameters.

Require ZFind_w.
Module W0 := ZFind_w.

Hint Resolve W0.W_F_mono Fmono_morph.

Section W_theory.

We want to model the following inductive type with non-uniform parameter a:
Inductive Wd (a:Arg) :=
| C : ∀ (x:A a), (∀ (i:B a x), Wd (f a x i)) -> Wd a.

Variable Arg : set.
Variable A : set -> set.
Variable B : set -> set -> set.
Variable f : set -> set -> set -> set.
Hypothesis Am : morph1 A.
Hypothesis Bm : morph2 B.
Hypothesis fm : Proper (eq_set ==>eq_set ==>eq_set ==>eq_set) f.
Hypothesis ftyp : ∀ a x y,
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  f a x y ∈ Arg.

The intended type operator: parameter is not part of the data-structure

Definition W_Fd (X:set->set) a :=
  sigma (A a) (fun x => cc_prod (B a x) (fun y => X (f a x y))).

Definition Wi o a := TIF Arg W_Fd o a.

Instance Wi_morph : morph2 Wi.
Qed.

Instance W_Fd_morph : Proper ((eq_set ==>eq_set )==>eq_set ==>eq_set) W_Fd.

Qed.

Lemma W_Fd_mono : mono_fam Arg W_Fd.
Hint Resolve W_Fd_mono.

Lemma W_Fd_eta w X a :
  morph1 X ->
  w ∈ W_Fd X a ->
  w == couple (fst w) (cc_lam (B a (fst w)) (fun i => cc_app (snd w) i)).

Lemma W_Fd_intro X x x' a a' g :
  morph1 X ->
  a ∈ Arg ->
  a == a' ->
  x ∈ A a' ->
  x == x' ->
  ext_fun (B a x') g ->
  (∀ i, i ∈ B a x' -> g i ∈ X (f a x' i)) ->
  couple x (cc_lam (B a x') g) ∈ W_Fd X a'.

The intermediate W-type: the parameter is turned into a constructor argument that we later on constrain (like indexes of inductive families) Arg appears in the data, so if it is big, the resulting inductive type is big.

Definition A' := sigma Arg A.
Definition B' a' := B (fst a') (snd a').
Instance B'_morph : morph1 B'.
Qed.

Lemma B'ext : ext_fun A' B'.
Hint Resolve B'ext.

Lemma A'_intro a x :
  a ∈ Arg ->
  x ∈ A a ->
  couple a x ∈ A'.

Lemma A'_elim x :
  x ∈ A' -> fst x ∈ Arg /\ snd x ∈ A (fst x) /\ x == couple (fst x) (snd x).

instance a w means tree w corresponds to the member of the family with index value a:

the Arg component of A' must be a
the condition is hereditary

Inductive instance a w : Prop :=
| I_node :
    a == fst (fst w) ->
    (∀ i, i ∈ B' (fst w) -> instance (f a (snd (fst w)) i) (cc_app (snd w) i)) ->
    instance a w.

Instance instance_morph : Proper (eq_set ==>eq_set ==>iff) instance.

Qed.

We show there is an iso between the intended type (Wi) and the encoding (W0.W A' B'): tr (f:X->Y) : W0.W_F A' B' X --> U_a (W_Fd (A a) (B a) Y) See also more refined result below.

Definition tr f w :=
couple (snd (fst w)) (cc_lam (B'(fst w)) (fun i => f (cc_app (snd w) i))).

Instance tr_morph : Proper ((eq_set ==> eq_set ) ==> eq_set ==> eq_set) tr.

Qed.

Let tr_cont o z :
isOrd o ->
(z ∈ TI (W0.W_F A' B') o <->
(exists2 o', o' ∈ o & z ∈ TI (W0.W_F A' B') (osucc o'))).
Qed.

Let tr_ext o g g' :
isOrd o ->
eq_fun (TI (W0.W_F A' B') o) g g' ->
eq_fun (TI (W0.W_F A' B') (osucc o)) (tr g) (tr g').

Qed.

Require Import ZFiso.

Isomorphism result for the step function.

the parameter constraint on subterms (of type X) is modelled by P

Lemma tr_iso a X Y P g :
  Proper (eq_set ==>eq_set ==>iff) P ->
  morph1 Y ->
  a ∈ Arg ->
  (∀ a, a ∈ Arg -> iso_fun (subset X (P a)) (Y a) g) ->
  let Wd := subset (W0.W_F A' B' X)
     (fun w => fst (fst w) == a /\
        ∀ i, i ∈ B a (snd (fst w)) -> P (f a (snd (fst w)) i) (cc_app (snd w) i)) in
  iso_fun Wd (W_Fd Y a) (tr g).

Require Import ZFlimit.

Lemma tr_iso_it a o :
  isOrd o ->
  a ∈ Arg ->
  iso_fun (subset (TI (W0.W_F A' B') o) (instance a))
          (TIF Arg W_Fd o a) (TRF tr o).

Fixpoint

Definition W_ord := W0.W_ord A' B'.

Lemma W_o_o : isOrd W_ord.
Hint Resolve W_o_o.

Definition W := Wi W_ord.

Lemma W_eqn a : a ∈ Arg -> W a == W_Fd W a.

Lemma W_post o :
isOrd o ->
incl_fam Arg (Wi o) W.

Universe facts

Require Import ZFgrothendieck.

Section W_Univ.

  Variable U : set.
  Hypothesis Ugrot : grot_univ U.
  Hypothesis Unontriv : omega ∈ U.

The size of Arg matters:

  Hypothesis ArgU : Arg ∈ U.
  Hypothesis aU : ∀ a, a ∈ Arg -> A a ∈ U.
  Hypothesis bU : ∀ a x, a ∈ Arg -> x ∈ A a -> B a x ∈ U.

  Lemma G_W_Fd X :
    morph1 X ->
    (∀ a, a ∈ Arg -> X a ∈ U) ->
    ∀ a, a ∈ Arg -> W_Fd X a ∈ U.

  Lemma G_Wi o a : isOrd o -> o ∈ U -> a ∈ Arg -> Wi o a ∈ U.

  Lemma G_W_ord : W_ord ∈ U.

  Lemma G_W a : a ∈ Arg -> W a ∈ U.

End W_Univ.

End W_theory.

Section MoreMorph.

Local Notation E := eq_set.
Lemma W_Fd_morph_all : Proper ((E ==>E )==>(E ==>E ==>E )==>(E ==>E ==>E ==>E )==>(E ==>E )==>E ==>E) W_Fd.

Lemma Wi_morph_all : Proper (E ==>(E ==>E )==>(E ==>E ==>E )==>(E ==>E ==>E ==>E )==>E ==>E ==>E) Wi.

Lemma W_ord_morph_all : Proper (E ==>(E ==>E )==>(E ==>E ==>E )==>E) W_ord.

Lemma W_morph_all : Proper (E ==>(E ==>E )==>(E ==>E ==>E )==>(E ==>E ==>E ==>E )==>E ==>E) W.

End MoreMorph.

Morphism between two instances of W-types

Section W_Simulation.

Variable Arg : set.
Variable A : set -> set.
Variable B : set -> set -> set.
Variable f : set -> set -> set -> set.
Hypothesis Am : morph1 A.
Hypothesis Bm : morph2 B.
Hypothesis fm : Proper (eq_set ==>eq_set ==>eq_set ==>eq_set) f.
Hypothesis ftyp : ∀ a x y,
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  f a x y ∈ Arg.

Variable Arg' : set.
Variable A' : set -> set.
Variable B' : set -> set -> set.
Variable f' : set -> set -> set -> set.
Hypothesis Am' : morph1 A'.
Hypothesis Bm' : morph2 B'.
Hypothesis fm' : Proper (eq_set ==>eq_set ==>eq_set ==>eq_set) f'.
Hypothesis ftyp' : ∀ a x y,
  a ∈ Arg' ->
  x ∈ A' a ->
  y ∈ B' a x ->
  f' a x y ∈ Arg'.

Lemma W_simul g p p' o o':
  morph1 g ->
  (∀ p, p ∈ Arg -> g p ∈ Arg') ->
  (∀ p, p ∈ Arg -> A p == A' (g p)) ->
  (∀ p a, p ∈ Arg -> a ∈ A p -> B p a == B' (g p) a) ->
  (∀ p a b, p ∈ Arg -> a ∈ A p -> b ∈ B p a ->
   g (f p a b) == f' (g p) a b) ->
  isOrd o ->
  p ∈ Arg ->
  g p == p' ->
  o == o' ->
  Wi Arg A B f o p == Wi Arg' A' B' f' o' p'.

End W_Simulation.

Support for definitions by case

Definition if_prop P x y :=
cond_set P x ∪ cond_set (~P) y.

Instance if_prop_morph : Proper (iff ==> eq_set ==> eq_set ==> eq_set) if_prop.
Qed.

Lemma if_left (P:Prop) x y : P -> if_prop P x y == x.

Lemma if_right (P:Prop) x y : ~P -> if_prop P x y == y.

Waiving the universe constraint on Arg:

Section BigParameter.

Variable Arg : set.
Variable A : set -> set.
Variable B : set -> set -> set.
Variable f : set -> set -> set -> set.
Hypothesis Am : morph1 A.
Hypothesis Bm : morph2 B.
Hypothesis fm : Proper (eq_set ==>eq_set ==>eq_set ==>eq_set) f.
Hypothesis ftyp : ∀ a x y,
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  f a x y ∈ Arg.

Encoding big parameters as (small) paths from a fixed parameter a. First, the type operator.

Let L X a :=
  singl empty ∪ sigma (A a) (fun x => sigma (B a x) (fun y => X (f a x y))).

Instance Lmorph : Proper ((eq_set ==>eq_set )==>eq_set ==>eq_set) L.

Qed.
Hint Resolve Lmorph.

Lemma L_intro1 X a : empty ∈ L X a.

Lemma L_intro2 a x y q X :
  morph1 X ->
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  q ∈ X (f a x y) ->
  couple x (couple y q) ∈ L X a.

Definition L_match q f g :=
  if_prop (q ==empty) f (g (fst q) (fst (snd q)) (snd (snd q))).

Lemma L_elim a q X :
  morph1 X ->
  a ∈ Arg ->
  q ∈ L X a ->
  q == empty \/
  exists2 x, x ∈ A a &
  exists2 y, y ∈ B a x &
  exists2 q', q' ∈ X (f a x y) &
  q == couple x (couple y q').

Lemma Lmono : mono_fam Arg L.
Hint Resolve Lmono.

The fixpoint: paths Arg' a == 1 + { x : A a ; y : B a x ; l : Arg' (f a x y) }

Definition Arg' : set -> set := TIF Arg L omega.

Instance Arg'_morph : morph1 Arg'.
Qed.

Lemma Arg'_ind P :
  Proper (eq_set ==> eq_set ==> iff) P ->
  (∀ a, a ∈ Arg -> P a empty) ->
  (∀ a x y q,
   a ∈ Arg ->
   x ∈ A a ->
   y ∈ B a x ->
   q ∈ Arg' (f a x y) ->
   P (f a x y) q ->
   P a (couple x (couple y q))) ->
  ∀ a q,
  a ∈ Arg ->
  q ∈ Arg' a ->
  P a q.

Lemma Arg'_eqn a :
  a ∈ Arg ->
  Arg' a == L Arg' a.

Lemma Arg'_intro1 a :
  a ∈ Arg ->
  empty ∈ Arg' a.

Lemma Arg'_intro2 a x y q :
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  q ∈ Arg' (f a x y) ->
  couple x (couple y q) ∈ Arg' a.

Require Import ZFfixrec.

Section Arg'_recursor.

Variable g : set -> set.
Variable h : set -> set -> set -> (set -> set) -> set -> set.
Hypothesis gm : morph1 g.
Hypothesis hm :
  Proper (eq_set ==>eq_set ==>eq_set ==>(eq_set ==>eq_set )==>eq_set ==>eq_set) h.
Definition Arg'_rec_rel q f' :=
  ∀ P,
  Proper (eq_set ==>(eq_set ==>eq_set )==>iff) P ->
  P empty g ->
  (∀ x y q' f',
   morph1 f' ->
   P q' f' ->
   P (couple x (couple y q')) (h x y q' f')) ->
  P q f'.

Instance Arg'_rec_rel_morph : Proper (eq_set ==>(eq_set ==>eq_set )==>iff) Arg'_rec_rel.
Qed.

Lemma Arg'_case q0 f' :
  Arg'_rec_rel q0 f' ->
  Arg'_rec_rel q0 f' /\
  (q0 == empty -> (eq_set ==>eq_set)%signature f' g ) /\
  ∀ x y q,
  q0 == couple x (couple y q) ->
  exists2 h', morph1 h' &
  Arg'_rec_rel q h' /\ (eq_set ==>eq_set)%signature f' (h x y q h').

Lemma Arg'_uniq q f1 q' f1':
  Arg'_rec_rel q f1 ->
  Arg'_rec_rel q' f1' ->
  q == q' -> (eq_set ==>eq_set)%signature f1 f1'.

Lemma Arg'_ex a q :
  a ∈ Arg ->
  q ∈ Arg' a ->
  exists2 f', morph1 f' & Arg'_rec_rel q f'.

Definition Arg'_rec q x :=
  uchoice (fun y => exists2 f', morph1 f' & Arg'_rec_rel q f' /\ y == f' x).

Lemma Arg'_rec_morph : morph2 Arg'_rec.

Lemma uchoice_Arg'_rec a q x :
  a ∈ Arg ->
  q ∈ Arg' a ->
  uchoice_pred (fun y => exists2 f', morph1 f' & Arg'_rec_rel q f' /\ y == f' x).

Lemma Arg'_def a q :
  a ∈ Arg ->
  q ∈ Arg' a ->
  Arg'_rec_rel q (Arg'_rec q).

Lemma Arg'_rec_mt a x :
  a ∈ Arg ->
  Arg'_rec empty x == g x.

Lemma Arg'_rec_cons a x y q z :
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  q ∈ Arg' (f a x y) ->
  Arg'_rec (couple x (couple y q)) z == h x y q (Arg'_rec q) z.

End Arg'_recursor.

Decoding paths as a parameter value

Definition Dec a q :=
  Arg'_rec (fun a => a) (fun x y q' F a => F (f a x y)) q a.

Lemma Dec_mt a : a ∈ Arg -> Dec a empty == a.

Lemma Dec_cons a x y q :
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  q ∈ Arg' (f a x y) ->
  Dec a (couple x (couple y q)) == Dec (f a x y) q.

Instance Dec_morph : morph2 Dec.
Qed.

Lemma Dec_typ a q :
  a ∈ Arg ->
  q ∈ Arg' a ->
  Dec a q ∈ Arg.

Extending a path

Definition extln q x y :=
  Arg'_rec (fun _ => couple x (couple y empty))
    (fun x' y' q' F z => couple x' (couple y' (F z))) q empty.

Instance extln_morph : Proper (eq_set ==>eq_set ==>eq_set ==>eq_set) extln.

Qed.

Lemma extln_cons a x y q x' y' :
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  q ∈ Arg' (f a x y) ->
  x' ∈ A (Dec (f a x y) q) ->
  y' ∈ B (Dec (f a x y) q) x' ->
  extln (couple x (couple y q)) x' y' == couple x (couple y (extln q x' y')).

Lemma extln_nil a x y :
  a ∈ Arg ->
  x ∈ A a ->
  y ∈ B a x ->
  extln empty x y == couple x (couple y empty).

Lemma extln_typ : ∀ a q x y,
  a ∈ Arg ->
  q ∈ Arg' a ->
  x ∈ A (Dec a q) ->
  y ∈ B (Dec a q) x ->
  extln q x y ∈ Arg' a.

WW is the encoded type with small index

Definition A'' a q := A (Dec a q).
Definition B'' a q := B (Dec a q).
Definition WW a := W (Arg' a) (A'' a) (B'' a) extln empty.

Instance A''_morph a : morph1 (A'' a).
Qed.

Instance B''_morph a : morph2 (B'' a).
Qed.

Instance WWf_morph a' : Proper ((eq_set ==> eq_set ) ==> eq_set ==> eq_set)
(W_Fd (A'' a') (B'' a') extln).
Qed.

Proving that the closure ordinal does not grow by changing the path base (from a to f a x y)

Section SmallerParameter.

Import ZFfix.

Variable (a x y : set)
(tya : a ∈ Arg)
(tyx : x ∈ A a)
(tyy : y ∈ B a x).
Let a' := f a x y.
Variable
(tya' : a' ∈ Arg).

Let cs q := couple x (couple y q).

Let arg'2arg : typ_fun cs (Arg' a') (Arg' a).
Qed.

Let csa p := couple (cs (fst p)) (snd p).
Let csam : morph1 csa.
Qed.

Lemma a'2a : typ_fun csa (A' (Arg' a') (A'' a')) (A' (Arg' a) (A'' a)).

Let ea z : ext_fun (A' (Arg' z) (A'' z)) (B' (B'' z)).
Qed.

Let idx_incl : sup (A' (Arg' a') (A'' a')) (B' (B'' a')) ⊆ sup (A' (Arg' a) (A'' a)) (B' (B'' a)).
Qed.

Let csw w := replf w (fun p => couple (fst p) (csa (snd p))).
Let cswe w : ext_fun w (fun p => couple (fst p) (csa (snd p))).
Qed.
Let cswm : morph1 csw.
Qed.

Notation Fa := (W0.Wf (A' (Arg' a) (A'' a)) (B' (B'' a))).
Notation Fa' := (W0.Wf (A' (Arg' a') (A'' a')) (B' (B'' a'))).
Notation dom_a := (W0.Wdom (A' (Arg' a) (A'' a)) (B' (B'' a))).
Notation dom_a' := (W0.Wdom (A' (Arg' a') (A'' a')) (B' (B'' a'))).

Let dom_incl : typ_fun csw dom_a' dom_a.

Qed.

Let cswse b g : ext_fun b (fun i => csw (cc_app g i)).
Qed.

Let csw_sup : ∀ w X,
  w ∈ W0.W_F (A' (Arg' a') (A'' a')) (B' (B'' a')) X ->
  csw (W0.Wsup (B' (B'' a')) w) ==
  W0.Wsup (B' (B'' a)) (couple (csa (fst w))
     (cc_lam (B' (B'' a) (csa (fst w))) (fun i => csw (cc_app (snd w) i)))).

Qed.

Let Fa_typ : ∀ X Y,
  typ_fun csw X Y ->
  typ_fun csw (Fa' X) (Fa Y).

Qed.

Let Fa_mono z : Proper (incl_set ==>incl_set) (W0.Wf (A' (Arg' z) (A'' z)) (B' (B'' z))).
Qed.

Let Fa_dom z : ∀ X,
  X ⊆ W0.Wdom (A' (Arg' z) (A'' z)) (B' (B'' z)) ->
  W0.Wf (A' (Arg' z) (A'' z)) (B' (B'' z)) X ⊆ W0.Wdom (A' (Arg' z) (A'' z)) (B' (B'' z)).
Qed.

Let dom_ti_incl : ∀ o, isOrd o -> typ_fun csw (TI Fa' o) (TI Fa o).
Qed.

Let fix_incl : typ_fun csw (Ffix Fa' dom_a') (Ffix Fa dom_a).
Qed.

Lemma wsup_fsub A0 B0 (bm : ext_fun A0 B0) o w :
  isOrd o ->
  w ∈ W0.W_F A0 B0 (TI (W0.Wf A0 B0) o) ->
  fsub (W0.Wf A0 B0) (W0.Wdom A0 B0) (W0.Wsup B0 w) == replf (B0 (fst w)) (fun i => cc_app (snd w) i).

Let csw_fsub : ∀ o w,
  isOrd o ->
  w ∈ Fa' (TI Fa' o) ->
  typ_fun csw (fsub Fa' dom_a' w) (fsub Fa dom_a (csw w)).

Qed.

Let Fra'_ord : ∀ x,
  x ∈ Ffix Fa' dom_a' ->
  isOrd (Fix_rec Fa' dom_a' (F_a Fa' dom_a') x).
Qed.

Let Fra_ord : ∀ x,
  x ∈ Ffix Fa' dom_a' ->
  isOrd (Fix_rec Fa dom_a (F_a Fa dom_a) (csw x)).
Qed.

Let F_a_ext : ∀ (x x' : set) (g g' : set -> set),
x ∈ Ffix Fa dom_a ->
eq_fun (fsub Fa dom_a x) g g' ->
x == x' -> F_a Fa dom_a g x == F_a Fa dom_a g' x'.
Qed.
Let F_a'_ext : ∀ (x x' : set) (g g' : set -> set),
x ∈ Ffix Fa' dom_a' ->
eq_fun (fsub Fa' dom_a' x) g g' ->
x == x' -> F_a Fa' dom_a' g x == F_a Fa' dom_a' g' x'.
Qed.

Lemma Faord : ∀ x,
  x ∈ Ffix Fa' dom_a' ->
  Fix_rec Fa' dom_a' (F_a Fa' dom_a') x ⊆
  Fix_rec Fa dom_a (F_a Fa dom_a) (csw x).

Lemma smaller_parameter :
  W_ord (Arg' a') (A'' a') (B'' a') ⊆ W_ord (Arg' a) (A'' a) (B'' a).

End SmallerParameter.

Lemma WW_eqn a : a ∈ Arg -> WW a == W_Fd A B f WW a.

Showing the encoding WW is small even when Arg is big

Section UniverseFacts.

  Variable U : set.
  Hypothesis Ugrot : grot_univ U.
  Hypothesis Unontriv : omega ∈ U.

We don't assume Arg is in U...

  Hypothesis aU : ∀ a, a ∈ Arg -> A a ∈ U.
  Hypothesis bU : ∀ a x, a ∈ Arg -> x ∈ A a -> B a x ∈ U.

  Lemma G_Arg' : ∀ a, a ∈ Arg -> Arg' a ∈ U.

  Lemma G_WW a : a ∈ Arg -> WW a ∈ U.

End UniverseFacts.

End BigParameter.

Section Test.
Let x := (WW_eqn , G_WW ).
Print Assumptions x.
End Test.