Require
Import
Lambda.Utils
.
Require
Import
Lambda.Tactics
.
Require
Import
Lambda.TPOSR.Terms
.
Require
Import
Lambda.TPOSR.Reduction
.
Require
Import
Lambda.TPOSR.Conv
.
Require
Import
Lambda.TPOSR.LiftSubst
.
Require
Import
Lambda.TPOSR.Env
.
Require
Import
Lambda.TPOSR.Types
.
Require
Import
Lambda.TPOSR.Thinning
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: lterm
.
Implicit
Types
e
f
g
: lenv
.
Reserved Notation
"G |-- T >>> U : s" (at
level
70, T
, U
, s
at
next
level
).
Inductive
coerces
: lenv
-> lterm
-> lterm
-> sort
-> Set
:=
| coerces_refl
: ∀ e
A
s
, e
|-- A
-> A
: s
-> e
|-- A
>>> A
: s
| coerces_prod
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-- A'
>>> A
: s
->
e
|-- A'
-> A'
: s
-> e
|-- A
-> A
: s
->
∀ s'
, (A'
:: e
) |-- B
>>> B'
: s'
->
A
:: e
|-- B
-> B
: s'
-> A'
:: e
|-- B'
-> B'
: s'
->
e
|-- (Prod_l
A
B
) >>> (Prod_l
A'
B'
) : s'
| coerces_sum
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-- A
>>> A'
: s
->
e
|-- A'
-> A'
: s
-> e
|-- A
-> A
: s
->
∀ s'
, (A
:: e
) |-- B
>>> B'
: s'
->
A
:: e
|-- B
-> B
: s'
-> A'
:: e
|-- B'
-> B'
: s'
->
∀ s''
, sum_sort
s
s'
s''
->
e
|-- (Sum_l
A
B
) >>> (Sum_l
A'
B'
) : s''
| coerces_sub_l
: ∀ e
U
P
U'
,
e
|-- U
>>> U'
: set
->
U
:: e
|-- P
-> P
: prop
->
e
|-- Subset_l
U
P
>>> U'
: set
| coerces_sub_r
: ∀ e
U
U'
P
,
e
|-- U
>>> U'
: set
->
U'
:: e
|-- P
-> P
: prop
->
e
|-- U
>>> (Subset_l
U'
P
) : set
| coerces_conv_l
: ∀ e
A
B
C
s
,
e
|-- A
-> A
: s
-> e
|-- B
-> B
: s
-> e
|-- C
-> C
: s
->
e
|-- A
~= B
: s
-> e
|-- B
>>> C
: s
-> e
|-- A
>>> C
: s
| coerces_conv_r
: ∀ e
A
B
C
s
,
e
|-- A
-> A
: s
-> e
|-- B
-> B
: s
-> e
|-- C
-> C
: s
->
e
|-- A
>>> B
: s
-> e
|-- B
~= C
: s
-> e
|-- A
>>> C
: s
where
"G |-- T >>> U : s" := (coerces
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_dep
:= Induction
for
coerces
Sort
Type
.
Require
Import
Coq.Arith.Max
.
Fixpoint
depth
(e
: lenv
) (T
U
: lterm
) (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
⇒
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
.
Require
Import
Lambda.TPOSR.CoerceDepth
.
Lemma
coerces_coerce_rc_depth
: ∀ G
T
U
s
, ∀ d
: G
|-- T
>>> U
: s
,
G
|-- T
>-> U
: s
[depth
d
].
Theorem
coerce_rc_depth_coerces
: ∀ e
T
U
s
n
, e
|-- T
>-> U
: s
[n
] ->
∃ d
: (e
|-- T
>>> U
: s
), depth
d
= n
.
Inductive
coerces_in_env
: lenv
-> lenv
-> Prop
:=
| coerces_env_hd
: ∀ e
t
u
s
, e
|-- t
>>> u
: s
->
coerces_in_env
(u
:: e
) (t
:: e
)
| coerces_env_tl
:
∀ e
f
t
, tposr_wf
(t
:: f
) -> coerces_in_env
e
f
-> coerces_in_env
(t
:: e
) (t
:: f
).
Hint
Resolve
coerces_env_hd
coerces_env_tl
: ecoc
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Lemma
coerces_coerce
: ∀ e
t
u
s
, e
|-- t
>>> u
: s
-> e
|-- t
>-> u
: s
.
Lemma
coerces_in_env_coerce_in_env
: ∀ e
f
, coerces_in_env
e
f
-> coerce_in_env
e
f
.
Hint
Resolve
coerces_in_env_coerce_in_env
: coc
.
Lemma
tposr_coerces_env
:
∀ e
t
T
, ∀ d
: (e
|-- t
-> t
: T
),
∀ f
, coerces_in_env
e
f
->
tposr_wf
f
-> f
|-- t
-> t
: T
.
Lemma
eq_coerces_env
:
∀ e
t
u
s
, ∀ d
: (e
|-- t
~= u
: s
),
∀ f
, coerces_in_env
e
f
->
tposr_wf
f
-> f
|-- t
~= u
: s
.
Lemma
coerces_coerces_env
:
∀ e
T
U
s
, ∀ d
: (e
|-- T
>>> U
: s
),
∀ f
, coerces_in_env
e
f
->
tposr_wf
f
->
{ d'
: f
|-- T
>>> U
: s
| (depth
d'
) = depth
d
}.
Lemma
coerces_sym
: ∀ e
A
B
s
, ∀ d
: e
|-- A
>>> B
: s
,
{ d'
: e
|-- B
>>> A
: s
| depth
d'
= depth
d
}.
Require
Import
Lambda.TPOSR.ChurchRosser
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Lemma
inv_eq_prod_l
: ∀ e
U
V
U'
V'
s
,
e
|-- Prod_l
U
V
~= Prod_l
U'
V'
: s
-> ∀ s1
, e
|-- U
-> U
: s1
-> e
|-- U
~= U'
: s1
.
Lemma
inv_eq_prod_r
: ∀ e
U
V
U'
V'
s
,
e
|-- Prod_l
U
V
~= Prod_l
U'
V'
: s
->
U'
:: e
|-- V
~= V'
: s
.
Lemma
inv_eq_sum_l
: ∀ e
U
V
U'
V'
s
,
e
|-- Sum_l
U
V
~= Sum_l
U'
V'
: s
->
∀ s1
: sort
, e
|-- U
-> U
: s1
-> e
|-- U
~= U'
: s1
.
Lemma
inv_eq_sum_r
: ∀ e
U
V
U'
V'
s
,
e
|-- Sum_l
U
V
~= Sum_l
U'
V'
: s
->
∀ s2
: sort
, U
:: e
|-- V
-> V
: s2
-> U
:: e
|-- V
~= V'
: s2
.
Lemma
inv_eq_subset_l_set
: ∀ e
U
V
U'
V'
s
,
e
|-- Subset_l
U
V
~= Subset_l
U'
V'
: s
-> e
|-- U
~= U'
: set
.