Library Int_stab





Require
 Export
 Int_typ.







Lemma
 int_typ_class:

  forall
 e
 t
 T
,

  typ e
 t
 T
 ->

  forall
 K
 ip
,

  typ e
 T
 K
 ->

  eq_map (cls_of_int ip
) (class_env e
) ->

  typ_cls (cl_term t
 (class_env e
)) (class_of_ik (int_typ t
 ip
)).

Proof
.

induction
 1; intros
.

elim
 inv_typ_kind with
 (1:=H0).




simpl
.

unfold
 cls_of_int
 in
 H2
; rewrite
 H2
.

fold
 (cl_term (Ref v
) (class_env e
)).

replace
 (class_env e
 v
) with
 (cl_term t
 (class_env e
)).

elim
 wf_sort_lift with
 (2:=H0); trivial
; intros
.

apply
 class_sound with
 (2:=H3); auto
 with
 coc
.

constructor
; trivial
.




inversion_clear
 H0
.

subst
 t
.

rewrite
 nth_class_env with
 (1:=H4).

unfold
 lift
.

apply
 class_lift.




simpl
; fold
 Can.

rewrite
 cl_term_ext with
 (1:=H3).

rewrite
 cl_term_ext 

 with
 (t
:=M) (f
:=cons_map (cl_term T
 (class_env e
)) (cls_of_int ip
))

  (g
:=class_env (T
::e)).

2:red;destruct
 i
; simpl
; auto
 with
 coc
.

unfold
 class_env
; fold
 (class_env (T
::e)) class_env.

apply
 inv_typ_prod with
 (1:=H2); intros
.

generalize
 (fun
 ip
 => IHtyp3
 _
 ip
 H5
); clear
 IHtyp3
.

elim
 class_sound with
 (1:=H1) (2:=H5); intros
; auto
 with
 coc
.

apply
 class_type with
 (1:=H); simpl
; intros
; auto
 with
 coc
.

apply
 H7
; simpl
; auto
 10 with
 coc
.




 elim
 type_case with
 (1 := H0
); intros
.

  inversion_clear
 H3
.

  apply
 inv_typ_prod with
 (1 := H4
); intros
.

  simpl
 in
 |- *.

  specialize
 IHtyp2
 with
 (1 := H4
) (2 := H2
).

  destruct
 (int_typ u
 ip
); simpl
 in
 *; intros
.

   inversion_clear
 IHtyp2
.

   specialize
 IHtyp1
 with
 (1 := H3
) (2 := H2
).

   destruct
 (int_typ v
 ip
); simpl
 in
 *; intros
.

    inversion_clear
 IHtyp1
.

    generalize
 c
; clear
 c
.

    case
 s
; simpl
 in
 |- *; constructor
.




    inversion_clear
 IHtyp1
; simpl
 in
 |- *.

    case
 s
; simpl
 in
 |- *; constructor
.




   inversion_clear
 IHtyp2
.

   constructor
.




   discriminate
.




simpl
.

rewrite
 cl_term_ext with
 (1:=H2).

unfold
 class_env
; fold
 (class_env (T
::e)) class_env.

apply
 class_type with
 (1:=H0); intros
; auto
 with
 coc
.

case
 (cl_term T
 (class_env e
)); simpl
; constructor
.

rewrite
 class_typ with
 (1:=H0) in
 H3
.

discriminate
.

destruct
 s2
.

elim
 inv_typ_kind with
 (1:=H1).

constructor
; eapply
 typ_wf; eauto
.




elim
 type_case with
 (1:=H); intros
.

inversion_clear
 H4
.

eapply
 IHtyp1
; eauto
.




elim
 inv_typ_conv_kind with
 (2:=H1).

elim
 H4
; auto
 with
 coc
.

Qed
.




Lemma
 int_typ_class_eq:

  forall
 e
 t
 T
,

  typ e
 t
 T
 ->

  forall
 K
 ip
,

  typ e
 T
 K
 ->

  eq_map (cls_of_int ip
) (class_env e
) ->

  class_of_ik (int_typ t
 ip
) = cl_term T
 (class_env e
).

Proof
.

intros
.

specialize
 int_typ_class with
 (1:=H) (2:=H0) (3:=H1).

specialize
 class_sound with
 (1:=H) (2:=H0).

destruct
 1; intro
 ty_2
; inversion
 ty_2
