Int_typ.v
Require Termes.
Require Conv.
Require Types.
Require Class.
Require Can.
(* Interpretations des variables de type *)
Inductive
Int_K: Type :=
iK: (s:skel)(Can s) -> Int_K
| iT: Int_K.
Definition
intP:=(TList Int_K).
Definition
class_of_ik :=
[ik:Int_K]Cases ik of
(iK s _) => (Knd s)
| iT => (Typ PROP)
end.
Definition
cls_of_int: intP->cls := (Tmap ? ? class_of_ik).
Definition
ext_ik := [T:term][ip:intP][s:skel][C:(Can s)]
Cases (cl_term T (cls_of_int ip)) of
(Knd _) => (iK s C)
| _ => iT
end.
Definition
int_cons := [T:term][ip:intP][s:skel][C:(Can s)]
(TCs ? (ext_ik T ip s C) ip).
Definition
def_cons: term->intP->intP :=
[T:term][I:intP](int_cons T I ?
(default_can (cv_skel (cl_term T (cls_of_int I))))).
Definition
skel_int := [t:term][I:intP]
(typ_skel (cl_term t (cls_of_int I))).
Lemma
ins_in_cls: (c:class)(y:Int_K)(k:nat)(ipe,ipf:intP)
(class_of_ik y)==c
->(TIns Int_K y k ipe ipf)
->(TIns ? c k (cls_of_int ipe) (cls_of_int ipf)).
Unfold cls_of_int.
Induction 1.
(Induction 1; Simpl; Auto).
Save.
Definition
coerce_CR: (s:skel)Int_K->(Can s) :=
[s:skel][i:Int_K]Cases i of
(iK si Ci) =>
Case (EQ_skel si s) of
[y:si===s]<[s:skel][_:si===s](Can s)>Case y of Ci end
[_:(notT si===s)](default_can s)
end
| _ => (default_can s)
end.
Lemma
extr_eq: (P:(s:skel)(Can s)->Prop)(s:skel)(c:(Can s))
(i:Int_K)(i==(iK s c))->(P s c)->(P s (coerce_CR s i)).
Intros.
Unfold coerce_CR.
Rewrite -> H.
Elim (EQ_skel s s).
Intro.
Change ([s0:skel]
[e:(identityT ? s s0)]
(P s0 <[s1:skel][_:(identityT ? s s1)](Can s1)>Case e of c
end) s y).
(Elim y; Auto).
(Induction 1; Auto).
Save.
Lemma
eq_can_extr: (s,si:skel)(X,Y:(Can s))(eq_can s X Y)
->(eq_can si (coerce_CR si (iK s X)) (coerce_CR si (iK s Y))).
Unfold coerce_CR .
Intros.
Elim (EQ_skel s si);Auto.
(Induction y;Auto).
Save.
Hint eq_can_extr.
Lemma
simpl_eq_extr: (s:skel)(X,Y:(Can s))
(eq_can s X Y)==(eq_can s (coerce_CR s (iK s X)) (coerce_CR s (iK s Y))).
Intros.
Unfold coerce_CR.
Elim (EQ_skel s s).
Intros.
Change ([s0:skel]
[e:s===s0]
(eq_can s X Y)
==(eq_can s0 <[s0:skel][_:s===s0](Can s0)>Case e of X
end
<[s0:skel][_:s===s0](Can s0)>Case e of Y
end) s y).
(Elim y; Auto).
(Induction 1; Auto).
Save.
Lemma
inv_eq_int: (sx,sy:skel)(X,X1:(Can sx))(Y,Y1:(Can sy))
(iK sx X)==(iK sy Y)->(iK sx X1)==(iK sy Y1)
->(eq_can sx X X1)==(eq_can sy Y Y1).
Intros.
Rewrite -> simpl_eq_extr.
(Rewrite -> H; Rewrite -> H0).
Replace sx with sy.
(Elim simpl_eq_extr; Auto).
Injection H;Auto.
Save.
Inductive
ik_eq: Int_K->Int_K->Prop :=
eqi_K: (s:skel)(X,Y:(Can s))
(eq_can s X X)->(eq_can s Y Y)->(eq_can s X Y)
->(ik_eq (iK s X) (iK s Y))
| eqi_T: (ik_eq iT iT).
Hint eqi_K eqi_T.
Lemma
iki_K: (s:skel)(C:(Can s))(eq_can s C C)->(ik_eq (iK s C) (iK s C)).
Auto.
Save.
Hint iki_K.
Definition
int_eq_can: intP->intP->Prop := (Tfor_all2 ? ? ik_eq).
Definition
int_inv := [i:intP](int_eq_can i i).
Hint Unfold int_eq_can int_inv.
Lemma
ins_int_inv: (e,f:intP)(k:nat)(y:Int_K)(TIns ? y k e f)
->(int_inv f)->(int_inv e).
Unfold int_inv int_eq_can.
(Induction 1; Intros; Auto).
(Inversion_clear H0; Auto).
(Inversion_clear H2; Auto).
Save.
Lemma
int_inv_int_eq_can: (i:intP)(int_inv i)->(int_eq_can i i).
Auto.
Save.
Hint int_inv_int_eq_can.
Lemma
int_eq_can_cls: (i,i':intP)(int_eq_can i i')
->(cls_of_int i)==(cls_of_int i').
Unfold cls_of_int.
(Induction 1; Simpl; Intros; Auto).
(Inversion_clear H0; Simpl; Intros; Elim H2; Auto).
Save.
Fixpoint
int_typ [T:term]: intP->(s:skel)(Can s) :=
[ip:intP][s:skel]Cases T of
(Srt _) => (default_can s)
| (Ref n) => (coerce_CR s (Tnth_def ? (iK PROP sn) ip n))
| (Abs A t) => Cases (cl_term A (cls_of_int ip)) of
(Knd _) =>
<[s0:skel](Can s0)>Cases s of
(PROD s1 s2) => [C:(Can s1)](int_typ t (TCs ? (iK s1 C) ip) s2)
| PROP => (default_can PROP)
end
| (Typ _) => (int_typ t (def_cons A ip) s)
| _ => (default_can s)
end
| (App u v) => Cases (cl_term v (cls_of_int ip)) of
Trm => (int_typ u ip s)
| (Typ sv) => ((int_typ u ip (PROD sv s)) (int_typ v ip sv))
| _ => (default_can s)
end
| (Prod A B) => <[s0:skel](Can s0)>Cases s of
PROP => ([s:skel]
(Pi s (int_typ A ip PROP)
[C:(Can s)](int_typ B (int_cons A ip s C) PROP))
(cv_skel (cl_term A (cls_of_int ip))))
| s1 => (default_can s1)
end
end.
13/02/97, 13:20