Library ModelCIC

Require Import List Bool Models.
Require Import ZFfunext ZFecc ZFind_nat.
Import ZF ZFsum ZFnats ZFrelations ZFord ZFfix ZFgrothendieck.
Require ModelZF.

Import ModelZF.CCM.
Import ModelZF.BuildModel.
Import T R J.

Derived rules of the basic judgements

Lemma eq_typ_betar : ∀ e N T M,
  typ e N T ->
  T <> kind ->
  eq_typ e (App (Abs T M) N) (subst N M).

Lemma typ_var0 : ∀ e n T,
  match nth_error e n with
    value T' => T' <> kind /\ sub_typ e (lift (S n) T') T
  | _ => False end ->
  typ e (Ref n) T.

Lemma typ_kind_univ e t : typ e t kind.

Subtyping

Definition sub_typ_covariant : ∀ e U1 U2 V1 V2,
  eq_typ e U1 U2 ->
  sub_typ (U1 ::e) V1 V2 ->
  sub_typ e (Prod U1 V1) (Prod U2 V2).

Qed.

Universes

Definition type (n:nat) := cst (ecc n).

Lemma typ_Prop : ∀ e, typ e prop (type 0).

Lemma typ_Type : ∀ e n, typ e (type n) (type (S n)).

Lemma cumul_Type : ∀ e n, sub_typ e (type n) (type (S n)).

Lemma cumul_Prop : ∀ e, sub_typ e prop (type 0).

Lemma typ_prod2 : ∀ e n T U,
  typ e T (type n) ->
  typ (T :: e) U (type n) ->
  typ e (Prod T U) (type n).

Ordinals

Closure ordinal

Definition Infty := cst omega.

A special judgment (class of ordinals). It is not a set but kind does not restrict to ordinals

Definition typ_ord e O := ∀ i, val_ok e i -> isOrd (int O i).

Lemma typ_ord_lift e n O :
  typ_ord (List.skipn n e) O ->
  typ_ord e (lift n O).

  Lemma typ_Infty e : typ_ord e Infty.

  Lemma typ_ord_ref : ∀ e n T,
    nth_error e n = value T ->
    T <> kind ->
    typ_ord e (lift (S n) T) ->
    typ_ord e (Ref n).

Ordinal successor (also type of ordinals less or equal to the argument)

Definition OSucc : term -> term.
intros o; left; exists (fun i => osucc (int o i)).
Defined.

Lemma typ_OSucc e O :
  typ_ord e O ->
  typ_ord e (OSucc O).

Lemma typ_ord_le e O O':
  typ_ord e O ->
  typ e O' (OSucc O) ->
  typ_ord e O'.

Lemma typ_le_inv i e O O':
  typ e O' (OSucc O) ->
  val_ok e i ->
  int O' i ⊆ int O i.

O ≤ O

Lemma typ_ord_max e O :
typ_ord e O ->
typ e O (OSucc O).

Nat

Definition Nat := cst NAT.

Definition NatI : term -> term.
intros o.
left; exists (fun i => NATi (int o i)).
Defined.

Lemma typ_natI : ∀ e o,
  typ e (NatI o) kind.

Definition Zero := cst ZERO.

Lemma typ_Zero : ∀ e O,
  typ_ord e O ->
  typ e Zero (NatI (OSucc O)).

Definition SuccI : term -> term.
intros o.
apply (Abs (NatI o)).
left; exists (fun i => SUCC (i 0)).
Defined.

Lemma typ_SuccI : ∀ e O,
  typ_ord e O ->
  typ e (SuccI O) (Prod (NatI O) (NatI (OSucc (lift 1 O)))).

Lemma typ_app_SuccI : ∀ e i n,
  typ_ord e i ->
  typ e n (NatI i) ->
  typ e (App (SuccI i) n) (NatI (OSucc i)).

Definition Natcase (fZ fS n : term) : term.
left; exists (fun i => NATCASE (int fZ i) (fun k => int fS (V.cons k i)) (int n i)).
Defined.

Instance Natcase_morph :
  Proper (eq_term ==> eq_term ==> eq_term ==> eq_term) Natcase.
Qed.

Lemma Natcase_succ : ∀ O e n fZ fS,
  typ_ord e O ->
  typ e n (NatI O) ->
  eq_typ e (Natcase fZ fS (App (SuccI O) n)) (subst n fS).

Lemma typ_natcase : ∀ e O P fZ fS n,
  typ_ord e O ->
  typ e fZ (App P Zero) ->
  typ (NatI O :: e) fS (App (lift 1 P) (App (SuccI (lift 1 O)) (Ref 0))) ->
  typ e n (NatI (OSucc O)) ->
  typ e (Natcase fZ fS n) (App P n).

Lemma typ_natcase' : ∀ e O P fZ fS n T,
  typ_ord e O ->
  sub_typ e (App P n) T ->
  typ e fZ (App P Zero) ->
  typ (NatI O :: e) fS
    (App (lift 1 P) (App (SuccI (lift 1 O)) (Ref 0))) ->
  typ e n (NatI (OSucc O)) ->
  typ e (Natcase fZ fS n) T.

Variance

Occurrences

Module Beq.
Definition t := bool.
Definition eq := @eq bool.
Definition eq_equiv : Equivalence eq := eq_equivalence.
End Beq.
Module B := VarMap.Make(Beq).

  Definition noccur (f:B.map) (T:term) : Prop :=
    ∀ i i',
    (∀ n, if f n then True else i n == i' n) ->
    int T i == int T i'.

  Lemma noc_var : ∀ f n, f n = false -> noccur f (Ref n).

  Lemma noc_kind : ∀ f, noccur f kind.

  Lemma noc_prop : ∀ f, noccur f prop.

  Lemma noc_app : ∀ f a b,
    noccur f a -> noccur f b -> noccur f (App a b).

Lemma noc_abs a b f :
  noccur f a ->
  noccur (B.cons false f) b ->
  noccur f (Abs a b).

Lemma noc_prod a b f :
  noccur f a ->
  noccur (B.cons false f) b ->
  noccur f (Prod a b).

Ltac noc_tac :=
  lazymatch goal with
    |- noccur _ (App _ _) => apply noc_app; noc_tac
  | |- noccur _ (Abs _ _) => apply noc_abs; noc_tac
  | |- noccur _ (Prod _ _) => apply noc_prod; noc_tac
  | |- noccur _ (Ref _) => apply noc_var; reflexivity
  | |- noccur _ _ => try (red; reflexivity)
  end.

Judgements with variance

Mark stage-irrelevant functions (domain information have to be repeated)

Module OTeq.
Definition t := option term.
Definition eq := @eq (option term).
Definition eq_equiv : Equivalence eq := eq_equivalence.
End OTeq.
Module OT := VarMap.Make(OTeq).

Environments with tags on ordinal and recursive function variables

Record fenv := {
  tenv : env;
  ords : B.map;
  fixs : OT.map
}.

Definition tinj e :=
  Build_fenv e (B.nil false) (OT.nil None).

Pushing an ordinary variable

Definition push_var e T :=
Build_fenv (T ::tenv e) (B.cons false (ords e)) (OT.cons None (fixs e)).

Pushing a stage-irrelevant function

Definition push_fun e dom rng :=
Build_fenv (Prod dom rng ::tenv e)
(B.cons false (ords e)) (OT.cons (Some dom) (fixs e)).

Pushing an ordinal (stage) variable

Definition push_ord e T :=
Build_fenv (T ::tenv e) (B.cons true (ords e)) (OT.cons None (fixs e)).

Semantics of contexts for variance judgments:

ordinal variables follow the ordinal order
stage-irrelevant function have to be compatible
regular variables have to be the same

Definition val_mono (e:fenv) i i' :=
    val_ok (tenv e) i /\
    val_ok (tenv e) i' /\
    ∀ n,
    if ords e n then i n ⊆ i' n
    else match fixs e n with
      Some T => fcompat (int T (V.shift (S n) i)) (i n) (i' n)
    | _ => i n == i' n
    end.

Lemma val_mono_refl : ∀ e i,
  val_ok (tenv e) i -> val_mono e i i.

Lemma val_push_var : ∀ e i i' x x' T,
  val_mono e i i' ->
  x == x' ->
  el T i x ->
  el T i' x' ->
  val_mono (push_var e T) (V.cons x i) (V.cons x' i').

Lemma val_push_ord : ∀ e i i' x x' T,
  val_mono e i i' ->
  x ⊆ x' ->
  el T i x ->
  el T i' x' ->
  val_mono (push_ord e T) (V.cons x i) (V.cons x' i').

Lemma val_push_fun : ∀ e i i' f g T U,
  val_mono e i i' ->
  f ∈ prod (int T i) (fun x => int U (V.cons x i)) ->
  g ∈ prod (int T i') (fun x => int U (V.cons x i')) ->
  fcompat (int T i) f g ->
  val_mono (push_fun e T U) (V.cons f i) (V.cons g i').

Invariance judgement

Definition var_equals e M :=
∀ i i', val_mono e i i' -> int M i == int M i'.

Function Extension judgment

Definition var_compat e dom M :=
∀ i i', val_mono e i i' ->
fcompat (int dom i) (int M i) (int M i').

Covariance judgment

Definition var_mono e M :=
∀ i i', val_mono e i i' ->
int M i ⊆ int M i'.

Invariance rules

  Definition spec_var e n :=
    ords e n || match fixs e n with Some _ => true | _ => false end.

  Lemma var_eq_noc : ∀ e t,
    noccur (spec_var e) t ->
    var_equals e t.

  Lemma var_eq_app : ∀ e u v,
    var_equals e u ->
    var_equals e v ->
    var_equals e (App u v).

  Lemma var_eq_abs : ∀ e T M,
    var_equals e T ->
    var_equals (push_var e T) M ->
    var_equals e (Abs T M).

  Lemma var_eq_prod : ∀ e T U,
    var_equals e T ->
    var_equals (push_var e T) U ->
    var_equals e (Prod T U).

  Lemma var_eq_NATi : ∀ e O,
    typ_ord (tenv e) O ->
    var_equals e O ->
    var_equals e (NatI O).

  Lemma var_eq_OSucc : ∀ e O,
    var_equals e O ->
    var_equals e (OSucc O).

  Lemma var_eq_Natcase : ∀ e O f1 f2 c,
    typ_ord (tenv e) O ->
    var_mono e O ->
    var_equals e f1 ->
    var_equals (push_var e (NatI O)) f2 ->
    typ (tenv e) c (NatI (OSucc O)) ->
    var_equals e c ->
    var_equals e (Natcase f1 f2 c).

Stage-irrelevance rules

  Lemma var_comp_ref : ∀ e dom n T,
    ords e n = false ->
    fixs e n = Some T ->
    T <> kind ->
    eq_typ (tenv e) (lift (S n) T) dom ->
    var_compat e dom (Ref n).
  Lemma abs_compat : ∀ e U T M,
    var_mono e T ->
    var_equals (push_var e T) M ->
    typ (T ::tenv e) M U ->
    U <> kind ->
    var_compat e T (Abs T M).

  Lemma succ_compat e O :
    typ_ord (tenv e) O ->
    var_mono e O ->
    var_compat e (NatI O) (SuccI O).

  Lemma var_comp_app : ∀ e dom u v,
    dom <> kind ->
    var_compat e dom u ->
    typ (tenv e) v dom ->
    var_equals e v ->
    var_equals e (App u v).

Covariance rules

  Lemma var_eq_sub : ∀ e M, var_equals e M -> var_mono e M.

  Lemma var_mono_ref : ∀ e n,
    ords e n = true ->
    var_mono e (Ref n).

  Lemma var_mono_prod : ∀ e T U,
    var_equals e T ->
    var_mono (push_var e T) U ->
    var_mono e (Prod T U).

  Lemma var_mono_NATi : ∀ e O,
    typ_ord (tenv e) O ->
    var_mono e O ->
    var_mono e (NatI O).

  Lemma var_mono_OSucc : ∀ e O,
    var_mono e O ->
    var_mono e (OSucc O).

Recursor (without case analysis)

Definition NatFix (O M:term) : term.
left.
exists (fun i =>
NATREC (fun o' f => int M (V.cons f (V.cons o' i))) (int O i)).
Defined.

Typing rules of NatFix

Section NatFixRules.

  Variable E : fenv.
  Let e := tenv E.
  Variable O U M : term.
  Hypothesis M_nk : ~ eq_term M kind.
  Hypothesis ty_O : typ_ord e O.
  Hypothesis ty_M : typ (Prod (NatI (Ref 0)) U ::OSucc O ::e)
    M (Prod (NatI (OSucc (Ref 1)))
         (lift1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))).

  Hypothesis stab : var_compat
    (push_fun (push_ord E (OSucc O)) (NatI (Ref 0)) U)
    (NatI (OSucc (Ref 1)))
    M.

  Let F i := fun o' f => int M (V.cons f (V.cons o' i)).

  Lemma morph_fix_body : ∀ i, morph2 (F i).

  Lemma ext_fun_ty : ∀ o i,
    ext_fun (NATi o) (fun x => int U (V.cons x (V.cons o i))).

  Hypothesis var_mono_U :
    var_mono (push_var (push_ord E (OSucc O)) (NatI (OSucc (Ref 0)))) U.

  Lemma ty_fix_body : ∀ i o f,
    val_ok e i ->
    o < osucc (int O i) ->
    f ∈ prod (NATi o) (fun x => int U (V.cons x (V.cons o i))) ->
    F i o f ∈
    prod (NATi (osucc o)) (fun x => int U (V.cons x (V.cons (osucc o) i))).

  Lemma fix_body_irrel : ∀ i,
    val_ok e i ->
    NAT_ord_irrel (int O i) (F i) (fun o' x => int U (V.cons x (V.cons o' i))).

  Lemma fix_codom_mono : ∀ o o' x x' i,
   val_ok e i ->
   isOrd o' ->
   o' ⊆ int O i ->
   isOrd o ->
   o ⊆ o' ->
   x ∈ NATi o ->
   x == x' ->
   int U (V.cons x (V.cons o i)) ⊆ int U (V.cons x' (V.cons o' i)).

  Hint Resolve morph_fix_body ext_fun_ty ty_fix_body fix_codom_mono fix_body_irrel.

  Lemma nat_fix_eqn : ∀ i,
    val_ok e i ->
    NATREC (F i) (int O i) ==
    cc_lam (NATi (int O i))
      (fun x => cc_app (F i (int O i) (NATREC (F i) (int O i))) x).

  Lemma typ_nat_fix : typ e (NatFix O M) (Prod (NatI O) (subst_rec O 1 U)).

  Lemma nat_fix_eq : ∀ N,
    typ e N (NatI O) ->
    eq_typ e (App (NatFix O M) N)
             (App (subst O (subst (lift 1 (NatFix O M)) M)) N).

  Lemma var_comp_fix :
    var_mono E O ->
    var_compat E (NatI O) (NatFix O M).

  Lemma var_eq_fix :
    var_equals E O ->
    var_equals E (NatFix O M).

