Library Types
Require Export Conv.
Require Export Env.
Section Typage.
Inductive wf : env -> Prop :=
| wf_nil : wf nil
| wf_var : ∀ e T s, typ e T (Srt s) -> wf (T :: e)
with typ : env -> term -> term -> Prop :=
| type_prop :
∀ e,
wf e ->
typ e (Srt prop) (Srt kind)
| type_var :
∀ e v t,
wf e ->
item_lift t e v ->
typ e (Ref v) t
| type_abs :
∀ 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 :
∀ 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 :
∀ 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 :
∀ 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 : ∀ e t T, typ e t T -> wf e.
simple induction 1; auto with coc.
Qed.
Hint Resolve typ_wf: coc.
Lemma wf_sort :
∀ n e f t,
trunc (S n) e f -> wf e -> item t e n -> exists s, typ f t (Srt s).
simple induction n.
do 4 intro.
inversion_clear H.
inversion_clear H0.
intros.
inversion_clear H0.
inversion_clear H.
eauto with coc.
do 6 intro.
inversion_clear H0.
intros.
inversion_clear H2.
inversion_clear H0.
elim H with e0 f t; intros; eauto with coc.
Qed.
Definition inv_type (P : Prop) e t T :=
match t with
| Srt prop => conv T (Srt kind) -> P
| Srt kind => True
| Ref n => ∀ x, item x e n -> conv T (lift (S n) x) -> P
| Abs A M =>
∀ 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 =>
∀ Ur V,
typ e v V -> typ e u (Prod V Ur) -> conv T (subst v Ur) -> P
| Prod A B =>
∀ s1 s2,
typ e A (Srt s1) -> typ (A :: e) B (Srt s2) -> conv T (Srt s2) -> P
end.
Lemma inv_type_conv :
∀ P e t U V, conv U V -> inv_type P e t U -> inv_type P e t V.
do 6 intro.
cut (∀ x : term, conv V x -> conv U x).
intro.
case t; simpl in |- *; intros.
generalize H1.
elim s; auto with coc; intros.
apply H1 with x; auto with coc.
apply H1 with s1 s2 U0; auto with coc.
apply H1 with Ur V0; auto with coc.
apply H1 with s1 s2; auto with coc.
intros.
apply trans_conv_conv with V; auto with coc.
Qed.
Theorem typ_inversion : ∀ P e t T, typ e t T -> inv_type P e t T -> P.
simple induction 1; simpl in |- *; intros.
auto with coc.
elim H1; intros.
apply H2 with x; auto with coc.
rewrite H3; auto with coc.
apply H6 with s1 s2 U; auto with coc.
apply H4 with Ur V; auto with coc.
apply H4 with s1 s2; auto with coc.
apply H1.
apply inv_type_conv with V; auto with coc.
Qed.
Lemma inv_typ_kind : ∀ e t, ~ typ e (Srt kind) t.
red in |- *; intros.
apply typ_inversion with e (Srt kind) t; simpl in |- *; auto with coc.
Qed.
Lemma inv_typ_prop : ∀ e T, typ e (Srt prop) T -> conv T (Srt kind).
intros.
apply typ_inversion with e (Srt prop) T; simpl in |- *; auto with coc.
Qed.
Lemma inv_typ_ref :
∀ (P : Prop) e T n,
typ e (Ref n) T ->
(∀ U : term, item U e n -> conv T (lift (S n) U) -> P) -> P.
intros.
apply typ_inversion with e (Ref n) T; simpl in |- *; intros; auto with coc.
apply H0 with x; auto with coc.
Qed.
Lemma inv_typ_abs :
∀ (P : Prop) e A M U,
typ e (Abs A M) U ->
(∀ 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.
intros.
apply typ_inversion with e (Abs A M) U; simpl in |- *; auto with coc; intros.
apply H0 with s1 s2 U0; auto with coc.
Qed.
Lemma inv_typ_app :
∀ (P : Prop) e u v T,
typ e (App u v) T ->
(∀ V Ur, typ e u (Prod V Ur) -> typ e v V -> conv T (subst v Ur) -> P) ->
P.
intros.
apply typ_inversion with e (App u v) T; simpl in |- *; auto with coc; intros.
apply H0 with V Ur; auto with coc.
Qed.
Lemma inv_typ_prod :
∀ (P : Prop) e T U s,
typ e (Prod T U) s ->
(∀ s1 s2,
typ e T (Srt s1) -> typ (T :: e) U (Srt s2) -> conv (Srt s2) s -> P) -> P.
intros.
apply typ_inversion with e (Prod T U) s; simpl in |- *; auto with coc; intros.
apply H0 with s1 s2; auto with coc.
Qed.
Lemma typ_mem_kind : ∀ e t T, mem_sort kind t -> ~ typ e t T.
red in |- *; intros.
apply typ_inversion with e t T; auto with coc.
generalize e T.
clear H0.
elim H; simpl in |- *; auto with coc; intros.
apply typ_inversion with e0 u (Srt s1); auto with coc.
apply typ_inversion with (u :: e0) v (Srt s2); auto with coc.
apply typ_inversion with e0 u (Srt s1); auto with coc.
apply typ_inversion with (u :: e0) v U; auto with coc.
apply typ_inversion with e0 u (Prod V Ur); auto with coc.
apply typ_inversion with e0 v V; auto with coc.
Qed.
Lemma inv_typ_conv_kind : ∀ e t T, conv t (Srt kind) -> ~ typ e t T.
intros.
apply typ_mem_kind.
apply red_sort_mem.
elim church_rosser with t (Srt kind); intros; auto with coc.
rewrite (red_normal (Srt kind) x); auto with coc.
red in |- *; red in |- *; intros.
inversion_clear H2.
Qed.
Lemma typ_weak_weak :
∀ A e t T,
typ e t T ->
∀ n f,
ins_in_env A n e f -> wf f -> typ f (lift_rec 1 t n) (lift_rec 1 T n).
simple induction 1; simpl in |- *; intros; auto with coc.
elim (le_gt_dec n v); intros; apply type_var; auto with coc.
apply ins_item_lift_ge with A e0; auto with coc.
apply ins_item_lift_lt with A e0; auto with coc.
cut (wf (lift_rec 1 T0 n :: f)).
intro.
apply type_abs with s1 s2; auto with coc.
apply wf_var with s1; auto with coc.
rewrite distr_lift_subst.
apply type_app with (lift_rec 1 V n); auto with coc.
cut (wf (lift_rec 1 T0 n :: f)).
intro.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_conv with (lift_rec 1 U n) s; auto with coc.
Qed.
Theorem thinning :
∀ e t T A,
typ e t T -> wf (A :: e) -> typ (A :: e) (lift 1 t) (lift 1 T).
unfold lift in |- *.
intros.
inversion_clear H0.
apply typ_weak_weak with A e; auto with coc.
apply wf_var with s; auto with coc.
Qed.
Lemma thinning_n :
∀ 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).
simple induction 1.
intros.
rewrite lift0.
rewrite lift0.
trivial.
intros.
rewrite simpl_lift; auto with coc.
pattern (lift (S k) T) in |- *.
rewrite simpl_lift; auto with coc.
apply thinning; auto with coc.
apply H1; trivial.
inversion_clear H3.
eauto with coc.
Qed.
Lemma wf_sort_lift :
∀ n e t, wf e -> item_lift t e n -> exists s, typ e t (Srt s).
simple induction n.
simple destruct e; intros.
elim H0; intros.
inversion_clear H2.
elim H0; intros.
rewrite H1.
inversion_clear H2.
inversion_clear H.
exists s.
replace (Srt s) with (lift 1 (Srt s)); auto with coc.
apply thinning; auto with coc.
apply wf_var with s; auto with coc.
intros.
elim H1; intros.
rewrite H2.
generalize H0.
inversion_clear H3; intros.
rewrite simpl_lift; auto with coc.
cut (wf l); intros.
elim H with l (lift (S n0) x); intros; auto with coc.
inversion_clear H3.
exists x0.
change (typ (y :: l) (lift 1 (lift (S n0) x)) (lift 1 (Srt x0))) in |- *.
apply thinning; auto with coc.
apply wf_var with s; auto with coc.
exists x; auto with coc.
inversion_clear H3.
eauto with coc.
Qed.
Lemma typ_sub_weak :
∀ g d t e u U,
typ g d t ->
typ e u U ->
∀ 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).
Proof.
simple induction 2; simpl in |- *; intros; auto with coc.
destruct (lt_eq_lt_dec n v) as [[fvar|eq_var]|bvar].
constructor; trivial.
apply sub_item_lift_sup with (1 := H3) (2 := fvar) (3 := H2).
subst v; rewrite sub_item_lift_eq with (1 := H3) (2 := H2).
apply thinning_n with g; auto with coc.
constructor; trivial.
apply nth_sub_inf with (1 := H3); trivial.
cut (wf (subst_rec d T n :: f)); intros.
apply type_abs with s1 s2; auto with coc.
apply wf_var with s1; auto with coc.
rewrite distr_subst.
apply type_app with (subst_rec d V n); auto with coc.
cut (wf (subst_rec d T n :: f)); intros.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_conv with (subst_rec d U0 n) s; auto with coc.
Qed.
Theorem substitution :
∀ e t u U d,
typ (t :: (e:env)) u U -> typ e d t -> typ e (subst d u) (subst d U).
intros.
unfold subst in |- *.
apply typ_sub_weak with e t (t :: e); auto with coc.
apply typ_wf with d t; auto with coc.
Qed.
Theorem typ_unique :
∀ e t T, typ e t T -> ∀ U, typ e t U -> conv T U.
simple induction 1; intros.
apply sym_conv.
apply inv_typ_prop with e0; auto with coc.
apply inv_typ_ref with e0 U v; auto with coc; intros.
elim H1; intros.
rewrite H5.
elim fun_item with (1 := H3) (2 := H6); auto with coc.
apply inv_typ_abs with (1 := H6); intros.
apply trans_conv_conv with (Prod T0 T1); auto with coc.
apply inv_typ_app with (1 := H4); intros.
apply trans_conv_conv with (subst v Ur0); auto with coc.
unfold subst in |- *; apply conv_conv_subst; auto with coc.
apply inv_conv_prod_r with (1 := H3 _ H5).
apply inv_typ_prod with (1 := H4); intros.
apply trans_conv_conv with (Srt s3); auto with coc.
apply trans_conv_conv with U; auto with coc.
Qed.
Theorem type_case :
∀ e t T, typ e t T -> (exists s, typ e T (Srt s)) \/ T = Srt kind.
simple induction 1; intros; auto with coc.
left.
elim wf_sort_lift with (2 := H1); trivial; intros.
exists x; auto with coc.
left.
exists s2.
apply type_prod with s1; auto with coc.
left.
elim H3; intros.
elim H4; intros.
apply inv_typ_prod with (1 := H5); intros.
exists s2.
replace (Srt s2) with (subst v (Srt s2)); auto with coc.
apply substitution with V; auto with coc.
discriminate H4.
case s2; auto with coc.
left.
exists kind.
apply type_prop.
apply typ_wf with (1 := H0).
left.
exists s; auto with coc.
Qed.
Lemma type_kind_not_conv :
∀ e t T, typ e t T -> typ e t (Srt kind) -> T = Srt kind.
intros.
elim type_case with e t T; intros; auto with coc.
elim H1; intros.
elim inv_typ_conv_kind with e T (Srt x); auto with coc.
apply typ_unique with e t; trivial.
Qed.
Lemma typ_red_env :
∀ e t T, typ e t T ->
∀ f, red1_in_env red1 e f -> wf f -> typ f t T.
simple induction 1; intros.
auto with coc.
elim red_item with (2 := H1) (3 := H2); auto with coc; intros.
inversion_clear H4.
inversion_clear H6.
elim H1; intros.
elim item_trunc with (1 := H8); intros.
elim wf_sort with (1 := H9) (3 := H8); eauto; intros.
apply type_conv with x x2; auto with coc.
rewrite H6.
replace (Srt x2) with (lift (S v) (Srt x2)); auto with coc.
apply thinning_n with x1; auto with coc.
cut (wf (T0 :: f)); intros.
apply type_abs with s1 s2; auto with coc.
apply wf_var with s1; auto with coc.
apply type_app with V; auto with coc.
cut (wf (T0 :: f)); intros.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_conv with U s; auto with coc.
Qed.
Lemma subj_red : ∀ e t T, typ e t T -> ∀ u, red1 t u -> typ e u T.
simple induction 1; intros.
inversion_clear H1.
inversion_clear H2.
inversion_clear H6.
cut (wf (M' :: e0)); intros.
apply type_conv with (Prod M' U) s2; auto with coc.
apply type_abs with s1 s2; auto with coc.
apply typ_red_env with (T0 :: e0); auto with coc.
apply typ_red_env with (T0 :: e0); auto with coc.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_abs with s1 s2; auto with coc.
elim type_case with (1 := H2); intros.
inversion_clear H5.
apply inv_typ_prod with (1 := H6); intros.
generalize H2 H3; clear H2 H3.
inversion_clear H4; intros.
apply inv_typ_abs with (1 := H2); intros.
apply type_conv with (subst v T1) s2; auto with coc.
apply substitution with T0; auto with coc.
apply type_conv with V s0; auto with coc.
apply sym_conv.
apply inv_conv_prod_l with (1 := H11).
unfold subst in |- *.
apply conv_conv_subst; auto with coc.
apply inv_conv_prod_r with (1 := H11); auto with coc.
replace (Srt s2) with (subst v (Srt s2)); auto with coc.
apply substitution with V; auto with coc.
apply type_app with V; auto with coc.
apply type_conv with (subst N2 Ur) s2; auto with coc.
apply type_app with V; auto with coc.
unfold subst in |- *.
apply conv_conv_subst; auto with coc.
replace (Srt s2) with (subst v (Srt s2)); auto with coc.
apply substitution with V; auto with coc.
discriminate H5.
inversion_clear H4.
apply type_prod with s1; auto with coc.
apply typ_red_env with (T0 :: e0); auto with coc.
apply wf_var with s1; auto with coc.
apply type_prod with s1; auto with coc.
apply type_conv with U s; auto with coc.
Qed.
Theorem subject_reduction :
∀ e t u, red t u -> ∀ T, typ e t T -> typ e u T.
simple induction 1; intros; auto with coc.
apply subj_red with P; intros; auto with coc.
Qed.
Lemma type_reduction : ∀ e t T U, red T U -> typ e t T -> typ e t U.
intros.
elim type_case with (1 := H0); intros.
inversion_clear H1.
apply type_conv with T x; auto with coc.
apply subject_reduction with T; trivial.
elim red_normal with (1 := H); trivial.
rewrite H1.
red in |- *; red in |- *; intros.
inversion_clear H2.
Qed.
Lemma typ_conv_conv :
∀ e u U v V, typ e u U -> typ e v V -> conv u v -> conv U V.
intros.
elim church_rosser with (1 := H1); auto with coc; intros.
apply typ_unique with e x.
apply subject_reduction with u; trivial.
apply subject_reduction with v; trivial.
Qed.
End Typage.
Require Export Env.
Section Typage.
Inductive wf : env -> Prop :=
| wf_nil : wf nil
| wf_var : ∀ e T s, typ e T (Srt s) -> wf (T :: e)
with typ : env -> term -> term -> Prop :=
| type_prop :
∀ e,
wf e ->
typ e (Srt prop) (Srt kind)
| type_var :
∀ e v t,
wf e ->
item_lift t e v ->
typ e (Ref v) t
| type_abs :
∀ 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 :
∀ 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 :
∀ 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 :
∀ 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 : ∀ e t T, typ e t T -> wf e.
simple induction 1; auto with coc.
Qed.
Hint Resolve typ_wf: coc.
Lemma wf_sort :
∀ n e f t,
trunc (S n) e f -> wf e -> item t e n -> exists s, typ f t (Srt s).
simple induction n.
do 4 intro.
inversion_clear H.
inversion_clear H0.
intros.
inversion_clear H0.
inversion_clear H.
eauto with coc.
do 6 intro.
inversion_clear H0.
intros.
inversion_clear H2.
inversion_clear H0.
elim H with e0 f t; intros; eauto with coc.
Qed.
Definition inv_type (P : Prop) e t T :=
match t with
| Srt prop => conv T (Srt kind) -> P
| Srt kind => True
| Ref n => ∀ x, item x e n -> conv T (lift (S n) x) -> P
| Abs A M =>
∀ 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 =>
∀ Ur V,
typ e v V -> typ e u (Prod V Ur) -> conv T (subst v Ur) -> P
| Prod A B =>
∀ s1 s2,
typ e A (Srt s1) -> typ (A :: e) B (Srt s2) -> conv T (Srt s2) -> P
end.
Lemma inv_type_conv :
∀ P e t U V, conv U V -> inv_type P e t U -> inv_type P e t V.
do 6 intro.
cut (∀ x : term, conv V x -> conv U x).
intro.
case t; simpl in |- *; intros.
generalize H1.
elim s; auto with coc; intros.
apply H1 with x; auto with coc.
apply H1 with s1 s2 U0; auto with coc.
apply H1 with Ur V0; auto with coc.
apply H1 with s1 s2; auto with coc.
intros.
apply trans_conv_conv with V; auto with coc.
Qed.
Theorem typ_inversion : ∀ P e t T, typ e t T -> inv_type P e t T -> P.
simple induction 1; simpl in |- *; intros.
auto with coc.
elim H1; intros.
apply H2 with x; auto with coc.
rewrite H3; auto with coc.
apply H6 with s1 s2 U; auto with coc.
apply H4 with Ur V; auto with coc.
apply H4 with s1 s2; auto with coc.
apply H1.
apply inv_type_conv with V; auto with coc.
Qed.
Lemma inv_typ_kind : ∀ e t, ~ typ e (Srt kind) t.
red in |- *; intros.
apply typ_inversion with e (Srt kind) t; simpl in |- *; auto with coc.
Qed.
Lemma inv_typ_prop : ∀ e T, typ e (Srt prop) T -> conv T (Srt kind).
intros.
apply typ_inversion with e (Srt prop) T; simpl in |- *; auto with coc.
Qed.
Lemma inv_typ_ref :
∀ (P : Prop) e T n,
typ e (Ref n) T ->
(∀ U : term, item U e n -> conv T (lift (S n) U) -> P) -> P.
intros.
apply typ_inversion with e (Ref n) T; simpl in |- *; intros; auto with coc.
apply H0 with x; auto with coc.
Qed.
Lemma inv_typ_abs :
∀ (P : Prop) e A M U,
typ e (Abs A M) U ->
(∀ 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.
intros.
apply typ_inversion with e (Abs A M) U; simpl in |- *; auto with coc; intros.
apply H0 with s1 s2 U0; auto with coc.
Qed.
Lemma inv_typ_app :
∀ (P : Prop) e u v T,
typ e (App u v) T ->
(∀ V Ur, typ e u (Prod V Ur) -> typ e v V -> conv T (subst v Ur) -> P) ->
P.
intros.
apply typ_inversion with e (App u v) T; simpl in |- *; auto with coc; intros.
apply H0 with V Ur; auto with coc.
Qed.
Lemma inv_typ_prod :
∀ (P : Prop) e T U s,
typ e (Prod T U) s ->
(∀ s1 s2,
typ e T (Srt s1) -> typ (T :: e) U (Srt s2) -> conv (Srt s2) s -> P) -> P.
intros.
apply typ_inversion with e (Prod T U) s; simpl in |- *; auto with coc; intros.
apply H0 with s1 s2; auto with coc.
Qed.
Lemma typ_mem_kind : ∀ e t T, mem_sort kind t -> ~ typ e t T.
red in |- *; intros.
apply typ_inversion with e t T; auto with coc.
generalize e T.
clear H0.
elim H; simpl in |- *; auto with coc; intros.
apply typ_inversion with e0 u (Srt s1); auto with coc.
apply typ_inversion with (u :: e0) v (Srt s2); auto with coc.
apply typ_inversion with e0 u (Srt s1); auto with coc.
apply typ_inversion with (u :: e0) v U; auto with coc.
apply typ_inversion with e0 u (Prod V Ur); auto with coc.
apply typ_inversion with e0 v V; auto with coc.
Qed.
Lemma inv_typ_conv_kind : ∀ e t T, conv t (Srt kind) -> ~ typ e t T.
intros.
apply typ_mem_kind.
apply red_sort_mem.
elim church_rosser with t (Srt kind); intros; auto with coc.
rewrite (red_normal (Srt kind) x); auto with coc.
red in |- *; red in |- *; intros.
inversion_clear H2.
Qed.
Lemma typ_weak_weak :
∀ A e t T,
typ e t T ->
∀ n f,
ins_in_env A n e f -> wf f -> typ f (lift_rec 1 t n) (lift_rec 1 T n).
simple induction 1; simpl in |- *; intros; auto with coc.
elim (le_gt_dec n v); intros; apply type_var; auto with coc.
apply ins_item_lift_ge with A e0; auto with coc.
apply ins_item_lift_lt with A e0; auto with coc.
cut (wf (lift_rec 1 T0 n :: f)).
intro.
apply type_abs with s1 s2; auto with coc.
apply wf_var with s1; auto with coc.
rewrite distr_lift_subst.
apply type_app with (lift_rec 1 V n); auto with coc.
cut (wf (lift_rec 1 T0 n :: f)).
intro.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_conv with (lift_rec 1 U n) s; auto with coc.
Qed.
Theorem thinning :
∀ e t T A,
typ e t T -> wf (A :: e) -> typ (A :: e) (lift 1 t) (lift 1 T).
unfold lift in |- *.
intros.
inversion_clear H0.
apply typ_weak_weak with A e; auto with coc.
apply wf_var with s; auto with coc.
Qed.
Lemma thinning_n :
∀ 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).
simple induction 1.
intros.
rewrite lift0.
rewrite lift0.
trivial.
intros.
rewrite simpl_lift; auto with coc.
pattern (lift (S k) T) in |- *.
rewrite simpl_lift; auto with coc.
apply thinning; auto with coc.
apply H1; trivial.
inversion_clear H3.
eauto with coc.
Qed.
Lemma wf_sort_lift :
∀ n e t, wf e -> item_lift t e n -> exists s, typ e t (Srt s).
simple induction n.
simple destruct e; intros.
elim H0; intros.
inversion_clear H2.
elim H0; intros.
rewrite H1.
inversion_clear H2.
inversion_clear H.
exists s.
replace (Srt s) with (lift 1 (Srt s)); auto with coc.
apply thinning; auto with coc.
apply wf_var with s; auto with coc.
intros.
elim H1; intros.
rewrite H2.
generalize H0.
inversion_clear H3; intros.
rewrite simpl_lift; auto with coc.
cut (wf l); intros.
elim H with l (lift (S n0) x); intros; auto with coc.
inversion_clear H3.
exists x0.
change (typ (y :: l) (lift 1 (lift (S n0) x)) (lift 1 (Srt x0))) in |- *.
apply thinning; auto with coc.
apply wf_var with s; auto with coc.
exists x; auto with coc.
inversion_clear H3.
eauto with coc.
Qed.
Lemma typ_sub_weak :
∀ g d t e u U,
typ g d t ->
typ e u U ->
∀ 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).
Proof.
simple induction 2; simpl in |- *; intros; auto with coc.
destruct (lt_eq_lt_dec n v) as [[fvar|eq_var]|bvar].
constructor; trivial.
apply sub_item_lift_sup with (1 := H3) (2 := fvar) (3 := H2).
subst v; rewrite sub_item_lift_eq with (1 := H3) (2 := H2).
apply thinning_n with g; auto with coc.
constructor; trivial.
apply nth_sub_inf with (1 := H3); trivial.
cut (wf (subst_rec d T n :: f)); intros.
apply type_abs with s1 s2; auto with coc.
apply wf_var with s1; auto with coc.
rewrite distr_subst.
apply type_app with (subst_rec d V n); auto with coc.
cut (wf (subst_rec d T n :: f)); intros.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_conv with (subst_rec d U0 n) s; auto with coc.
Qed.
Theorem substitution :
∀ e t u U d,
typ (t :: (e:env)) u U -> typ e d t -> typ e (subst d u) (subst d U).
intros.
unfold subst in |- *.
apply typ_sub_weak with e t (t :: e); auto with coc.
apply typ_wf with d t; auto with coc.
Qed.
Theorem typ_unique :
∀ e t T, typ e t T -> ∀ U, typ e t U -> conv T U.
simple induction 1; intros.
apply sym_conv.
apply inv_typ_prop with e0; auto with coc.
apply inv_typ_ref with e0 U v; auto with coc; intros.
elim H1; intros.
rewrite H5.
elim fun_item with (1 := H3) (2 := H6); auto with coc.
apply inv_typ_abs with (1 := H6); intros.
apply trans_conv_conv with (Prod T0 T1); auto with coc.
apply inv_typ_app with (1 := H4); intros.
apply trans_conv_conv with (subst v Ur0); auto with coc.
unfold subst in |- *; apply conv_conv_subst; auto with coc.
apply inv_conv_prod_r with (1 := H3 _ H5).
apply inv_typ_prod with (1 := H4); intros.
apply trans_conv_conv with (Srt s3); auto with coc.
apply trans_conv_conv with U; auto with coc.
Qed.
Theorem type_case :
∀ e t T, typ e t T -> (exists s, typ e T (Srt s)) \/ T = Srt kind.
simple induction 1; intros; auto with coc.
left.
elim wf_sort_lift with (2 := H1); trivial; intros.
exists x; auto with coc.
left.
exists s2.
apply type_prod with s1; auto with coc.
left.
elim H3; intros.
elim H4; intros.
apply inv_typ_prod with (1 := H5); intros.
exists s2.
replace (Srt s2) with (subst v (Srt s2)); auto with coc.
apply substitution with V; auto with coc.
discriminate H4.
case s2; auto with coc.
left.
exists kind.
apply type_prop.
apply typ_wf with (1 := H0).
left.
exists s; auto with coc.
Qed.
Lemma type_kind_not_conv :
∀ e t T, typ e t T -> typ e t (Srt kind) -> T = Srt kind.
intros.
elim type_case with e t T; intros; auto with coc.
elim H1; intros.
elim inv_typ_conv_kind with e T (Srt x); auto with coc.
apply typ_unique with e t; trivial.
Qed.
Lemma typ_red_env :
∀ e t T, typ e t T ->
∀ f, red1_in_env red1 e f -> wf f -> typ f t T.
simple induction 1; intros.
auto with coc.
elim red_item with (2 := H1) (3 := H2); auto with coc; intros.
inversion_clear H4.
inversion_clear H6.
elim H1; intros.
elim item_trunc with (1 := H8); intros.
elim wf_sort with (1 := H9) (3 := H8); eauto; intros.
apply type_conv with x x2; auto with coc.
rewrite H6.
replace (Srt x2) with (lift (S v) (Srt x2)); auto with coc.
apply thinning_n with x1; auto with coc.
cut (wf (T0 :: f)); intros.
apply type_abs with s1 s2; auto with coc.
apply wf_var with s1; auto with coc.
apply type_app with V; auto with coc.
cut (wf (T0 :: f)); intros.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_conv with U s; auto with coc.
Qed.
Lemma subj_red : ∀ e t T, typ e t T -> ∀ u, red1 t u -> typ e u T.
simple induction 1; intros.
inversion_clear H1.
inversion_clear H2.
inversion_clear H6.
cut (wf (M' :: e0)); intros.
apply type_conv with (Prod M' U) s2; auto with coc.
apply type_abs with s1 s2; auto with coc.
apply typ_red_env with (T0 :: e0); auto with coc.
apply typ_red_env with (T0 :: e0); auto with coc.
apply type_prod with s1; auto with coc.
apply wf_var with s1; auto with coc.
apply type_abs with s1 s2; auto with coc.
elim type_case with (1 := H2); intros.
inversion_clear H5.
apply inv_typ_prod with (1 := H6); intros.
generalize H2 H3; clear H2 H3.
inversion_clear H4; intros.
apply inv_typ_abs with (1 := H2); intros.
apply type_conv with (subst v T1) s2; auto with coc.
apply substitution with T0; auto with coc.
apply type_conv with V s0; auto with coc.
apply sym_conv.
apply inv_conv_prod_l with (1 := H11).
unfold subst in |- *.
apply conv_conv_subst; auto with coc.
apply inv_conv_prod_r with (1 := H11); auto with coc.
replace (Srt s2) with (subst v (Srt s2)); auto with coc.
apply substitution with V; auto with coc.
apply type_app with V; auto with coc.
apply type_conv with (subst N2 Ur) s2; auto with coc.
apply type_app with V; auto with coc.
unfold subst in |- *.
apply conv_conv_subst; auto with coc.
replace (Srt s2) with (subst v (Srt s2)); auto with coc.
apply substitution with V; auto with coc.
discriminate H5.
inversion_clear H4.
apply type_prod with s1; auto with coc.
apply typ_red_env with (T0 :: e0); auto with coc.
apply wf_var with s1; auto with coc.
apply type_prod with s1; auto with coc.
apply type_conv with U s; auto with coc.
Qed.
Theorem subject_reduction :
∀ e t u, red t u -> ∀ T, typ e t T -> typ e u T.
simple induction 1; intros; auto with coc.
apply subj_red with P; intros; auto with coc.
Qed.
Lemma type_reduction : ∀ e t T U, red T U -> typ e t T -> typ e t U.
intros.
elim type_case with (1 := H0); intros.
inversion_clear H1.
apply type_conv with T x; auto with coc.
apply subject_reduction with T; trivial.
elim red_normal with (1 := H); trivial.
rewrite H1.
red in |- *; red in |- *; intros.
inversion_clear H2.
Qed.
Lemma typ_conv_conv :
∀ e u U v V, typ e u U -> typ e v V -> conv u v -> conv U V.
intros.
elim church_rosser with (1 := H1); auto with coc; intros.
apply typ_unique with e x.
apply subject_reduction with u; trivial.
apply subject_reduction with v; trivial.
Qed.
End Typage.