Library Infer


Require
Import
Strong_Norm
.
Require
Import
Conv_Dec
.

  
Lemma
is_sort
:
forall
t
, {
s
:
_
|
t
=
Srt
s
} + {(
forall
s
,
t
<>
Srt
s
)}.
simple
destruct
t
;
intros
;
try
(
right
;
red
in
|- *;
intros
;
discriminate
).
left
;
exists
s
;
trivial
.
Qed
.

  
Lemma
is_prod
:
   
forall
t
,
   {
p
:
_
*
_
|
let
(
T
,
U
) :=
p
in
t
=
Prod
T
U
} +
   {(
forall
T
U
,
t
<>
Prod
T
U
)}.
simple
destruct
t
;
intros
;
try
(
right
;
red
in
|- *;
intros
;
discriminate
).
left
;
exists
(
t0
,
t1
);
trivial
.
Qed
.


  
Lemma
red_to_sort
:
   
forall
t
,
sn
t
-> {
s
:_|
red
t
(
Srt
s
)} + {
forall
s
, ~
conv
t
(
Srt
s
)}.
Proof
.
intros
t
sn_t
.
elim
(
compute_nf
t
);
auto
with
coc
;
intros
nt
t_red
t_norm
.
elim
(
is_sort
nt
).
intros
(
s
,
eq_s
).
left
;
exists
s
.
elim
eq_s
;
trivial
.

intros
not_s
;
right
;
red
in
|- *;
intros
.
elim
church_rosser
with
(
Srt
s
)
nt
;
intros
.
apply
red_sort_sort
with
s
nt
;
trivial
.
rewrite
red_normal
with
(1 :=
H1
);
trivial
.

apply
trans_conv_conv
with
t
;
auto
with
coc
.
Qed
.

  
Lemma
red_to_prod
:
   
forall
t
,
   
sn
t
->
   {
p
:term*term|
let
(
u
,v):=
p
in
red
t
(
Prod
u
v
)} +
   {
forall
u
v
, ~
conv
t
(
Prod
u
v
)}.
intros
t
sn_t
.
elim
(
compute_nf
t
);
auto
with
coc
;
intros
nt
t_red
t_norm
.
elim
(
is_prod
nt
).
intros
((
T
,
U
),
eq_pi
).
left
;
exists
(
T
,
U
).
elim
eq_pi
;
trivial
.

intros
diff_pi
;
right
;
red
in
|- *;
intros
.
elim
church_rosser
with
(
Prod
u
v
)
nt
;
intros
.
apply
red_prod_prod
with
u
v
nt
;
auto
;
intros
.
rewrite
red_normal
with
(1 :=
H1
);
trivial
.

elim
diff_pi
with
(1 :=
H2
).

apply
trans_conv_conv
with
t
;
auto
with
coc
.
Qed
.

Section
Decidabilite_typage
.

  
Theorem
infer
:
   
forall
e
t
,
wf
e
-> {
T
:
_
|
typ
e
t
T
} + {(
forall
T
, ~
typ
e
t
T
)}.
intros
e
t
.
generalize
e
;
clear
e
.
elim
t
;
clear
t
.
intros
[| ]
e
wfe
.
right
;
red
in
|- *;
intros
.
elim
inv_typ_kind
with
e
T
;
auto
.

left
;
exists
(
Srt
kind
).
apply
type_prop
;
trivial
.

intros
n
e
wfe
.
elim
(
list_item
e
n
).
intros
(
t
,
t_item
).
left
;
exists
(
lift
(
S
n
)
t
).
apply
type_var
;
auto
.
exists
t
;
auto
.

right
;
red
in
|- *;
intros
.
apply
inv_typ_ref
with
(1 :=
H
);
intros
.
elim
b
with
U
;
auto
.

intros
t
typ_t
b
typ_b
e
wfe
.
elim
(
typ_t
e
);
trivial
.
intros
(
T
,
ty_t
).
elim
(
red_to_sort
T
).
intros
(
s1
,
T_srt
).
elim
(
typ_b
(
t
::
e
)).
intros
(
B
,
ty_b
).
elim
(
eqterm
(
Srt
kind
)
B
).
intros
B_kind
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_abs
with
(1 :=
H
);
intros
.
elim
inv_typ_conv_kind
with
(2 :=
H2
).
rewrite
B_kind
.
apply
typ_unique
with
(1 :=
H1
);
trivial
.

