Library Types

Require Export Conv.
Require Export Env.

Section Typage.

  Inductive wf : env -> Prop :=
    | wf_nil : wf nil
    | wf_var : forall e T s, typ e T (Srt s) -> wf (T :: e)
  with typ : env -> term -> term -> Prop :=
    | type_prop :
        forall e,
        wf e ->
        typ e (Srt prop) (Srt kind)
    | type_var :
        forall e v t,
        wf e ->
        item_lift t e v ->
        typ e (Ref v) t
    | type_abs :
        forall e T M U s1 s2,
        typ e T (Srt s1) ->
        typ (T :: e) U (Srt s2) ->
        typ (T :: e) M U ->
        typ e (Abs T M) (Prod T U)
    | type_app :
        forall e u v V Ur,
        typ e v V ->
        typ e u (Prod V Ur) ->
        typ e (App u v) (subst v Ur)
    | type_prod :
        forall e T U s1 s2,
        typ e T (Srt s1) ->
        typ (T :: e) U (Srt s2) ->
        typ e (Prod T U) (Srt s2)
    | type_conv :
        forall e t U V s,
        typ e t U ->
        conv U V ->
        typ e V (Srt s) ->
        typ e t V.

  Hint Resolve wf_nil type_prop type_var: coc.

Scheme typ_mind := Minimality for typ Sort Prop
  with wf_mind := Minimality for wf Sort Prop.

  Lemma typ_wf : forall e t T, typ e t T -> wf e.

  Hint Resolve typ_wf: coc.

  Lemma wf_sort :
   forall n e f t,
   trunc (S n) e f -> wf e -> item t e n -> exists s, typ f t (Srt s).

  Definition inv_type (P : Prop) e t T :=
    match t with
    | Srt prop => conv T (Srt kind) -> P
    | Srt kind => True
    | Ref n => forall x, item x e n -> conv T (lift (S n) x) -> P
    | Abs A M =>
        forall s1 s2 U,
        typ e A (Srt s1) ->
        typ (A :: e) M U -> typ (A :: e) U (Srt s2) -> conv T (Prod A U) -> P
    | App u v =>
        forall Ur V,
        typ e v V -> typ e u (Prod V Ur) -> conv T (subst v Ur) -> P
    | Prod A B =>
        forall s1 s2,
        typ e A (Srt s1) -> typ (A :: e) B (Srt s2) -> conv T (Srt s2) -> P
    end.

  Lemma inv_type_conv :
   forall P e t U V, conv U V -> inv_type P e t U -> inv_type P e t V.

  Theorem typ_inversion : forall P e t T, typ e t T -> inv_type P e t T -> P.

  Lemma inv_typ_kind : forall e t, ~ typ e (Srt kind) t.

  Lemma inv_typ_prop : forall e T, typ e (Srt prop) T -> conv T (Srt kind).

  Lemma inv_typ_ref :
   forall (P : Prop) e T n,
   typ e (Ref n) T ->
   (forall U : term, item U e n -> conv T (lift (S n) U) -> P) -> P.

  Lemma inv_typ_abs :
   forall (P : Prop) e A M U,
   typ e (Abs A M) U ->
   (forall s1 s2 T,
    typ e A (Srt s1) ->
    typ (A :: e) M T -> typ (A :: e) T (Srt s2) -> conv (Prod A T) U -> P) ->
   P.

  Lemma inv_typ_app :
   forall (P : Prop) e u v T,
   typ e (App u v) T ->
   (forall V Ur, typ e u (Prod V Ur) -> typ e v V -> conv T (subst v Ur) -> P) ->
   P.

  Lemma inv_typ_prod :
   forall (P : Prop) e T U s,
   typ e (Prod T U) s ->
   (forall s1 s2,
    typ e T (Srt s1) -> typ (T :: e) U (Srt s2) -> conv (Srt s2) s -> P) -> P.

  Lemma typ_mem_kind : forall e t T, mem_sort kind t -> ~ typ e t T.

  Lemma inv_typ_conv_kind : forall e t T, conv t (Srt kind) -> ~ typ e t T.

  Lemma typ_weak_weak :
   forall A e t T,
   typ e t T ->
   forall n f,
   ins_in_env A n e f -> wf f -> typ f (lift_rec 1 t n) (lift_rec 1 T n).

  Theorem thinning :
   forall e t T A,
   typ e t T -> wf (A :: e) -> typ (A :: e) (lift 1 t) (lift 1 T).

  Lemma thinning_n :
   forall n e f t T,
   trunc n (e:env) (f:env) ->
   typ f t T -> wf e -> typ e (lift n t) (lift n T).

  Lemma wf_sort_lift :
   forall n e t, wf e -> item_lift t e n -> exists s, typ e t (Srt s).

  Lemma typ_sub_weak :
   forall g d t e u U,
   typ g d t ->
   typ e u U ->
   forall f n,
   sub_in_env d t n e f ->
   wf f -> trunc n f g -> typ f (subst_rec d u n) (subst_rec d U n).

  Theorem substitution :
   forall e t u U d,
   typ (t :: (e:env)) u U -> typ e d t -> typ e (subst d u) (subst d U).

  Theorem typ_unique :
   forall e t T, typ e t T -> forall U, typ e t U -> conv T U.

  Theorem type_case :
   forall e t T, typ e t T -> (exists s, typ e T (Srt s)) \/ T = Srt kind.

  Lemma type_kind_not_conv :
   forall e t T, typ e t T -> typ e t (Srt kind) -> T = Srt kind.

  Lemma typ_red_env :
   forall e t T, typ e t T ->
   forall f, red1_in_env red1 e f -> wf f -> typ f t T.

  Lemma subj_red : forall e t T, typ e t T -> forall u, red1 t u -> typ u T.

  Theorem subject_reduction :
   forall e t u, red t u -> forall T, typ e t T -> typ e u T.

  Lemma type_reduction : forall e t T U, red T U -> typ e t T -> typ e t U.

  Lemma typ_conv_conv :
   forall e u U v V, typ e u U -> typ e v V -> conv u v -> conv U V.

End Typage.