Library ModelCIC


Require Import List Models.
Require ZFecc ZFindtypes.
Require ModelZF.
Import ZFgrothendieck.
Import ZF ZFsum ZFnats ZFord ZFfix ZFecc ZFindtypes IZF.

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

Lemma simpl_int_lift : forall i n x T,
  int (lift (S n) T) (V.cons x i) == int (lift n T) i.

Lemma lift0_term : forall T, eq_term (lift 0 T) T.

Lemma simpl_int_lift1 : forall i x T,
  int (lift 1 T) (V.cons x i) == int T i.

Lemma simpl_lift1 : forall i n x y T,
  int (lift1 (S n) T) (V.cons x (V.cons y i)) == int (lift1 n T) (V.cons x i).

Lemma lift10: forall T, eq_term (lift1 0 T) T.


Parameter toOrd : set -> set.
Parameter toOrd_morph : morph1 toOrd.
Parameter toOrd_ord : forall o, isOrd o -> toOrd o == o.
Parameter toOrd_isOrd : forall x, isOrd (toOrd x).


Definition sub_typ_covariant : forall e U V1 V2,
  sub_typ (U::e) V1 V2 ->
  sub_typ e (Prod U V1) (Prod U V2).

Qed.


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

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

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

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

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

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


Definition Ord (o:set) := cst o.

Definition typ_ord_kind : forall e o, typ e (Ord o) kind.
Qed.

Definition typ_ord_ord : forall e o o',
  lt o o' -> typ e (Ord o) (Ord o').
Qed.

Definition OSucc : term -> term.
Defined.


Definition Nat := cst NAT.

Definition Nati (o:set) := cst (NATi o).

Definition NatI : term -> term.
Defined.

Lemma typ_nati : forall e o,
  isOrd o -> typ e (Nati o) kind.

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


Definition Zero := cst ZERO.

Lemma typ_zero : forall e o,
  isOrd o -> typ e Zero (Nati (osucc o)).


Definition SuccI : term -> term.
Defined.

Lemma typ_succi : forall e o i,
  isOrd o ->
  typ e i (Ord o) ->
  typ e (SuccI i) (Prod (NatI i) (NatI (OSucc (lift 1 i)))).


Definition Natcase (fZ fS n : term) : term.


Defined.

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

Qed.

Lemma Natcase_zero : forall e fZ fS,
  eq_typ e (Natcase fZ fS Zero) fZ.

Lemma Natcase_succ : forall o O e n fZ fS,
  isOrd o ->
  typ e O (Ord o) ->
  typ e n (NatI O) ->
  eq_typ e (Natcase fZ fS (App (SuccI O) n)) (subst n fS).


Lemma typ_natcase : forall o e O P fZ fS n,
  isOrd o ->
  typ e O (Ord 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).


Require Import ZFfixfuntyp.
Require Import ZFrelations.
Import ModelZF.CCM.

Parameter fextends : set -> set -> set -> Prop.
Parameter fext_morph : Proper (eq_set ==> eq_set ==> eq_set ==> iff) fextends.

Lemma fext_trans : forall x y f g h,
  fextends x f g -> fextends y g h -> fextends x f h.
Parameter extends_app : forall f g x A B,
  f \in prod A B ->
  fextends A f g ->
  x \in A ->
  app f x == app g x.

Parameter fext_intro : forall A B f g,
  f \in prod A B ->
  (forall x, x \in A -> app f x == app g x) ->
  fextends A f g.

Lemma fext_lam : forall A B F f g,
    eq_fun A f f ->
    eq_fun B g g ->
    eq_fun A F F ->
    (forall x, x \in A -> x \in B) ->
    (forall x, x \in A -> f x \in F x) ->
    (forall x, x \in A -> f x == g x) ->
    fextends A (lam A f) (lam B g).

Definition fincreasing_bounded o A F :=
  forall x x', lt x' o -> lt x x' -> fextends (A x) (F x) (F x').

Parameter prd_sup : forall o o' A f,
  isOrd o ->
  fincreasing_bounded o A f ->
  lt o' o ->
  fextends (A o') (f o') (sup o f).

Parameter prd_sup_lub : forall o A f g,
  isOrd o ->
  fincreasing_bounded o A f ->
  (forall o', lt o' o -> fextends (A o') (f o') g) ->
  fextends (sup o A) (sup o f) g.

