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
.