End NatFixRules.

Print Assumptions typ_nat_fix.

Compound judgements : typing + variance

Definition typ_inv e M T :=
  var_equals e M /\ typ (tenv e) M T.

Definition typ_ext e M A B :=
  var_compat e A M /\ typ (tenv e) M (Prod A B).

Definition typ_mono e M T :=
  var_mono e M /\ typ (tenv e) M T.

Instance typ_inv_morph e : Proper (eq_term ==> eq_term ==> iff) (typ_inv e).

Qed.

Inference rules

Inclusion relation between judgements

Lemma typ_inv_mono : ∀ e M T, typ_inv e M T -> typ_mono e M T.

Lemma typ_inv_ext : ∀ e M A B, typ_inv e M (Prod A B) -> typ_ext e M A B.

Subsumption

Lemma typ_inv_subsumption e M T T' :
typ_inv e M T -> sub_typ (tenv e) T T' -> T <> kind -> typ_inv e M T'.

Typing the three kind of variables

  Lemma typ_inv_ref : ∀ e n T,
    spec_var e n = false ->
    nth_error (tenv e) n = value T ->
    typ_inv e (Ref n) (lift (S n) T).

  Lemma typ_mono_ref : ∀ e n T,
    ords e n = true ->
    nth_error (tenv e) n = value T ->
    typ_mono e (Ref n) (lift (S n) T).