intros
B_not_kind
.
left
;
exists
(
Prod
t
B
).
elim
type_case
with
(1 :=
ty_b
);
intros
.
inversion_clear
H
.
apply
type_abs
with
s1
x
;
auto
.
apply
type_reduction
with
T
;
auto
.

elim
B_not_kind
;
auto
.

intros
b_not_ty
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_abs
with
(1 :=
H
);
intros
.
elim
b_not_ty
with
T1
;
auto
.

apply
wf_var
with
s1
.
apply
type_reduction
with
T
;
auto
.

intros
T_not_s
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_abs
with
(1 :=
H
);
intros
.
elim
T_not_s
with
s1
.
apply
typ_unique
with
e
t
;
auto
.

apply
type_sn
with
e
t
;
auto
.

intros
t_not_ty
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_abs
with
(1 :=
H
);
intros
.
elim
t_not_ty
with
(
Srt
s1
);
auto
.

intros
t
typ_t
b
typ_b
e
wfe
.
elim
(
typ_t
e
);
trivial
.
intros
(
T
,
ty_t
).
elim
(
red_to_prod
T
).
intros
((
V
,
Ur
),
red_T
).
elim
(
typ_b
e
);
trivial
.
intros
(
B
,
ty_b
).
elim
(
is_conv
V
B
).
intros
ty_conv
.
left
;
exists
(
subst
b
Ur
).
elim
type_case
with
(1 :=
ty_t
);
intros
.
inversion_clear
H
.
apply
type_app
with
V
;
auto
.
apply
inv_typ_prod
with
(1 :=
subject_reduction
_
_
_
red_T
_
H0
);
intros
.
apply
type_conv
with
B
s1
;
auto
with
coc
.

apply
type_reduction
with
T
;
auto
.

elim
conv_sort_prod
with
kind
V
Ur
.
elim
H
;
auto
with
coc
.

intros
not_conv
.
right
;
red
in
|- *;
intros
.
apply
not_conv
.
apply
inv_typ_app
with
(1 :=
H
);
intros
.
apply
trans_conv_conv
with
V0
.
apply
inv_conv_prod_l
with
Ur
Ur0
.
apply
typ_unique
with
e
t
;
auto
.
apply
type_reduction
with
T
;
auto
.

apply
typ_unique
with
e
b
;
auto
.

apply
subterm_sn
with
(
Prod
V
Ur
);
auto
with
coc
.
apply
sn_red_sn
with
T
;
auto
.
apply
type_sn
with
e
t
;
auto
.

apply
type_sn
with
e
b
;
auto
.

intros
not_ty_b
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_app
with
(1 :=
H
);
intros
.
elim
not_ty_b
with
V0
;
auto
.

intros
not_prod
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_app
with
(1 :=
H
);
intros
.
elim
not_prod
with
V
Ur
.
apply
typ_unique
with
e
t
;
auto
.

apply
type_sn
with
e
t
;
auto
.

intros
not_ty_t
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_app
with
(1 :=
H
);
intros
.
elim
not_ty_t
with
(
Prod
V
Ur
);
auto
.

intros
t
typ_t
b
typ_b
e
wfe
.
elim
(
typ_t
e
);
trivial
.
intros
(
T
,
ty_t
).
elim
(
red_to_sort
T
).
intros
(
s1
,
T_srt
).
elim
(
typ_b
(
t
::
e
)).
intros
(
B
,
ty_b
).
elim
(
red_to_sort
B
).
intros
(
s2
,
B_srt
).
left
;
exists
(
Srt
s2
).
apply
type_prod
with
s1
.
apply
type_reduction
with
(1 :=
T_srt
);
trivial
.

apply
type_reduction
with
(1 :=
B_srt
);
trivial
.

intros
B_not_s
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_prod
with
(1 :=
H
);
intros
.
elim
B_not_s
with
s2
;
auto
.
apply
typ_unique
with
(
t
::
e
)
b
;
auto
.

apply
type_sn
with
(1 :=
ty_b
).

intros
b_not_ty
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_prod
with
(1 :=
H
);
intros
.
elim
b_not_ty
with
(
Srt
s2
);
auto
.

apply
wf_var
with
s1
;
auto
.
apply
type_reduction
with
(1 :=
T_srt
);
trivial
.

intros
T_not_s
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_prod
with
(1 :=
H
);
intros
.
elim
T_not_s
with
s1
.
apply
typ_unique
with
e
t
;
auto
.

