Library Strong_Norm





Require
 Export
 Types
.

Require
 Import
 Int_term.

Require
 Import
 Int_stab.

Require
 Import
 Int_typ.




  Definition
 sem_typ it
 ip
 t
 T
 :=

    coerce_CR PROP (int_typ T
 ip
) (int_term t
 it
).




  Definition
 trm_in_int (e
:env) (ip
:intP) (itt
:intt) :=

    forall
 n
 T
, item T
 e
 n
 ->

     coerce_CR PROP (int_typ T
 (del_map (S n
) 0 ip
)) (itt
 n
).




  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 : forall
 i
, cls_of_int ip
 i
 = class_env e
 i
}.




Lemma
 int_adapt_cons :

  forall
 e
 ip
 it
 i
 T
 n
,

  wf
 (T
::e) ->

  int_adapt e
 ip
 it
 ->

  coerce_CR PROP (int_typ T
 ip
) n
 ->

  can_interp i
 ->

  class_of_ik i
 = cl_term T
 (class_env e
) ->

  int_adapt (T
::e) (cons_map i
 ip
) (cons_map n
 it
).

Proof
.

intros
.

destruct
 H0
 as
 (trm_adapt
, can_adapt
, eq_cls
).

constructor
; intros
; auto
 with
 coc
.

 red
 in
 |- *; intros
.

   inversion_clear
 H0
; simpl
 in
 |- *.

  apply
 eq_cand_incl with
 (coerce_CR PROP (int_typ T
 ip
)); trivial
.

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

    fold
 (eq_can PROP) in
 |- *; apply
 eq_can_coerce.

    apply
 int_equiv_int_typ.

    change
 (int_eq_can ip
 ip
) in
 |- *; auto
 with
 coc
.

  exact
 (trm_adapt
 _
 _
 H4
).

 unfold
 cls_of_int
 in
 |- *.

   destruct
 i0
; simpl
 in
 |- *; auto
 with
 coc
.

   exact
 (eq_cls
 i0
).

Qed
.




  Lemma
 int_var_sound : forall
 t
 e
 n
 ip
 it
,

    item_lift
 t
 e
 n
 ->

    int_adapt e
 ip
 it
 ->

    coerce_CR PROP (int_typ t
 ip
) (it
 n
).

Proof
.

intros
.

destruct
 H
 as
 (A
, itm_A
); subst
 t
.

apply
 eq_cand_incl

 with
 (coerce_CR PROP (int_typ A
 (del_map (S n
) 0 ip
))).

apply
 eq_can_coerce.

unfold
 lift
.

apply
 lift_int_typ.

destruct
 H0
; auto
 with
 coc
.




apply
 (adapt_trm_in_int _
 _
 _
 H0
); trivial
.

Qed
.




  Lemma
 interp_is_sound :

   forall
 e
 t
 T
,

   typ e
 t
 T
 ->

   forall
 ip
 it
, int_adapt e
 ip
 it
 ->

   sem_typ it
 ip
 t
 T
.

Proof
.

unfold
 sem_typ
, int_term
.

simple
 induction
 1;

 unfold
 int_typ
, int_term_rec
; fold
 int_term_rec int_typ Can;

 intros
; try
 rewrite
 coerce_refl.

simpl
.

red
 in
 |- *; apply
 Acc_intro; intros
.

inversion_clear
 H2
.




simpl
; rewrite
 lift0; rewrite
 <- minus_n_O.

apply
 int_var_sound with
 e0
; trivial
.




specialize
 H1
 with
 (1 := H6
); rewrite
 coerce_refl in
 H1
.

case
 H6
; intros
 trm_adapt
 typ_adapt
 eq_cls
.

apply
 ik_pi_intro; intros
; auto
 with
 coc
.

unfold
 subst
 in
 |- *.

rewrite
 int_term_subst; auto
 with
 coc
.

apply
 H5
.

apply
 int_adapt_cons; trivial
.

apply
 wf_var with
 s1
; trivial
.

rewrite
 <- cl_term_ext with
 (1:=eq_cls); trivial
.

rewrite
 cl_term_ext with
 (1 := eq_cls
).

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




specialize
 H1
 with
 (1:=H4).

specialize
 H3
 with
 (1:=H4).

destruct
 H4
 as
 (trm_ad
, can_ad
, same_cls
).

elim
 type_case with
 e0
 u
 (Prod V
 Ur
); intros
; auto
 with
 coc
.

2:discriminate.

destruct
 H4
 as
 (s
, ty_prod
).

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




apply
 eq_cand_incl

  with
 (coerce_CR PROP (int_typ Ur
 (cons_map (int_typ v
 ip
) ip
))).

apply
 eq_can_coerce.

apply
 subst_int_typ0 with
 (1:=H5) (2:=H0); auto
 with
 coc
.




apply
 ik_pi_elim with
 (1 := H3
); auto
 with
 coc
.

rewrite
 cl_term_ext with
 (1:=same_cls).

apply
 int_typ_class_eq with
 (1:=H0) (2:=H4) (3:=same_cls); intro
.




simpl
.

specialize
 H1
 with
 (1:=H4); rewrite
 coerce_refl in
 H1
.

rewrite
 coerce_refl in
 H3
; simpl
 in
 H3
.

apply
 sn_prod; trivial
.




apply
 sn_subst with
 (Ref 0).

unfold
 subst
 in
 |- *.

rewrite
 int_term_subst.

apply
 H3
 with
 (cons_map (def_ik (cl_term T0
 (class_env e0
))) ip
).

apply
 int_adapt_cons; auto
 with
 coc
.

 apply
 wf_var with
 s1
