Class.v
Require Termes.
Require Conv.
Require Types.
Inductive
Set class:= Trm:class | Typ: class | Ord: class.
Definition
cls:= (list class).
Syntactic Definition
nthf:= (nth_def class Trm).
Inductive
lift_cls: class->class->Prop :=
lift_t: (lift_cls Trm Typ)
| lift_T: (lift_cls Typ Ord).
Hint lift_t lift_T.
Fixpoint
cl_term [t:term]: cls->class :=
[i:cls]Cases t of
(Srt _) => Ord
| (Ref n) => Cases (nthf i n) of
Ord => Typ
| _ => Trm
end
| (Abs A B) => (cl_term B (cons ? (cl_term A i) i))
| (App u v) => (cl_term u i)
| (Prod T U) => (cl_term U (cons ? (cl_term T i) i))
end.
Fixpoint
class_env [e:env]: cls :=
Cases e of
nil => (nil ?)
| (cons t f) => (cons ? (cl_term t (class_env f)) (class_env f))
end.
Definition
cl_judge:= [e:env][t:term](cl_term t (class_env e)).
Lemma
cl_term_lift: (x:class)(t:term)(k:nat)(f,g:cls)(insert ? x k f g)
->(cl_term t f)=(cl_term (lift_rec (S O) t k) g).
Induction t;Simpl;Intros;Auto.
(Elim (le_gt_dec k n);Simpl;Intros).
(Elim ins_le with class k f g Trm x n ;Auto).
(Elim ins_gt with class k f g Trm x n ;Auto).
(Elim H with k f g ;Auto).
(Elim H with k f g ;Auto).
Save.
Lemma
class_env_lift: (e,f:env)(k:nat)(x:term)(ins_in_env x k e f)
->(insert ? (cl_judge e (lift k x)) k (class_env e) (class_env f)).
(Induction 1;Intros).
Rewrite -> lift0.
Simpl;Auto.
Rewrite -> simpl_lift.
Simpl.
Unfold cl_judge 1 lift ;Simpl.
Elim cl_term_lift with (cl_term t (class_env e0)) (lift n x) O (
class_env e0) (cons ? (cl_term t (class_env e0)) (class_env e0)) ;Auto.
Elim cl_term_lift with (cl_judge e0 (lift n x)) t n (class_env e0) (
class_env f0) ;Auto.
Save.
Lemma
cl_judge_lift: (e,f:env)(k:nat)(x,t:term)(ins_in_env x k e f)
->(cl_judge e t)=(cl_judge f (lift_rec (S O) t k)).
Unfold cl_judge .
Intros.
Apply cl_term_lift with (cl_judge e (lift k x)) .
(Apply class_env_lift;Auto).
Save.
Lemma
cl_term_subst: (a:class)(G:cls)(x:term)(lift_cls (cl_term x G) a)
->(t:term)(k:nat)(E,F:cls)(insert ? a k E F)
->(trunc ? k E G)
->(cl_term t F)=(cl_term (subst_rec x t k) E).
(Induction t;Simpl;Intros;Auto).
(Elim (lt_eq_lt_dec k n);Simpl;Intros).
Elim y.
(Case n;Simpl;Intros).
Inversion_clear y0.
(Elim ins_le with class k E F Trm a n0 ;Auto).
Induction 1.
(Rewrite -> (ins_eq class k E F Trm a);Auto).
Replace (cl_term (lift k x) E) with (cl_term x G).
Inversion_clear H;Auto.
Elim H1;Intros.
Rewrite -> lift0;Auto.
Rewrite -> H3.
Rewrite -> simpl_lift.
Unfold 2 lift .
(Apply cl_term_lift with x0 ;Auto).
(Elim ins_gt with class k E F Trm a n ;Auto).
(Elim H0 with k E F ;Auto).
(Elim H0 with k E F ;Auto).
Save.
Lemma
sub_env_ins:
(g:env)(v,V:term)(lift_cls (cl_judge g v) (cl_judge g V))
->(k:nat)(e,f:env)(sub_in_env v V k e f)
->(trunc ? k f g)
->(insert ? (cl_judge g V) k (class_env f) (class_env e)).
Induction 2;Simpl;Intros.
Inversion_clear H1.
(Unfold cl_judge ;Auto).
Inversion_clear H3.
Elim cl_term_subst with (cl_judge g V) (class_env g) v u n (class_env f0) (
class_env e0) ;Auto.
Elim H4;Simpl;Auto.
Save.
Lemma
cl_judge_subst:
(g:env)(v,V:term)(lift_cls (cl_judge g v) (cl_judge g V))
->(k:nat)(e,f:env)(sub_in_env v V k e f)
->(trunc ? k f g)
->(t:term)(cl_judge e t)=(cl_judge f (subst_rec v t k)).
Unfold cl_judge .
Intros.
Cut (trunc ? k (class_env f) (class_env g));Intros.
Apply cl_term_subst with (cl_judge g V) (class_env g) ;Auto.
Apply sub_env_ins with v ;Auto.
(Elim H1;Simpl;Auto).
Save.
Lemma
class_sound_w: (e:env)(t,T:term)(typ e t T)->
((n:nat)(x:term)(item ? x e n)->(f:env)(trunc ? (S n) e f)->
(((typ f x (Srt prop))->(nthf (class_env e) n)=Typ)
/\ ((typ f x (Srt kind))->(nthf (class_env e) n)=Ord)))
-> ((typ e T (Srt prop))->(cl_judge e t)=Trm)
/\ ((typ e T (Srt kind))->(cl_judge e t)=Typ)
/\ ((T=(Srt kind))->(cl_judge e t)=Ord).
(Induction 1; Simpl; Intros).
(Split; Intros).
(Elim inv_typ_kind with e0 (Srt prop); Auto).
(Split; Intros).
(Elim inv_typ_kind with e0 (Srt kind); Auto).
(Simpl; Auto).
(Elim H1; Intros).
Rewrite -> H3.
(Elim item_trunc with term v e0 x; Intros; Auto).
(Elim H2 with v x x0; Intros; Auto).
(Elim wf_sort with v e0 x0 x; Auto).
(Unfold cl_judge ; Simpl).
Intros.
Cut (typ e0 (lift (S v) x) (Srt x1)).
Intro.
(Split; Intros).
(Rewrite -> H6; Auto).
(Elim conv_sort with x1 prop; Auto).
(Apply typ_unique with e0 (lift (S v) x); Auto).
(Split; Intros).
(Rewrite -> H7; Auto).
(Elim conv_sort with x1 kind; Auto).
(Apply typ_unique with e0 (lift (S v) x); Auto).
Elim inv_typ_kind with e0 (Srt x1).
(Elim H10; Auto).
(Replace (Srt x1) with (lift (S v) (Srt x1)); Auto).
(Apply thinning_n with x0; Auto).
(Elim H5; Auto).
Clear H1 H3 H5 H6.
Intros.
(Elim H3; Intros).
Clear H3.
(Split; Intros).
Apply H1.
(Apply inv_typ_prod with e0 T0 U (Srt prop); Auto; Intros).
(Elim conv_sort with s3 prop; Auto).
(Split; Intros).
Apply H5.
(Apply inv_typ_prod with e0 T0 U (Srt kind); Auto; Intros).
(Elim conv_sort with s3 kind; Auto).
Discriminate H3.
Clear H3 H5.
(Destruct n; Simpl; Intros).
(Elim H1; Auto; Intros).
(Elim H8; Intros).
Clear H1 H6 H8.
Inversion_clear H3.
Inversion_clear H5.
Inversion H1.
Elim H6.
(Split; Intros).
Apply H9.
(Elim conv_sort with prop s1; Auto).
Apply type_prop.
(Apply typ_wf with T0 (Srt s1); Auto).
(Apply typ_unique with e0 T0; Auto).
Apply H10.
(Elim conv_sort with s1 kind; Auto).
(Apply typ_unique with e0 T0; Auto).
Inversion_clear H3.
Inversion_clear H5.
(Apply H6; Auto).
(Elim H3; Auto; Induction 2; Intros).
Clear H1 H3 H4 H6 H8.
(Elim type_case with e0 u (Prod V Ur); Intros; Auto).
(Elim H1; Intros).
Clear H1.
(Cut (typ e0 (subst v Ur) (Srt x)); Intros).
(Split; Intros).
Apply H5.
(Elim conv_sort with x prop; Auto).
(Apply typ_unique with e0 (subst v Ur); Auto).
(Split; Intros).
Apply H7.
(Elim conv_sort with x kind; Auto).
(Apply typ_unique with e0 (subst v Ur); Auto).
Elim inv_typ_kind with e0 (Srt x).
(Elim H4; Auto).
(Apply inv_typ_prod with e0 V Ur (Srt x); Auto; Intros).
Replace (Srt x) with (subst v (Srt s2)).
(Apply substitution with V; Auto).
(Elim conv_sort with s2 x; Auto).
Discriminate H1.
Elim H3.
(Induction 2; Intros).
Clear H1 H3 H4 H6.
(Split; Intros).
Apply H5.
(Replace (Srt s2) with (lift (S O) (Srt s2)); Auto).
(Replace (Srt prop) with (lift (S O) (Srt prop)); Auto).
(Apply thinning; Auto).
(Apply wf_var with s1; Auto).
(Split; Intros; Auto).
Apply H7.
(Replace (Srt s2) with (lift (S O) (Srt s2)); Auto).
(Replace (Srt kind) with (lift (S O) (Srt kind)); Auto).
(Apply thinning; Auto).
(Apply wf_var with s1; Auto).
(Destruct n; Simpl; Intros).
(Elim H1; Auto; Intros).
(Elim H8; Intros).
Clear H1 H3 H4 H8.
Inversion_clear H5.
Inversion_clear H6.
Inversion H1.
Elim H5.
(Split; Intros).
Apply H9.
(Elim conv_sort with prop s1; Auto).
Apply type_prop.
(Apply typ_wf with T0 (Srt s1); Auto).
(Apply typ_unique with e0 T0; Auto).
Apply H10.
(Elim conv_sort with kind s1; Auto).
(Apply typ_unique with e0 T0; Auto).
Clear H1 H3.
Inversion_clear H5.
Inversion_clear H6.
Auto.
(Elim H1; Auto; Induction 2; Intros).
Clear H1 H4 H5 H7.
(Cut (typ e0 U (Srt s)); Intros).
(Split; Intros).
Apply H6.
(Elim conv_sort with s prop; Auto).
(Apply typ_unique with e0 V; Auto).
(Split; Intros).
Apply H8.
(Elim conv_sort with s kind; Auto).
(Apply typ_unique with e0 V; Auto).
(Elim inv_typ_kind with e0 (Srt s); Auto).
(Elim H4; Auto).
(Elim type_case with e0 t0 U; Auto; Intros).
(Elim H1; Intros).
(Elim conv_sort with x s; Auto).
(Apply typ_conv_conv with e0 U V; Auto).
(Elim inv_typ_conv_kind with e0 V (Srt s); Auto).
(Elim H1; Auto).
Save.
Lemma
corr_class_env: (e:env)(wf e)->(n:nat)(x:term)(item ? x e n)->
(f:env)(trunc ? (S n) e f)->
(((typ f x (Srt prop))->(nthf (class_env e) n)=Typ)
/\ ((typ f x (Srt kind))->(nthf (class_env e) n)=Ord)).
(Induction e; Simpl).
Intros.
Inversion_clear H0.
(Destruct n; Simpl; Intros).
Inversion_clear H1.
Inversion_clear H2.
Inversion H1.
Elim H4.
Inversion_clear H0.
(Elim class_sound_w with l a (Srt s); Intros; Auto).
(Elim H6; Intros).
Clear H6.
(Split; Intros).
Apply H7.
(Elim conv_sort with prop s; Auto).
(Apply type_prop; Apply typ_wf with a (Srt s); Auto).
(Apply typ_unique with l a; Auto).
Apply H8.
(Elim conv_sort with s kind; Auto).
(Apply typ_unique with l a; Auto).
(Apply H; Auto).
(Apply typ_wf with a (Srt s); Auto).
Inversion_clear H1.
Inversion_clear H2.
(Apply H; Auto).
Inversion_clear H0.
(Apply typ_wf with a (Srt s); Auto).
Save.
Lemma
class_trm: (e:env)(t,T:term)(typ e t T)->(typ e T (Srt prop))
->(cl_judge e t)=Trm.
Intros.
Elim class_sound_w with e t T ;Auto.
Intros.
(Apply corr_class_env;Auto).
(Apply typ_wf with t T ;Auto).
Save.
Lemma
class_typ: (e:env)(t,T:term)(typ e t T)->(typ e T (Srt kind))
->(cl_judge e t)=Typ.
Intros.
(Elim class_sound_w with e t T ;Auto).
Intros.
(Elim H2;Auto).
Intros.
Apply corr_class_env;Auto.
Apply typ_wf with t T ;Auto.
Save.
Lemma
class_ord: (e:env)(t:term)(typ e t (Srt kind))->(cl_judge e t)=Ord.
Intros.
Elim class_sound_w with e t (Srt kind) ;Auto.
Intros.
Elim H1;Auto.
Intros.
(Apply corr_class_env;Auto).
(Apply typ_wf with t (Srt kind) ;Auto).
Save.
Lemma
inv_class: (e:env)(t,T:term)(typ e t T)
-> Cases (cl_judge e t) of
Trm => (typ e T (Srt prop))
| Typ => (typ e T (Srt kind))
| Ord => T=(Srt kind)
end.
Intros.
Elim type_case with e t T ;Intros;Auto.
Elim H0.
(Induction x;Intros).
Rewrite -> (class_typ e t T);Auto.
Rewrite -> (class_trm e t T);Auto.
Rewrite -> (class_ord e t);Auto.
(Elim H0;Auto).
Save.
Lemma
corr_lift: (e:env)(t,T,s:term)(typ e t T)->(typ e T s)
->(lift_cls (cl_judge e t) (cl_judge e T)).
Intros.
Generalize (inv_class e t T H) .
Elim (cl_judge e t);Intros.
Rewrite -> (class_typ e T (Srt prop));Auto.
Apply type_prop;Apply typ_wf with t T ;Auto.
Rewrite -> (class_ord e T);Auto.
Elim inv_typ_kind with e s ;Auto.
Elim H1;Auto.
Save.
Lemma
class_subst: (e:env)(t,v,V,s:term)(typ e v V)->(typ e V s)
->(cl_judge (cons ? V e) t)=(cl_judge e (subst v t)).
Intros.
Unfold subst .
(Apply cl_judge_subst with e V ;Auto).
(Apply corr_lift with s ;Auto).
Save.
Lemma
cl_judge_red: (e:env)(T,K:term)(typ e T K)->(U:term)(red T U)
->(cl_judge e T)=(cl_judge e U).
Intros.
Cut (typ e U K);Intros.
Elim type_case with e T K ;Intros;Auto.
Elim H2.
(Induction x;Intros).
Rewrite -> (class_typ e T K);Auto.
Rewrite -> (class_typ e U K);Auto.
Rewrite -> (class_trm e T K);Auto.
Rewrite -> (class_trm e U K);Auto.
Rewrite -> (class_ord e T).
Rewrite -> (class_ord e U);Auto.
Elim H2;Auto.
Elim H2;Auto.
Apply subject_reduction with T ;Auto.
Save.
Lemma
class_env_red1: (e,f:env)(red1_in_env e f)->(wf e)
->(class_env e)=(class_env f).
Induction 1;Simpl;Auto;Intros.
Change (eq ? (cons ? (cl_judge e0 t) (class_env e0))
(cons ? (cl_judge e0 u) (class_env e0))).
Inversion_clear H1.
Elim cl_judge_red with e0 t (Srt s) u ;Auto.
Inversion_clear H2.
Elim H1;Auto.
Apply typ_wf with t (Srt s) ;Auto.
Save.
20/01/97, 14:42