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