Library ZFsposd

Require Import ZF ZFpairs ZFsum ZFrelations ZFcoc ZFord ZFfix ZFfixfun.
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.

Require Import ZFind_wd.

Section InductiveFamily.

Variable Arg : set.

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.

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.

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

Variable A : set.
Variable B : set -> set.
Hypothesis Bext : ext_fun A B.

Index type

Variable Arg : set.

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.

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.