Library ZFsposd
Require Import ZF ZFpairs ZFsum ZFrelations ZFcoc ZFord ZFfix ZFfixfun.
Require Import ZFstable ZFiso ZFind_w ZFspos.
Require Import ZFstable ZFiso ZFind_w ZFspos.
Inductive families. Indexes are modelled as a constraint over an inductive
type defined without considering the index values.
Given a function f that computes the index of any element of X,
index(f) shall compute the index of any element of F(X) it assumes
the index information is stored within the data (not the case of non-uniform
parameters...).
Record dpositive := mkDPositive {
carrier :> positive;
dpos_oper : (set -> set) -> set -> set;
w3 : set -> set -> set;
w4 : set -> set -> Prop
}.
Definition eqdpos (p1 p2:dpositive) :=
eqpos p1 p2 /\
(∀ X X' a a', (eq_set==>eq_set)%signature X X' -> a==a' -> dpos_oper p1 X a == dpos_oper p2 X' a') /\
(∀ x x' i i', x==x' -> i==i' -> w3 p1 x i == w3 p2 x' i') /\
(∀ x x' i i', x==x' -> i==i' -> (w4 p1 x i <-> w4 p2 x' i')).
Record isDPositive (p:dpositive) := {
dpos_pos : isPositive p;
dpm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) (dpos_oper p);
dpmono : mono_fam Arg (dpos_oper p);
w3m : morph2 (w3 p);
w4m : Proper (eq_set==>eq_set==>iff) (w4 p);
w3typ : ∀ x i, x ∈ w1 p -> i ∈ w2 p x -> w3 p x i ∈ Arg;
dpm_iso : ∀ X a,
ext_fun Arg X ->
a ∈ Arg ->
dpos_oper p X a == subset (pos_oper p (sup Arg X))
(fun w => let w := wf p w in
w4 p (fst w) a /\ ∀ i, i ∈ w2 p (fst w) -> cc_app (snd w) i ∈ X (w3 p (fst w) i))
}.
Definition dINDi p := TIF Arg (dpos_oper p).
Hint Resolve dpmono.
Lemma dINDi_succ_eq : ∀ p o a,
isDPositive p -> isOrd o -> a ∈ Arg -> dINDi p (osucc o) a == dpos_oper p (dINDi p o) a.
Lemma INDi_mono : ∀ p o o',
isDPositive p -> isOrd o -> isOrd o' -> o ⊆ o' ->
incl_fam Arg (dINDi p o) (dINDi p o').
Definition dIND (p:dpositive) := dINDi p (IND_clos_ord p).
Lemma dIND_eq : ∀ p a, isDPositive p -> a ∈ Arg -> dIND p a == dpos_oper p (dIND p) a.
Lemma dINDi_dIND : ∀ p o,
isDPositive p ->
isOrd o ->
∀ a, a ∈ Arg ->
dINDi p o a ⊆ dIND p a.
carrier :> positive;
dpos_oper : (set -> set) -> set -> set;
w3 : set -> set -> set;
w4 : set -> set -> Prop
}.
Definition eqdpos (p1 p2:dpositive) :=
eqpos p1 p2 /\
(∀ X X' a a', (eq_set==>eq_set)%signature X X' -> a==a' -> dpos_oper p1 X a == dpos_oper p2 X' a') /\
(∀ x x' i i', x==x' -> i==i' -> w3 p1 x i == w3 p2 x' i') /\
(∀ x x' i i', x==x' -> i==i' -> (w4 p1 x i <-> w4 p2 x' i')).
Record isDPositive (p:dpositive) := {
dpos_pos : isPositive p;
dpm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) (dpos_oper p);
dpmono : mono_fam Arg (dpos_oper p);
w3m : morph2 (w3 p);
w4m : Proper (eq_set==>eq_set==>iff) (w4 p);
w3typ : ∀ x i, x ∈ w1 p -> i ∈ w2 p x -> w3 p x i ∈ Arg;
dpm_iso : ∀ X a,
ext_fun Arg X ->
a ∈ Arg ->
dpos_oper p X a == subset (pos_oper p (sup Arg X))
(fun w => let w := wf p w in
w4 p (fst w) a /\ ∀ i, i ∈ w2 p (fst w) -> cc_app (snd w) i ∈ X (w3 p (fst w) i))
}.
Definition dINDi p := TIF Arg (dpos_oper p).
Hint Resolve dpmono.
Lemma dINDi_succ_eq : ∀ p o a,
isDPositive p -> isOrd o -> a ∈ Arg -> dINDi p (osucc o) a == dpos_oper p (dINDi p o) a.
Lemma INDi_mono : ∀ p o o',
isDPositive p -> isOrd o -> isOrd o' -> o ⊆ o' ->
incl_fam Arg (dINDi p o) (dINDi p o').
Definition dIND (p:dpositive) := dINDi p (IND_clos_ord p).
Lemma dIND_eq : ∀ p a, isDPositive p -> a ∈ Arg -> dIND p a == dpos_oper p (dIND p) a.
Lemma dINDi_dIND : ∀ p o,
isDPositive p ->
isOrd o ->
∀ a, a ∈ Arg ->
dINDi p o a ⊆ dIND p a.
Library of dependent positive operators
Constraint on the index: corresponds to the conclusion of the constructor
Definition dpos_inst i :=
mkDPositive (pos_cst (singl empty)) (fun _ a => cond_set (i==a) (singl empty))
(fun _ _ => empty) (fun _ a => i==a).
Lemma isDPos_inst i : isDPositive (dpos_inst i).
Definition dpos_cst A := mkDPositive (pos_cst A) (fun _ _ => A) (fun _ _ => empty) (fun _ _ => True).
Lemma isDPos_cst A : isDPositive (dpos_cst A).
Definition dpos_rec j := mkDPositive pos_rec (fun X _ => X j) (fun _ _ => j) (fun _ _ => True).
Lemma isDPos_rec j : j ∈ Arg -> isDPositive (dpos_rec j).
Require Import ZFsum.
Definition dpos_sum (F G:dpositive) :=
mkDPositive (pos_sum F G)
(fun X a => sum (dpos_oper F X a) (dpos_oper G X a))
(fun x i => sum_case (fun x1 => w3 F x1 i) (fun x2 => w3 G x2 i) x)
(fun x i => (∀ x1, x == inl x1 -> w4 F x1 i) /\
(∀ x2, x == inr x2 -> w4 G x2 i)).
Lemma isDPos_sum F G :
isDPositive F ->
isDPositive G ->
isDPositive (dpos_sum F G).
Definition dpos_consrec (F G:dpositive) :=
mkDPositive (pos_consrec F G)
(fun X a => prodcart (dpos_oper F X a) (dpos_oper G X a))
(fun x => sum_case (w3 F (fst x)) (w3 G (snd x)))
(fun x i => w4 F (fst x) i /\ w4 G (snd x) i).
Lemma isDPos_consrec F G :
isDPositive F ->
isDPositive G ->
isDPositive (dpos_consrec F G).
Definition dpos_norec (A:set) (F:set->dpositive) :=
mkDPositive (pos_norec A F)
(fun X a => sigma A (fun y => dpos_oper (F y) X a))
(fun x i => w3 (F (fst x)) (snd x) i)
(fun x i => w4 (F (fst x)) (snd x) i).
Lemma isDPos_norec A F :
Proper (eq_set ==> eqdpos) F ->
(∀ x, x ∈ A -> isDPositive (F x)) ->
isDPositive (dpos_norec A F).
Definition dpos_param (A:set) (F:set->dpositive) :=
mkDPositive (pos_param A F)
(fun X a => cc_prod A (fun y => dpos_oper (F y) X a))
(fun x i => w3 (F (fst i)) (cc_app x (fst i)) (snd i))
(fun x i => ∀ k, k ∈ A -> w4 (F k) (cc_app x k) i).
Lemma isDPos_param A F :
Proper (eq_set ==> eqdpos) F ->
(∀ x, x ∈ A -> isDPositive (F x)) ->
isDPositive (dpos_param A F).
End InductiveFamily.
mkDPositive (pos_cst (singl empty)) (fun _ a => cond_set (i==a) (singl empty))
(fun _ _ => empty) (fun _ a => i==a).
Lemma isDPos_inst i : isDPositive (dpos_inst i).
Definition dpos_cst A := mkDPositive (pos_cst A) (fun _ _ => A) (fun _ _ => empty) (fun _ _ => True).
Lemma isDPos_cst A : isDPositive (dpos_cst A).
Definition dpos_rec j := mkDPositive pos_rec (fun X _ => X j) (fun _ _ => j) (fun _ _ => True).
Lemma isDPos_rec j : j ∈ Arg -> isDPositive (dpos_rec j).
Require Import ZFsum.
Definition dpos_sum (F G:dpositive) :=
mkDPositive (pos_sum F G)
(fun X a => sum (dpos_oper F X a) (dpos_oper G X a))
(fun x i => sum_case (fun x1 => w3 F x1 i) (fun x2 => w3 G x2 i) x)
(fun x i => (∀ x1, x == inl x1 -> w4 F x1 i) /\
(∀ x2, x == inr x2 -> w4 G x2 i)).
Lemma isDPos_sum F G :
isDPositive F ->
isDPositive G ->
isDPositive (dpos_sum F G).
Definition dpos_consrec (F G:dpositive) :=
mkDPositive (pos_consrec F G)
(fun X a => prodcart (dpos_oper F X a) (dpos_oper G X a))
(fun x => sum_case (w3 F (fst x)) (w3 G (snd x)))
(fun x i => w4 F (fst x) i /\ w4 G (snd x) i).
Lemma isDPos_consrec F G :
isDPositive F ->
isDPositive G ->
isDPositive (dpos_consrec F G).
Definition dpos_norec (A:set) (F:set->dpositive) :=
mkDPositive (pos_norec A F)
(fun X a => sigma A (fun y => dpos_oper (F y) X a))
(fun x i => w3 (F (fst x)) (snd x) i)
(fun x i => w4 (F (fst x)) (snd x) i).
Lemma isDPos_norec A F :
Proper (eq_set ==> eqdpos) F ->
(∀ x, x ∈ A -> isDPositive (F x)) ->
isDPositive (dpos_norec A F).
Definition dpos_param (A:set) (F:set->dpositive) :=
mkDPositive (pos_param A F)
(fun X a => cc_prod A (fun y => dpos_oper (F y) X a))
(fun x i => w3 (F (fst i)) (cc_app x (fst i)) (snd i))
(fun x i => ∀ k, k ∈ A -> w4 (F k) (cc_app x k) i).
Lemma isDPos_param A F :
Proper (eq_set ==> eqdpos) F ->
(∀ x, x ∈ A -> isDPositive (F x)) ->
isDPositive (dpos_param A F).
End InductiveFamily.
Examples
Module Vectors.
Require Import ZFnats.
Definition vect A :=
dpos_sum
(dpos_inst zero)
(dpos_norec N (fun k => dpos_consrec (dpos_cst A) (dpos_consrec (dpos_rec k) (dpos_inst (succ k))))).
Lemma vect_pos A : isDPositive N (vect A).
Definition nil := inl empty.
Lemma nil_typ A X :
morph1 X ->
nil ∈ dpos_oper (vect A) X zero.
Definition cons k x l :=
inr (couple k (couple x (couple l empty))).
Lemma cons_typ A X k x l :
morph1 X ->
k ∈ N ->
x ∈ A ->
l ∈ X k ->
cons k x l ∈ dpos_oper (vect A) X (succ k).
End Vectors.
Module Wd.
Section Wd.
Parameters of W-types
Index type
Constraints on the subterms
Hypothesis f : set -> set -> set.
Hypothesis fm : morph2 f.
Hypothesis ftyp : ∀ x i,
x ∈ A -> i ∈ B x -> f x i ∈ Arg.
Hypothesis fm : morph2 f.
Hypothesis ftyp : ∀ x i,
x ∈ A -> i ∈ B x -> f x i ∈ Arg.
Instance introduced by the constructors
Hypothesis g : set -> set.
Hypothesis gm : morph1 g.
Definition Wdp : dpositive :=
dpos_norec A (fun x => dpos_consrec (dpos_param (B x) (fun i => dpos_rec (f x i))) (dpos_inst (g x))).
Definition Wsup x h := couple x (couple (cc_lam (B x) h) empty).
Lemma sup_typ X x h :
morph1 X ->
morph1 h ->
x ∈ A ->
(∀ i, i ∈ B x -> h i ∈ X (f x i)) ->
Wsup x h ∈ dpos_oper Wdp X (g x).
End Wd.
End Wd.
Hypothesis gm : morph1 g.
Definition Wdp : dpositive :=
dpos_norec A (fun x => dpos_consrec (dpos_param (B x) (fun i => dpos_rec (f x i))) (dpos_inst (g x))).
Definition Wsup x h := couple x (couple (cc_lam (B x) h) empty).
Lemma sup_typ X x h :
morph1 X ->
morph1 h ->
x ∈ A ->
(∀ i, i ∈ B x -> h i ∈ X (f x i)) ->
Wsup x h ∈ dpos_oper Wdp X (g x).
End Wd.
End Wd.