Library Strengthen
Require
Import
Types
.
Lemma
lift_inj
: forall
n
t
u
k
, lift_rec
n
t
k
= lift_rec
n
u
k
-> t
= u
.
Proof
.
induction
n
; intros
.
repeat
rewrite
lift_rec0
in
H
; trivial
.
apply
IHn
with
k
.
rewrite
<- simpl_subst_rec
with
(p
:=k) (N
:=t); auto
with
arith
.
rewrite
<- simpl_subst_rec
with
(M
:=u) (p
:=k) (N
:=t); auto
with
arith
.
rewrite
H
; trivial
.
Qed
.
Lemma
lift_ref_inv
:
forall
n
t
k
i
,
lift_rec
n
t
k
= Ref
i
->
k
> i
/\ t
= Ref
i
\/
n
+k <= i
/\ t
= Ref
(i
-n).
Proof
.
destruct
t
; try
(intros
;discriminate
).
simpl
.
intros
k
i
.
case
(le_gt_dec
k
n0
); intros
;auto
.
injection
H
;intros
; subst
i
.
right
; split
;auto
with
arith
.
injection
H
;intros
; subst
i
.
auto
.
Qed
.
Lemma
lift_srt_inv
:
forall
n
t
k
s
,
lift_rec
n
t
k
= Srt
s
-> t
= Srt
s
.
Proof
.
destruct
t
; simpl
; intros
; try
discriminate
; trivial
.
destruct
(le_gt_dec
k
n0
); discriminate
.
Qed
.
Lemma
lift_abs_inv
:
forall
n
t
k
T
M
,
lift_rec
n
t
k
= Abs
T
M
->
(exists
T'
, lift_rec
n
T'
k
= T
) /\ (exists
M'
, lift_rec
n
M'
(S
k
) = M
).
Proof
.
destruct
t
; simpl
; intros
; try
discriminate
; trivial
.
destruct
(le_gt_dec
k
n0
); discriminate
.
injection
H
; split
.
exists
t1
;trivial
.
exists
t2
;trivial
.
Qed
.
Lemma
lift_app_inv
:
forall
n
t
k
u
v
,
lift_rec
n
t
k
= App
u
v
->
(exists
u'
, lift_rec
n
u'
k
= u
) /\ (exists
v'
, lift_rec
n
v'
k
= v
).
Proof
.
destruct
t
; simpl
; intros
; try
discriminate
; trivial
.
destruct
(le_gt_dec
k
n0
); discriminate
.
injection
H
; split
.
exists
t1
;trivial
.
exists
t2
;trivial
.
Qed
.
Lemma
lift_prod_inv
:
forall
n
t
k
T
M
,
lift_rec
n
t
k
= Prod
T
M
->
(exists
T'
, lift_rec
n
T'
k
= T
) /\ (exists
M'
, lift_rec
n
M'
(S
k
) = M
).
Proof
.
destruct
t
; simpl
; intros
; try
discriminate
; trivial
.
destruct
(le_gt_dec
k
n0
); discriminate
.
injection
H
; split
.
exists
t1
;trivial
.
exists
t2
;trivial
.
Qed
.
Lemma
red1_red1_lift_ex
:
forall
n
t
u
, red1
t
u
-> forall
k
t'
, lift_rec
n
t'
k
= t
->
exists2
u'
, red1
t'
u'
& u
=lift_rec n
u'
k
.
Proof
.
induction
1; intros
.
elim
lift_app_inv
with
(1:=H).
intros
(U'
, eqU'
) (N'
,eqN').
subst
N
.
elim
lift_abs_inv
with
(1:=eqU').
intros
(T'
,eqT') (M'
,eqM').
subst
T
M
.
rewrite
<- distr_lift_subst
.
exists
(subst
N'
M'
); auto
.
replace
t'
with
(App
(Abs
T'
M'
) N'
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
elim
lift_abs_inv
with
(1:=H0).
intros
(a
,eqa) (b
,eqb).
subst
M
N
.
elim
IHred1
with
k
a
; auto
; intros
.
subst
M'
.
exists
(Abs
x
b
); auto
with
coc
.
replace
t'
with
(Abs
a
b
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
elim
lift_abs_inv
with
(1:=H0).
intros
(a
,eqa) (b
,eqb).
subst
M
N
.
elim
IHred1
with
(S
k
) b
; auto
; intros
.
subst
M'
.
exists
(Abs
a
x
); auto
with
coc
.
replace
t'
with
(Abs
a
b
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
elim
lift_app_inv
with
(1:=H0).
intros
(a
,eqa) (b
,eqb).
subst
M1
M2
.
elim
IHred1
with
k
a
; auto
; intros
.
subst
N1
.
exists
(App
x
b
); auto
with
coc
.
replace
t'
with
(App
a
b
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
elim
lift_app_inv
with
(1:=H0).
intros
(a
,eqa) (b
,eqb).
subst
M1
M2
.
elim
IHred1
with
k
b
; auto
; intros
.
subst
N2
.
exists
(App
a
x
); auto
with
coc
.
replace
t'
with
(App
a
b
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
elim
lift_prod_inv
with
(1:=H0).
intros
(a
,eqa) (b
,eqb).
subst
M1
M2
.
elim
IHred1
with
k
a
; auto
; intros
.
subst
N1
.
exists
(Prod
x
b
); auto
with
coc
.
replace
t'
with
(Prod
a
b
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
elim
lift_prod_inv
with
(1:=H0).
intros
(a
,eqa) (b
,eqb).
subst
M1
M2
.
elim
IHred1
with
(S
k
) b
; auto
; intros
.
subst
N2
.
exists
(Prod
a
x
); auto
with
coc
.
replace
t'
with
(Prod
a
b
); auto
with
coc
.
apply
lift_inj
with
n
k
; simpl
; auto
.
Qed
.
Lemma
red_red_lift_ex
:
forall
n
t
k
u
,
red
(lift_rec
n
t
k
) u
->
exists2
u'
, red
t
u'
& u
=lift_rec n
u'
k
.
Proof
.
induction
1; intros
.
exists
t
; auto
with
coc
.
elim
IHred
;intros
.
elim
red1_red1_lift_ex
with
(1:=H0) (2:=sym_equal H2
);intros
.
exists
x0
; trivial
.
constructor
2 with
x
; trivial
.
Qed
.
Lemma
red_lift_lift_inv
:
forall
n
t
u
k
, red
(lift_rec
n
t
k
) (lift_rec
n
u
k
) -> red
t
u
.
Proof
.
intros
.
elim
red_red_lift_ex
with
(1 := H
); intros
.
rewrite
(lift_inj
_
_
_
_
H1
); trivial
.
Qed
.
Lemma
red_red_lift
:
forall
n
t
u
k
, red
t
u
-> red
(lift_rec
n
t
k
) (lift_rec
n
u
k
).
induction
1; intros
; auto
with
coc
.
constructor
2 with
(lift_rec
n
P
k
); auto
with
coc
.
Qed
.
Lemma
red_red_subst
:
forall
x
t
u
k
, red
t
u
-> red
(subst_rec
x
t
k
) (subst_rec
x
u
k
).
induction
1; intros
; auto
with
coc
.
constructor
2 with
(subst_rec
x
P
k
); auto
with
coc
.
Qed
.
Lemma
ins_item_ge_inv
:
forall
A
n
e
f
,
ins_in_env
A
n
e
f
-> forall
v
t
, n
<= v
-> item
t
f
(S
v
) -> item
t
e
v
.
Proof
.
induction
1; intros
.
inversion
H0
; trivial
.
destruct
v
.
inversion
H0
.
inversion_clear
H1
; auto
10 with
coc
arith
.
Qed
.
Lemma
ins_item_lt_inv
:
forall
A
n
e
f
,
ins_in_env
A
n
e
f
->
forall
v
t
, n
> v
->
item_lift
t
f
v
->
exists2
t'
, t
= lift_rec
1 t'
n
& item_lift
t'
e
v
.
Proof
.
induction
1; intros
.
inversion
H
.
destruct
v
.
destruct
H1
.
subst
t0
.
inversion_clear
H2
.
rewrite
permute_lift
.
exists
(lift
1 t
); auto
.
exists
t
; auto
.
destruct
H1
.
inversion_clear
H2
.
elim
IHins_in_env
with
v
(lift
(S
v
) x
); intros
; auto
with
arith
.
subst
t0
.
rewrite
simpl_lift
.
rewrite
H2
.
rewrite
permute_lift
.
exists
(lift
1 x0
); auto
.
destruct
H4
.
subst
x0
.
rewrite
<- simpl_lift
.
exists
x1
; auto
.
exists
x
;auto
.
Qed
.
Lemma
pre_strength
:
forall
A
e
M
T
,
typ
e
M
T
->
forall
f
k
M'
,
lift_rec
1 M'
k
= M
->
ins_in_env
A
k
f
e
->
wf
f
->
exists2
T'
, red
T
(lift_rec
1 T'
k
) & typ
f
M'
T'
.
Proof
.
induction
1; intros
.
rewrite
lift_srt_inv
with
(1:=H0).
exists
(Srt
kind
); auto
with
coc
.
constructor
; trivial
.
elim
lift_ref_inv
with
(1:=H1);destruct
1; intros
; subst
M'
.
specialize
ins_item_lt_inv
with
(1:=H2) (2:=H4) (3:=H0); intro
.
destruct
H5
.
subst
t
.
exists
x
; auto
with
coc
.
constructor
; trivial
.
destruct
v
; simpl
.
inversion
H4
.
rewrite
<- minus_n_O
.
destruct
H0
.
assert
(k
<=v); auto
with
arith
.
specialize
ins_item_ge_inv
with
(1:=H2) (2:=H6) (3:=H5); intro
.
exists
(lift
(S
v
) x
).
subst
t
.
unfold
lift
; rewrite
simpl_lift_rec
; simpl
; auto
with
arith
coc
.
constructor
; trivial
.
exists
x
; trivial
.
elim
lift_abs_inv
with
(1:=H2).
intros
(T'
, eqT'
) (M''
, eqM''
).
elim
IHtyp1
with
(1:= eqT'
) (2:=H3) (3:=H4); intros
.
assert
(x
=Srt s1
).
apply
lift_srt_inv
with
1 k
.
rewrite
red_normal
with
(1:=H5); trivial
.
red
;red
;intros
.
inversion
H7
.
subst
x
.
assert
(wf
(T'
:: f
)). apply
wf_var
with
s1
; trivial
.
assert
(ins_in_env
A
(S
k
) (T'
::f) (T
::e)).
subst
T
; constructor
; trivial
.
elim
IHtyp3
with
(1:=eqM'') (2:=H8) (3:=H7); intros
.
exists
(Prod
T'
x
).
subst
T
; simpl
; auto
with
coc
.
replace
M'
with
(Abs
T'
M''
).
apply
type_abs
with
s1
s2
; trivial
.
specialize
type_case
with
(1:=H10);intro
.
destruct
H11
.
destruct
H11
.
replace
s2
with
x0
; trivial
.
assert
(conv
(Srt
x0
) (Srt
s2
)).
apply
typ_conv_conv
with
(u
:=(lift_rec 1 x
(S
k
))) (2:=H0).
change
(typ
(T
::e) (lift_rec
1 x
(S
k
)) (lift_rec
1 (Srt
x0
) (S
k
))).
apply
typ_weak_weak
with
(2:=H8); trivial
.
apply
wf_var
with
s1
; trivial
.
apply
sym_conv
.
auto
with
coc
.
apply
conv_sort
; trivial
.
elim
inv_typ_conv_kind
with
(2:=H0).
rewrite
H11
in
H9
; simpl
in
H9
.
auto
with
coc
.
apply
lift_inj
with
1 k
; simpl
.
rewrite
eqT'
; rewrite
eqM''
; auto
.
elim
lift_app_inv
with
(1:=H1).
intros
(u'
,equ') (v'
,eqv').
elim
IHtyp2
with
(1:=equ') (2:=H2) (3:=H3); intros
.
elim
IHtyp1
with
(1:= eqv'
) (2:=H2) (3:=H3); intros
.
apply
red_prod_prod
with
(1:=H4); intros
.
elim
lift_prod_inv
with
(1:=H8).
intros
(a'
,eqa') (b'
,eqb').
clear
IHtyp1
IHtyp2
.
subst
a
b
u
v
.
exists
(subst
v'
b'
).
rewrite
distr_lift_subst
.
unfold
subst
.
apply
red_red_subst
; trivial
.
replace
M'
with
(App
u'
v'
).
assert
(x
=Prod a'
b'
).
apply
lift_inj
with
1 k
; simpl
; trivial
.
apply
type_app
with
a'
.
clear
H8
; subst
x
.
elim
type_case
with
(1:=H5); intros
.
inversion_clear
H8
.
apply
inv_typ_prod
with
(1:=H11);intros
.
apply
type_conv
with
x0
s1
; auto
with
coc
.
elim
church_rosser
with
(lift_rec
1 a'
k
) (lift_rec
1 x0
k
); intros
.
elim
red_red_lift_ex
with
(1:=H14); intros
.
elim
red_red_lift_ex
with
(1:=H15); intros
.
apply
trans_conv_conv
with
x3
; auto
with
coc
.
replace
x3
with
x2
.
apply
sym_conv
.
auto
with
coc
.
apply
lift_inj
with
1 k
; subst
x1
; auto
.
apply
trans_conv_conv
with
V
; auto
with
coc
.
apply
sym_conv
; auto
with
coc
.
discriminate
.
elim
H11
; trivial
.
apply
lift_inj
with
1 k
; simpl
; auto
.
elim
lift_prod_inv
with
(1:=H1).
intros
(T'
, eqT'
) (U'
, eqU'
).
elim
IHtyp1
with
(1:=eqT') (2:=H2) (3:=H3); intros
.
assert
(x
=Srt s1
).
apply
lift_srt_inv
with
1 k
.
rewrite
red_normal
with
(1:=H4); trivial
.
red
;red
;intros
.
inversion
H6
.
subst
x
.
assert
(wf
(T'
:: f
)). apply
wf_var
with
s1
; trivial
.
assert
(ins_in_env
A
(S
k
) (T'
::f) (T
::e)).
subst
T
; constructor
; trivial
.
elim
IHtyp2
with
(1:=eqU') (2:=H7) (3:=H6); intros
.
exists
(Srt
s2
); auto
with
coc
.
replace
M'
with
(Prod
T'
U'
).
apply
type_prod
with
s1
; trivial
.
replace
(Srt
s2
) with
x
; trivial
.
apply
lift_inj
with
1 (S
k
); simpl
.
rewrite
red_normal
with
(1:=H8); trivial
.
red
;red
;intros
.
inversion
H10
.
apply
lift_inj
with
1 k
; simpl
.
rewrite
eqT'
; rewrite
eqU'
; auto
.
elim
IHtyp1
with
(1:=H2) (2:=H3) (3:=H4); intros
.
elim
church_rosser
with
V
(lift_rec
1 x
k
); intros
.
elim
red_red_lift_ex
with
(1:=H8);intros
.
subst
x0
.
exists
x1
; trivial
.
apply
type_reduction
with
x
; trivial
.
apply
trans_conv_conv
with
U
; auto
with
coc
.
Qed
.
Lemma
strengthening_env
:
forall
A
k
e
f
,
ins_in_env
A
k
f
e
->
wf
e
->
wf
f
.
Proof
.
induction
1; intros
.
inversion_clear
H
.
apply
typ_wf
with
(1 := H0
).
inversion_clear
H0
.
apply
wf_var
with
s
.
elim
pre_strength
with
(1 := H1
) (M'
:= t
) (3 := H
); intros
; auto
.
replace
(Srt
s
) with
x
; trivial
.
apply
lift_srt_inv
with
1 n
.
symmetry
in
|- *.
apply
red_normal
; trivial
.
red
in
|- *; red
in
|- *; intros
.
inversion
H3
.
specialize
typ_wf
with
(1 := H1
); auto
.
Qed
.
Lemma
strengthening
:
forall
A
e
f
M
T
k
,
typ
e
(lift_rec
1 M
k
) (lift_rec
1 T
k
) ->
ins_in_env
A
k
f
e
->
typ
f
M
T
.
Proof
.
intros
.
elim
pre_strength
with
(1 := H
) (M'
:= M
) (3 := H0
); trivial
; intros
.
elim
type_case
with
(1 := H
); intros
.
inversion_clear
H3
.
apply
type_conv
with
x
x0
; trivial
.
apply
sym_conv
.
apply
red_conv
.
apply
red_lift_lift_inv
with
(1 := H1
).
elim
pre_strength
with
(1 := H4
) (M'
:= T
) (3 := H0
); intros
; trivial
.
replace
(Srt
x0
) with
x1
; trivial
.
apply
lift_srt_inv
with
1 k
.
symmetry
in
|- *.
apply
red_normal
; trivial
.
red
in
|- *; red
in
|- *; intros
.
inversion_clear
H6
.
apply
typ_wf
with
(1 := H2
).
specialize
lift_srt_inv
with
(1 := H3
).
intro
.
rewrite
H4
.
specialize
red_lift_lift_inv
with
(1 := H1
).
rewrite
H4
; intro
.
rewrite
red_normal
with
(1 := H5
); trivial
.
red
in
|- *; red
in
|- *; intros
.
inversion
H6
.
apply
strengthening_env
with
(1 := H0
).
apply
typ_wf
with
(1 := H
).
Qed
.
Lemma
strengthening0
:
forall
A
e
M
T
,
typ
(cons
A
e
) (lift
1 M
) (lift
1 T
) ->
typ
e
M
T
.
Proof
.
intros
.
apply
strengthening
with
A
(A
:: e
) 0; trivial
.
constructor
.
Qed
.