Strong_Norm.v
Require Termes.
Require Conv.
Require Types.
Require Class.
Require Skel.
Require Can.
Require Interp.
Inductive
can_adapt: intP->Prop :=
ca_nl: (can_adapt (TNl ?))
| ca_cs: (ip:intP)(s:skel)(x:term)(C:(Can s))(can_adapt ip)
->(is_can s C)->(eq_can s C C)
->(can_adapt (TCs ? (iK s C) ip)).
Hint ca_nl ca_cs.
Lemma
adapt_int_inv: (ip:intP)(can_adapt ip)->(int_inv ip).
(Induction 1;Simpl;Intros;Auto).
Save.
Hint adapt_int_inv.
Lemma
int_typ_cr: (t:term)(e:env)(ip:intP)(can_adapt ip)
->(s:skel)(is_can s (int_typ t e ip ?)).
(Induction t;Simpl;Intros;Auto).
Generalize n .
(Elim H;Simpl;Intros).
(Elim (EQ_skel PROP s);Auto).
(Induction y;Simpl;Auto).
(Case n0;Simpl;Auto).
Elim (EQ_skel s0 s);Auto.
(Induction y;Auto).
Unfold def_cons .
(Elim (cl_judge e t0);Auto).
(Case s;Simpl;Auto).
(Elim (cl_judge e t0);Auto).
(Elim (cl_judge e t1);Auto).
(Generalize (H e ip H1 (PROD (typ_skel t1 e) s)) ;Simpl;Auto).
(Case s;Simpl;Auto).
(Apply CR_pi;Simpl;Auto).
Save.
Hint int_typ_cr.
Inductive
int_adapt: env->intP->intt->Prop :=
int_nil: (it:intt)(int_adapt (nil ?) (TNl ?) it)
| int_cs: (e:env)(ip:intP)(it:intt)(int_adapt e ip it)
->(s:skel)(T:term)(cv_skel T (class_env e))==s
->(C:(Can s))(is_can s C)->(eq_can s C C)
->(x:term)(int_typ T e ip PROP x)
->(int_adapt (cons ? T e) (TCs ? (iK s C) ip) (shift_intt it x)).
Hint int_nil int_cs.
Lemma
int_can_adapt: (e:env)(ip:intP)(it:intt)(int_adapt e ip it)
->(can_adapt ip).
(Induction 1;Auto).
Save.
Lemma
int_sound: (e:env)(t,T:term)(typ e t T)
->(ip:intP)(it:intt)(int_adapt e ip it)
->(int_typ T e ip PROP (int_term t it O)).
Induction 1;Simpl;Intros.
Red;Apply Acc_intro;Intros.
Inversion_clear H2.
(Elim (le_gt_dec O v);Intros).
Rewrite -> lift0.
Elim minus_n_O with v .
(Elim H1;Intros).
Rewrite -> H3.
Generalize v H4 .
Clear H4 H3 y H1 t0 v H0 H e t T.
(Elim H2;Intros).
Inversion_clear H4.
Cut (eq_can PROP (int_typ (lift v x) e ip0 PROP)
(int_typ (lift_rec (S O) (lift v x) O) (cons term T e)
(TCs Int_K (iK s C) ip0) PROP)).
Generalize H6 .
Clear H6.
(Case v;Simpl).
Intro.
Inversion_clear H6.
Rewrite -> lift0.
Unfold lift .
Intro.
Elim H6 with x0 ;Auto.
Intros.
Inversion_clear H6.
Rewrite -> simpl_lift.
Unfold 1 lift .
Elim H7 with (it0 n) ;Auto.
(Apply lift_int_typ with (iK s C) T ;Auto).
Cut (int_inv ip0);Auto.
Apply adapt_int_inv.
Apply int_can_adapt with e it0 ;Auto.
Inversion_clear y.
Cut (can_adapt ip);Intros.
Apply Pi_sound;Simpl;Auto;Intros.
Unfold subst .
Rewrite -> int_term_subst;Auto.
Apply H1 with ip ;Auto.
Apply int_can_adapt with e0 it ;Auto.
(Elim type_case with e0 u (Prod V Ur) ;Intros;Auto).
Inversion_clear H5.
(Apply inv_typ_prod with e0 V Ur (Srt x) ;Auto;Intros).
Cut (can_adapt ip);Intros.
Cut (eq_can PROP
(int_typ Ur (cons ? V e0)
(TCs ?
(iK (cv_skel V (class_env e0))
(int_typ v e0 ip (cv_skel V (class_env e0))))
ip) PROP)
(int_typ (subst_rec v Ur O) e0 ip PROP)).
Simpl;Intros;Unfold subst .
(Elim H10 with (App (int_term u it O) (int_term v it O)) ;Intros).
Apply H11;Auto.
Clear H10 H11 H12.
Unfold Pi in H3.
(Apply H3;Auto).
Replace PROP with (typ_skel Ur (cons ? V e0)).
Generalize H5 .
Elim s1;Intros.
Apply subst_int_typ with e0 V ip (Srt s2) ;Auto.
Apply class_typ with V ;Auto.
(Elim skel_sound with e0 v V ;Auto).
(Apply subst_int_typ_trm with e0 V (iK (cv_skel V (class_env e0))
(int_typ v e0 ip (cv_skel V (class_env e0)))) (Srt s2) ;Auto).
(Apply class_trm with V ;Auto).
Generalize H7 .
(Elim s2;Intros).
(Rewrite -> (class_ord (cons ? V e0) Ur);Auto).
Discriminate.
(Rewrite -> (class_typ (cons ? V e0) Ur (Srt prop));Auto).
Discriminate.
Apply type_prop.
(Apply typ_wf with Ur (Srt s2) ;Auto).
(Elim skel_sound with (cons ? V e0) Ur (Srt s2) ;Auto).
Apply int_can_adapt with e0 it ;Auto.
Discriminate H5.
Apply sn_prod.
Apply H1 with ip ;Auto.
Apply sn_subst with (Ref O).
Unfold subst.
Rewrite -> int_term_subst.
Apply H3 with (def_cons (class_env e0) T0 ip) .
Unfold def_cons .
Apply int_cs;Auto.
(Apply (int_var O (int_typ T0 e0 ip PROP));Auto).
Cut (can_adapt ip);Auto.
(Apply int_can_adapt with e0 it ;Auto).
Cut (typ e0 U (Srt s));Intros.
Cut (not (eq ? (cl_judge e0 U) Trm));Intros.
(Cut (can_adapt ip);Intros).
Generalize (conv_int_typ e0 U V (Srt s) H2 H6 H3 H7 ip) .
Replace (typ_skel U e0) with PROP.
Simpl;Intros.
Elim H9 with (int_term t0 it O) ;Auto.
Elim skel_sound with e0 U (Srt s) ;Auto.
Apply int_can_adapt with e0 it ;Auto.
Generalize H6 .
Elim s;Intros.
Rewrite -> (class_ord e0 U);Auto.
Discriminate.
Rewrite -> (class_typ e0 U (Srt prop));Auto.
Discriminate.
Apply type_prop.
Apply typ_wf with t0 U ;Auto.
Elim type_case with e0 t0 U ;Intros;Auto.
Inversion_clear H6.
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 H6;Auto.
Save.
Fixpoint
def_intp [e:env]: intP :=
Cases e of
nil => (TNl ?)
| (cons t f) => (def_cons (class_env f) t (def_intp f))
end.
Fixpoint
def_intt [e:env]: nat->intt :=
[k:nat]Cases e of
nil => [p:nat](Ref (plus k p))
| (cons _ f) => (shift_intt (def_intt f (S k)) (Ref k))
end.
Lemma
def_intp_can: (e:env)(can_adapt (def_intp e)).
(Induction e;Simpl;Auto;Intros).
(Unfold def_cons ;Auto).
Save.
Lemma
def_adapt: (e:env)(k:nat)(int_adapt e (def_intp e) (def_intt e k)).
Induction e;Simpl;Auto.
Intros.
Unfold def_cons .
(Apply int_cs;Auto).
(Apply (int_var k (int_typ a l (def_intp l) PROP));Auto).
(Cut (can_adapt (def_intp l));Auto).
(Apply int_can_adapt with l (def_intt l O) ;Auto).
Save.
Hint def_intp_can def_adapt.
Lemma
def_intt_id: (n:nat)(e:env)(k:nat)(def_intt e k n)=(Ref (plus k n)).
(Induction n;Destruct e;Simpl;Auto;Intros).
Replace (plus k O) with k;Auto.
Rewrite -> H.
Replace (plus k (S n0)) with (S (plus k n0));Auto.
Save.
Lemma
id_int_term: (e:env)(t:term)(k:nat)(int_term t (def_intt e O) k)=t.
Induction t;Simpl;Intros;Auto.
Elim (le_gt_dec k n);Intros;Auto.
Rewrite -> def_intt_id.
(Simpl;Unfold lift ).
Rewrite lift_ref_ge;Auto.
Replace (plus k (minus n k)) with n;Auto.
(Rewrite -> H;Rewrite -> H0;Auto).
(Rewrite -> H;Rewrite -> H0;Auto).
(Rewrite -> H;Rewrite -> H0;Auto).
Save.
Theorem
fort_norm: (e:env)(t,T:term)(typ e t T)->(sn t).
Intros.
Cut (is_can PROP (int_typ T e (def_intp e) PROP));Auto.
Simpl;Intros.
Cut (int_typ T e (def_intp e) PROP t).
Elim H0;Auto.
Elim id_int_term with e t O .
(Apply int_sound;Auto).
Save.
Lemma
type_sn: (e:env)(t,T:term)(typ e t T)->(sn T).
Intros.
Elim type_case with e t T ;Intros;Auto.
(Elim H0;Intros).
(Apply fort_norm with e (Srt x) ;Auto).
Rewrite -> H0.
(Red;Apply Acc_intro;Intros).
Inversion_clear H1.
Save.
06/11/96, 12:36