; reflexivity
.

Qed
.




Opaque
 ik_lam ik_app ik_pi.







  Lemma
 int_equiv_int_typ :

   forall
 T
 i
 i'
,

   int_eq_can i
 i'
 -> ik_eq_can (int_typ T
 i
) (int_typ T
 i'
).

Proof
.

simple
 induction
 T
; simpl
 in
 |- *; fold
 Can in
 |- *; intros
; auto
 with
 coc
.

 fold
 (default_can PROP) in
 |- *; auto
 with
 coc
.

 apply
 ik_lam_ext; intros
; auto
 with
 coc
.

 apply
 ik_app_ext; auto
 with
 coc
.

 apply
 ik_pi_ext; auto
 with
 coc
.

Qed
.




  Hint
 Resolve
 int_equiv_int_typ: coc
.







 Lemma
 lift_int_typ :

   forall
 n
 T
 k
 ip
 ip'
,

   int_eq_can ip
 (del_map n
 k
 ip'
) ->

   ik_eq_can (int_typ T
 ip
) (int_typ (lift_rec n
 T
 k
) ip'
).

Proof
.

simple
 induction
 T
; intros
.

 simpl
 in
 |- *; fold
 (default_can PROP) in
 |- *; auto
 with
 coc
.

 generalize
 (H
 n0
).

   unfold
 del_map
 in
 |- *; simpl
 in
 |- *.

   elim
 (le_gt_dec k
 n0
); simpl
 in
 |- *; auto
 with
 coc
.

simpl
; apply
 ik_lam_ext; intros
; auto
 with
 coc
.

   rewrite
 class_lift.

    apply
 cl_term_ext; auto
 with
 coc
.

    red
; intros
; generalize
 (H1
 i
); unfold
 cls_of_int
, del_map
 in
 |- *.

    case
 (le_gt_dec k
 i
); destruct
 2; reflexivity
.

   rewrite
 class_lift.

    apply
 cl_term_ext; auto
 with
 coc
.

    red
; intros
; rewrite
 del_cons_map; destruct
 i
; simpl
; auto
 with
 coc
.

    generalize
 (H1
 i
); unfold
 cls_of_int
, del_map
 in
 |- *.

    case
 (le_gt_dec k
 i
); destruct
 2; reflexivity
.




simpl
; apply
 ik_app_ext; auto
 with
 coc
.




simpl
; apply
 ik_pi_ext; intros
; auto
 with
 coc
.

   rewrite
 class_lift.

    apply
 cl_term_ext; auto
 with
 coc
.

    red
; intros
; generalize
 (H1
 i
); unfold
 cls_of_int
, del_map
 in
 |- *.

    case
 (le_gt_dec k
 i
); destruct
 2; reflexivity
.

Qed
.




  Lemma
 subst_int_typ :

   forall
 e
 T
 K
,

   typ e
 T
 K
 ->

   forall
 k
 v
 ip
 ip'
,

   let
 ipv
 := del_map k
 0 ip'
 in


   let
 iv
 := int_typ v
 ipv
 in


   eq_map (cls_of_int ip
) (class_env e
) ->

   int_eq_can ip
 (ins_map k
 iv
 ip'
) ->

   typ_cls (cl_term v
 (cls_of_int ipv
)) (class_of_ik iv
) ->

   ik_eq_can (int_typ T
 ip
) (int_typ (subst_rec v
 T
 k
) ip'
).

Proof
.

simple
 induction
 1; intros
.

simpl
 in
 |- *; fold
 (default_can PROP); auto
 with
 coc
.




simpl
 in
 |- *.

generalize
 (H3
 v
).

unfold
 ins_map
 in
 |- *.

destruct
 (lt_eq_lt_dec k
 v
) as
 [[_
| eq_k_v
]| _
]; simpl
 in
 |- *; intros
;

 auto
 with
 coc
.

subst
 v
.

apply
 ik_eq_can_trans with
 (1 := H5
).

unfold
 lift
, iv
, ipv
 in
 |- *.

apply
 lift_int_typ; auto
 with
 coc
.

apply
 del_int_eq_can.

apply
 ins_int_eq_can_inv with
 k
 iv
 iv
.

eapply
 int_eq_can_right; eauto
.




simpl
; fold
 Can; clear
 H1
 H3
.

apply
 ik_lam_ext; intros
.




