Library ZFspos
Require Import ZF ZFpairs ZFsum ZFrelations ZFcoc ZFord ZFfix.
Require Import ZFstable ZFiso ZFind_w.
Require Import ZFstable ZFiso ZFind_w.
Here we define the (semantic) notion of strictly positiveness.
We then show that it fulfills all the requirements for the existence
of a fixpoint:
- monotonicity
- isomorphism with a W-type
Record positive := mkPositive {
pos_oper : set -> set ;
w1 : set;
w2 : set->set;
wf : set -> set
}.
Definition eqpos p1 p2 :=
(eq_set==>eq_set)%signature (pos_oper p1) (pos_oper p2) /\
w1 p1 == w1 p2 /\
(eq_set==>eq_set)%signature (w2 p1) (w2 p2) /\
(eq_set==>eq_set)%signature (wf p1) (wf p2).
Instance eqpos_sym : Symmetric eqpos.
Qed.
Instance eqpos_trans : Transitive eqpos.
Qed.
Record isPositive (p:positive) := {
pos_mono : Proper (incl_set ==> incl_set) (pos_oper p);
w2m : ext_fun (w1 p) (w2 p);
w_iso : ∀ X, iso_fun (pos_oper p X) (W_F (w1 p) (w2 p) X) (wf p)
}.
Instance pos_oper_morph : Proper (eqpos==>eq_set==>eq_set) pos_oper.
Qed.
Instance w1_morph : Proper (eqpos==>eq_set) w1.
Qed.
Instance w2_morph : Proper (eqpos==>eq_set==>eq_set) w2.
Qed.
Instance wf_morph : Proper (eqpos==>eq_set==>eq_set) wf.
Qed.
Lemma pos_oper_stable : ∀ p, isPositive p ->
stable (pos_oper p).
General properties of positive definitions (independent of convergence)
Definition INDi p o :=
TI (pos_oper p) o.
Instance INDi_morph_gen : Proper (eqpos ==> eq_set ==> eq_set) INDi.
Qed.
Instance INDi_morph p : isPositive p -> morph1 (INDi p).
Qed.
Lemma INDi_succ_eq : ∀ p o,
isPositive p -> isOrd o -> INDi p (osucc o) == pos_oper p (INDi p o).
Lemma INDi_stable : ∀ p, isPositive p -> stable_ord (INDi p).
Lemma INDi_mono : ∀ p o o',
isPositive p -> isOrd o -> isOrd o' -> o ⊆ o' ->
INDi p o ⊆ INDi p o'.
Section InductiveFixpoint.
Variable p : positive.
Hypothesis p_ok : isPositive p.
Let Wpf := pos_oper p.
Let Wp := W (w1 p) (w2 p).
Let Wff := Wf (w1 p) (w2 p).
Let Wd := Wdom (w1 p) (w2 p).
Let Bext : ext_fun (w1 p) (w2 p).
Qed.
Let Wff_mono : Proper (incl_set ==> incl_set) Wff.
Qed.
Let Wff_typ : ∀ X, X ⊆ Wd -> Wff X ⊆ Wd.
Qed.
The closure ordinal
Definition IND_clos_ord := W_ord (w1 p) (w2 p).
Definition IND := INDi p IND_clos_ord.
Let WFf := W_F (w1 p) (w2 p).
Let Wp2 := W (w1 p) (w2 p).
Definition wf' f := comp_iso (wf p) (WFmap (w2 p) f).
Lemma wf'iso X Y f :
iso_fun X Y f ->
iso_fun (pos_oper p X) (WFf Y) (wf' f).
Lemma IND_eq : IND == pos_oper p IND.
Lemma INDi_IND : ∀ o,
isOrd o ->
INDi p o ⊆ IND.
End InductiveFixpoint.
Definition IND := INDi p IND_clos_ord.
Let WFf := W_F (w1 p) (w2 p).
Let Wp2 := W (w1 p) (w2 p).
Definition wf' f := comp_iso (wf p) (WFmap (w2 p) f).
Lemma wf'iso X Y f :
iso_fun X Y f ->
iso_fun (pos_oper p X) (WFf Y) (wf' f).
Lemma IND_eq : IND == pos_oper p IND.
Lemma INDi_IND : ∀ o,
isOrd o ->
INDi p o ⊆ IND.
End InductiveFixpoint.
A library of positive operators
- constant
- recursive subterm
- sum
- prodcart
- sigma
- cc_prod
- nested...
Definition trad_cst :=
sigma_1r_iso (fun _ => cc_lam empty (fun _ => empty)).
Lemma iso_cst : ∀ A X,
iso_fun A (W_F A (fun _ => empty) X) trad_cst.
Definition pos_cst A :=
mkPositive (fun _ => A) A (fun _ => empty) trad_cst.
Lemma isPos_cst A : isPositive (pos_cst A).
sigma_1r_iso (fun _ => cc_lam empty (fun _ => empty)).
Lemma iso_cst : ∀ A X,
iso_fun A (W_F A (fun _ => empty) X) trad_cst.
Definition pos_cst A :=
mkPositive (fun _ => A) A (fun _ => empty) trad_cst.
Lemma isPos_cst A : isPositive (pos_cst A).
Recursive subterm
Definition trad_reccall :=
comp_iso (fun x => cc_lam (singl empty) (fun _ => x)) (couple empty).
Lemma iso_reccall : ∀ X,
iso_fun X (W_F (singl empty) (fun _ => singl empty) X) trad_reccall.
Definition pos_rec :=
mkPositive (fun X => X) (singl empty) (fun _ => singl empty) trad_reccall.
Lemma isPos_rec : isPositive pos_rec.
Disjoint sum
Definition trad_sum f g :=
comp_iso (sum_isomap f g) sum_sigma_iso.
Lemma cc_prod_sum_case_commut A1 A2 B1 B2 Y x x':
ext_fun A1 B1 ->
ext_fun A2 B2 ->
x ∈ sum A1 A2 ->
x == x' ->
sum_case (fun x => cc_arr (B1 x) Y) (fun x => cc_arr (B2 x) Y) x ==
cc_arr (sum_case B1 B2 x') Y.
Lemma W_F_sum_commut A1 A2 B1 B2 X:
ext_fun A1 B1 ->
ext_fun A2 B2 ->
sigma (sum A1 A2)
(sum_case (fun x => cc_arr (B1 x) X) (fun x => cc_arr (B2 x) X)) ==
W_F (sum A1 A2) (sum_case B1 B2) X.
Lemma iso_sum : ∀ X1 X2 A1 A2 B1 B2 Y f g,
ext_fun A1 B1 ->
ext_fun A2 B2 ->
iso_fun X1 (W_F A1 B1 Y) f ->
iso_fun X2 (W_F A2 B2 Y) g ->
iso_fun (sum X1 X2) (W_F (sum A1 A2) (sum_case B1 B2) Y) (trad_sum f g).
Definition pos_sum F G :=
mkPositive (fun X => sum (pos_oper F X) (pos_oper G X))
(sum (w1 F) (w1 G)) (sum_case (w2 F) (w2 G)) (trad_sum (wf F) (wf G)).
Lemma isPos_sum F G :
isPositive F ->
isPositive G ->
isPositive (pos_sum F G).
Concatenating recursive argument
Definition trad_prodcart B1 B2 f g :=
comp_iso (sigma_isomap f (fun _ => g))
(comp_iso prodcart_sigma_iso
(sigma_isomap (fun x => x)
(fun x => prodcart_cc_prod_iso (sum (B1 (fst x)) (B2 (snd x)))))).
Lemma iso_prodcart : ∀ X1 X2 A1 A2 B1 B2 Y f g,
ext_fun A1 B1 ->
ext_fun A2 B2 ->
iso_fun X1 (W_F A1 B1 Y) f ->
iso_fun X2 (W_F A2 B2 Y) g ->
iso_fun (prodcart X1 X2)
(W_F (prodcart A1 A2) (fun i => sum (B1 (fst i)) (B2 (snd i))) Y)
(trad_prodcart B1 B2 f g).
Definition pos_consrec F G :=
mkPositive (fun X => prodcart (pos_oper F X) (pos_oper G X))
(prodcart (w1 F) (w1 G))
(fun c => sum (w2 F (fst c)) (w2 G (snd c)))
(trad_prodcart (w2 F) (w2 G) (wf F) (wf G)).
Lemma isPos_consrec F G :
isPositive F ->
isPositive G ->
isPositive (pos_consrec F G).
Concatenating non-recursive argument
Definition trad_sigma f :=
comp_iso (sigma_isomap (fun x => x) f) sigma_isoassoc.
Definition pos_norec A F :=
mkPositive
(fun X => sigma A (fun x => pos_oper (F x) X))
(sigma A (fun x => w1 (F x)))
(fun c => w2 (F (fst c)) (snd c))
(trad_sigma (fun x => wf (F x))).
Lemma iso_arg_norec : ∀ P X A B Y f,
ext_fun P X ->
ext_fun P A ->
ext_fun2 P A B ->
ext_fun2 P X f ->
(∀ x, x ∈ P -> iso_fun (X x) (W_F (A x) (B x) Y) (f x)) ->
iso_fun (sigma P X)
(W_F (sigma P A) (fun p => B (fst p) (snd p)) Y)
(trad_sigma f).
Lemma isPos_consnonrec A F :
Proper (eq_set ==> eqpos) F ->
(∀ x, x ∈ A -> isPositive (F x)) ->
isPositive (pos_norec A F).
Indexed recursive subterms
Definition trad_cc_prod P B f :=
comp_iso (cc_prod_isomap P (fun x => x) f)
(comp_iso (cc_prod_sigma_iso P)
(sigma_isomap (fun x => x)
(fun x => cc_prod_isocurry P (fun y => B y (cc_app x y))))).
Lemma iso_param : ∀ P X A B Y f,
ext_fun P X ->
ext_fun P A ->
ext_fun2 P A B ->
ext_fun2 P X f ->
(∀ x, x ∈ P -> iso_fun (X x) (W_F (A x) (B x) Y) (f x)) ->
iso_fun (cc_prod P X)
(W_F (cc_prod P A) (fun p => sigma P (fun x => B x (cc_app p x))) Y)
(trad_cc_prod P B f).
Definition pos_param A F :=
mkPositive
(fun X => cc_prod A (fun x => pos_oper (F x) X))
(cc_prod A (fun x => w1 (F x)))
(fun f => sigma A (fun x => w2 (F x) (cc_app f x)))
(trad_cc_prod A (fun a => w2 (F a)) (fun a => wf (F a))).
Lemma isPos_param A F :
Proper (eq_set ==> eqpos) F ->
(∀ x, x ∈ A -> isPositive (F x)) ->
isPositive (pos_param A F).
Require Import ZFgrothendieck.
Section InductiveUniverse.
Variable U : set.
Hypothesis Ugrot : grot_univ U.
Hypothesis Unontriv : omega ∈ U.
Let Unonmt : empty ∈ U.
Qed.
The predicativity condition: the operator remains within U.
We also need the invariant that w1 and w2 also belong to the universe U
Record pos_universe p := {
G_pos_oper : ∀ X, X ∈ U -> pos_oper p X ∈ U;
G_w1 : w1 p ∈ U;
G_w2 : ∀ x, x ∈ w1 p -> w2 p x ∈ U
}.
Variable p : positive.
Hypothesis p_ok : isPositive p.
Hypothesis p_univ : pos_universe p.
Lemma G_IND : IND p ∈ U.
Lemma G_INDi o : isOrd o -> INDi p o ∈ U.
Lemma pos_univ_cst A : A ∈ U -> pos_universe (pos_cst A).
Lemma pos_univ_rec : pos_universe pos_rec.
Lemma pos_univ_sum p1 p2 :
pos_universe p1 -> pos_universe p2 -> pos_universe (pos_sum p1 p2).
Lemma pos_univ_prodcart p1 p2 :
pos_universe p1 -> pos_universe p2 -> pos_universe (pos_consrec p1 p2).
Lemma pos_univ_norec A p' :
Proper (eq_set==>eqpos) p' ->
A ∈ U -> (∀ x, x ∈ A -> pos_universe (p' x)) ->
pos_universe (pos_norec A p').
Lemma pos_univ_param A p' :
Proper (eq_set==>eqpos) p' ->
A ∈ U -> (∀ x, x ∈ A -> pos_universe (p' x)) ->
pos_universe (pos_param A p').
End InductiveUniverse.
G_pos_oper : ∀ X, X ∈ U -> pos_oper p X ∈ U;
G_w1 : w1 p ∈ U;
G_w2 : ∀ x, x ∈ w1 p -> w2 p x ∈ U
}.
Variable p : positive.
Hypothesis p_ok : isPositive p.
Hypothesis p_univ : pos_universe p.
Lemma G_IND : IND p ∈ U.
Lemma G_INDi o : isOrd o -> INDi p o ∈ U.
Lemma pos_univ_cst A : A ∈ U -> pos_universe (pos_cst A).
Lemma pos_univ_rec : pos_universe pos_rec.
Lemma pos_univ_sum p1 p2 :
pos_universe p1 -> pos_universe p2 -> pos_universe (pos_sum p1 p2).
Lemma pos_univ_prodcart p1 p2 :
pos_universe p1 -> pos_universe p2 -> pos_universe (pos_consrec p1 p2).
Lemma pos_univ_norec A p' :
Proper (eq_set==>eqpos) p' ->
A ∈ U -> (∀ x, x ∈ A -> pos_universe (p' x)) ->
pos_universe (pos_norec A p').
Lemma pos_univ_param A p' :
Proper (eq_set==>eqpos) p' ->
A ∈ U -> (∀ x, x ∈ A -> pos_universe (p' x)) ->
pos_universe (pos_param A p').
End InductiveUniverse.