Library TypeECC
Require Export ConvECC.
Require Export EnvECC.
Require Import Peano_dec.
Require Import Max.
Section Typage.
Definition ecc_prod s1 s2 s3 :=
match s2, s1, s3 with
prop, _, prop => true
| kind n, prop, kind n' => if eq_nat_dec n n' then true else false
| kind n, kind m, kind n' => if eq_nat_dec (max n m) n' then true else false
| _, _, _ => false
end.
Axiom ecc_prod_fun : forall s1 s2 s3 s1' s2' s3',
ecc_prod s1 s2 s3 = true ->
ecc_prod s1' s2' s3' = true ->
s1 = s1' ->
s2 = s2' ->
s3 = s3'.
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 0))
| type_kind :
forall e n,
wf e ->
typ e (Srt (kind n)) (Srt (kind (S n)))
| 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 s3,
typ e T (Srt s1) ->
typ (T :: e) U (Srt s2) ->
typ (T :: e) M U ->
ecc_prod s1 s2 s3 = true ->
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 s3,
typ e T (Srt s1) ->
typ (T :: e) U (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
typ e (Prod T U) (Srt s3)
| 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_kind 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 0)) -> P
| Srt (kind n) => conv T (Srt (kind (S n))) -> P
| Ref n => forall x, item x e n -> conv T (lift (S n) x) -> P
| Abs A M =>
forall s1 s2 s3 U,
typ e A (Srt s1) ->
typ (A :: e) M U -> typ (A :: e) U (Srt s2) ->
ecc_prod s1 s2 s3 = true -> 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 s3,
typ e A (Srt s1) -> typ (A :: e) B (Srt s2) ->
ecc_prod s1 s2 s3 = true -> conv T (Srt s3) -> 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 n, typ e (Srt (kind n)) T -> conv T (Srt (kind (S n))).
Lemma inv_typ_prop : forall e T, typ e (Srt prop) T -> conv T (Srt (kind 0)).
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 s3 T,
typ e A (Srt s1) ->
typ (A :: e) M T -> typ (A :: e) T (Srt s2) ->
ecc_prod s1 s2 s3 = true -> 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 s3,
typ e T (Srt s1) -> typ (T :: e) U (Srt s2) -> ecc_prod s1 s2 s3 = true ->
conv (Srt s3) s -> P) -> P.
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 type_case : forall e t T, typ e t T -> exists s, typ e T (Srt s).
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.
Theorem typ_unique :
forall e t T, typ e t T -> forall U, typ e t U -> conv 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 EnvECC.
Require Import Peano_dec.
Require Import Max.
Section Typage.
Definition ecc_prod s1 s2 s3 :=
match s2, s1, s3 with
prop, _, prop => true
| kind n, prop, kind n' => if eq_nat_dec n n' then true else false
| kind n, kind m, kind n' => if eq_nat_dec (max n m) n' then true else false
| _, _, _ => false
end.
Axiom ecc_prod_fun : forall s1 s2 s3 s1' s2' s3',
ecc_prod s1 s2 s3 = true ->
ecc_prod s1' s2' s3' = true ->
s1 = s1' ->
s2 = s2' ->
s3 = s3'.
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 0))
| type_kind :
forall e n,
wf e ->
typ e (Srt (kind n)) (Srt (kind (S n)))
| 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 s3,
typ e T (Srt s1) ->
typ (T :: e) U (Srt s2) ->
typ (T :: e) M U ->
ecc_prod s1 s2 s3 = true ->
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 s3,
typ e T (Srt s1) ->
typ (T :: e) U (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
typ e (Prod T U) (Srt s3)
| 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_kind 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 0)) -> P
| Srt (kind n) => conv T (Srt (kind (S n))) -> P
| Ref n => forall x, item x e n -> conv T (lift (S n) x) -> P
| Abs A M =>
forall s1 s2 s3 U,
typ e A (Srt s1) ->
typ (A :: e) M U -> typ (A :: e) U (Srt s2) ->
ecc_prod s1 s2 s3 = true -> 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 s3,
typ e A (Srt s1) -> typ (A :: e) B (Srt s2) ->
ecc_prod s1 s2 s3 = true -> conv T (Srt s3) -> 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 n, typ e (Srt (kind n)) T -> conv T (Srt (kind (S n))).
Lemma inv_typ_prop : forall e T, typ e (Srt prop) T -> conv T (Srt (kind 0)).
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 s3 T,
typ e A (Srt s1) ->
typ (A :: e) M T -> typ (A :: e) T (Srt s2) ->
ecc_prod s1 s2 s3 = true -> 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 s3,
typ e T (Srt s1) -> typ (T :: e) U (Srt s2) -> ecc_prod s1 s2 s3 = true ->
conv (Srt s3) s -> P) -> P.
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 type_case : forall e t T, typ e t T -> exists s, typ e T (Srt s).
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.
Theorem typ_unique :
forall e t T, typ e t T -> forall U, typ e t U -> conv 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.