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