Parameter prd_union : forall o f A B,
  isOrd o ->
  fincreasing_bounded o A f ->
  (forall o', lt o' o -> f o' \in prod (A o') B) ->
  sup o f \in prod (sup o A) B.

Section NatRec.

  Variable eps : set.
  Hypothesis epsOrd : isOrd eps.
  Variable F : set -> set -> set.
  Hypothesis Fm : morph2 F.
  Variable U : set -> set.
  Hypothesis Um : forall o, lt o eps -> ext_fun (NATi o) U.
  Let Ty o := prod (NATi o) U.
  Hypothesis Ftyp : forall o f, lt o eps ->
    f \in Ty o -> F o f \in Ty (osucc o).

  Definition stab_fix_prop :=
    forall o o' f g,
    lt o' eps -> lt o o' ->
    f \in Ty o -> g \in Ty o' ->
    fextends (NATi o) f g ->
    fextends (NATf (NATi o)) (F o f) (F o' g).

  Hypothesis Fstab : stab_fix_prop.

  Definition NATREC := TIO F.

  Lemma NATREC_inv :
    forall x', lt x' eps ->
    TIO F x' \in Ty x' /\
    forall x, lt x x' ->
    fextends (NATi x) (TIO F x) (TIO F x').

  Lemma NATREC_wt : forall o, lt o eps -> NATREC o \in Ty o.

  Lemma NATREC_step : forall o,
    lt o eps ->
    fextends (NATi o) (NATREC o) (F o (NATREC o)).

Section NATREC_Eqn.

  Variable o : set.
  Hypothesis lt_eps : lt o eps.

  Let o_ord : isOrd o.
Qed.

  Lemma NATREC_expand : forall n,
    n \in NATi o -> app (NATREC o) n == app (F o (NATREC o)) n.

  Lemma NATREC_eqn :
    NATREC o == lam (NATi o) (fun x => app (F o (NATREC o)) x).

End NATREC_Eqn.

End NatRec.

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

Lemma NATREC_morph :
  forall f1 f2,
  (eq_set ==> eq_set ==> eq_set)%signature f1 f2 ->
  forall o1 o2, isOrd o1 ->
  o1 == o2 ->
  NATREC f1 o1 == NATREC f2 o2.

Definition NatFix (O U M:term) : term.



Defined.

Definition val_mono (e:env) (doms:env) (ords fixs:B.map) i i' :=
    val_ok e i /\
    val_ok e i' /\
    forall n,
    if ords n then isOrd (i' n) /\ lt (i n) (i' n)
    else if fixs n then
      forall T, nth_error doms n = value T ->
      fextends (int (lift (S n) T) i) (i n) (i' n)
    else i n == i' n.

Definition fx_extends e doms ords fixs dom M :=
    forall i i', val_mono e doms ords fixs i i' ->
    fextends (int dom i) (int M i) (int M i').

Section NatFixRules.

  Variable eps : set.
  Hypothesis eps_ord : isOrd eps.
  Variable e : env.
  Variable O U M : term.
  Hypothesis M_nk : ~ eq_term M kind.
  Hypothesis ty_O : typ e O (Ord eps).
  Hypothesis ty_M : typ (Prod (NatI (Ref 0)) (lift1 1 U)::OSucc O::e)
    M (Prod (NatI (OSucc (Ref 1))) (lift1 2 U)).

  Hypothesis stab : fx_extends (Prod (NatI (Ref 0)) (lift1 1 U) :: OSucc O :: e)
   (NatI (Ref 0) :: nil)
   (B.cons false (B.cons true (B.nil false)))
   (B.cons true (B.cons false (B.nil false)))
   (NatI (OSucc (Ref 1)))
   M.

  Lemma morph_fix_body : forall i M,
    morph2 (fun o' f => int M (V.cons f (V.cons o' i))).

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

  Lemma val_M_ok : forall i o f,
    val_ok e i ->
    lt o (osucc (int O i)) ->
    f \in prod (NATi o) (fun x => int U (V.cons x i)) ->
    val_ok (Prod (NatI (Ref 0)) (lift1 1 U) :: OSucc O :: e)
      (V.cons f (V.cons o i)).

  Lemma ty_fix_body : forall i o f,
   val_ok e i ->
   lt o (osucc (int O i)) ->
   f \in prod (NATi o) (fun x => int U (V.cons x i)) ->
   int M (V.cons f (V.cons o i)) \in
   prod (NATi (osucc o)) (fun x => int U (V.cons x i)).

  Lemma stab_fix_body : forall i,
    val_ok e i ->
    stab_fix_prop (osucc (int O i))
      (fun o' f => int M (V.cons f (V.cons o' i)))
      (fun x => int U (V.cons x i)).

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

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