rewrite
 class_subst with
 (a
:=class_of_ik iv
); trivial
.

apply
 cl_term_ext.

red
; intros
; generalize
 (H7
 i
); unfold
 cls_of_int
, ins_map
 in
 |- *.

destruct
 (lt_eq_lt_dec k
 i
) as
 [[_
|_]|_]; destruct
 1; auto
 with
 coc
.




rewrite
 class_subst with
 (a
:=class_of_ik iv
); trivial
.

apply
 cl_term_ext; red
; auto
 with
 coc
.

intros
; rewrite
 ins_cons_map; destruct
 i
; simpl
; auto
 with
 coc
.

generalize
 (H7
 i
); unfold
 cls_of_int
, ins_map
 in
 |- *.

destruct
 (lt_eq_lt_dec k
 i
) as
 [[_
|_]|_]; destruct
 1; auto
 with
 coc
.




rewrite
 cl_term_ext with
 (1:=H6).

red
; intros
; apply
 H5
; simpl
; auto
 with
 coc
.




simpl
.

apply
 ik_app_ext; subst
 ipv
 iv
; eauto
 with
 coc
.




simpl
; fold
 Can.

apply
 ik_pi_ext; intros
; auto
 with
 coc
.




rewrite
 class_subst with
 (a
:=class_of_ik iv
); trivial
.

apply
 cl_term_ext.

red
; intros
; generalize
 (H5
 i
); unfold
 cls_of_int
, ins_map
 in
 |- *.

destruct
 (lt_eq_lt_dec k
 i
) as
 [[_
|_]|_]; destruct
 1; auto
 with
 coc
.




subst
 ipv
 iv
; apply
 H3
; auto
 with
 coc
.

  apply
 int_eq_can_cons_class.

  simpl
; apply
 cons_map_ext; auto
 with
 coc
.

  generalize
 H7
.

  rewrite
 cl_term_ext with
 (g
 := class_env e0
); auto
.

  apply
 class_type with
 (1 := H0
); intros
; trivial
.

  elim
 H9
 with
 s
; trivial
.




subst
 ipv
 iv
; apply
 H3
; auto
 with
 coc
.

  rewrite
 cl_term_ext with
 (1:=H4) in
 H7
.

  simpl
; auto
 with
 coc
.




unfold
 iv
, ipv
; apply
 H1
; eauto
.

Qed
.




  Lemma
 subst_int_typ0 :

   forall
 e
 T
 K
 v
 V
 ip
 ip'
,

   typ (V
::e) T
 K
 ->

   typ e
 v
 V
 ->

   eq_map (cls_of_int ip'
) (class_env e
) ->

   int_eq_can ip
 (cons_map (int_typ v
 ip'
) ip'
) ->

   ik_eq_can (int_typ T
 ip
) (int_typ (subst v
 T
) ip'
).

Proof
.

intros
.

specialize
 typ_wf with
 (1 := H
); intro
.

inversion_clear
 H3
.

specialize
 int_typ_class with
 (1 := H0
) (2 := H4
) (3 := H1
); intro
.

specialize
 class_sound with
 (1 := H0
) (2 := H4
); intro
.

assert
 (ik_eq_can (int_typ v
 ip'
) (int_typ v
 (del_map 0 0 ip'
))).

 apply
 int_equiv_int_typ.

 change
 (int_eq_can ip'
 ip'
).

 apply
 tail_int_eq_can with
 (int_typ v
 ip'
) (int_typ v
 ip'
) .

 eapply
 int_eq_can_right; eauto
.

unfold
 subst
 in
 |- *.

apply
 subst_int_typ with
 (1 := H
); auto
.

  red
; unfold
 cls_of_int
 in
 |- *; destruct
 i
; simpl
 in
 |- *; auto
 with
 coc
.

   generalize
 (H2
 0); simpl
 in
 |- *; intro
.

      replace
 (class_of_ik (ip
 0)) with
 (class_of_ik (int_typ v
 ip'
)).

    destruct
 H3
; inversion_clear
 H5
; reflexivity
.

    destruct
 H7
; reflexivity
.

    rewrite
 <- H1
.

     generalize
 (H2
 (S i
)); simpl
 in
 |- *; intro
.

     unfold
 cls_of_int
 in
 |- *.

     elim
 H7
; reflexivity
.

  red
 in
 |- *; intro
