Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Conv_Dec
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Env
.
Require
Import
Lambda.JRussell.Types
.
Require
Import
Lambda.JRussell.Basic
.
Require
Import
Lambda.JRussell.Conversion
.
Require
Import
Lambda.JRussell.Coercion
.
Require
Import
Lambda.JRussell.Thinning
.
Require
Import
Lambda.JRussell.Substitution
.
Require
Import
Lambda.JRussell.PreFunctionality
.
Require
Import
Lambda.JRussell.Generation
.
Require
Import
Lambda.JRussell.Validity
.
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
coerce_free
: env
→ term
→ term
→ sort
→ Prop
:=
| coerce_free_conv
: ∀ e
A
B
s
, e
|-= A
= B
: Srt
s
→ e
|-= A
>>> B
: s
| coerce_free_weak
: ∀ e
A
B
s
, e
|-= A
>>> B
: s
→
∀ T
s'
, e
|-= T
: Srt
s'
→
(T
:: e
) |-= lift
1 A
>>> lift
1 B
: s
| coerce_free_prod
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-= A'
>>> A
: s
→
∀ s'
, (A'
:: e
) |-= B
>>> B'
: s'
→
e
|-= (Prod
A
B
) >>> (Prod
A'
B'
) : s'
| coerce_free_sum
: ∀ e
A
B
A'
B'
,
∀ s
, e
|-= A
>>> A'
: s
→
∀ s'
, (A
:: e
) |-= B
>>> B'
: s'
→
∀ s''
, sum_sort
s
s'
s''
→
e
|-= (Sum
A
B
) >>> (Sum
A'
B'
) : s''
| coerce_free_sub_l
: ∀ e
U
P
U'
,
e
|-= U
>>> U'
: set
→
U
:: e
|-= P
: Srt
prop
→
e
|-= Subset
U
P
>>> U'
: set
| coerce_free_sub_r
: ∀ e
U
U'
P
,
e
|-= U
>>> U'
: set
→
U'
:: e
|-= P
: Srt
prop
→
e
|-= U
>>> (Subset
U'
P
) : set
| coerce_free_sym
: ∀ e
U
V
s
, e
|-= U
>>> V
: s
→ e
|-= V
>>> U
: s
| coerce_free_trans
: ∀ e
A
B
C
s
,
e
|-= A
>>> B
: s
→ e
|-= B
>>> C
: s
→ e
|-= A
>>> C
: s
where
"G |-= T >>> U : s" := (coerce_free
G
T
U
s
).
Hint
Constructors
coerce_free
: coc
.
Lemma
coerce_coerce_free
: Î Î
“ T
U
s
, Î
“ |-= T
>> U
: s
→ Î
“ |-= T
>>> U
: s
.
Require
Import
Program
.
Ltac
coerce_env
:=
match
goal
with
| [ H
: ?G |-= ?T : ?s |- ?G' |-= ?T : ?s ] ⇒ apply
typ_coerce_env
with
G
| [ H
: ?G |-= ?T = ?U : ?s |-
?G' |-= ?T : ?s ] ⇒
apply
jeq_coerce_env
with
G
| [ H
: ?G |-= ?T >> ?U : ?s |-
?G' |-= ?T >> ?U : ?s ] ⇒
apply
coerce_coerce_env
with
G
end
.
Ltac
sat_types
:=
match
goal
with
| [ H
: ?G |-= ?T >> ?U : ?s |- _
] ⇒ let
H'
:= fresh
in
add_hypothesis
H'
(coerce_sort_l
H
) ;
let
H''
:= fresh
in
add_hypothesis
H''
(coerce_sort_r
H
)
| [ H
: ?G |-= ?T = ?U : ?s |- _
] ⇒ let
H'
:= fresh
in
add_hypothesis
H'
(jeq_type_l
H
) ;
let
H''
:= fresh
in
add_hypothesis
H''
(jeq_type_r
H
)
end
.
Hint
Extern
4 ⇒ coerce_env
: coc
.
Ltac
solve
:= repeat
sat_types
; eauto
with
coc
.
Lemma
coerce_free_coerce
: Î G
T
U
s
, G
|-= T
>>> U
: s
→ G
|-= T
>> U
: s
.