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
.