.

    specialize
 (H2
 i
); simpl
 in
 |- *.

    unfold
 ins_map
, del_map
 in
 |- *; simpl
 in
 |- *.

    destruct
 i
; simpl
 in
 |- *; auto
.

    intros
.

    apply
 ik_eq_can_trans with
 (1 := H2
) (2 := H6
).

   rewrite
 cl_term_ext with
 (g
 := class_env e
).

   generalize
 H3
; inversion_clear
 H6
; simpl
 in
 |- *; trivial
.

   exact
 H1
.

Qed
.




  Lemma
 int_typ_red1 :

   forall
 U
 V
,

   red1 U
 V
 ->

   forall
 e
 K
 ip
 ip'
,

   typ e
 U
 K
 ->

   eq_map (cls_of_int ip
) (class_env e
) ->

   int_eq_can ip
 ip'
 ->

   ik_eq_can (int_typ U
 ip
) (int_typ V
 ip'
).

Proof
.

simple
 induction
 1; intros
.

apply
 inv_typ_app with
 e
 (Abs T
 M
) N
 K
; intros
; auto
 with
 coc
.

elim
 type_case with
 e
 (Abs T
 M
) (Prod V0
 Ur
); intros
; auto
 with
 coc
.

2:discriminate.

destruct
 H6
 as
 (s
, ty_prod
).

apply
 inv_typ_prod with
 e
 V0
 Ur
 (Srt s
); intros
; auto
 with
 coc
.

apply
 inv_typ_abs with
 e
 T
 M
 (Prod V0
 Ur
); intros
; auto
 with
 coc
.

assert
 (typ e
 N
 T
); intros
.

apply
 type_conv with
 V0
 s0
; auto
 with
 coc
.

apply
 inv_conv_prod_l with
 Ur
 T0
; auto
 with
 coc
.

specialize
 int_typ_class_eq with
 (1 := H13
) (2 := H9
) (3 := H1
); intro
.




   simpl
 in
 |- *.

     rewrite
 ik_beta_redex.

    apply
 subst_int_typ0 with
 (1 := H10
) (2 := H13
); auto
 with
 coc
.

     intro
.

        rewrite
 <- H1
.

       unfold
 cls_of_int
 in
 |- *.

       elim
 (H2
 i
); reflexivity
.

    repeat
  rewrite
 cl_term_ext with
 (1 := H1
).

       rewrite
 cl_term_ext with
 (t
 := M
) (g
 := class_env (T
 :: e
));

       simpl
 in
 |- *; auto
 with
 coc
.

      apply
 int_typ_class with
 (1 := H10
) (2 := H11
); simpl
 in
 |- *;

       auto
 with
 coc
.

     rewrite
 cl_term_ext with
 (1 := H1
); auto
.




 apply
 inv_typ_abs with
 e
 M
 N
 K
; intros
; auto
 with
 coc
.

   simpl
 in
 |- *; fold
 Can in
 |- *.

   apply
 ik_lam_ext; auto
 with
 coc
.

   rewrite
 cl_term_ext with
 (t
 := M
) (1 := H3
).

     rewrite
 class_red with
 (1 := H5
) (U
 := M'
); auto
 with
 coc
.

    apply
 cl_term_ext.

    apply
 trans_eq_map with
 (cls_of_int ip
); auto
 with
 coc
.




 apply
 inv_typ_abs with
 e
 N
 M
 K
; intros
; auto
 with
 coc
.

   simpl
 in
 |- *; fold
 Can in
 |- *.

   apply
 ik_lam_ext; intros
; auto
 with
 coc
.

  rewrite
 <- H9
.

     rewrite
 cl_term_ext with
 (1 := H3
).

     rewrite
 cl_term_ext with
 (t
 := M
) (g
 := class_env (N
 :: e
)).

     2:simpl; auto
 with
 coc
.

     rewrite
 class_red with
 (1 := H6
) (U
 := M'
); auto
 with
 coc
.

     apply
 cl_term_ext.

     simpl
; apply
 cons_map_ext; trivial
.

     apply
 trans_eq_map with
 (cls_of_int ip
); auto
 with
 coc
.

  red
; intros
; apply
 H1
 with
 (1 := H6
); auto
 with
 coc
.

    rewrite
 cl_term_ext with
 (1 := H3
) in
 H10
.

    simpl
; auto
 with
 coc