Lemma typ_ext_ref e n A B :
    ords e n = false ->
    fixs e n = Some A ->
    A <> kind ->
    nth_error (tenv e) n = value (Prod A B) ->
    typ_ext e (Ref n) (lift (S n) A) (lift1 (S n) B).

Abstraction

  Lemma typ_inv_abs : ∀ e U T M,
    U <> kind ->
    var_equals e T ->
    typ_inv (push_var e T) M U ->
    typ_inv e (Abs T M) (Prod T U).

  Lemma typ_ext_abs : ∀ e U T M,
    var_mono e T ->
    typ_inv (push_var e T) M U ->
    U <> kind ->
    typ_ext e (Abs T M) T U.

Application

  Lemma typ_ext_app : ∀ e u v A B,
    A <> kind ->
    typ_ext e u A B ->
    typ_inv e v A ->
    typ_inv e (App u v) (subst v B).

Natural numbers: type and constructors

  Lemma typ_inv_Zero e O :
    typ_ord (tenv e) O ->

    typ_inv e Zero (NatI (OSucc O)).

  Lemma typ_inv_Succ e O :
    typ_ord (tenv e) O ->
    var_equals e O ->
    typ_inv e (SuccI O) (Prod (NatI O) (NatI (OSucc (lift 1 O)))).

  Lemma typ_ext_Succ e O :
    typ_ord (tenv e) O ->
    var_mono e O ->
    typ_ext e (SuccI O) (NatI O) (NatI (OSucc (lift 1 O))).

