Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Env
.
Require
Import
Lambda.Russell.Types
.
Require
Import
Lambda.Russell.Thinning
.
Require
Import
Lambda.Russell.Substitution
.
Require
Import
Lambda.Russell.Depth
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: term
.
Implicit
Types
e
f
g
: env
.
Reserved Notation
"G |-- T >>>> U : s" (at
level
70, T
, U
, s
at
next
level
).
Inductive
coerces
: env
→ term
→ term
→ sort
→ Set
:=
| coerce_refl
: ∀ e
A
s
, e
|-- A
: Srt
s
→ e
|-- A
>>>> A
: s
| coerce_prod
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-- A'
>>>> A
: s
→
e
|-- A'
: Srt
s
→ e
|-- A
: Srt
s
→
∀ s'
, (A'
:: e
) |-- B
>>>> B'
: s'
→
A
:: e
|-- B
: Srt
s'
→ A'
:: e
|-- B'
: Srt
s'
→
e
|-- (Prod
A
B
) >>>> (Prod
A'
B'
) : s'
| coerce_sum
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-- A
>>>> A'
: s
→
e
|-- A'
: Srt
s
→ e
|-- A
: Srt
s
→
∀ s'
, (A
:: e
) |-- B
>>>> B'
: s'
→
A
:: e
|-- B
: Srt
s'
→ A'
:: e
|-- B'
: Srt
s'
→
∀ s''
, sum_sort
s
s'
s''
→ sum_sort
s
s'
s''
→
e
|-- (Sum
A
B
) >>>> (Sum
A'
B'
) : s''
| coerce_sub_l
: ∀ e
U
P
U'
,
e
|-- U
>>>> U'
: set
→
U
:: e
|-- P
: Srt
prop
→
e
|-- Subset
U
P
>>>> U'
: set
| coerce_sub_r
: ∀ e
U
U'
P
,
e
|-- U
>>>> U'
: set
→
U'
:: e
|-- P
: Srt
prop
→
e
|-- U
>>>> (Subset
U'
P
) : set
| coerce_conv
: ∀ e
A
B
C
D
s
,
e
|-- A
: Srt
s
→ e
|-- B
: Srt
s
→ e
|-- C
: Srt
s
→ e
|-- D
: Srt
s
→
conv
A
B
→ e
|-- B
>>>> C
: s
→ conv
C
D
→ e
|-- A
>>>> D
: s
where
"G |-- T >>>> U : s" := (coerces
G
T
U
s
).
Hint
Resolve
coerce_refl
coerce_prod
coerce_sum
coerce_sub_l
coerce_sub_r
: coc
.
Hint
Resolve
coerce_conv
: coc
.
Reserved Notation
"G |-- T >>> U : s" (at
level
70, T
, U
, s
at
next
level
).
Inductive
coerces_db
: env
→ term
→ term
→ sort
→ Set
:=
| coerces_refl
: ∀ e
A
s
, e
|-- A
: Srt
s
→ e
|-- A
>>> A
: s
| coerces_prod
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-- A'
>>> A
: s
→
e
|-- A'
: Srt
s
→ e
|-- A
: Srt
s
→
∀ s'
, (A'
:: e
) |-- B
>>> B'
: s'
→
A
:: e
|-- B
: Srt
s'
→ A'
:: e
|-- B'
: Srt
s'
→
e
|-- (Prod
A
B
) >>> (Prod
A'
B'
) : s'
| coerces_sum
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-- A
>>> A'
: s
→
e
|-- A'
: Srt
s
→ e
|-- A
: Srt
s
→
∀ s'
, (A
:: e
) |-- B
>>> B'
: s'
→
A
:: e
|-- B
: Srt
s'
→ A'
:: e
|-- B'
: Srt
s'
→
∀ s''
, sum_sort
s
s'
s''
→ sum_sort
s
s'
s''
→
e
|-- (Sum
A
B
) >>> (Sum
A'
B'
) : s''
| coerces_sub_l
: ∀ e
U
P
U'
,
e
|-- U
>>> U'
: set
→
U
:: e
|-- P
: Srt
prop
→
e
|-- Subset
U
P
>>> U'
: set
| coerces_sub_r
: ∀ e
U
U'
P
,
e
|-- U
>>> U'
: set
→
U'
:: e
|-- P
: Srt
prop
→
e
|-- U
>>> (Subset
U'
P
) : set
| coerces_conv_l
: ∀ e
A
B
C
s
,
e
|-- A
: Srt
s
→ e
|-- B
: Srt
s
→ e
|-- C
: Srt
s
→
conv
A
B
→ e
|-- B
>>> C
: s
→ e
|-- A
>>> C
: s
| coerces_conv_r
: ∀ e
A
B
C
s
,
e
|-- A
: Srt
s
→ e
|-- B
: Srt
s
→ e
|-- C
: Srt
s
→
e
|-- A
>>> B
: s
→ conv
B
C
→ e
|-- A
>>> C
: s
where
"G |-- T >>> U : s" := (coerces_db
G
T
U
s
).
Hint
Resolve
coerces_refl
coerces_prod
coerces_sum
coerces_sub_l
coerces_sub_r
: coc
.
Hint
Resolve
coerces_conv_l
coerces_conv_r
: coc
.
Scheme
coerces_db_dep
:= Induction
for
coerces_db
Sort
Type
.
Require
Import
Coq.Arith.Max
.
Fixpoint
depth
(e
: env
) (T
U
: term
) (s
: sort
) (d
: e
|-- T
>>> U
: s
) {struct
d
}: nat
:=
match
d
with
| coerces_refl
e
A
s
As
⇒ 0
| coerces_prod
e
A
B
A'
B'
s
HsubA
A's
As
s'
HsubBB'
Bs
B's
⇒
S
(max
(depth
HsubA
) (depth
HsubBB'
))
| coerces_sum
e
A
B
A'
B'
s
HsubA
A's
As
s'
HsubBB'
Bs
B's
s''
sum
sum'
⇒
S
(max
(depth
HsubA
) (depth
HsubBB'
))
| coerces_sub_l
e
U
P
U'
HsubU
Ps
⇒ S
(depth
HsubU
)
| coerces_sub_r
e
U
U'
P
HsubU
Ps
⇒ S
(depth
HsubU
)
| coerces_conv_l
e
A
B
C
s
As
Bs
Cs
convAB
HsubBC
⇒ S
(depth
HsubBC
)
| coerces_conv_r
e
A
B
C
s
As
Bs
Cs
HsubAB
convBC
⇒ S
(depth
HsubAB
)
end
.
Lemma
coerces_coerces_db
: ∀ G
T
U
s
, G
|-- T
>>>> U
: s
→ G
|-- T
>>> U
: s
.
Lemma
coerces_db_coerces
: ∀ G
T
U
s
, G
|-- T
>>> U
: s
→ G
|-- T
>>>> U
: s
.
Require
Import
Lambda.Russell.Coercion
.
Inductive
coerce_in_env
: env
→ env
→ Prop
:=
| coerce_env_hd
: ∀ e
t
u
s
, e
|-- t
>>> u
: s
→
coerce_in_env
(u
:: e
) (t
:: e
)
| coerce_env_tl
:
∀ e
f
t
, wf
(t
:: f
) → coerce_in_env
e
f
→ coerce_in_env
(t
:: e
) (t
:: f
).
Hint
Resolve
coerce_env_hd
coerce_env_tl
: coc
.
Theorem
coerces_db_depth
: ∀ e
T
U
s
n1
, Depth.coerces_db
e
T
U
s
n1
→
∃ d
: (coerces_db
e
T
U
s
), depth
d
= n1
.
Theorem
depth_coerces_db
: ∀ e
T
U
s
, coerces_db
e
T
U
s
→ ∃ n
,
Depth.coerces_db
e
T
U
s
n
.
Lemma
coerces_coerce
: ∀ e
T
U
s
, e
|-- T
>>> U
: s
→ e
|-- T
>> U
: s
.
Lemma
coerce_in_env_to_coercion
: ∀ e
f
, coerce_in_env
e
f
→ Coercion.coerce_in_env
e
f
.
Lemma
coerce_in_env_from_coercion
: ∀ e
f
, Coercion.coerce_in_env
e
f
→ coerce_in_env
e
f
.
Lemma
typ_conv_env
:
∀ e
t
T
, ∀ d
: (e
|-- t
: T
),
∀ f
, coerce_in_env
e
f
→
wf
f
→ f
|-- t
: T
.
Lemma
coerce_conv_env
:
∀ e
T
U
s
, ∀ d
: (e
|-- T
>>> U
: s
),
∀ f
, coerce_in_env
e
f
→
wf
f
→
{ d'
: f
|-- T
>>> U
: s
| (depth
d'
) = depth
d
}.