.




apply
 inv_typ_app with
 e
 M1
 M2
 K
; intros
; auto
 with
 coc
.

simpl
.

apply
 ik_app_ext; eauto
 with
 coc
.




apply
 inv_typ_app with
 e
 M1
 M2
 K
; intros
; auto
 with
 coc
.

simpl
.

apply
 ik_app_ext; eauto
 with
 coc
.




apply
 inv_typ_prod with
 e
 M1
 M2
 K
; intros
; auto
 with
 coc
.

simpl
; fold
 Can.

apply
 ik_pi_ext; intros
; auto
 with
 coc
.

rewrite
 cl_term_ext with
 (1:=H3).

rewrite
 class_red with
 (1:=H5) (U
:=N1); auto
 with
 coc
.

apply
 cl_term_ext.

apply
 trans_eq_map with
 (cls_of_int ip
); auto
 with
 coc
.

apply
 H1
 with
 (1:=H5); trivial
.




apply
 inv_typ_prod with
 e
 M1
 M2
 K
; intros
; auto
 with
 coc
.

simpl
; fold
 Can.

apply
 ik_pi_ext; intros
; auto
 with
 coc
.




  apply
 H1
 with
 (1 := H6
); auto
 with
 coc
.

   apply
 int_eq_can_cons_class.

   simpl
; apply
 cons_map_ext; auto
 with
 coc
.

   generalize
 H8
.

   rewrite
 cl_term_ext with
 (1 := H3
).

   apply
 class_type with
 (1 := H5
); intros
; trivial
.

   elim
 H10
 with
 s
; trivial
.

  apply
 H1
 with
 (1 := H6
); auto
 with
 coc
.

   rewrite
 cl_term_ext with
 (1 := H3
) in
 H8
; simpl
; auto
 with
 coc
.

Qed
.




  Lemma
 red_int_typ :

   forall
 e
 U
 V
 K
 ip
 ip'
,

   typ e
 U
 K
 ->

   eq_map (cls_of_int ip
) (class_env e
) ->

   int_eq_can ip
 ip'
 ->

   red U
 V
 -> ik_eq_can (int_typ U
 ip
) (int_typ V
 ip'
).

Proof
.

induction
 4; auto
 with
 coc
; intros
.

apply
 ik_eq_can_trans with
 (int_typ P
 ip'
); auto
 with
 coc
.

apply
 int_typ_red1 with
 e
 K
; auto
 with
 coc
.

apply
 subject_reduction with
 U
; auto
 with
 coc
.

apply
 trans_eq_map with
 (2:=H0); auto
 with
 coc
.

apply
 sym_eq_map; auto
 with
 coc
.

eapply
 int_eq_can_right; eauto
.

Qed
.




  Lemma
 conv_int_typ :

   forall
 e
 U
 V
 K
 ip
 ip'
,

   conv U
 V
 ->

   typ e
 U
 K
 ->

   typ e
 V
 K
 ->

   eq_map (cls_of_int ip
) (class_env e
) ->

   int_eq_can ip
 ip'
 ->

   ik_eq_can (int_typ U
 ip
) (int_typ V
 ip'
).

Proof
.

intros
.

elim
 church_rosser with
 U
 V
; intros
; auto
 with
 coc
.

apply
 ik_eq_can_trans with
 (int_typ x
 ip'
); auto
 with
 coc
.

apply
 red_int_typ with
 e
 K
; auto
 with
 coc
.




apply
 ik_eq_can_sym.

apply
 red_int_typ with
 e
 K
; auto
 with
 coc
.

apply
 trans_eq_map with
 (2:=H2).

apply
 sym_eq_map; auto
 with
 coc
.

eapply
 int_eq_can_right; eauto
.

Qed
.







  Lemma
 int_typ_is_can :

    forall
 t
 ip
, can_adapt ip
 -> can_interp (int_typ t
 ip
).

simple
 induction
 t
; simpl
 in
 |- *; fold
 Can in
 |- *; intros
; auto
 with
 coc
.

 fold
 (default_can PROP) in
 |- *; auto
 with
 coc
.

 apply
 ik_lam_can; auto
 with
 coc
.

 apply
 ik_app_can; auto
 with
 coc
.

 apply
 ik_pi_can; auto
 with
 coc
.

Qed
.




  Hint
 Resolve
 int_typ_is_can : coc
.