Case-analysis

  Lemma typ_inv_natcase : ∀ e O P fZ fS n T,
    typ_ord (tenv e) O ->
    var_mono e O ->
    sub_typ (tenv e) (App P n) T ->
    typ_inv e fZ (App P Zero) ->
    typ_inv (push_var e (NatI O)) fS
      (App (lift 1 P) (App (SuccI (lift 1 O)) (Ref 0))) ->
    typ_inv e n (NatI (OSucc O)) ->
    typ_inv e (Natcase fZ fS n) T.

Fixpoint

  Lemma typ_ext_fix : ∀ e O U M,
    typ_ord (tenv e) O ->
    var_mono e O ->
    typ_ext (push_fun (push_ord e (OSucc O)) (NatI (Ref 0)) U) M
      (NatI (OSucc (Ref 1))) (lift1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    var_mono (push_var (push_ord e (OSucc O)) (NatI (OSucc (Ref 0)))) U ->
    typ_ext e (NatFix O M) (NatI O) (subst_rec O 1 U).

  Lemma typ_inv_fix : ∀ e O U M,
    typ_ord (tenv e) O ->
    var_equals e O ->
    typ_ext (push_fun (push_ord e (OSucc O)) (NatI (Ref 0)) U) M
      (NatI (OSucc (Ref 1))) (lift1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    var_mono (push_var (push_ord e (OSucc O)) (NatI (OSucc (Ref 0)))) U ->
    typ_inv e (NatFix O M) (Prod (NatI O) (subst_rec O 1 U)).

Derived rules for practical examples (basically applies subsumption beforehand)

  Lemma typ_inv_ref' : ∀ e n t T,
    spec_var e n = false ->
    nth_error (tenv e) n = value t ->
    t <> kind ->
    sub_typ (tenv e) (lift (S n) t) T ->
    typ_inv e (Ref n) T.

  Lemma typ_inv_app : ∀ e u v V Ur T,
    V <> kind ->
    Ur <> kind ->
    sub_typ (tenv e) (subst v Ur) T ->
    typ_inv e u (Prod V Ur) ->
    typ_inv e v V ->
    typ_inv e (App u v) T.

  Lemma typ_inv_rec_call : ∀ e n x t u T,
    ords e n = false ->
    fixs e n = Some t ->
    t <> kind ->
    u <> kind ->
    nth_error (tenv e) n = value (Prod t u) ->
    sub_typ (tenv e) (subst x (lift1 (S n) u)) T ->
    typ_inv e x (lift (S n) t) ->
    typ_inv e (App (Ref n) x) T.

  Lemma typ_inv_fix' : ∀ e O U M T,
    sub_typ (tenv e) (Prod (NatI O) (subst_rec O 1 U)) T ->
    typ_ord (tenv e) O ->
    var_equals e O ->
    var_mono (push_var (push_ord e (OSucc O)) (NatI (OSucc (Ref 0)))) U ->
    typ_ext (push_fun (push_ord e (OSucc O)) (NatI (Ref 0)) U) M
      (NatI (OSucc (Ref 1))) (lift1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    typ_inv e (NatFix O M) T.

Two examples of derived principles:

the standard recursor for Nat
subtraction with size information

Section Example.

Definition nat_ind_typ K :=
   Prod (Prod (NatI Infty) K)
  (Prod (App (Ref 0) Zero)
  (Prod (Prod (NatI Infty) (Prod (App (Ref 2) (Ref 0))
                        (App (Ref 3) (App (SuccI Infty) (Ref 1)))))
  (Prod (NatI Infty) (App (Ref 3) (Ref 0))))).

Definition nat_ind K :=
   Abs (Prod (NatI Infty) K)
  (Abs (App (Ref 0) Zero)
  (Abs (Prod (NatI Infty) (Prod (App (Ref 2) (Ref 0))
                                   (App (Ref 3) (App (SuccI Infty) (Ref 1)))))
  (NatFix Infty

    (Abs (NatI (OSucc (Ref 1)))
      (Natcase
        (Ref 4)
        (App (App (Ref 4) (Ref 0))
                  (App (Ref 2) (Ref 0)))
        (Ref 0)))))).

Lemma nat_ind_def e K (cK:∀ f, noccur(B.cons false f)K) :
  typ_inv e (nat_ind K) (nat_ind_typ K).

Subtraction

Definition minus O :=
  NatFix O

    (Abs (NatI (OSucc (Ref1)))
    (Abs (NatI Infty)
    (Natcase
       Zero

       (Natcase
         (Ref 2)

         (App (App (Ref4) (Ref1)) (Ref0))
         (Ref1))
       (Ref1)))).

Definition minus_typ O := Prod (NatI O) (Prod (NatI Infty) (NatI (lift 2 O))).

Lemma minus_def e O :
  typ_ord (tenv e) O ->
  var_equals e O ->
  typ_inv e (minus O) (minus_typ O).

End Example.