Int_stab.v
Require Termes.
Require Conv.
Require Types.
Require Class.
Require Can.
Require Int_typ.
Lemma
int_equiv_int_typ: (T:term)(i,i':intP)(int_eq_can i i')
->(s:skel)(eq_can s (int_typ T i s) (int_typ T i' s)).
(Induction T; Simpl; Intros; Auto).
Generalize n .
(Elim H; Auto).
Unfold Tnth_def.
Intros.
Apply eq_can_extr.
(Simpl; Auto).
(Destruct n; Intros; Auto).
Unfold Tnth_def.
(Inversion_clear H0; Apply eq_can_extr Orelse Simpl; Auto).
(Simpl; Auto).
Unfold def_cons int_cons ext_ik.
(Elim int_eq_can_cls with i i'; Auto).
(Elim (cl_term t (cls_of_int i)); Simpl; Auto).
(Case s; Simpl; Auto).
Unfold skel_int.
(Elim int_eq_can_cls with i i'; Auto).
(Elim (cl_term t0 (cls_of_int i)); Auto).
Intros.
Generalize (H i i' H1 (PROD s0 s)) .
Unfold skel_int.
(Simpl; Intros).
(Apply H2; Auto).
(Apply H0; Auto).
(Elim H1; Intros; Auto).
(Inversion_clear H3; Auto).
(Apply H0; Auto).
(Elim H1; Intros; Auto).
(Inversion_clear H3; Auto).
(Case s; Simpl; Auto).
Unfold int_cons ext_ik.
(Elim int_eq_can_cls with i i'; Auto).
(Apply eq_can_Pi; Auto).
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
Apply H0.
Pattern 1 3 (cl_term t (cls_of_int i)) .
(Elim (cl_term t (cls_of_int i)); Auto).
Save.
Hint int_equiv_int_typ.
Inductive
can_interp: Int_K->Prop :=
ca_K: (s:skel)(C:(Can s))(is_can s C)->(eq_can s C C)->(can_interp (iK s C))
| ca_T: (can_interp iT).
Hint ca_K ca_T.
Definition
can_adapt: intP->Prop := (Tfor_all ? can_interp).
Hint Unfold can_adapt.
Lemma
adapt_int_inv: (ip:intP)(can_adapt ip)->(int_inv ip).
(Induction 1; Simpl; Auto).
(Induction 1; Auto).
Save.
Hint adapt_int_inv.
Lemma
int_typ_cr: (t:term)(ip:intP)(can_adapt ip)
->(s:skel)(is_can s (int_typ t 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).
(Inversion_clear H0; Simpl; Auto).
(Elim (EQ_skel s0 s); Auto).
(Induction y; Auto).
Unfold def_cons int_cons ext_ik.
(Elim (cl_term t0 (cls_of_int ip)); Auto).
(Case s; Simpl; Auto).
(Elim (cl_term t1 (cls_of_int ip)); Auto).
Intros.
(Generalize (H ip H1 (PROD s0 s)) ; Simpl; Auto).
(Case s; Simpl; Auto).
(Apply is_can_Pi; Simpl; Intros; Auto).
Unfold def_cons int_cons ext_ik.
Generalize X H2 H3 .
(Elim (cl_term t0 (cls_of_int ip)); Auto).
Simpl.
Intros.
(Change (is_can PROP (int_typ t1 (TCs Int_K (iK s0 X0) ip) PROP)); Auto).
Save.
(*
Hint int_typ_cr.
*)
Lemma
nth_lift_int: (y:Int_K)(s0:skel)(ipe,ipf:intP)(n,k:nat)
(TIns ? y k ipe ipf)
-> (int_typ (lift_rec (S O) (Ref n) k) ipf s0)
==(int_typ (Ref n) ipe s0).
(Simpl; Intros).
Elim (le_gt_dec k n).
Generalize n .
(Elim H; Simpl; Auto).
(Destruct n0; Intros; Auto).
Inversion_clear y1.
Generalize n .
(Elim H; Simpl; Auto).
Intros.
Inversion_clear y0.
(Destruct n0; Intros; Auto).
Save.
Lemma
lift_int_typ: (y:Int_K)(T:term)(k:nat)(ipe,ipf:intP)(TIns ? y k ipe ipf)
->(int_inv ipf)
->(s:skel)(eq_can s (int_typ T ipe s)
(int_typ (lift_rec (S O) T k) ipf s)).
Induction T.
(Simpl; Auto).
Intros.
(Elim nth_lift_int with y s ipe ipf n k; Intros; Auto).
(Simpl; Intros).
Unfold def_cons int_cons ext_ik.
(Elim cl_term_lift with (class_of_ik y) t k (cls_of_int ipe) (cls_of_int
ipf);
Auto).
(Elim (cl_term t (cls_of_int ipe)); Auto).
(Case s; Simpl; Intros; Auto).
(Apply eq_can_trans with (int_typ (lift_rec (S O) t0 (S k))
(TCs ? (iK s0 X1) ipf) s1); Auto 10).
(Apply ins_in_cls with y; Auto).
(Simpl; Intros).
(Elim cl_term_lift with (class_of_ik y) t k (cls_of_int ipe) (cls_of_int
ipf);
Auto).
(Elim cl_term_lift with (class_of_ik y) t0 k (cls_of_int ipe) (
cls_of_int ipf); Auto).
(Elim (cl_term t0 (cls_of_int ipe)); Auto).
Intros.
Generalize (H k ipe ipf H1 H2 (PROD s0 s)) .
(Simpl; Intros).
(Apply H3; Auto).
Apply int_equiv_int_typ.
Apply int_inv_int_eq_can.
(Apply ins_int_inv with ipf k y; Auto).
(Apply ins_in_cls with y; Auto).
(Apply ins_in_cls with y; Auto).
(Simpl; Intros).
(Case s; Simpl; Intros; Auto).
Unfold def_cons int_cons ext_ik.
(Elim cl_term_lift with (class_of_ik y) t k (cls_of_int ipe) (cls_of_int
ipf);
Auto).
(Apply eq_can_Pi; Auto).
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
Pattern 1 3 (cl_term t (cls_of_int ipe)) .
(Elim (cl_term t (cls_of_int ipe)); Auto; Intros).
(Apply eq_can_trans with (int_typ (lift_rec (S O) t0 (S k))
(TCs Int_K
(iK (cv_skel (cl_term t (cls_of_int ipe)))
X1) ipf) PROP); Auto 10).
(Apply ins_in_cls with y; Auto).
Save.
Inductive
int_var_sound [t:term; ip:intP]: Int_K->Prop :=
ivs_K: (s:skel)(cl_term t (cls_of_int ip))==(Typ s)
->(int_var_sound t ip (iK ? (int_typ t ip s)))
| ivs_T: (cl_term t (cls_of_int ip))==Trm
->(int_var_sound t ip iT).
Lemma
int_var_sound_lift: (t:term)(ip:intP)(i:Int_K)(int_var_sound t ip i)
->(typ_cls (cl_term t (cls_of_int ip)) (class_of_ik i)).
Intros.
(Elim H; Simpl; Intros; Rewrite -> H0; Auto).
Save.
Hint ivs_K ivs_T int_var_sound_lift.
Lemma
subst_int_typ: (v:term)(ipg:intP)(i:Int_K)
(int_var_sound v ipg i)
->(e:env)(T,K:term)(typ e T K)
->(k:nat)(ipe,ipf:intP)(TIns ? i k ipf ipe)
->(TTrunc ? k ipf ipg)
->(cls_of_int ipe)==(class_env e)
->(int_inv ipe)
->~(cl_term T (cls_of_int ipe))==Trm
->(eq_can (skel_int T ipe) (int_typ T ipe ?)
(int_typ (subst_rec v T k) ipf ?)).
(Induction 2; Intros).
(Simpl; Auto).
Unfold subst_rec.
(Elim (lt_eq_lt_dec k v0); Intros).
(Elim y; Intros).
Generalize y0 .
Clear y0 y.
(Case v0; Intros).
Inversion_clear y0.
Unfold pred.
(Elim nth_lift_int with i (skel_int (Ref (S n)) ipe) ipf ipe n k; Auto).
(Rewrite -> lift_ref_ge; Auto).
Generalize H4 H6 H7 .
Elim y0.
Clear H4 H6 H7 y y0.
(Elim H3; Simpl; Intros).
Rewrite -> lift0.
Unfold skel_int.
Simpl.
Generalize H7 .
(Inversion_clear H; Intros; Simpl in H9).
Unfold class_of_ik typ_skel.
Pattern s (coerce_CR s (iK s (int_typ v ipg s))) .
(Apply extr_eq with (int_typ v ipg s); Auto).
Generalize H6 .
(Inversion_clear H4; Intros).
(Inversion_clear H4; Auto).
(Elim H9; Auto).
(Replace (skel_int (Ref (S n)) (TCs Int_K y il)) with (skel_int (
Ref n) il);
Auto).
Rewrite -> simpl_lift.
Apply eq_can_trans with (int_typ (lift n v) l (skel_int (Ref n) il)).
(Apply H6; Auto).
(Inversion_clear H7; Auto).
(Inversion_clear H8; Auto).
Inversion_clear H8.
Apply int_equiv_int_typ.
Apply int_inv_int_eq_can.
(Apply ins_int_inv with il n i; Auto).
Unfold 2 lift.
(Apply lift_int_typ with y; Auto).
(Apply ins_int_inv with (TCs ? y il) (S n) i; Auto).
(Elim nth_lift_int with i (skel_int (Ref v0) ipe) ipf ipe v0 k; Auto).
(Rewrite -> lift_ref_lt; Auto).
Unfold skel_int.
Simpl.
Replace (cl_term M
(TCs class (cl_term T0 (cls_of_int ipe)) (cls_of_int ipe))) with (
Typ (typ_skel (cl_term M (class_env (cons ? T0 e0))))).
Unfold def_cons int_cons ext_ik.
(Elim class_subst with (class_of_ik i) (cls_of_int ipg) v T0 k (
cls_of_int ipf) (cls_of_int ipe); Auto).
Generalize H11 .
Simpl.
Generalize (refl_eqT ? (cl_term T0 (class_env e0))) .
Rewrite -> H9.
Pattern 1 (cl_term T0 (class_env e0)) .
(Apply class_typ_ord with s1; Auto; Induction 1; Auto).
Simpl.
Rewrite -> H12.
Replace (typ_skel
(cl_term M
(TCs class (cl_term T0 (class_env e0)) (class_env e0)))) with (
skel_int M (TCs Int_K iT ipe)).
Intros.
(Apply H6; Auto).
Simpl.
Elim H12.
(Elim skel_sound with e0 T0 (Srt s1); Auto).
(Unfold cls_of_int; Simpl; Elim H9; Auto).
Unfold cls_of_int.
Simpl.
(Red; Intros; Apply H13).
Elim H12.
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
Elim H9.
Unfold cls_of_int.
Rewrite -> H14.
Auto.
Elim H12.
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
(Unfold skel_int cls_of_int; Simpl; Auto; Elim H9; Auto).
Simpl.
Intros.
Replace (typ_skel
(cl_term M
(TCs class (Knd (cv_skel (cl_term T0 (class_env e0))))
(class_env e0)))) with (skel_int M
(TCs Int_K
(iK
(cv_skel
(cl_term T0 (class_env e0)))
X2) ipe)).
(Apply eq_can_trans with (int_typ M
(TCs Int_K
(iK (cv_skel (cl_term T0 (class_env e0)))
X2) ipe)
(skel_int M
(TCs Int_K
(iK
(cv_skel (cl_term T0 (class_env e0)))
X2) ipe))); Auto).
(Apply H6; Auto).
Unfold cls_of_int.
Simpl.
Elim H12.
(Elim H9; Auto).
Unfold cls_of_int.
Simpl.
Elim H9.
Unfold cls_of_int.
(Red; Intros; Apply H13).
Elim H9.
Unfold cls_of_int.
(Rewrite -> H17; Auto).
Unfold skel_int.
Unfold cls_of_int.
Simpl.
(Elim H9; Auto).
(Apply ins_in_cls with i; Auto).
Unfold cls_of_int.
(Elim H8; Simpl; Auto).
Generalize H11 .
Simpl.
Rewrite -> H9.
(Replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0)); Auto).
(Elim class_sound with (cons ? T0 e0) M U (Srt s2); Auto; Intros).
(Elim H12; Auto).
(Elim type_case with e0 u (Prod V Ur); Intros; Auto).
Inversion_clear H10.
(Apply inv_typ_prod with e0 V Ur (Srt x); Auto; Intros).
Unfold skel_int.
Simpl.
(Elim class_subst with (class_of_ik i) (cls_of_int ipg) v u k (
cls_of_int ipf) (cls_of_int ipe); Auto).
Cut (eqT ? (cl_term u (cls_of_int ipe))
(Typ (typ_skel (cl_term u (cls_of_int ipe))))).
Intro.
Rewrite -> H14.
(Elim class_subst with (class_of_ik i) (cls_of_int ipg) v v0 k (
cls_of_int ipf) (cls_of_int ipe); Auto).
Rewrite -> H7.
Generalize (refl_eqT ? (cl_term v0 (class_env e0))) .
Pattern 1 (cl_term v0 (class_env e0)) (cl_term V (class_env e0)) .
(Elim class_sound with e0 v0 V (Srt s1); Auto; Intros).
Elim H15.
Replace (typ_skel
<class>Case (typ_skel (cl_term u (class_env e0))) of
(Typ (typ_skel (cl_term u (class_env e0))))
[_:skel]
[_:skel](Typ (typ_skel (cl_term u (class_env e0))))
end) with (skel_int u ipe).
(Apply H4; Auto).
Rewrite -> H14.
Discriminate.
Unfold skel_int.
Elim H7.
(Case (typ_skel (cl_term u (cls_of_int ipe))); Auto).
Elim H15.
(Elim skel_sound with e0 u (Prod V Ur); Auto).
(Cut (eqT ? (cl_term V (class_env e0)) (Knd s)); Intros).
(Cut (eqT ?
(cl_term Ur
(TCs class (cl_term V (class_env e0)) (class_env e0)))
(Knd (cv_skel (cl_term Ur (class_env (cons ? V e0))))));
Intros).
Simpl.
Rewrite -> H17.
Rewrite -> H16.
Simpl.
Generalize (H4 k ipe ipf H5 H6 H7 H8) .
Replace (skel_int u ipe) with (PROD s
(cv_skel
(cl_term Ur
(TCs class
(cl_term V (class_env e0))
(class_env e0))))).
(Simpl; Intros).
(Apply H18; Auto).
Rewrite -> H14.
Discriminate.
Replace s with (skel_int v0 ipe).
(Apply H2; Auto).
Rewrite -> H7.
Elim H15.
Discriminate.
Unfold skel_int.
Rewrite -> H7.
(Elim H15; Simpl; Auto).
Apply int_equiv_int_typ.
Apply int_inv_int_eq_can.
(Apply ins_int_inv with ipe k i; Auto).
Unfold skel_int.
Rewrite -> H7.
(Elim skel_sound with e0 u (Prod V Ur); Auto).
Simpl.
Rewrite -> H17.
Rewrite -> H16.
(Simpl; Auto).
Generalize (class_sound e0 u (Prod V Ur) H3 (Srt x) H11) .
Simpl.
Rewrite -> H16.
Elim H7.
Rewrite -> H14.
(Elim (cl_term Ur (TCs class (Knd s) (cls_of_int ipe))); Simpl;
Intros; Auto).
Inversion_clear H17.
Inversion_clear H17.
Replace s with (cv_skel (cl_term V (class_env e0))).
Generalize H15 .
(Elim class_sound with e0 v0 V (Srt s1); Simpl; Auto; Intros).
Inversion_clear H16.
Generalize H15 .
(Rewrite -> (skel_sound e0 v0 V); Auto).
(Elim (cl_term v0 (class_env e0)); Simpl; Intros).
Discriminate H16.
(Injection H16; Auto).
Discriminate H16.
Unfold cls_of_int.
(Elim H5; Simpl; Auto).
Unfold cls_of_int.
(Elim H6; Simpl; Auto).
Generalize H9 .
Rewrite -> H7.
Simpl.
(Elim class_sound with e0 u (Prod V Ur) (Srt x); Simpl; Auto; Intros).
(Elim H14; Auto).
Unfold cls_of_int.
(Elim H5; Simpl; Auto).
Unfold cls_of_int.
(Elim H6; Simpl; Auto).
Discriminate H10.
Unfold skel_int.
Simpl.
(Elim class_subst with (class_of_ik i) (cls_of_int ipg) v T0 k (
cls_of_int ipf) (cls_of_int ipe); Auto).
Replace (typ_skel
<class>
Case
(cl_term U
(TCs class (cl_term T0 (cls_of_int ipe)) (cls_of_int ipe)))
of
(cl_term U
(TCs class (cl_term T0 (cls_of_int ipe))
(cls_of_int ipe)))
[s:skel](Typ s)
[s2:skel]
<class>Case (cl_term T0 (cls_of_int ipe)) of
(Knd s2)
[_:skel](Knd s2)
[s1:skel](Knd (PROD s1 s2))
end
end) with PROP.
(Apply eq_can_Pi; Simpl; Intros; Auto).
(Replace eq_cand with (eq_can PROP); Auto).
Replace PROP with (skel_int T0 ipe).
(Apply H2; Auto).
Rewrite -> H7.
(Apply class_typ_ord with s1; Auto).
Discriminate.
Discriminate.
Unfold skel_int.
Rewrite -> H7.
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ U
(int_cons T0 ipe
(cv_skel (cl_term T0 (cls_of_int ipe))) X2)
PROP); Auto).
Apply int_equiv_int_typ.
Unfold int_cons ext_ik.
Pattern 1 3 (cl_term T0 (cls_of_int ipe)) .
(Elim (cl_term T0 (cls_of_int ipe)); Auto).
Apply int_equiv_int_typ.
Unfold int_cons ext_ik.
Pattern 1 3 (cl_term T0 (cls_of_int ipe)) .
(Elim (cl_term T0 (cls_of_int ipe)); Auto).
Replace PROP with (skel_int U
(int_cons T0 ipe
(cv_skel (cl_term T0 (cls_of_int ipe))) X2)).
(Apply H4; Auto).
Unfold int_cons ext_ik.
(Elim class_subst with (class_of_ik i) (cls_of_int ipg) v T0 k (
cls_of_int ipf) (cls_of_int ipe); Auto).
Unfold cls_of_int.
(Elim H5; Simpl; Auto).
Unfold cls_of_int.
(Elim H6; Simpl; Auto).
(Unfold int_cons; Auto).
Unfold int_cons ext_ik.
Unfold 1 cls_of_int.
Simpl.
Cut (eqT ? (typ_skel (cl_term T0 (class_env e0))) PROP).
Generalize X2 .
Rewrite -> H7.
Pattern (cl_term T0 (class_env e0)) .
(Apply class_typ_ord with s1; Simpl; Auto).
Intros.
Rewrite -> H13.
(Elim H7; Auto).
Intros.
(Elim H7; Auto).
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
Unfold int_cons ext_ik.
Pattern 1 (cl_term T0 (cls_of_int ipe)) .
(Elim (cl_term T0 (cls_of_int ipe)); Auto).
Replace (cls_of_int
(int_cons T0 ipe (cv_skel (cl_term T0 (cls_of_int ipe))) X2)) with (
class_env (cons ? T0 e0)).
(Apply class_typ_ord with s2; Auto).
Discriminate.
Discriminate.
Unfold cls_of_int int_cons ext_ik.
Unfold int_cons ext_ik.
Simpl.
Rewrite -> H7.
Cut (eqT ? (typ_skel (cl_term T0 (class_env e0))) PROP).
Generalize X2 .
Unfold cls_of_int.
(Replace (Tmap Int_K class class_of_ik ipe) with (cls_of_int ipe); Auto).
Rewrite -> H7.
Pattern (cl_term T0 (class_env e0)) .
(Apply class_typ_ord with s1; Simpl; Auto).
Intros.
(Rewrite -> H13; Auto).
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
Unfold skel_int.
Replace (cls_of_int
(int_cons T0 ipe (cv_skel (cl_term T0 (cls_of_int ipe))) X2)) with (
class_env (cons ? T0 e0)).
(Elim skel_sound with (cons ? T0 e0) U (Srt s2); Simpl; Auto).
Unfold int_cons ext_ik.
Unfold 1 cls_of_int.
Simpl.
Cut (eqT ? (typ_skel (cl_term T0 (class_env e0))) PROP).
Generalize X2 .
Rewrite -> H7.
Pattern (cl_term T0 (class_env e0)) .
(Apply class_typ_ord with s1; Simpl; Auto).
Intros.
Rewrite -> H13.
(Elim H7; Auto).
Intros.
(Elim H7; Auto).
(Elim skel_sound with e0 T0 (Srt s1); Simpl; Auto).
Generalize (skel_sound (cons ? T0 e0) U (Srt s2) H3) .
Simpl.
Rewrite -> H7.
(Elim (cl_term U (TCs class (cl_term T0 (class_env e0)) (class_env e0)));
Simpl; Auto).
(Elim (cl_term T0 (class_env e0)); Simpl; Auto).
Unfold cls_of_int.
(Elim H5; Simpl; Auto).
Unfold cls_of_int.
(Elim H6; Simpl; Auto).
(Apply H2; Auto).
Save.
Lemma
int_cons_equal: (ip:intP)(e:env)(cls_of_int ip)==(class_env e)
->(N:term)(s1:sort)(typ e N (Srt s1))
->(C:(Can (cv_skel (cl_term N (class_env e)))))
(cls_of_int (int_cons N ip ? C))==(class_env (cons ? N e)).
Intros.
Unfold int_cons ext_ik.
Rewrite -> H.
Simpl.
Generalize C .
Pattern (cl_term N (class_env e)) .
(Apply class_typ_ord with s1; Auto).
(Simpl; Intros).
(Elim skel_sound with e N (Srt s1); Simpl; Intros; Auto).
(Unfold cls_of_int; Simpl; Elim H; Auto).
(Unfold cls_of_int; Simpl; Elim H; Auto).
Save.
Lemma
int_typ_red1: (U,V:term)(red1 U V)
->(e:env)(K:term)(typ e U K)
->(ip:intP)(cls_of_int ip)==(class_env e)
->(int_inv ip)
->~(cl_term U (cls_of_int ip))==Trm
->(eq_can (skel_int U ip) (int_typ U ip ?) (int_typ V ip ?)).
(Induction 1; Intros).
Unfold skel_int.
(Apply inv_typ_app with e (Abs T M) N K; Intros; Auto).
(Elim type_case with e (Abs T M) (Prod V0 Ur); Intros; Auto).
Inversion_clear H7.
(Apply inv_typ_prod with e V0 Ur (Srt x); Intros; Auto).
(Apply inv_typ_abs with e T M (Prod V0 Ur); Intros; Auto).
(Cut (typ e N T); Intros).
Cut (eqT ?
(cl_term M (TCs ? (cl_term T (cls_of_int ip)) (cls_of_int ip)))
(Typ (typ_skel (cl_term M (class_env (cons ? T e)))))).
Cut (int_var_sound N ip (ext_ik T ip ? (int_typ N ip (skel_int N ip)))).
(Simpl; Unfold def_cons int_cons ext_ik; Simpl; Rewrite -> H1).
Cut (eqT ? (cl_term T (cls_of_int ip)) (cl_term T (class_env e))).
(Elim class_sound with e N T (Srt s0); Intros; Auto; Rewrite -> H18).
Simpl.
Replace (typ_skel
<class>
Case
(typ_skel (cl_term M (TCs class (Typ PROP) (class_env e))))
of
(Typ
(typ_skel
(cl_term M (TCs class (Typ PROP) (class_env e)))))
[_:skel]
[_:skel]
(Typ
(typ_skel
(cl_term M (TCs class (Typ PROP) (class_env e)))))
end) with (skel_int M (TCs Int_K iT ip)).
Unfold subst.
(Apply subst_int_typ with ip iT (cons ? T e) T0; Auto).
Unfold cls_of_int.
Simpl.
Elim H16.
(Elim H1; Auto).
(Red; Intro; Apply H3).
Simpl.
Replace (TCs class (cl_term T (cls_of_int ip)) (cls_of_int ip)) with (
cls_of_int (TCs Int_K iT ip)).
(Rewrite -> H19; Auto).
Unfold 1 cls_of_int.
Simpl.
(Elim H16; Auto).
Unfold skel_int.
Unfold cls_of_int.
Simpl.
Elim H1.
Unfold cls_of_int.
(Elim (typ_skel
(cl_term M
(TCs class (Typ PROP) (Tmap Int_K class class_of_ik ip))));
Auto).
Elim H18.
Unfold subst.
Replace (typ_skel (cl_term M (TCs class (Knd s) (class_env e)))) with (
skel_int M (TCs Int_K (iK s (int_typ N ip s)) ip)).
(Apply subst_int_typ with ip (iK s (int_typ N ip s)) (cons ? T e) T0;
Auto).
Apply ivs_K.
Generalize H16 .
Rewrite -> H1.
(Elim class_sound with e N T (Srt s0); Auto; Intros).
Discriminate H19.
(Inversion_clear H19; Auto).
Unfold cls_of_int.
Simpl.
Elim H1.
(Rewrite -> H16; Auto).
Auto 10.
Unfold cls_of_int.
Simpl.
(Red; Intro; Apply H3).
Simpl.
Rewrite -> H16.
Unfold cls_of_int.
(Rewrite -> H19; Auto).
Unfold skel_int.
Unfold cls_of_int.
Simpl.
(Elim H1; Auto).
(Elim H1; Auto).
Unfold ext_ik.
Unfold skel_int.
Generalize (ivs_T N ip) (ivs_K N ip) .
Rewrite -> H1.
(Elim class_sound with e N T (Srt s0); Auto; Intros).
Generalize H3 .
Simpl.
Rewrite -> H1.
(Replace (TCs class (cl_term T (class_env e)) (class_env e)) with (
class_env (cons ? T e)); Auto).
(Elim class_sound with (cons ? T e) M T0 (Srt s3); Auto).
(Induction 1; Auto).
(Apply type_conv with V0 s0; Auto).
(Apply inv_conv_prod_l with Ur T0; Auto).
Discriminate H7.
(Apply inv_typ_abs with e M N K; Intros; Auto).
Unfold skel_int.
Rewrite -> H3.
Simpl.
Unfold def_cons.
(Replace (TCs ? (cl_term M (class_env e)) (class_env e)) with (
class_env (cons ? M e)); Auto).
(Elim class_sound with (cons ? M e) N T (Srt s2); Auto).
Simpl.
Unfold int_cons.
Unfold ext_ik.
Rewrite -> H3.
(Elim class_red with e M M' (Srt s1); Auto).
Unfold int_cons ext_ik.
Rewrite -> H3.
(Elim class_red with e M M' (Srt s1); Auto).
Cut (eqT ? (cl_term M (cls_of_int ip)) (cl_term M (class_env e))).
(Elim (cl_term M (class_env e)); Simpl; Intros; Auto).
(Elim H3; Auto).
(Apply inv_typ_abs with e N M K; Intros; Auto).
Unfold skel_int.
Simpl.
Rewrite -> H3.
(Replace (TCs ? (cl_term M (class_env e)) (class_env e)) with (
class_env (cons ? M e)); Auto).
Replace (cl_term M (TCs class (cl_term N (class_env e)) (class_env e))) with (
Typ (typ_skel (cl_term M (class_env (cons ? N e))))).
Cut (eqT ? (cl_term N (cls_of_int ip)) (cl_term N (class_env e))).
Pattern (cl_term N (class_env e)) .
(Apply class_typ_ord with s1; Intros; Auto).
Simpl.
Replace (typ_skel
(cl_term M
(TCs class (cl_term N (class_env e)) (class_env e)))) with (
skel_int M (def_cons N ip)).
(Apply H1 with (cons term N e) T; Auto).
Unfold def_cons int_cons ext_ik.
Simpl.
Rewrite -> H3.
Unfold cls_of_int.
Simpl.
Pattern (cl_term N (class_env e)) .
(Apply class_typ_ord with s1; Intros; Auto).
Simpl.
(Elim skel_sound with e N (Srt s1); Simpl; Auto).
(Elim H3; Auto).
Simpl.
(Elim H3; Auto).
Unfold def_cons int_cons ext_ik.
Rewrite -> H3.
Pattern (cl_term N (class_env e)) .
(Apply class_typ_ord with s1; Auto).
Unfold def_cons.
(Red; Intro; Apply H5).
Simpl.
Replace (TCs class (cl_term N (cls_of_int ip)) (cls_of_int ip)) with (
cls_of_int
(int_cons N ip (cv_skel (cl_term N (cls_of_int ip)))
(default_can (cv_skel (cl_term N (cls_of_int ip)))))).
(Rewrite -> H11; Auto).
(Replace (TCs class (cl_term N (cls_of_int ip)) (cls_of_int ip)) with (
class_env (cons ? N e)); Auto).
Rewrite -> H3.
(Apply int_cons_equal with s1; Auto).
(Rewrite -> H3; Auto).
Unfold skel_int.
Replace (cls_of_int (def_cons N ip)) with (TCs class
(cl_term N (class_env e))
(class_env e)).
Auto.
Symmetry.
Unfold def_cons.
(Replace (TCs class (cl_term N (class_env e)) (class_env e)) with (
class_env (cons ? N e)); Auto).
Rewrite -> H3.
(Apply int_cons_equal with s1; Auto).
Simpl.
Intros.
Replace (typ_skel
(cl_term M
(TCs class (cl_term N (class_env e)) (class_env e)))) with (
skel_int M (TCs Int_K (iK (cv_skel (cl_term N (class_env e))) X2) ip)).
(Apply eq_can_trans with (int_typ M
(TCs Int_K
(iK (cv_skel (cl_term N (class_env e))) X2)
ip)
(skel_int M
(TCs Int_K
(iK (cv_skel (cl_term N (class_env e)))
X2) ip))); Auto).
(Apply H1 with (cons ? N e) T; Auto).
(Elim int_cons_equal with ip e N s1 X2; Auto).
Unfold cls_of_int.
Simpl.
Unfold ext_ik.
(Rewrite -> H10; Simpl; Auto).
Unfold cls_of_int.
Simpl.
(Red; Intros; Apply H5).
Simpl.
Rewrite -> H10.
Simpl.
Unfold cls_of_int.
(Rewrite -> H14; Auto).
Unfold skel_int.
Unfold cls_of_int.
Simpl.
Elim H3.
(Rewrite -> H10; Auto).
(Elim H3; Auto).
Generalize H5 .
Simpl.
Rewrite -> H3.
(Replace (TCs class (cl_term N (class_env e)) (class_env e)) with (
class_env (cons ? N e)); Auto).
(Elim class_sound with (cons ? N e) M T (Srt s2); Simpl; Intros; Auto).
(Elim H10; Auto).
(Apply inv_typ_app with e M1 M2 K; Intros; Auto).
(Elim type_case with e M1 (Prod V0 Ur); Intros; Auto).
Inversion_clear H9.
(Apply inv_typ_prod with e V0 Ur (Srt x); Intros; Auto).
Unfold skel_int.
Simpl.
Rewrite -> H3.
(Elim class_red with e M1 N1 (Prod V0 Ur); Auto).
Cut (eqT ? (cl_term M1 (class_env e))
(Typ (typ_skel (cl_term M1 (class_env e))))).
Intro.
Rewrite -> H13.
Cut (eqT ? (cl_term M2 (cls_of_int ip)) (cl_term M2 (class_env e))).
(Elim class_sound with e M2 V0 (Srt s1); Auto; Intros).
Replace (typ_skel
<class>Case (typ_skel (cl_term M1 (class_env e))) of
(Typ (typ_skel (cl_term M1 (class_env e))))
[_:skel]
[_:skel](Typ (typ_skel (cl_term M1 (class_env e))))
end) with (skel_int M1 ip).
(Apply H1 with e (Prod V0 Ur); Auto).
(Red; Intro; Apply H5).
Simpl.
(Rewrite -> H15; Auto).
Unfold skel_int.
Elim H3.
(Elim (typ_skel (cl_term M1 (cls_of_int ip))); Auto).
Generalize (H1 e (Prod V0 Ur) H6 ip H3 H4) .
Replace (skel_int M1 ip) with (PROD s
(typ_skel
<class>
Case
(typ_skel
(cl_term M1 (class_env e))) of
(Typ
(typ_skel
(cl_term M1 (class_env e))))
[_:skel][s2:skel](Typ s2)
end)).
(Simpl; Intros).
(Apply H15; Auto).
(Red; Intro; Apply H5).
Simpl.
(Rewrite -> H16; Auto).
Unfold skel_int.
Rewrite -> H3.
(Elim skel_sound with e M1 (Prod V0 Ur); Auto).
Simpl.
(Cut (eqT ? (cl_term V0 (class_env e)) (Knd s)); Intros).
(Cut (eqT ?
(cl_term Ur (TCs class (cl_term V0 (class_env e)) (class_env e)))
(Knd (cv_skel (cl_term Ur (class_env (cons ? V0 e))))));
Intros).
Rewrite -> H16.
(Rewrite -> H15; Simpl; Auto).
Generalize (class_sound e M1 (Prod V0 Ur) H6 (Srt x) H10) .
Simpl.
Rewrite -> H15.
Rewrite -> H13.
(Elim (cl_term Ur (TCs class (Knd s) (class_env e))); Intros; Auto).
Inversion_clear H16.
Inversion_clear H16.
Generalize H14 .
Rewrite -> H3.
(Elim class_sound with e M2 V0 (Srt s1); Intros; Auto).
Discriminate H15.
(Inversion_clear H15; Auto).
(Elim H3; Auto).
Generalize H5 .
Simpl.
Rewrite -> H3.
(Elim class_sound with e M1 (Prod V0 Ur) (Srt x); Intros; Auto).
(Elim H13; Auto).
Discriminate H9.
(Cut ~(eqT ? (cl_term M1 (cls_of_int ip)) Trm); Intros).
(Apply inv_typ_app with e M1 M2 K; Intros; Auto).
(Elim type_case with e M1 (Prod V0 Ur); Intros; Auto).
Inversion_clear H10.
(Apply inv_typ_prod with e V0 Ur (Srt x); Intros; Auto).
Unfold skel_int.
Simpl.
Rewrite -> H3.
(Elim class_red with e M2 N2 V0; Auto).
Cut (eqT ? (cl_term M1 (class_env e))
(Typ (typ_skel (cl_term M1 (class_env e))))).
Intro.
Rewrite -> H14.
Cut (eqT ? (cl_term M2 (cls_of_int ip)) (cl_term M2 (class_env e))).
(Elim class_sound with e M2 V0 (Srt s1); Auto; Intros).
Cut (eq_can ?
(int_typ M1 ip
(PROD s
(typ_skel
<class>Case (typ_skel (cl_term M1 (class_env e))) of
(Typ (typ_skel (cl_term M1 (class_env e))))
[_:skel][s2:skel](Typ s2)
end)))
(int_typ M1 ip
(PROD s
(typ_skel
<class>Case (typ_skel (cl_term M1 (class_env e))) of
(Typ (typ_skel (cl_term M1 (class_env e))))
[_:skel][s2:skel](Typ s2)
end)))).
(Simpl; Intros).
(Apply H16; Auto).
Replace s with (skel_int M2 ip).
(Apply H1 with e V0; Auto).
Rewrite -> H15.
Discriminate.
Unfold skel_int.
Generalize H15 .
Rewrite -> H3.
(Elim class_sound with e M2 V0 (Srt s1); Intros; Auto).
Discriminate H17.
(Inversion_clear H17; Auto).
Auto.
(Elim H3; Auto).
Generalize H6 .
Rewrite -> H3.
(Elim class_sound with e M1 (Prod V0 Ur) (Srt x); Auto; Intros).
(Elim H14; Auto).
Discriminate H10.
(Red; Intros; Apply H5).
Simpl.
(Rewrite -> H6; Auto).
(Apply inv_typ_prod with e M1 M2 K; Intros; Auto).
Unfold skel_int.
Simpl.
Rewrite -> H3.
(Elim class_red with e M1 N1 (Srt s1); Auto).
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
(Cut (eqT ? (skel_int M1 ip) PROP); Intros).
Pattern (cl_term M2 (class_env (cons term M1 e))) .
(Apply class_typ_ord with s2; Auto).
(Elim skel_sound with (cons ? M1 e) M2 (Srt s2); Simpl; Auto).
(Apply eq_can_Pi; Auto).
Elim H9.
(Apply H1 with e (Srt s1); Auto).
Rewrite -> H3.
(Apply class_typ_ord with s1; Auto).
Discriminate.
Discriminate.
(Simpl; Intros).
Unfold int_cons ext_ik.
Rewrite -> H3.
(Elim class_red with e M1 N1 (Srt s1); Auto).
Pattern 1 3 (cl_term M1 (class_env e)) .
(Elim (cl_term M1 (class_env e)); Auto).
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
Pattern (cl_term M1 (class_env e)) .
(Apply class_typ_ord with s1; Auto).
Simpl.
(Apply eq_can_Pi; Auto).
Elim H9.
(Apply H1 with e (Srt s1); Auto).
Rewrite -> H3.
(Apply class_typ_ord with s1; Auto).
Discriminate.
Discriminate.
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
Apply int_equiv_int_typ.
Unfold int_cons ext_ik.
Rewrite -> H3.
(Elim class_red with e M1 N1 (Srt s1); Auto).
(Elim (cl_term M1 (class_env e)); Auto).
Simpl.
(Apply eq_can_Pi; Auto).
Elim H9.
(Apply H1 with e (Srt s1); Auto).
Rewrite -> H3.
(Apply class_typ_ord with s1; Auto).
Discriminate.
Discriminate.
(Simpl; Intros).
Change (eq_can PROP
(int_typ M2
(int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X1)
PROP)
(int_typ M2
(int_cons N1 ip (cv_skel (cl_term M1 (class_env e))) X2)
PROP)).
Unfold int_cons ext_ik.
Rewrite -> H3.
(Elim class_red with e M1 N1 (Srt s1); Auto).
Pattern 1 3 (cl_term M1 (class_env e)) .
(Elim (cl_term M1 (class_env e)); Auto).
Unfold skel_int.
Rewrite -> H3.
(Elim skel_sound with e M1 (Srt s1); Simpl; Auto).
(Apply inv_typ_prod with e M1 M2 K; Intros; Auto).
Unfold skel_int.
Simpl.
Rewrite -> H3.
(Elim class_red with (cons ? M1 e) M2 N2 (Srt s2); Auto).
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
Pattern (cl_term M2 (class_env (cons term M1 e))) .
(Apply class_typ_ord with s2; Auto).
(Elim skel_sound with (cons ? M1 e) M2 (Srt s2); Simpl; Auto).
(Apply eq_can_Pi; Auto).
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ M2
(int_cons M1 ip
(cv_skel (cl_term M1 (class_env e))) X2)
PROP); Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Replace PROP with (skel_int M2
(int_cons M1 ip
(cv_skel (cl_term M1 (class_env e))) X2)).
(Apply H1 with (cons ? M1 e) (Srt s2); Auto).
(Apply int_cons_equal with s1; Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
(Red; Intros).
Apply H5.
Simpl.
Replace (TCs class (cl_term M1 (cls_of_int ip)) (cls_of_int ip)) with (
cls_of_int (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)).
(Rewrite -> H12; Auto).
Rewrite -> H3.
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
(Apply int_cons_equal with s1; Auto).
Unfold skel_int.
Replace (cls_of_int
(int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)) with (
class_env (cons ? M1 e)).
(Elim skel_sound with (cons ? M1 e) M2 (Srt s2); Auto).
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
Symmetry.
(Apply int_cons_equal with s1; Auto).
Cut (eqT ? (cl_term M1 (cls_of_int ip)) (cl_term M1 (class_env e))).
Pattern (cl_term M1 (class_env e)) .
(Apply class_typ_ord with s1; Auto).
(Simpl; Intros).
(Apply eq_can_Pi; Auto).
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ M2 (int_cons M1 ip PROP X2) PROP);
Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Pattern 1 3 5 PROP .
Replace PROP with (skel_int M2 (int_cons M1 ip PROP X2)).
(Cut (eqT ? (cv_skel (cl_term M1 (class_env e))) PROP); Intros).
(Apply H1 with (cons ? M1 e) (Srt s2); Auto).
Generalize X2 H12 .
Change (X2:(Can PROP))
(eq_can PROP X2 X2)
->(eqT cls (cls_of_int (int_cons M1 ip PROP X2))
(class_env (cons term M1 e))).
Elim H13.
Intros.
(Apply int_cons_equal with s1; Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Replace (cls_of_int (int_cons M1 ip PROP X2)) with (class_env
(cons ? M1 e)).
(Red; Intros; Apply H5).
Simpl.
Rewrite -> H3.
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
(Rewrite -> H14; Auto).
Generalize X2 H12 .
Change (X2:(Can PROP))
(eq_can PROP X2 X2)
->(eqT cls (class_env (cons term M1 e))
(cls_of_int (int_cons M1 ip PROP X2))).
Elim H13.
Intros.
Symmetry.
(Apply int_cons_equal with s1; Auto).
Elim H3.
(Rewrite -> H9; Simpl; Auto).
Unfold skel_int.
Replace (cls_of_int (int_cons M1 ip PROP X2)) with (class_env
(cons ? M1 e)).
(Elim skel_sound with (cons ? M1 e) M2 (Srt s2); Auto).
Generalize X2 H12 .
Change (X2:(Can PROP))
(eq_can PROP X2 X2)
->(eqT cls (class_env (cons term M1 e))
(cls_of_int (int_cons M1 ip PROP X2))).
Replace PROP with (cv_skel (cl_term M1 (class_env e))).
Intros.
Symmetry.
(Apply int_cons_equal with s1; Auto).
Elim H3.
(Rewrite -> H9; Auto).
Intros.
Simpl.
(Apply eq_can_Pi; Auto).
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ M2
(int_cons M1 ip
(cv_skel (cl_term M1 (class_env e))) X2)
PROP); Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
Replace PROP with (skel_int M2
(int_cons M1 ip
(cv_skel (cl_term M1 (class_env e))) X2)).
(Apply H1 with (cons ? M1 e) (Srt s2); Auto).
(Apply int_cons_equal with s1; Auto).
Unfold int_cons ext_ik.
(Elim (cl_term M1 (cls_of_int ip)); Auto).
(Red; Intros).
Apply H5.
Simpl.
Replace (TCs class (cl_term M1 (cls_of_int ip)) (cls_of_int ip)) with (
cls_of_int (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)).
(Rewrite -> H13; Auto).
Rewrite -> H3.
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
(Apply int_cons_equal with s1; Auto).
Unfold skel_int.
Replace (cls_of_int
(int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)) with (
class_env (cons ? M1 e)).
(Elim skel_sound with (cons ? M1 e) M2 (Srt s2); Auto).
(Replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (
class_env (cons ? M1 e)); Auto).
Symmetry.
(Apply int_cons_equal with s1; Auto).
(Elim H3; Auto).
Save.
Lemma
red_int_typ: (e:env)(U,K:term)(typ e U K)
->(ip:intP)(cls_of_int ip)==(class_env e)
->(int_inv ip)
->~(cl_term U (class_env e))==Trm
->(V:term)(red U V)
->(eq_can (skel_int U ip) (int_typ U ip ?) (int_typ V ip ?)).
(Induction 5; Auto; Intros).
(Apply eq_can_trans with (int_typ P ip (skel_int U ip)); Auto).
Replace (skel_int U ip) with (skel_int P ip).
(Apply int_typ_red1 with e K; Auto).
(Apply subject_reduction with U; Auto).
Rewrite -> H0.
(Elim class_red with e U P K; Auto).
Unfold skel_int.
Rewrite -> H0.
(Elim skel_sound with e U K; Auto).
(Elim skel_sound with e P K; Auto).
(Apply subject_reduction with U; Auto).
Save.
Lemma
conv_int_typ: (e:env)(U,V,K:term)(conv U V)
->(typ e U K)->(typ e V K)
->(ip:intP)(cls_of_int ip)==(class_env e)
->(int_inv ip)
->~(cl_term U (class_env e))==Trm
->(eq_can (skel_int U ip) (int_typ U ip ?) (int_typ V ip ?)).
Intros.
(Elim church_rosser with U V; Intros; Auto).
(Apply eq_can_trans with (int_typ x ip (skel_int U ip)); Auto).
(Apply red_int_typ with e K; Auto).
Apply eq_can_sym.
Replace (skel_int U ip) with (skel_int V ip).
(Apply red_int_typ with e K; Auto).
(Rewrite -> (class_red e V x K); Auto).
(Elim class_red with e U x K; Auto).
Unfold skel_int.
Rewrite -> H2.
(Elim skel_sound with e U K; Auto).
(Elim skel_sound with e V K; Auto).
Save.
13/02/97, 13:20