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
.