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