Library TypeJudgeECC
Require Import TypeECC.
Section Typage.
Inductive eq_typ : env -> term -> term -> term -> Prop :=
| type_prop : forall e,
wf e ->
eq_typ e (Srt prop) (Srt prop) (Srt (kind 0))
| type_kind : forall e n,
wf e ->
eq_typ e (Srt (kind n)) (Srt (kind n)) (Srt (kind(S n)))
| type_var :
forall e v t,
wf e ->
item_lift t e v ->
eq_typ e (Ref v) (Ref v) t
| type_abs :
forall e T T' M M' U U' s1 s2 s3,
eq_typ e T T' (Srt s1) ->
eq_typ (T :: e) U U' (Srt s2) ->
eq_typ (T :: e) M M' U ->
ecc_prod s1 s2 s3 = true ->
eq_typ e (Abs T M) (Abs T' M') (Prod T U)
| type_app :
forall e u u' v v' V V' Ur Ur' s1 s2 s3,
eq_typ e v v' V ->
eq_typ e V V' (Srt s1) ->
eq_typ e u u' (Prod V Ur) ->
eq_typ (V::e) Ur Ur' (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
eq_typ e (App u v) (App u' v') (subst v Ur)
| type_prod :
forall e T T' U U' s1 s2 s3,
eq_typ e T T' (Srt s1) ->
eq_typ (T :: e) U U' (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
eq_typ e (Prod T U) (Prod T' U') (Srt s3)
| type_beta : forall e T T' M M' N N' U U' s1 s2 s3,
eq_typ e N N' T ->
eq_typ e T T' (Srt s1) ->
eq_typ (T::e) M M' U ->
eq_typ (T::e) U U' (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
eq_typ e (App (Abs T M) N) (subst N' M') (subst N U)
| type_red : forall e M M' T T' s,
eq_typ e M M' T ->
eq_typ e T T' (Srt s) ->
eq_typ e M M' T'
| type_exp : forall e M M' T T' s,
eq_typ e M M' T' ->
eq_typ e T T' (Srt s) ->
eq_typ e M M' T
with wf : env -> Prop :=
wf_nil : wf nil
| wf_var : forall e T T' s,
eq_typ e T T' (Srt s) ->
wf (T::e).
Scheme eq_typ_mind := Minimality for eq_typ Sort Prop
with wf_mind := Minimality for wf Sort Prop.
Lemma typ_wf : forall e t t' T, eq_typ e t t' T -> wf e.
Lemma typ_refl : forall e t t' T, eq_typ e t t' T -> eq_typ e t t T.
Lemma typ_thin :
forall g A e t t' T,
wf (A::g) ->
eq_typ e t t' T ->
forall n f,
ins_in_env A n e f ->
trunc n e g ->
eq_typ f (lift_rec 1 t n) (lift_rec 1 t' n) (lift_rec 1 T n).
Lemma typ_thinning :
forall A e t t' T,
wf (A::e) ->
eq_typ e t t' T ->
eq_typ (A::e) (lift 1 t) (lift 1 t') (lift 1 T).
Lemma typ_thinning_n :
forall f t t' T n e,
wf e ->
eq_typ f t t' T ->
trunc n e f ->
eq_typ e (lift n t) (lift n t') (lift n T).
Lemma typ_sub :
forall g d t e u u' U,
eq_typ e u u' U ->
forall d' n f,
eq_typ g d d' t ->
sub_in_env d t n e f ->
trunc n f g ->
wf f ->
eq_typ f (subst_rec d u n) (subst_rec d' u' n) (subst_rec d U n).
Theorem substitution :
forall e t u u' U d d',
eq_typ (t :: (e:env)) u u' U ->
eq_typ e d d' t ->
eq_typ e (subst d u) (subst d' u') (subst d U).
Inductive red1_in_env : env -> env -> Prop :=
| red1_env_hd : forall e t u s, eq_typ e t u (Srt s) ->
red1_in_env (t :: e) (u :: e)
| red1_env_tl :
forall e f t, red1_in_env e f -> red1_in_env (t :: e) (t :: f).
Hint Constructors red1_in_env: coc.
Lemma red_item :
forall n t e f,
item_lift t e n ->
red1_in_env e f ->
wf f ->
item_lift t f n \/
(forall g, trunc (S n) e g -> trunc (S n) f g) /\
(exists2 u, exists s, eq_typ f t u (Srt s) & item_lift u f n).
Lemma typ_red_env :
forall e t t' T, eq_typ e t t' T -> forall f, red1_in_env e f -> wf f ->
eq_typ f t t' T.
Lemma typ_refl2 : forall e M M' T, eq_typ e M M' T -> eq_typ e M' M' T.
Lemma wf_sort_lift :
forall n e t, wf e -> item_lift t e n ->
exists s, eq_typ e t t (Srt s).
Theorem type_case :
forall e t t' T, eq_typ e t t' T ->
exists s, eq_typ e T T (Srt s).
Require Import Relation_Operators.
Definition eq_typ_eq e :=
clos_refl_sym_trans _ (fun x y => exists s, eq_typ e x y (Srt s)).
Hint Unfold eq_typ_eq : coc.
Lemma eq_typ_eq_red : forall e T T' s,
eq_typ e T T' (Srt s) -> eq_typ_eq e T T'.
Lemma eq_typ_eq_exp : forall e T T' s,
eq_typ e T T' (Srt s) -> eq_typ_eq e T' T.
Lemma type_conv_gen : forall e M M' T T',
eq_typ_eq e T T' ->
(eq_typ e M M' T -> eq_typ e M M' T') /\
(eq_typ e M M' T' -> eq_typ e M M' T).
Lemma type_conv : forall e M M' T T',
eq_typ e M M' T -> eq_typ_eq e T T' -> eq_typ e M M' T'.
Definition inv_type (P : Prop) e t t' T :=
match t with
| Srt prop => eq_typ_eq e (Srt (kind 0)) T -> t' = Srt prop -> P
| Srt (kind n) => eq_typ_eq e (Srt (kind (S n))) T -> t' = Srt (kind n) -> P
| Ref n =>
forall x, item_lift x e n -> eq_typ_eq e x T -> t' = Ref n -> P
| Abs A M =>
forall s1 s2 s3 A' M' U U',
eq_typ e A A' (Srt s1) ->
eq_typ (A :: e) M M' U ->
eq_typ (A :: e) U U' (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
eq_typ_eq e (Prod A U) T -> t' = Abs A' M' -> P
| App u v =>
forall u' v' Ur Ur' V V' s1 s2 s3,
eq_typ e v v' V ->
eq_typ e V V' (Srt s1) ->
eq_typ e u u' (Prod V Ur) ->
eq_typ (V::e) Ur Ur' (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
t' = App u' v' \/
(exists2 M, u=Abs V M &
exists2 M', eq_typ (V::e) M M' Ur & t' = subst v' M') ->
eq_typ_eq e (subst v Ur) T -> P
| Prod A B =>
forall A' B' s1 s2 s3,
eq_typ e A A' (Srt s1) ->
eq_typ (A :: e) B B' (Srt s2) ->
ecc_prod s1 s2 s3 = true ->
eq_typ_eq e (Srt s3) T -> t' = Prod A' B' -> P
end.
Lemma inv_type_conv :
forall P e t t' U V, eq_typ_eq e U V ->
inv_type P e t t' V -> inv_type P e t t' U.
Theorem typ_inversion :
forall P e t t' T, eq_typ e t t' T -> inv_type P e t t' T -> P.
End Typage.