End NatFixRules.


  Definition noccur (f:nat->bool) (T:term) : Prop :=
    forall i i',
    (forall n, if f n then True else i n == i' n) ->
    int T i == int T i'.

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

  Lemma noc_kind : forall f, noccur f kind.

  Lemma noc_prop : forall f, noccur f prop.

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

  Definition fx_equals e doms ords fixs M :=
    forall i i', val_mono e doms ords fixs i i' ->
    int M i == int M i'.

  Definition fx_sub e doms ords fixs M :=
    forall i i', val_mono e doms ords fixs i i' ->
    int M i \incl int M i'.

  Lemma fx_abs : forall e doms ords fixs U T T' M,
    fx_sub e doms ords fixs T ->
    fx_equals (T::e) (T'::doms) (B.cons false ords) (B.cons false fixs) M ->
    typ (T::e) M U ->
    U <> kind ->
    fx_extends e doms ords fixs T (Abs T M).

  Lemma NATi_sub : forall e doms ords fixs o O,
    isOrd o ->
    typ e O (Ord o) ->
    fx_sub e doms ords fixs O ->
    fx_sub e doms ords fixs (NatI O).

  Lemma OSucc_sub : forall e doms ords fixs O,
    fx_sub e doms ords fixs O ->
    fx_sub e doms ords fixs (OSucc O).

  Lemma var_sub : forall e doms ords fixs n,
    ords n = true ->
    fx_sub e doms ords fixs (Ref n).

  Lemma fx_eq_app : forall e doms ords fixs u v,
    fx_equals e doms ords fixs u ->
    fx_equals e doms ords fixs v ->
    fx_equals e doms ords fixs (App u v).

Import Bool.
  Lemma fx_eq_noc : forall e doms ords fixs t,
    noccur (fun n => ords n || fixs n) t ->
    fx_equals e doms ords fixs t.

  Lemma fx_eq_rec_call : forall e doms ords fixs n x T U,
    ords n = false ->
    fixs n = true ->
    nth_error doms n = value T ->
    T <> kind ->
    typ e (Ref n) (Prod (lift (S n) T) U) ->
    fx_equals e doms ords fixs x ->
    typ e x (lift (S n) T) ->
    fx_equals e doms ords fixs (App (Ref n) x).

Section Example.

Definition nat_ind_typ :=
   Prod (Prod (NatI (Ord omega)) prop)
  (Prod (App (Ref 0) Zero)
  (Prod (Prod (NatI (Ord omega)) (Prod (App (Ref 2) (Ref 0))
                        (App (Ref 3) (App (SuccI (Ord omega)) (Ref 1)))))
  (Prod (NatI (Ord omega)) (App (Ref 3) (Ref 0))))).

Definition nat_ind :=
   Abs (Prod (NatI (Ord omega)) prop)
  (Abs (App (Ref 0) Zero)
  (Abs (Prod (NatI (Ord omega)) (Prod (App (Ref 2) (Ref 0))
                                   (App (Ref 3) (App (SuccI (Ord omega)) (Ref 1)))))
  (NatFix (Ord omega) (App (Ref 3) (Ref 0))
    
    (Abs (NatI (OSucc (Ref 1)))
      (Natcase
        (Ref 4)
        (App (App (Ref 4) (Ref 0))
                  (App (Ref 2) (Ref 0)))
        (Ref 0)))))).

Lemma typ_var' : forall e n T,
  match nth_error e n with value T' => eq_term (lift (S n) T') T | _ => False end ->
  typ e (Ref n) T.

Lemma typ_app0 : forall e u v U V Ur,
  typ e v V ->
  typ e u (Prod V Ur) ->
  V <> kind ->
  Ur <> kind ->
  sub_typ e (subst v Ur) U ->
  typ e (App u v) U.

Lemma typ_app' : forall e u v U V Ur,
  typ e v V ->
  typ e u (Prod V Ur) ->
  V <> kind ->
  eq_term U (subst v Ur) ->
  typ e (App u v) U.

Lemma eqterm_subst_App : forall N u v,
  eq_term (subst N (App u v)) (App (subst N u) (subst N v)).

Lemma nat_ind_def :
  forall e, typ e nat_ind nat_ind_typ.

End Example.