Strong_Norm.v



Require Termes.
Require Conv.
Require Types.
Require Class.
Require Can.
Require Int_term.
Require Int_typ.
Require Int_stab.






  Inductive trm_in_int: env->intP->intt->Prop :=
    int_nil: (itt:intt)(trm_in_int (nil ?) (TNl ?) itt)
  | int_cs: (e:env)(ip:intP)(itt:intt)(trm_in_int e ip itt)
              ->(y:Int_K)(t,T:term)(int_typ T ip PROP t)
               ->(trm_in_int (cons ? T e) (TCs ? y ip) (shift_intt itt t)).

  Hint int_nil int_cs.


  Record int_adapt [e:env; ip:intP; itt:intt]: Prop := {
    adapt_trm_in_int: (trm_in_int e ip itt);
    int_can_adapt: (can_adapt ip);
    adapt_class_equal: (cls_of_int ip)==(class_env e)
  }.



  Lemma int_sound: (e:env)(t,T:term)(typ e t T)
                      ->(ip:intP)(it:intt)(int_adapt e ip it)
                         ->(int_typ T 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 ip it H2 .
Clear H3 y H2 it ip H1 t0.
(Elim H4; Intros).
Elim H2.
Intro.
(Inversion_clear adapt_trm_in_int0; Simpl; Intros).
(Apply eq_cand_incl with (int_typ x ip0 PROP); Auto).
Unfold lift.
(Apply lift_int_typ with y; Auto).

Elim H3.
Intro.
(Inversion_clear adapt_trm_in_int0; Intros).
Simpl.
Rewrite -> simpl_lift.
Apply eq_cand_incl with (int_typ (lift (S n) x) ip0 PROP).
Unfold 2 lift.
(Apply lift_int_typ with y0; Auto).

Apply H2.
(Apply Build_int_adapt; Auto).
(Inversion_clear int_can_adapt0; Auto).

(Injection adapt_class_equal0; Auto).

Inversion_clear y.

Inversion H6.
(Apply Abs_sound; Intros; Auto).
(Apply int_typ_cr; Auto).

(Simpl; Intros).
Change (is_can PROP
         (int_typ U
           (int_cons T0 ip (cv_skel (cl_term T0 (cls_of_int ip))) X)
           PROP)).
Apply int_typ_cr.
Unfold int_cons ext_ik.
Generalize X H7 H8 .
(Elim (cl_term T0 (cls_of_int ip)); Auto).

Unfold subst.
(Rewrite -> int_term_subst; Auto).
Apply H5.
Unfold int_cons ext_ik.
(Apply Build_int_adapt; Auto).
Generalize C H8 H9 .
(Elim (cl_term T0 (cls_of_int ip)); Auto).

Simpl.
Generalize C .
Rewrite -> adapt_class_equal0.
Unfold cls_of_int.
Pattern (cl_term T0 (class_env e0)) .
(Apply class_typ_ord with s1; Elim adapt_class_equal0; Simpl; Auto).
Rewrite -> adapt_class_equal0.
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
(Elim adapt_class_equal0; Auto).

(Apply H1 with ip; Auto).

Inversion H4.
(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).
Apply eq_cand_incl with (int_typ Ur
                          (int_cons V ip
                            (cv_skel (cl_term V (cls_of_int ip)))
                            (int_typ v ip ?)) PROP).
Replace PROP with (skel_int Ur
                    (int_cons V ip
                      (cv_skel (cl_term V (cls_of_int ip)))
                      (int_typ v ip
                        (cv_skel (cl_term V (cls_of_int ip)))))).
Unfold subst int_cons.
(Apply subst_int_typ with ip (ext_ik V ip
                               (cv_skel (cl_term V (cls_of_int ip)))
                               (int_typ v ip
                                 (cv_skel (cl_term V (cls_of_int ip))))) (
 cons ? V e0) (Srt s2); Auto).
Unfold ext_ik.
Rewrite -> adapt_class_equal0.
Cut (eqT ? (cl_term v (cls_of_int ip)) (cl_term v (class_env e0))).
(Elim class_sound with e0 v V (Srt s1); Intros; Auto).

(Elim adapt_class_equal0; Auto).

Simpl.
Unfold ext_ik.
Rewrite -> adapt_class_equal0.
Unfold cls_of_int.
(Apply class_typ_ord with s1; Elim adapt_class_equal0; Simpl; Auto).
Rewrite -> adapt_class_equal0.
(Elim skel_sound with e0 V (Srt s1); Simpl; Auto).
(Elim adapt_class_equal0; Auto).

Unfold ext_ik.
(Red; Red; Auto).
(Apply Tfa2_cs; Auto).
(Elim (cl_term V (cls_of_int ip)); Auto).

Change (int_inv ip).
(Apply adapt_int_inv; Auto).

Replace (cls_of_int
          (TCs Int_K
            (ext_ik V ip (cv_skel (cl_term V (cls_of_int ip)))
              (int_typ v ip (cv_skel (cl_term V (cls_of_int ip))))) ip)) with (
class_env (cons ? V e0)).
(Apply class_typ_ord with s2; Auto).
Discriminate.

Discriminate.

Simpl.
Unfold 1 cls_of_int ext_ik.
Rewrite -> adapt_class_equal0.
Pattern (cl_term V (class_env e0)) .
(Apply class_typ_ord with s1; Elim adapt_class_equal0; Simpl; Auto).
Rewrite -> adapt_class_equal0.
(Elim skel_sound with e0 V (Srt s1); Simpl; Auto).
(Elim adapt_class_equal0; Auto).

Unfold int_cons skel_int.
Replace (cls_of_int
          (TCs Int_K
            (ext_ik V ip ?
              (int_typ v ip (cv_skel (cl_term V (cls_of_int ip))))) ip)) with (
class_env (cons ? V e0)).
(Elim skel_sound with (cons ? V e0) Ur (Srt s2); Simpl; Auto).

Simpl.
Unfold ext_ik.
Rewrite -> adapt_class_equal0.
Unfold cls_of_int.
(Elim class_sound with e0 v V (Srt s1); Auto).
Simpl.
(Elim adapt_class_equal0; Auto).

Simpl.
(Elim adapt_class_equal0; Auto).

Unfold Pi in H3.
(Apply H3; Auto).
(Apply int_typ_cr; Auto).

Discriminate H5.

Apply sn_prod.
(Apply H1 with ip; Auto).

Apply sn_subst with (Ref O).
Unfold subst.
Rewrite -> int_term_subst.
Inversion H4.
Apply H3 with (def_cons T0 ip).
Unfold def_cons int_cons.
Apply Build_int_adapt.
(Apply int_cs; Auto).
(Apply (var_in_cand O (int_typ T0 ip PROP)); Auto).
Exact (int_typ_cr T0 ip int_can_adapt0 PROP).

Red.
(Apply Tfa_cs; Auto).
Unfold ext_ik.
(Elim (cl_term T0 (cls_of_int ip)); Auto).

Unfold ext_ik.
Rewrite -> adapt_class_equal0.
Unfold cls_of_int.
Simpl.
Pattern (cl_term T0 (class_env e0)) .
(Apply class_typ_ord with s1; Simpl; Elim adapt_class_equal0; Auto).
Rewrite -> adapt_class_equal0.
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
(Elim adapt_class_equal0; Auto).

(Cut (typ e0 U (Srt s)); Auto).
Intros.
(Apply eq_cand_incl with (int_typ U ip PROP); Auto).
Replace PROP with (skel_int U ip).
Inversion H5.
(Apply conv_int_typ with e0 (Srt s); Auto).
(Apply class_typ_ord with s; Auto).
Discriminate.

Discriminate.

Unfold skel_int.
Inversion H5.
Rewrite -> adapt_class_equal0.
(Elim skel_sound with e0 U (Srt s); Simpl; 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 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 int_cons ext_ik.
(Elim (cl_term a (cls_of_int (def_intp l))); Auto).
Save.


  Lemma def_adapt: (e:env)(wf e)->(k:nat)(int_adapt e (def_intp e) (def_intt e k)).
(Induction e; Simpl; Intros).
(Apply Build_int_adapt; Auto).

Inversion_clear H0.
(Cut (wf l); Intros).
(Elim H with (S k); Intros; Auto).
Unfold def_cons int_cons.
(Apply Build_int_adapt; Auto).
(Apply int_cs; Auto).
(Apply (var_in_cand k (int_typ a (def_intp l) PROP)); Auto).
Change (is_can PROP (int_typ a (def_intp l) PROP)).
(Apply int_typ_cr; Auto).

Unfold ext_ik.
Rewrite -> adapt_class_equal0.
Pattern (cl_term a (class_env l)) .
(Apply class_typ_ord with s; Auto).

Simpl.
Unfold ext_ik.
Rewrite -> adapt_class_equal0.
Pattern (cl_term a (class_env l)) .
(Apply class_typ_ord with s; Unfold cls_of_int;
 Elim adapt_class_equal0; Auto).
Simpl.
Rewrite -> adapt_class_equal0.
(Elim skel_sound with l a (Srt s); Auto).
(Simpl; Auto).
(Elim adapt_class_equal0; Auto).

(Apply typ_wf with a (Srt s); 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 str_norm: (e:env)(t,T:term)(typ e t T)->(sn t).
Intros.
(Cut (is_can PROP (int_typ T (def_intp e) PROP)); Auto).
(Simpl; Intros).
Cut (int_typ T (def_intp e) PROP t).
(Elim H0; Auto).

Elim id_int_term with e t O.
(Apply int_sound with e; Auto).
Apply def_adapt.
(Apply typ_wf with t T; Auto).

Apply int_typ_cr;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 str_norm with e (Srt x) ;Auto).

Rewrite -> H0.
(Red;Apply Acc_intro;Intros).
Inversion_clear H1.
Save.


13/02/97, 13:20