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
.
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
.
Lemma
app_cons_app_app
: ∀ e'
a
e
, e'
++ a
:: e
= (e'
++ a
:: nil
) ++ e
.
Lemma
strength_sort_judgement
: ∀ e
s
s'
, e
|-= Srt
s
: Srt
s'
→ nil
|-= Srt
s
: Srt
s'
.
Lemma
trunc_list
: ∀ e
, trunc
_
(length
e
) e
nil
.
Lemma
sort_judgement_empty_env
: ∀ s
s'
, nil
|-= Srt
s
: Srt
s'
→
∀ e
, consistent
e
→ e
|-= Srt
s
: Srt
s'
.
Lemma
weak_one_sort_judgement
: ∀ T
e
s
s'
, T
:: e
|-= Srt
s
: Srt
s'
→
e
|-= Srt
s
: Srt
s'
.
Hint
Resolve
weak_one_sort_judgement
: coc
.
Lemma
validity_ind
:
(∀ e
t
T
, e
|-= t
: T
→
T
= Srt
kind
∨ ∃ s
, e
|-= T
: Srt
s
) ∧
(∀ e
T
U
s
, e
|-= T
>> U
: s
→
e
|-= T
: Srt
s
∧ e
|-= U
: Srt
s
) ∧
(∀ e
t
u
T
, e
|-= t
= u
: T
→
(e
|-= t
: T
∧ e
|-= u
: T
) ∧
(T
= Srt
kind
∨ ∃ s
, e
|-= T
: Srt
s
)).
Lemma
validity_typ
:
∀ e
t
T
, e
|-= t
: T
→
T
= Srt
kind
∨ ∃ s
, e
|-= T
: Srt
s
.
Lemma
validity_coerce
:
∀ e
T
U
s
, e
|-= T
>> U
: s
→
e
|-= T
: Srt
s
∧ e
|-= U
: Srt
s
.
Lemma
validity_jeq
:
∀ e
t
u
T
, e
|-= t
= u
: T
→
(e
|-= t
: T
∧ e
|-= u
: T
) ∧
(T
= Srt
kind
∨ ∃ s
, e
|-= T
: Srt
s
).
Inductive
conv_env
: env
→ env
→ Prop
:=
| conv_env_hd
: ∀ e
t
u
s
, e
|-= t
= u
: Srt
s
→ conv_env
(t
:: e
) (u
:: e
)
| conv_env_tl
:
∀ e
f
t
, conv_in_env
e
f
→ conv_env
(t
:: e
) (t
:: f
).
Lemma
conv_env_conv_in_env
: ∀ e
e'
, conv_env
e
e'
→ conv_in_env
e
e'
.
Lemma
type_conv_env
: ∀ e
t
T
, e
|-= t
: T
→
∀ f
, conv_env
e
f
→ f
|-= t
: T
.
Lemma
coerce_conv_env
: ∀ e
T
U
s
, e
|-= T
>> U
: s
→
∀ f
, conv_env
e
f
→ f
|-= T
>> U
: s
.
Lemma
jeq_conv_env
: ∀ e
U
V
T
, e
|-= U
= V
: T
→
∀ f
, conv_env
e
f
→ f
|-= U
= V
: T
.
Lemma
functionality_rec
: ∀ g
(d
: term
) t
,
∀ d'
, g
|-= d
= d'
: t
→
∀ e
U
T
, e
|-= U
: T
→
∀ f
n
, sub_in_env
d
t
n
e
f
→ trunc
_
n
f
g
→
f
|-= (subst_rec
d
U
n
) = (subst_rec
d'
U
n
) : (subst_rec
d
T
n
).
Lemma
functionality
:forall e
(d
: term
) t
, e
|-= d
: t
→
∀ d'
, e
|-= d
= d'
: t
→
∀ U
T
, t
:: e
|-= U
: T
→
e
|-= (subst
d
U
) = (subst
d'
U
) : (subst
d
T
).
Lemma
jeq_type_l
: ∀ e
u
v
T
, e
|-= u
= v
: T
→ e
|-= u
: T
.
Lemma
jeq_type_r
: ∀ e
u
v
T
, e
|-= u
= v
: T
→ e
|-= v
: T
.
Lemma
coerce_sort_l
: ∀ e
U
V
s
, e
|-= U
>> V
: s
→ e
|-= U
: Srt
s
.
Lemma
coerce_sort_r
: ∀ e
U
V
s
, e
|-= U
>> V
: s
→ e
|-= V
: Srt
s
.
Hint
Resolve
jeq_type_l
jeq_type_r
coerce_sort_l
coerce_sort_r
: coc
.
Lemma
jeq_subst_par
: ∀ e
u
u'
v
v'
A
B
, e
|-= u
= u'
: A
→ A
:: e
|-= v
= v'
: B
→
e
|-= subst
u
v
= subst
u'
v'
: subst
u
B
.