Library Lambda.JRussell.Types
Require
Import
Lambda.Terms
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Env
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: term
.
Reserved Notation
"G |-= T = U : s" (at
level
70, T
, U
, s
at
next
level
).
Reserved Notation
"G |-= T >> U : s" (at
level
70, T
, U
, s
at
next
level
).
Reserved Notation
"G |-= T : U" (at
level
70, T
, U
at
next
level
).
Definition
sum_sort
s1
s2
s3
:=
(s1
= set
∧ s2
= set
∧ s3
= set
) ∨
(s1
= prop
∧ s2
= prop
∧ s3
= prop
).
Inductive
coerce
: env
→ term
→ term
→ sort
→ Prop
:=
| coerce_conv
: ∀ e
A
B
s
, e
|-= A
= B
: Srt
s
→ e
|-= A
>> B
: s
| coerce_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_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
→
e
|-= U
: Srt
set
→ e
|-= U'
: Srt
set
→
U
:: e
|-= P
: Srt
prop
→
e
|-= Subset
U
P
>> U'
: set
| coerce_sub_r
: ∀ e
U
U'
P
,
e
|-= U
>> U'
: set
→
e
|-= U
: Srt
set
→ e
|-= U'
: Srt
set
→
U'
:: e
|-= P
: Srt
prop
→
e
|-= U
>> (Subset
U'
P
) : set
| coerce_sym
: ∀ e
U
V
s
, e
|-= U
>> V
: s
→ e
|-= V
>> U
: s
| coerce_trans
: ∀ e
A
B
C
s
,
e
|-= A
>> B
: s
→ e
|-= B
>> C
: s
→ e
|-= A
>> C
: s
where
"G |-= T >> U : s" := (coerce
G
T
U
s
)
with
jeq
: env
→ term
→ term
→ term
→ Prop
:=
| jeq_weak
: ∀ e
M
N
A
, e
|-= M
= N
: A
→
∀ B
s
, e
|-= B
: Srt
s
→
(B
:: e
) |-= lift
1 M
= lift
1 N
: lift
1 A
| jeq_prod
: ∀ e
U
V
U'
V'
s1
s2
,
e
|-= U
= U'
: Srt
s1
→ U
:: e
|-= V
= V'
: Srt
s2
→
e
|-= Prod
U
V
= Prod
U'
V'
: Srt
s2
| jeq_abs
: ∀ e
A
A'
s1
, e
|-= A
= A'
: Srt
s1
→
∀ B
s2
, (A
:: e
) |-= B
: Srt
s2
→
∀ M
M'
, (A
:: e
) |-= M
= M'
: B
→
e
|-= Abs
A
M
= Abs
A'
M'
: (Prod
A
B
)
| jeq_app
: ∀ e
A
B
M
M'
, e
|-= M
= M'
: (Prod
A
B
) →
∀ N
N'
, e
|-= N
= N'
: A
→
e
|-= App
M
N
= App
M'
N'
: subst
N
B
| jeq_beta
: ∀ e
A
s1
, e
|-= A
: Srt
s1
→
∀ B
s2
, (A
:: e
) |-= B
: Srt
s2
→
∀ M
, (A
:: e
) |-= M
: B
→
∀ N
, e
|-= N
: A
→
e
|-= App
(Abs
A
M
) N
= subst
N
M
: subst
N
B
| jeq_sum
: ∀ e
A
A'
s1
, e
|-= A
= A'
: Srt
s1
→
∀ B
B'
s2
, (A
:: e
) |-= B
= B'
: Srt
s2
→
∀ s3
, sum_sort
s1
s2
s3
→
e
|-= Sum
A
B
= Sum
A'
B'
: Srt
s3
| jeq_pair
: ∀ e
A
A'
s1
, e
|-= A
= A'
: Srt
s1
→
∀ B
B'
s2
, (A
:: e
) |-= B
= B'
: Srt
s2
→
∀ s3
, sum_sort
s1
s2
s3
→
∀ u
u'
, e
|-= u
= u'
: A
→
∀ v
v'
, e
|-= v
= v'
: subst
u
B
→
e
|-= Pair
(Sum
A
B
) u
v
= Pair
(Sum
A'
B'
) u'
v'
: Sum
A
B
| jeq_pi1
: ∀ e
t
t'
A
B
, e
|-= t
= t'
: Sum
A
B
→
e
|-= Pi1
t
= Pi1
t'
: A
| jeq_pi1_red
: ∀ e
A
s1
, e
|-= A
: Srt
s1
→
∀ B
s2
, (A
:: e
) |-= B
: Srt
s2
→
∀ s3
, sum_sort
s1
s2
s3
→
∀ u
, e
|-= u
: A
→ ∀ v
, e
|-= v
: subst
u
B
→
e
|-= Pi1
(Pair
(Sum
A
B
) u
v
) = u
: A
| jeq_pi2
: ∀ e
t
t'
A
B
, e
|-= t
= t'
: Sum
A
B
→
e
|-= Pi2
t
= Pi2
t'
: subst
(Pi1
t
) B
| jeq_pi2_red
: ∀ e
A
s1
, e
|-= A
: Srt
s1
→
∀ B
s2
, (A
:: e
) |-= B
: Srt
s2
→
∀ s3
, sum_sort
s1
s2
s3
→
∀ u
, e
|-= u
: A
→ ∀ v
, e
|-= v
: subst
u
B
→
e
|-= Pi2
(Pair
(Sum
A
B
) u
v
) = v
: subst
u
B
| jeq_subset
: ∀ e
A
A'
, e
|-= A
= A'
: Srt
set
→
∀ B
B'
, (A
:: e
) |-= B
= B'
: Srt
prop
→
e
|-= Subset
A
B
= Subset
A'
B'
: Srt
set
| jeq_refl
: ∀ e
M
A
, e
|-= M
: A
→ e
|-= M
= M
: A
| jeq_sym
: ∀ e
M
N
A
, e
|-= M
= N
: A
→ e
|-= N
= M
: A
| jeq_trans
: ∀ e
M
N
P
A
, e
|-= M
= N
: A
→ e
|-= N
= P
: A
→ e
|-= M
= P
: A
| jeq_conv
: ∀ e
M
N
A
B
s
, e
|-= M
= N
: A
→ e
|-= A
>> B
: s
→ e
|-= M
= N
: B
where
"G |-= T = U : s" := (jeq
G
T
U
s
)
with
typ
: env
→ term
→ term
→ Prop
:=
| type_prop
: nil
|-= (Srt
prop
) : (Srt
kind
)
| type_set
: nil
|-= (Srt
set
) : (Srt
kind
)
| type_var
:
∀ e
T
s
, e
|-= T
: Srt
s
→ (T
:: e
) |-= (Ref
0) : (lift
1 T
)
| type_weak
:
∀ e
t
T
, e
|-= t
: T
→ ∀ U
s
, e
|-= U
: Srt
s
→
(U
:: e
) |-= lift
1 t
: lift
1 T
| type_abs
:
∀ e
T
s1
,
e
|-= T
: (Srt
s1
) →
∀ M
(U
: term
) s2
,
(T
:: e
) |-= U
: (Srt
s2
) →
(T
:: e
) |-= M
: U
→
e
|-= (Abs
T
M
) : (Prod
T
U
)
| type_app
:
∀ e
v
(V
: term
), e
|-= v
: V
→
∀ u
(Ur
: term
), e
|-= u
: (Prod
V
Ur
) →
e
|-= (App
u
v
) : (subst
v
Ur
)
| type_pair
:
∀ e
(U
: term
) s1
, e
|-= U
: (Srt
s1
) →
∀ u
, e
|-= u
: U
→
∀ V
s2
, (U
:: e
) |-= V
: (Srt
s2
) →
∀ v
, e
|-= v
: (subst
u
V
) →
∀ s3
, sum_sort
s1
s2
s3
→
e
|-= (Pair
(Sum
U
V
) u
v
) : (Sum
U
V
)
| type_prod
:
∀ e
T
s1
,
e
|-= T
: (Srt
s1
) →
∀ (U
: term
) s2
,
(T
:: e
) |-= U
: (Srt
s2
) →
e
|-= (Prod
T
U
) : (Srt
s2
)
| type_sum
:
∀ e
T
s1
,
e
|-= T
: (Srt
s1
) →
∀ (U
: term
) s2
,
(T
:: e
) |-= U
: (Srt
s2
) →
∀ s3
, sum_sort
s1
s2
s3
→
e
|-= (Sum
T
U
) : Srt
s3
| type_subset
:
∀ e
T
, e
|-= T
: (Srt
set
) →
∀ (U
: term
), (T
:: e
) |-= U
: (Srt
prop
) →
e
|-= (Subset
T
U
) : (Srt
set
)
| type_pi1
:
∀ e
t
U
V
, e
|-= t
: (Sum
U
V
) →
e
|-= (Pi1
t
) : U
| type_pi2
:
∀ e
t
U
V
, e
|-= t
: (Sum
U
V
) →
e
|-= (Pi2
t
) : (subst
(Pi1
t
) V
)
| type_conv
:
∀ e
t
(U
V
: term
),
e
|-= t
: U
→
∀ s
, e
|-= U
>> V
: s
→
e
|-= t
: V
where
"G |-= T : U" := (typ
G
T
U
).
Inductive
consistent
: env
→ Prop
:=
| consistent_nil
: consistent
nil
| consistent_cons
: ∀ e
, consistent
e
→
∀ T
s
, e
|-= T
: Srt
s
→ consistent
(T
:: e
).
Hint
Resolve
consistent_nil
consistent_cons
: coc
.
Scheme
typ_dep
:= Induction
for
typ
Sort
Prop
.
Scheme
typ_coerce_mutind
:= Induction
for
typ
Sort
Prop
with
coerce_typ_mutind
:= Induction
for
coerce
Sort
Prop
.
Scheme
typ_coerce_jeq_mutind
:= Induction
for
typ
Sort
Prop
with
coerce_typ_jeq_mutind
:= Induction
for
coerce
Sort
Prop
with
jeq_typ_coerce_mutind
:= Induction
for
jeq
Sort
Prop
.