Library ZFspos

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

General properties of "strictly positive" inductive definitions

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

Convergence

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.

A library of positive operators

A library of positive operators that generate all inductive types:

constant
recursive subterm
sum
prodcart
sigma
cc_prod
nested...

Non-recursive arguments

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

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

Universe constraints: predicativity

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.