Skel.v
Require Termes.
Require Conv.
Require Types.
Require Class.
Require Export MyLogicType.
Inductive
skel: Type :=
PROP: skel
| PROD: skel->skel->skel.
Definition
predl: skel->skel :=
[a:skel]Cases a of
(PROD a1 _) => a1
| _ => PROP
end.
Definition
predr: skel->skel :=
[a:skel]Cases a of
(PROD _ a2) => a2
| _ => PROP
end.
Lemma
EQ_skel: (a,b:skel)(ORT (a===b) (notT (a===b))).
(Induction a; Destruct b; Intros).
(Left; Auto).
(Right; Red; Intros).
Inversion X.
(Right; Red; Intros).
Inversion X1.
(Elim X with s1; Intros).
Elim y.
(Elim X0 with s2; Intros).
Elim y0.
(Left; Auto).
(Right; Red; Intros; Apply y0).
(Injection X1; Auto).
(Right; Red; Intros; Apply y).
(Injection X1; Auto).
Save.
Fixpoint
cv_skel [K:term]: cls->skel :=
[F:cls]Cases K of
(Prod T U) => ([G:cls]Cases (cl_term U G) (cl_term T F) of
Ord Ord => (PROD (cv_skel T F) (cv_skel U G))
| Ord Typ => (cv_skel U G)
| _ _ => PROP
end
(cons ? (cl_term T F) F))
| _ => PROP
end.
Fixpoint
typ_skel [T:term]: env->skel :=
[e:env]Cases T of
(Srt _) => PROP
| (Ref k) => (Fix nthk {nthk/1: env->nat->skel :=
[e:env][n:nat]Cases e n of
(cons _ f) (S m) => (nthk f m)
| (cons h f) O => (cv_skel h (class_env f))
| _ _ => PROP
end} e k)
| (Abs A t) => Cases (cl_judge (cons ? A e) t) (cl_judge e A) of
Typ Ord => (PROD (cv_skel A (class_env e))
(typ_skel t (cons ? A e)))
| Typ Typ => (typ_skel t (cons ? A e))
| _ _ => PROP
end
| (App u v) => Cases (cl_judge e u) (cl_judge e v) of
Typ Typ => (predr (typ_skel u e))
| Typ Trm => (typ_skel u e)
| _ _ => PROP
end
| (Prod _ _) => PROP
end.
Lemma
skel_not_ord: (T,K:term)(e:env)(lift_cls (cl_judge e T) (cl_judge e K))
->(cv_skel T (class_env e))==PROP.
Destruct T;Simpl;Auto.
Unfold 1 cl_judge .
Simpl.
Destruct 1;Auto.
Save.
Lemma
cv_skel_lift: (x:class)(t:term)(f,g:cls)(k:nat)(insert ? x k f g)
->(cv_skel t f)==(cv_skel (lift_rec (S O) t k) g).
(Induction t;Simpl;Intros;Auto).
(Elim (le_gt_dec k n);Simpl;Auto).
(Elim cl_term_lift with x t0 k f g ;Auto).
(Elim cl_term_lift with x t1 (S k) (cons ? (cl_term t0 f) f)
(cons ? (cl_term t0 f) g) ;Auto).
Elim H with f g k ;Auto.
Elim H0 with (cons ? (cl_term t0 f) f) (cons ? (cl_term t0 f) g)(S k) ;Auto.
Save.
Lemma
cv_skel_subst:
(g:env)(v,V:term)(lift_cls (cl_judge g v) (cl_judge g V))
->(t:term)(k:nat)(e,f:env)(sub_in_env v V k e f)
->(trunc ? k f g)
->(cv_skel t (class_env e))==(cv_skel (subst_rec v t k) (class_env f)).
(Induction t;Simpl;Intros;Auto).
(Elim (lt_eq_lt_dec k n);Simpl;Intros;Auto).
(Elim y;Simpl;Intros;Auto).
Generalize H1 .
Elim H0;Intros.
Rewrite -> lift0.
Symmetry.
(Apply skel_not_ord with V ;Auto).
Inversion_clear H2;Auto.
Inversion_clear H4.
Rewrite -> simpl_lift.
Unfold 1 lift .
Rewrite -> H3;Auto.
Simpl.
(Apply cv_skel_lift with (cl_term (subst_rec v u n0) (class_env f0)) ;Auto).
Replace (cons ? (cl_term t0 (class_env e)) (class_env e)) with (
class_env (cons ? t0 e));Auto.
Replace (cons ? (cl_term (subst_rec v t0 k) (class_env f))
(class_env f)) with (class_env (cons ? (subst_rec v t0 k) f));Auto.
Replace (cl_term t1 (class_env (cons ? t0 e))) with (cl_judge
(cons ? t0 e) t1);Auto.
Replace (cl_term (subst_rec v t1 (S k)) (class_env (cons ?
(subst_rec v t0 k) f))) with (cl_judge (cons ? ( subst_rec v t0 k) f)
(subst_rec v t1 ( S k)));Auto.
(Replace (cl_term (subst_rec v t0 k) (class_env f)) with (cl_judge f
(subst_rec v t0 k));Auto).
Elim cl_judge_subst with g v V (S k) (cons ? t0 e) (cons ?
(subst_rec v t0 k) f) t1 ;Auto.
Elim cl_judge_subst with g v V k e f t0 ;Auto.
(Elim H0 with k e f ;Auto).
(Elim H1 with (S k) (cons ? t0 e) (cons ? (subst_rec v t0 k) f) ;Auto).
Save.
Lemma
typ_skel_lift: (t:term)(k:nat)(f,g:env)(x:term)(ins_in_env x k f g)
->(typ_skel t f)==(typ_skel (lift_rec (S O) t k) g).
(Induction t;Simpl;Auto).
Induction n.
(Destruct 1;Intros).
(Elim (le_gt_dec O O);Intros;Auto).
Simpl.
Auto.
Inversion_clear y.
(Elim (le_gt_dec (S n0) O);Intros).
Inversion_clear y.
Simpl.
(Apply cv_skel_lift with (cl_judge e (lift n0 x)) ;Auto).
(Apply class_env_lift;Auto).
(Destruct 2;Simpl;Intros).
(Elim (le_gt_dec O (S n0));Simpl;Auto;Intros).
Inversion_clear y.
(Rewrite -> (H n1 e f0 x);Auto).
Elim (le_gt_dec n1 n0);Elim (le_gt_dec (S n1) (S n0));Intros;Auto.
Absurd (le n1 n0);Auto.
Absurd (le (S n1) (S n0));Auto.
Intros.
Elim cl_judge_lift with f g k x t0 ;Auto.
Elim cl_judge_lift with (cons ? t0 f) (cons ? (lift_rec (S O) t0 k) g) (
S k) x t1 ;Auto.
Elim H0 with (S k) (cons ? t0 f) (cons ? (lift_rec (S O) t0 k) g) x ;Auto.
(Elim cv_skel_lift with (cl_judge f (lift k x)) t0 (class_env f) (
class_env g) k ;Auto).
Apply class_env_lift;Auto.
Intros.
(Elim H with k f g x ;Auto).
(Elim cl_judge_lift with f g k x t0 ;Auto).
Elim cl_judge_lift with f g k x t1 ;Auto.
Save.
Lemma
typ_skel_subst: (g:env)(v,V:term)
(lift_cls (cl_judge g v) (cl_judge g V))
->(typ_skel v g)==(cv_skel V (class_env g))
->(t:term)(k:nat)(e,f:env)(sub_in_env v V k e f)
->(trunc ? k f g)
->(typ_skel t e)==(typ_skel (subst_rec v t k) f).
Induction t;Simpl;Auto.
Induction n.
Intros.
Elim (lt_eq_lt_dec k O);Intros.
Elim y;Intros.
Inversion_clear y0.
Generalize H1 H2 .
Rewrite -> y0;Intros.
Rewrite -> lift0.
Inversion_clear H3.
Inversion_clear H4;Auto.
Generalize y H1 H2 .
(Case k;Intros).
Inversion_clear y0.
Generalize H4 .
Inversion_clear H3;Intros.
Inversion_clear H3.
Simpl.
(Apply cv_skel_subst with g V ;Auto).
Destruct 2;Intros.
Inversion_clear H3.
Elim (lt_eq_lt_dec O (S n0));Intros.
Elim y;Intros.
Simpl.
Auto.
Discriminate y0.
Inversion_clear y.
Inversion_clear H4.
Rewrite -> (H1 n1 e0 f0);Auto;Intros.
Elim (lt_eq_lt_dec n1 n0);Intros.
Elim (lt_eq_lt_dec (S n1) (S n0));Intros.
Elim y;Elim y0;Auto.
Case n0;Intros;Auto.
Inversion_clear y2.
Intro.
Inversion_clear y1;Intros.
Elim lt_n_n with n0 ;Auto.
Intros.
Inversion_clear y2 in y1.
Elim lt_n_n with (S n0) ;Auto.
Intros.
Rewrite -> simpl_lift.
Unfold 2 lift .
Apply typ_skel_lift with (subst_rec v u n1) ;Auto.
Elim y;Intros.
Absurd (le (S n1) n0);Auto.
Inversion_clear y1 in y0.
Elim lt_n_n with (S n0) ;Auto.
Elim (lt_eq_lt_dec (S n1) (S n0));Intros.
Elim y0;Intros.
Absurd (le (S n0) n1);Auto.
Inversion_clear y1 in y.
Elim lt_n_n with n0 ;Auto.
Simpl;Auto.
Intros.
Elim cl_judge_subst with g v V k e f t0 ;Auto.
Elim cl_judge_subst with g v V (S k) (cons ? t0 e) (cons ?
(subst_rec v t0 k)
f) t1 ;Auto.
Elim cv_skel_subst with g v V t0 k e f ;Auto.
Elim H2 with (S k) (cons ? t0 e) (cons ? (subst_rec v t0 k) f) ;Auto.
Intros.
Elim cl_judge_subst with g v V k e f t0 ;Auto.
Elim cl_judge_subst with g v V k e f t1 ;Auto.
Elim H1 with k e f ;Auto.
Save.
Lemma
skel_red1: (e:env)(A,T:term)(typ e A T)->(B:term)(red1 A B)
->(cv_skel A (class_env e))==(cv_skel B (class_env e)).
(Induction 1;Intros;Auto).
Inversion_clear H1.
Inversion_clear H2.
Simpl.
(Inversion_clear H6;Simpl;Auto).
Generalize H2 .
(Inversion_clear H4;Simpl;Auto;Intros).
(Apply inv_typ_abs with e0 T0 M (Prod V Ur) ;Auto;Intros).
Symmetry.
Apply skel_not_ord with (subst v T1) .
Apply corr_lift with (Srt s2) ;Auto.
Apply substitution with T0 ;Auto.
(Apply type_conv with V s1 ;Auto).
(Apply inv_conv_prod_l with Ur T1 ;Auto).
(Replace (Srt s2) with (subst v (Srt s2));Auto).
Apply substitution with T0 ;Auto.
(Apply type_conv with V s1 ;Auto).
(Apply inv_conv_prod_l with Ur T1 ;Auto).
(Inversion_clear H4;Simpl).
Replace (cl_term N1 (class_env e0)) with (cl_judge e0 T0).
(Elim H1 with N1 ;Auto).
Change (eq ? (cl_judge e0 T0) (cl_judge e0 N1)).
Apply cl_judge_red with (Srt s1) ;Auto.
(Replace (cons ? (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0));Auto).
Elim H3 with N2 ;Auto.
(Replace (cl_term N2 (class_env (cons ? T0 e0))) with (cl_term U
(class_env
(cons ? T0 e0)));Auto).
Change (eq ? (cl_judge (cons ? T0 e0) U) (cl_judge (cons ? T0 e0) N2)).
(Apply cl_judge_red with (Srt s2) ;Auto).
Save.
Lemma
skel_red: (A,B:term)(red A B)->(e:env)(T:term)(typ e A T)
->(cv_skel A (class_env e))==(cv_skel B (class_env e)).
Induction 1;Intros;Auto.
Rewrite -> (H1 e T);Auto.
(Apply skel_red1 with T ;Auto).
(Apply subject_reduction with A ;Auto).
Save.
Lemma
skel_conv: (e:env)(A,T:term)(typ e A T)->(B,U:term)(typ e B U)
->(conv A B)->(cv_skel A (class_env e))==(cv_skel B (class_env e)).
Intros.
(Elim church_rosser with A B ;Intros;Auto).
(Rewrite -> (skel_red A x H2 e T);Auto).
(Elim skel_red with B x e U ;Auto).
Save.
Lemma
skel_sound: (e:env)(t,T:term)(typ e t T)
->(cv_skel T (class_env e))==(typ_skel t e).
Induction 1;Auto.
Do 3 Intro.
Generalize e0 .
Elim v.
Destruct e0;Intros.
(Elim H1;Intros).
Inversion_clear H3.
(Elim H1;Intros).
Rewrite -> H2.
Inversion_clear H3.
(Simpl;Unfold lift ).
Symmetry.
Apply cv_skel_lift with (cl_term t0 (class_env l)) ;Auto.
(Destruct 2;Intros).
Rewrite -> H3.
(Inversion_clear H4;Simpl).
Rewrite -> simpl_lift.
Unfold 1 lift .
(Elim cv_skel_lift with (cl_term y (class_env l)) (lift (S n) x) (
class_env l) (cons ? (cl_term y (class_env l)) (class_env l)) O ;Auto).
Simpl in H1.
Apply H1.
(Exists x ;Auto).
Simpl;Intros.
Rewrite -> H5.
Replace (cl_term U (cons ? (cl_term T0 (class_env e0)) (class_env e0))) with (
cl_judge (cons ? T0 e0) U);Auto.
(Elim corr_lift with (cons ? T0 e0) M U (Srt s2) ;Auto).
(Simpl;Intros).
Elim H3;Clear H3.
(Elim type_case with e0 u (Prod V Ur) ;Intros;Auto).
Elim H3;Intros.
Apply inv_typ_prod with e0 V Ur (Srt x) ;Auto;Intros.
Unfold subst .
Elim cv_skel_subst with e0 v V Ur O (cons ? V e0) e0 ;Auto.
Replace (cons ? (cl_term V (class_env e0)) (class_env e0)) with (
class_env (cons ? V e0));Auto.
(Replace (cl_term V (class_env e0)) with (cl_judge e0 V);Auto).
Replace (cl_term Ur (class_env (cons ? V e0))) with (cl_judge e0
(Prod V Ur));Auto.
Generalize (inv_class e0 (Prod V Ur) (Srt x) H4) .
(Elim corr_lift with e0 u (Prod V Ur) (Srt x) ;Auto).
Intro.
Apply skel_not_ord with (Srt x) .
Change (lift_cls (cl_judge e0 (Prod V Ur)) Ord).
(Rewrite -> (class_typ e0 (Prod V Ur) (Srt x));Auto).
Intro.
(Elim corr_lift with e0 v V (Srt s1) ;Auto).
(Apply corr_lift with (Srt s1) ;Auto).
Discriminate H3.
Intros.
(Elim type_case with e0 t0 U ;Intros;Auto).
(Elim H5;Intros).
Elim H1.
(Apply skel_conv with (Srt s) (Srt x) ;Auto).
(Elim inv_typ_conv_kind with e0 V (Srt s) ;Auto).
(Elim H5;Auto).
Save.
Lemma
typ_skel_red1: (e:env)(T,U,K:term)(typ e T K)->(red1 T U)
->(typ_skel T e)==(typ_skel U e).Intros.
(Elim skel_sound with e T K ;Auto).
(Apply skel_sound;Auto).
(Apply subject_reduction with T ;Auto).
Save.
Lemma
typ_skel_red_env: (e:env)(t,s:term)(typ e t s)
->(f:env)(red1_in_env e f)
->(typ_skel t e)==(typ_skel t f).
Induction 1;Simpl;Intros;Auto.
Generalize e0 f H2 H0 .
(Elim v;Simpl;Auto).
(Destruct 1;Intros).
Inversion_clear H5.
Apply skel_red1 with (Srt s0) ;Auto.
Elim class_env_red1 with e2 f1 ;Auto.
Inversion_clear H5.
(Apply typ_wf with t1 (Srt s0) ;Auto).
(Destruct 2;Simpl;Intros;Auto).
(Apply H3;Auto).
Inversion_clear H6.
(Apply typ_wf with t1 (Srt s0) ;Auto).
Unfold cl_judge .
Elim class_env_red1 with (cons ? T e0) (cons ? T f) ;Auto.
Elim class_env_red1 with e0 f ;Auto.
(Elim H5 with (cons ? T f) ;Auto).
(Apply typ_wf with T (Srt s1) ;Auto).
(Apply wf_var with s1 ;Auto).
Unfold cl_judge .
Elim class_env_red1 with e0 f ;Auto.
(Elim H3 with f ;Auto).
Apply typ_wf with v V ;Auto.
Save.
06/11/96, 12:34