; trivial
.




 apply
 var_in_cand with
 (X
 := coerce_CR PROP (int_typ T0
 ip
)).

 elim
 H4
; auto
 with
 coc
.




 unfold
 def_ik
.

 apply
 class_type with
 (1 := H0
); reflexivity
.




apply
 eq_cand_incl with
 (coerce_CR PROP (int_typ U
 ip
)); auto
 with
 coc
.

apply
 eq_can_coerce.

destruct
 H5
 as
 (_
,can_adapt,eq_cls).

apply
 conv_int_typ with
 e0
 (Srt s
); auto
 with
 coc
.

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

destruct
 H5
 as
 (s'
, ty_U
).

elim
 conv_sort with
 s'
 s
; auto
 with
 coc
.

eapply
 typ_conv_conv; eauto
.




elim
 inv_typ_conv_kind with
 e0
 V
 (Srt s
); auto
 with
 coc
.

elim
 H5
; auto
 with
 coc
.

Qed
.




  Fixpoint
 def_intp (e
 : env
) : intP :=

    match
 e
 with


    | nil => nil_intP

    | t
 :: f
 => cons_map (def_ik (cl_term t
 (class_env f
))) (def_intp f
)

    end
.




  Fixpoint
 def_intt (e
 : env
) (k
 : nat) {struct
 e
} : intt :=

    match
 e
 with


    | nil => fun
 p
 => Ref (k
 + p
)

    | _
 :: f
 => cons_map (Ref k
) (def_intt f
 (S k
))

    end
.




  Lemma
 def_intp_can : forall
 e
, can_adapt (def_intp e
).

Proof
.

simple
 induction
 e
; simpl
 in
 |- *; auto
 with
 coc
; intros
.

Qed
.




  Lemma
 def_adapt :

   forall
 e
 k
, wf
 e
 -> int_adapt e
 (def_intp e
) (def_intt e
 k
).

simple
 induction
 e
; simpl
 in
 |- *; intros
.

constructor
; auto
 with
 coc
.

red
; intros
.

apply
 var_in_cand

 with
 (X
:=coerce_CR PROP (int_typ T
 (del_map (S n
) 0 nil_intP))).

apply
 is_can_prop.

apply
 is_can_coerce.

apply
 int_typ_is_can; auto
 with
 coc
.




inversion_clear
 H0
.

assert
 (wf
 l
). eapply
 typ_wf; eauto
.

elim
 H
 with
 (S k
); intros
; auto
 with
 coc
.

constructor
.

red
; intros
.

inversion_clear
 H2
.

unfold
 del_map
; simpl
.

apply
 var_in_cand

 with
 (X
:=coerce_CR PROP (int_typ a
 (fun
 i
 => def_intp l
 i
))).

apply
 is_can_prop.

apply
 is_can_coerce.

apply
 int_typ_is_can; auto
 with
 coc
.

exact
 (adapt_trm_in_int0
 _
 _
 H3
).




red
.

destruct
 i
; intros
.

unfold
 cons_map
; simpl
.

case
 (cl_term a
 (cls_of_int (def_intp l
))); simpl
; auto
 with
 coc
.

exact
 (int_can_adapt0
 i
).




unfold
 cls_of_int
; destruct
 i
; simpl
; intros
.

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

exact
 (adapt_class_equal0
 i
).

Qed
.




  Hint
 Resolve
 def_intp_can def_adapt: coc
.




  Lemma
 def_intt_id : forall
 n
 e
 k
, def_intt e
 k
 n
 = Ref (k
 + n
).

simple
 induction
 n
; simple
 destruct
 e
; simpl
 in
 |- *; auto
 with
 coc
; intros
.

replace
 (k
 + 0) with
 k
; auto
 with
 coc
.




rewrite
 H
.

replace
 (k
 + S n0
) with
 (S (k
 + n0
)); auto
 with
 coc
.

Qed
.




  Lemma
 id_int_term : forall
 e
 t
, int_term t
 (def_intt e
 0) = t
.

unfold
 int_term
.

assert
 (forall
 e
 t
 k
, int_term_rec t
 (def_intt e
 0) k
 = t
); auto
.

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

elim
 (le_gt_dec k
 n
); intros
; auto
 with
 coc
.

rewrite
 def_intt_id.

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

rewrite
 lift_ref_ge; auto
 with
 arith
.




rewrite
 H
; rewrite
 H0
; auto
 with
 coc
.




rewrite
 H
; rewrite
 H0
; auto
 with
 coc
.




rewrite
 H
; rewrite
 H0
; auto
 with
 coc
.

Qed
.




  Theorem
 strong_norm : forall
 e
 t
 T
, typ e
 t
 T
 -> sn t
.

intros
.

set
 (CR
 := coerce_CR PROP (int_typ T
 (def_intp e
))).

assert
 (int_is_can
 : is_can _
 CR
).

   unfold
 CR
; auto
 with
 coc
.

assert
 (t_in_interp
 : CR
 t
).

elim
 id_int_term with
 e
 t
.

unfold
 CR
; apply
 interp_is_sound with
 e
; auto
 with
 coc
.

apply
 def_adapt.

apply
 typ_wf with
 t
 T
; trivial
.




apply
 incl_sn with
 (1:=int_is_can) (2:=t_in_interp).

Qed
.




  Lemma
 type_sn : forall
 e
 t
 T
, typ e
 t
 T
 -> sn T
.

intros
.

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

elim
 H0
; intros
.

apply
 strong_norm with
 e
 (Srt x
); auto
 with
 coc
.




rewrite
 H0
.

red
 in
 |- *; apply
 Acc_intro; intros
.

inversion_clear
 H1
.

Qed
.