Library SN_CIC

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

Import SN_CC_Real.
Import SN_CC_Real.CCSN.
Import SN_CC_Real.SN.
Opaque Real.
Import Sat Sat.SatSet.

Lemma Real_intro x t T :
  x ∈ El T ->
  (x ∈ El T -> inSAT t (Real T x)) ->
  [x,t] \real T.

Lemma Real_ax x t T R :
  (∀ x x', x ∈ T -> x==x' -> eqSAT (R x) (R x')) ->
  ([x,t] \real mkTY T R <-> x ∈ T /\ inSAT t (R x)).

Lemma Real_intro2 x t T R :
  (∀ x x', x ∈ T -> x==x' -> eqSAT (R x) (R x')) ->
  x ∈ T ->
  (x ∈ T -> inSAT t (R x)) ->
  [x,t] \real mkTY T R.

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 T, nth_error e n with
    Some _, value T' => T' <> kind /\ sub_typ e (lift (S n) T') T
  | _,_ => False end ->
  typ e (Ref n) T.

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

Definition Ord (o:set) : trm :=
  cst o Lc.K (fun _ _ => eq_refl) (fun _ _ _ => eq_refl).

Definition Ordt (o:set) : trm :=
  cst (mkTY o (fun _ => snSAT)) Lc.K (fun _ _ => eq_refl) (fun _ _ _ => eq_refl).

Definition typ_ord_kind : ∀ e o, zero ∈ o -> typ e (Ordt o) kind.


Qed.

Definition typ_ord_ord : ∀ e o o',
  o < o' -> typ e (Ord o) (Ordt o').
Qed.

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

Definition OSucct : trm -> trm.
intros o; left; exists (fun i => mkTY (osucc (int i o)) (fun _ => snSAT)) (fun j => tm j o).
Defined.

Lemma tyord_inv : ∀ e i j o o',
  isOrd o' ->
  typ e o (Ordt o') ->
  val_ok e i j ->
  isOrd (int i o) /\ int i o < o' /\ Lc.sn (tm j o).

Require Import SATnat.
Opaque cNAT.

Definition Nat : trm.
left; exists (fun _ => mkTY NAT cNAT) (fun _ => Lc.K).
Defined.

Definition NatI (O:trm) : trm.
left; exists (fun i => mkTY (NATi (int i O)) cNAT) (fun j => tm j O).

Defined.

Lemma typ_natI : ∀ e eps o,
  isOrd eps ->
  typ e o (Ordt eps) ->
  typ e (NatI o) kind.

Lemma realNati_def x t i O :
 isOrd (int i O) ->
 ([x,t] \real int i (NatI O) <->
  x ∈ NATi (int i O) /\ inSAT t (cNAT x)).


Definition Zero : trm.
left; exists (fun _ => ZERO) (fun _ => ZE).
Defined.

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


Definition Succ (o:trm): trm.
left; exists (fun i => lam (int i (NatI o)) SUCC) (fun _ => SU).





Defined.

Lemma El_prod A Ar B Br :
  ext_fun A B ->
  El (prod(mkTY A Ar) (fun x => mkTY (B x) (Br x))) ==
  cc_prod A B.

Lemma typ_succi : ∀ e o i,
  isOrd o ->
  typ e i (Ordt o) ->
  typ e (Succ i) (Prod (NatI i) (NatI (OSucc (lift 1 i)))).


Definition Natcase (fZ fS n : trm) : trm.
left; exists (fun i => NATCASE (int i fZ) (fun k => int (V.cons k i) fS) (int i n))
       (fun j => NCASE (tm j fZ) (Lc.Abs (tm (Lc.ilift j) fS)) (tm j n)).
Defined.

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

Qed.

Notation "'int0' x y" := (int y x) (at level 10, x at level 9, y at level 9).

Lemma Natcase_succ : ∀ o O e n fZ fS,
  isOrd o ->
  typ e O (Ordt o) ->
  typ e n (NatI O) ->
  eq_typ e (Natcase fZ fS (App (Succ O) n)) (subst n fS).

Lemma NCASE_fNAT' o f g n k (A B:family) :
  isOrd o ->
  k ∈ NATi (osucc o) ->
  inSAT n (fNAT A k) ->
  inSAT f (B ZERO) ->
  inSAT g (piNATi(fun m => prodSAT (A m) (B (SUCC m)))o) ->
  inSAT (NCASE f g n) (B k).
Admitted.

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


Lemma typ_natcase' : ∀ o e O P fZ fS n T,
  isOrd o ->
  T <> kind ->
  typ e O (Ordt o) ->
  sub_typ e (App P n) T ->
  typ e fZ (App P Zero) ->
  typ (NatI O :: e) fS
    (App (lift 1 P) (App (Succ (lift 1 O)) (Ref 0))) ->
  typ e n (NatI (OSucc O)) ->
  typ e (Natcase fZ fS n) T.

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

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

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

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

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

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

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

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

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

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

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

Lemma val_push_var : ∀ e i j i' j' x t x' t' T,
  val_mono e i j i' j' ->
  x == x' ->
  [x,t] \real int i T ->
  [x',t'] \real int i' T ->
  T <> kind ->
  val_mono (push_var e T) (V.cons x i) (I.cons t j) (V.cons x' i') (I.cons t' j').

Lemma val_push_ord : ∀ e i j i' j' x t x' t' T,
  val_mono e i j i' j' ->
  x ⊆ x' ->
  [x,t] \real int i T ->
  [x',t'] \real int i' T ->
  T <> kind ->
  val_mono (push_ord e T) (V.cons x i) (I.cons t j) (V.cons x' i') (I.cons t' j').

Lemma val_push_fun : ∀ e i j i' j' f tf g tg T U,
  val_mono e i j i' j' ->
  [f,tf] \real prod (int i T) (fun x => int (V.cons x i) U) ->
  [g,tg] \real prod (int i' T) (fun x => int (V.cons x i') U) ->
  fcompat (El(int i T)) f g ->
  val_mono (push_fun e T U) (V.cons f i) (I.cons tf j) (V.cons g i') (I.cons tg j').

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

Definition fx_sub e M :=
  ∀ i i' j j', val_mono e i j i' j' ->
  ∀ x t, [x,t] \real int i M -> [x,t] \real int i' M.

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

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

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

  Lemma fx_eq_noc : ∀ e t,
    noccur (spec_var e) t ->
    fx_equals e t.

  Lemma fx_eq_app : ∀ e u v,
    fx_equals e u ->
    fx_equals e v ->
    fx_equals e (App u v).

  Lemma fx_eq_abs : ∀ e T M,
    T <> kind ->
    fx_equals e T ->
    fx_equals (push_var e T) M ->
    fx_equals e (Abs T M).

  Lemma fx_eq_rec_call : ∀ e n x T U,
    ords e n = false ->
    fixs e n = Some T ->
    T <> kind ->
    typ (tenv e) (Ref n) (Prod (lift (S n) T) U) ->
    fx_equals e x ->
    typ (tenv e) x (lift (S n) T) ->
    fx_equals e (App (Ref n) x).


  Lemma fx_equals_subval : ∀ e M, fx_equals e M -> fx_subval e M.

  Lemma fx_equals_sub : ∀ e M, fx_equals e M -> fx_sub e M.

  Lemma var_sub : ∀ e n,
    ords e n = true ->
    fx_subval e (Ref n).

Lemma fx_sub_prod : ∀ e T U,
  T <> kind ->
  fx_equals e T ->
  fx_sub (push_var e T) U ->
  fx_sub e (Prod T U).

  Lemma NATi_sub : ∀ e o O,
    isOrd o ->
    typ (tenv e) O (Ordt o) ->
    fx_subval e O ->
    fx_sub e (NatI O).

  Lemma OSucc_sub : ∀ e O,
    fx_subval e O ->
    fx_subval e (OSucc O).


  Lemma fx_abs : ∀ e U T M,
    T <> kind ->
    fx_sub e T ->
    fx_equals (push_var e T) M ->
    typ (T::tenv e) M U ->
    U <> kind ->
    fx_extends e T (Abs T M).

Definition NatFix (O M:trm) : trm.
left.
exists (fun i =>
         NATREC (fun o' f => int (V.cons f (V.cons o' i)) M) (int i O))
       (fun j => NATFIX (Lc.Abs (tm (Lc.ilift (I.cons (tm j O) j)) M))).
Defined.

Section NatFixRules.

  Variable infty : set.
  Hypothesis infty_ord : isOrd infty.
  Variable E : fenv.
  Let e := tenv E.
  Variable O U M : trm.
  Hypothesis M_nk : ~ eq_trm M kind.
  Hypothesis ty_O : typ e O (Ordt infty).
  Hypothesis ty_M : typ (Prod (NatI (Ref 0)) U::OSucct O::e)
    M (Prod (NatI (OSucc (Ref 1)))
         (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))).

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

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

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

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

  Hypothesis fx_sub_U :
    fx_sub (push_var (push_ord E (OSucct O)) (NatI (OSucc (Ref 0)))) U.

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

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

  Lemma fix_codom_mono : ∀ o o' x x' i j,
   val_ok e i j ->
   isOrd o' ->
   o' ⊆ int i O ->
   isOrd o ->
   o ⊆ o' ->
   x ∈ NATi o ->
   x == x' ->
   El (int (V.cons x (V.cons o i)) U) ⊆ El(int (V.cons x' (V.cons o' i)) U).
  Hint Resolve morph_fix_body ext_fun_ty ty_fix_body fix_codom_mono fix_body_irrel.