apply
type_sn
with
(1 :=
ty_t
).

intros
t_not_ty
.
right
;
red
in
|- *;
intros
.
apply
inv_typ_prod
with
(1 :=
H
);
intros
.
elim
t_not_ty
with
(
Srt
s1
);
auto
.
Qed
.

  
Lemma
check_typ
:
forall
e
t
tp
,
wf
e
-> {
typ
e
t
tp
} + {~
typ
e
t
tp
}.
intros
e
t
tp
wfe
.
elim
(
infer
e
t
);
trivial
.
intros
(
tp'
,
ty_t
).
elim
(
eqterm
tp'
(
Srt
kind
)).
intros
is_knd'
.
elim
(
eqterm
tp
(
Srt
kind
)).
intros
is_knd
.
left
.
rewrite
is_knd
;
rewrite
is_knd'
in
ty_t
;
trivial
.

intros
not_knd
.
right
;
red
in
|- *;
intros
;
apply
not_knd
.
apply
type_kind_not_conv
with
(1 :=
H
).
elim
is_knd'
;
trivial
.

intros
not_knd'
.
elim
(
infer
e
tp
);
trivial
.
intros
(
U
,
ty_tp
).
elim
(
is_conv
tp'
tp
).
intros
is_cnv
.
left
.
elim
red_to_sort
with
U
;
intros
.
inversion_clear
a
.
apply
type_conv
with
tp'
x
;
trivial
.
apply
type_reduction
with
(1 :=
H
);
trivial
.

elim
type_case
with
(1 :=
ty_t
);
intros
.
inversion_clear
H
.
elim
b
with
x
.
apply
sym_conv
.
apply
typ_conv_conv
with
(1 :=
H0
) (3 :=
is_cnv
);
trivial
.

elim
not_knd'
;
trivial
.

apply
type_sn
with
(1 :=
ty_tp
).

intros
not_conv
.
right
;
red
in
|- *;
intros
;
apply
not_conv
.
apply
typ_unique
with
(1 :=
ty_t
);
trivial
.

apply
type_sn
with
(1 :=
ty_t
).

apply
strong_norm
with
(1 :=
ty_tp
).

intros
tp_not_ty
.
right
;
red
in
|- *;
intros
.
elim
type_case
with
(1 :=
H
);
intros
.
inversion_clear
H0
.
elim
tp_not_ty
with
(1 :=
H1
).

apply
not_knd'
.
apply
type_kind_not_conv
with
(1 :=
ty_t
);
auto
.
elim
H0
;
trivial
.

intros
t_not_ty
.
right
;
auto
.
Qed
.

  
Lemma
add_typ
:
forall
e
t
,
wf
e
-> {
wf
(
t
::
e
)} + {~
wf
(
t
::
e
)}.
intros
e
t
wfe
.
elim
(
infer
e
t
);
trivial
.
intros
(
u
,
ty_t
).
elim
(
red_to_sort
u
);
auto
.
intros
(
s
,
u_srt
).
left
.
apply
wf_var
with
s
.
apply
type_reduction
with
(1 :=
u_srt
);
trivial
.

intros
not_sort
.
right
;
red
in
|- *;
intros
.
inversion_clear
H
.
elim
not_sort
with
s
.
apply
typ_unique
with
(1 :=
ty_t
);
trivial
.

apply
type_sn
with
(1 :=
ty_t
).

intros
t_not_ty
.
right
;
red
in
|- *;
intros
.
inversion_clear
H
.
elim
t_not_ty
with
(1 :=
H0
).
Qed
.

  
Lemma
decide_wf
:
forall
e
, {
wf
e
} + {~
wf
e
}.
simple
induction
e
;
intros
.
left
;
apply
wf_nil
.

elim
H
;
intros
.
elim
add_typ
with
l
a
;
auto
;
intros
.

right
;
red
in
|- *;
intros
;
apply
b
.
inversion_clear
H0
.
apply
typ_wf
with
a
(
Srt
s
);
auto
.
Qed
.

  
Lemma
decide_typ
:
forall
e
t
tp
, {
typ
e
t
tp
} + {~
typ
e
t
tp
}.
intros
.
elim
decide_wf
with
e
;
intros
.
apply
check_typ
;
auto
.

right
;
red
in
|- *;
intros
;
apply
b
.
apply
typ_wf
with
t
tp
;
auto
.
Qed
.

End
Decidabilite_typage
.