Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.Conv_Dec
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.InvLiftSubst
.
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
.
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
.
Ltac
extensionalpattern
a
:=
let
t
:= fresh
"t" in
(
let
H
:= fresh
"H" in
(
let
Heqt
:= fresh
"Heqt" in
(
set
(t
:= a
) ; intro
H
;
assert
(Heqt
: t
= a
) ; [ (unfold
t
; reflexivity
) |
generalize
H
Heqt
; clear
H
Heqt
;
generalize
t
; clear
t
; intros
t
]))).
Lemma
jeq_not_kind
: ∀ e
T
U
W
, e
|-= T
= U
: W
→ (T
= Srt
kind
→ False
) ∧ (U
= Srt
kind
→ False
).
Lemma
coerce_not_kind
: ∀ e
T
U
s
, e
|-= T
>> U
: s
→ (T
= Srt
kind
→ False
) ∧ (U
= Srt
kind
→ False
).
Inductive
equiv
: env
→ term
→ term
→ Prop
:=
|equiv_refl : ∀ e
T
, equiv
e
T
T
|equiv_step : ∀ e
T
U
s
, e
|-= T
>> U
: s
→ ∀ V
, equiv
e
U
V
→ equiv
e
T
V
.
Lemma
equiv_lift
: ∀ e
T
U
, equiv
e
T
U
→
∀ V
s
, e
|-= V
: Srt
s
→ equiv
(V
:: e
) (lift
1 T
) (lift
1 U
).
Hint
Resolve
equiv_refl
: coc
.
Lemma
equiv_coerce
: ∀ e
V
V'
, equiv
e
V
V'
→ ∀ T
U
,
∀ s
, e
|-= T
>> U
: s
→
∀ s'
, e
|-= T
>> V
: s'
→ equiv
e
U
V'
.
Lemma
equiv_kind
: ∀ e
U
, equiv
e
U
(Srt
kind
) → U
= Srt
kind
.
Lemma
generation_sort
: ∀ e
s
T
, e
|-= Srt
s
: T
→ equiv
e
T
(Srt
kind
).
Lemma
inv_lift_ref
: ∀ t
n
, lift
1 t
= Ref
n
→ ∃ n'
, t
= Ref
n'
∧ S
n'
= n
.
Lemma
generation_var_aux
: ∀ e
T
A
, e
|-= T
: A
→
∀ n
, T
= Ref
n
→
∃ B
, item_lift
B
e
n
∧ equiv
e
A
B
.
Lemma
generation_var
: ∀ e
n
A
, e
|-= Ref
n
: A
→
∃ B
, item_lift
B
e
n
∧ equiv
e
A
B
.
Lemma
generation_prod_aux
: ∀ e
T
A
, e
|-= T
: A
→ ∀ U
V
, T
= Prod
U
V
→
∃ s1
, ∃ s2
, e
|-= U
: Srt
s1
∧ U
:: e
|-= V
: Srt
s2
∧ equiv
e
A
(Srt
s2
).
Lemma
generation_prod
: ∀ e
U
V
A
, e
|-= Prod
U
V
: A
→
∃ s1
, ∃ s2
, e
|-= U
: Srt
s1
∧ U
:: e
|-= V
: Srt
s2
∧ equiv
e
A
(Srt
s2
).
Lemma
generation_sum_aux
: ∀ e
T
A
, e
|-= T
: A
→ ∀ U
V
, T
= Sum
U
V
→
∃ s1
, ∃ s2
, ∃ s3
,
e
|-= U
: Srt
s1
∧
U
:: e
|-= V
: Srt
s2
∧
sum_sort
s1
s2
s3
∧
equiv
e
A
(Srt
s3
).
Lemma
generation_sum
: ∀ e
U
V
A
, e
|-= Sum
U
V
: A
→
∃ s1
, ∃ s2
, ∃ s3
,
e
|-= U
: Srt
s1
∧
U
:: e
|-= V
: Srt
s2
∧
sum_sort
s1
s2
s3
∧
equiv
e
A
(Srt
s3
).
Lemma
generation_lambda_aux
: ∀ e
t
A
, e
|-= t
: A
→ ∀ T
M
, t
= Abs
T
M
→
∃ s1
, ∃ s2
, ∃ C
,
e
|-= T
: Srt
s1
∧
T
:: e
|-= C
: Srt
s2
∧
T
:: e
|-= M
: C
∧
equiv
e
A
(Prod
T
C
).
Lemma
generation_lambda
: ∀ e
T
M
A
, e
|-= Abs
T
M
: A
→
∃ s1
, ∃ s2
, ∃ C
,
e
|-= T
: Srt
s1
∧
T
:: e
|-= C
: Srt
s2
∧
T
:: e
|-= M
: C
∧
equiv
e
A
(Prod
T
C
).
Lemma
generation_app_aux
: ∀ e
t
C
, e
|-= t
: C
→ ∀ M
N
, t
= App
M
N
→
∃ A
, ∃ B
,
e
|-= M
: Prod
A
B
∧
e
|-= N
: A
∧
equiv
e
C
(subst
N
B
).
Lemma
generation_app
: ∀ e
M
N
C
, e
|-= App
M
N
: C
→
∃ A
, ∃ B
,
e
|-= M
: Prod
A
B
∧
e
|-= N
: A
∧
equiv
e
C
(subst
N
B
).
Lemma
generation_pair_aux
: ∀ e
t
C
, e
|-= t
: C
→ ∀ T
M
N
, t
= Pair
T
M
N
→
∃ A
, ∃ B
, ∃ s1
, ∃ s2
, ∃ s3
,
T
= Sum
A
B
∧
e
|-= A
: Srt
s1
∧
A
:: e
|-= B
: Srt
s2
∧
sum_sort
s1
s2
s3
∧
e
|-= M
: A
∧
e
|-= N
: subst
M
B
∧
equiv
e
C
(Sum
A
B
).
Lemma
generation_pair
: ∀ e
T
M
N
C
, e
|-= Pair
T
M
N
: C
→
∃ A
, ∃ B
, ∃ s1
, ∃ s2
, ∃ s3
,
T
= Sum
A
B
∧
e
|-= A
: Srt
s1
∧
A
:: e
|-= B
: Srt
s2
∧
sum_sort
s1
s2
s3
∧
e
|-= M
: A
∧
e
|-= N
: subst
M
B
∧
equiv
e
C
(Sum
A
B
).
Lemma
generation_pi1_aux
: ∀ e
t
C
, e
|-= t
: C
→ ∀ M
, t
= Pi1
M
→
∃ A
, ∃ B
,
e
|-= M
: Sum
A
B
∧
equiv
e
C
A
.
Lemma
generation_pi1
: ∀ e
M
C
, e
|-= Pi1
M
: C
→
∃ A
, ∃ B
,
e
|-= M
: Sum
A
B
∧
equiv
e
C
A
.
Lemma
generation_pi2_aux
: ∀ e
t
C
, e
|-= t
: C
→ ∀ M
, t
= Pi2
M
→
∃ A
, ∃ B
,
e
|-= M
: Sum
A
B
∧
equiv
e
C
(subst
(Pi1
M
) B
).
Lemma
generation_pi2
: ∀ e
M
C
, e
|-= Pi2
M
: C
→
∃ A
, ∃ B
,
e
|-= M
: Sum
A
B
∧
equiv
e
C
(subst
(Pi1
M
) B
).