Let fix_typ o i j:
  val_ok e i j ->
  isOrd o ->
  isOrd (int i O) ->
  o ⊆ int i O ->
  NATREC (F i) o
   ∈ cc_prod (NATi o) (fun n => El (int (V.cons n (V.cons o i)) U)).



Qed.

  Lemma fix_irr i j o o' x :
    val_ok e i j ->
    isOrd o ->
    isOrd o' ->
    isOrd (int i O) ->
    o ⊆ o' ->
    o' ⊆ int i O ->
    x ∈ NATi o ->
    cc_app (NATREC (F i) o) x == cc_app (NATREC (F i) o') x.

Lemma fix_eqn : ∀ i j o n,
  val_ok e i j ->
  isOrd o ->
  isOrd (int i O) ->
  o ⊆ int i O ->
  n ∈ NATi (osucc o) ->
  cc_app (NATREC (F i) (osucc o)) n ==
  cc_app (int (V.cons (NATREC (F i) o) (V.cons o i)) M) n.

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

Lemma equiv_piSAT_piNAT o B B' f:
isOrd o ->
(∀ n, n ∈ NATi o -> eqSAT (Real (B n) (f n)) (B' n)) ->
eqSAT (piSAT (mkTY (NATi o) cNAT) B f)
      (piNATi (fun n => prodSAT (cNAT n) (B' n)) o).

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 nat_fix_extend :
  fx_subval E O ->
  fx_extends E (NatI O) (NatFix O M).

Lemma nat_fix_equals :
  fx_equals E O ->
  fx_equals E (NatFix O M).

End NatFixRules.

Print Assumptions typ_nat_fix.

Lemma typ_nat_fix' : ∀ infty e O U M T,
       T <> kind ->
       isOrd infty ->
       typ e O (Ordt infty) ->
       typ (Prod (NatI (Ref 0)) U :: OSucct O :: e) M
         (Prod (NatI (OSucc (Ref 1)))
           (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))) ->
       fx_extends (push_fun (push_ord (tinj e) (OSucct O)) (NatI (Ref 0)) U)
         (NatI (OSucc (Ref 1))) M ->
       fx_sub (push_var (push_ord (tinj e) (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
       sub_typ e (Prod (NatI O) (subst_rec O 1 U)) T ->
       typ e (NatFix O M) T.

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

Definition typ_mono e M :=
  fx_sub e M /\ typs (tenv e) M.

Definition typ_monoval e M T :=
  fx_subval e M /\ typ (tenv e) M T.

Definition typ_impl e M T :=
  fx_equals e M /\ typ (tenv e) M T.

Instance typ_impl_morph e : Proper (eq_trm ==> eq_trm ==> iff) (typ_impl e).

Qed.

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

  Lemma impl_abs : ∀ e s1 U T T' M,
    T <> kind ->
    U <> kind ->
    s1=prop \/ s1=kind ->
    eq_typ (tenv e) T T' ->
    typ_impl e T s1 ->
    typ_impl (push_var e T) M U ->
    typ_impl e (Abs T M) (Prod T' U).

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

  Lemma NATi_fx_sub : ∀ e o O,
    isOrd o ->
    typ_monoval e O (Ordt o) ->
    fx_sub e (NatI O).

  Lemma OSucc_fx_sub : ∀ e O o,
    isOrd o ->
    typ_monoval e O (Ordt o)->
    typ_monoval e (OSucc O) (Ordt (osucc o)).

  Lemma typ_var_mono : ∀ e n t T,
    ords e n = true ->
    nth_error (tenv e) n = value t ->
    T <> kind ->
    t <> kind ->
    sub_typ (tenv e) (lift (S n) t) T ->
    typ_monoval e (Ref n) T.

  Lemma ext_abs : ∀ e U T M,
    T <> kind ->
    U <> kind ->
    typ_mono e T ->
    typ_impl (push_var e T) M U ->
    typ_ext e (Abs T M) T U.


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

Lemma typ_nat_fix'' : ∀ infty e O U M T,
       isOrd infty ->
       T <> kind ->
       sub_typ (tenv e) (Prod (NatI O) (subst_rec O 1 U)) T ->
       typ (tenv e) O (Ordt infty) ->
       typ_mono (push_var (push_ord e (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
       typ_ext (push_fun (push_ord e (OSucct O)) (NatI (Ref 0)) U)
         M (NatI (OSucc (Ref 1)))
           (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
       typ (tenv e) (NatFix O M) T.

  Lemma typ_ext_fix : ∀ eps e O U M,
    isOrd eps ->
    typ_monoval e O (Ordt eps) ->
    typ_ext (push_fun (push_ord e (OSucct O)) (NatI (Ref 0)) U) M
      (NatI (OSucc (Ref 1))) (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    fx_sub (push_var (push_ord e (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
    typ_ext e (NatFix O M) (NatI O) (subst_rec O 1 U).

  Lemma typ_impl_fix : ∀ eps e O U M,
    isOrd eps ->
    typ_impl e O (Ordt eps) ->
    typ_ext (push_fun (push_ord e (OSucct O)) (NatI (Ref 0)) U) M
      (NatI (OSucc (Ref 1))) (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
    fx_sub (push_var (push_ord e (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
    typ_impl e (NatFix O M) (Prod (NatI O) (subst_rec O 1 U)).