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.Basic
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.TypesDepth
.
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
.
Definition
eq_kind
U
V
:= U
= Srt_l
kind
∧ V
= Srt_l
kind
.
Hint
Unfold
eq_kind
: coc
.
Lemma
eq_kind_sym
: ∀ U
V
, eq_kind
U
V
-> eq_kind
V
U
.
Hint
Resolve
eq_kind_sym
: coc
.
Lemma
eq_kind_typ_l_l
: ∀ U
V
, eq_kind
U
V
-> ∀ e
x1
x2
, ¬ (e
|-- U
-> x1
: x2
).
Lemma
eq_kind_typ_r_l
: ∀ U
V
, eq_kind
U
V
-> ∀ e
x1
x2
, ¬ (e
|-- V
-> x1
: x2
).
Lemma
eq_kind_typ_l_r
: ∀ U
V
, eq_kind
U
V
-> ∀ e
x1
x2
, ¬ (e
|-- x1
-> U
: x2
).
Lemma
eq_kind_typ_r_r
: ∀ U
V
, eq_kind
U
V
-> ∀ e
x1
x2
, ¬ (e
|-- x1
-> V
: x2
).
Hint
Resolve
eq_kind_typ_l_l
eq_kind_typ_l_r
eq_kind_typ_r_l
eq_kind_typ_r_r
: coc
.
Definition
equiv
e
A
B
:= (eq_kind
A
B
∨ ∃ s
, e
|-- A
>-> B
: s
).
Definition
equiv_sort
e
A
B
s
:= e
|-- A
>-> B
: s
.
Definition
tposr_eq_equiv
: ∀ e
A
B
s
, e
|-- A
~= B
: s
-> equiv
e
A
B
.
Hint
Resolve
tposr_eq_equiv
: ecoc
.
Definition
tposr_coerce_equiv
: ∀ e
A
B
s
, e
|-- A
>-> B
: s
-> equiv
e
A
B
.
Hint
Resolve
tposr_coerce_equiv
: ecoc
.
Hint
Unfold
eq_kind
equiv
: coc
.
Lemma
tposr_equiv_l
: ∀ e
A
B
, equiv
e
A
B
-> ∀ M
N
,
e
|-- M
-> N
: A
-> e
|-- M
-> N
: B
.
Lemma
tposrp_equiv_l
: ∀ e
A
B
, equiv
e
A
B
-> ∀ M
N
,
e
|-- M
-+> N
: A
-> e
|-- M
-+> N
: B
.
Lemma
tposr_equiv_r
: ∀ e
A
B
, equiv
e
A
B
-> ∀ M
N
,
e
|-- M
-> N
: B
-> e
|-- M
-> N
: A
.
Lemma
tposrd_unique_sort
: ∀ G
M
M'
M''
s
s'
n
m
, G
|-- M
-> M'
: Srt_l
s
[n
] ->
G
|-- M
-> M''
: Srt_l
s'
[m
] -> s
= s'
.
Lemma
tposr_unique_sort_right
: ∀ G
A
B
C
s
s'
, G
|-- A
-> C
: Srt_l
s
->
G
|-- B
-> C
: Srt_l
s'
-> s
= s'
.
Lemma
tposr_eq_unique_sort_right
: ∀ G
A
B
C
s
s'
, G
|-- A
~= C
: s
->
G
|-- B
~= C
: s'
-> s
= s'
.
Lemma
tposr_coerce_unique_sort_right
: ∀ G
A
B
C
s
s'
, G
|-- A
>-> C
: s
->
G
|-- B
>-> C
: s'
-> s
= s'
.
Lemma
equiv_sort_trans
: ∀ G
A
B
C
s
s'
, equiv_sort
G
A
C
s
-> equiv_sort
G
B
C
s'
-> equiv_sort
G
A
B
s
.
Lemma
equiv_trans
: ∀ G
A
B
C
, equiv
G
A
C
-> equiv
G
B
C
-> equiv
G
A
B
.
Lemma
equiv_coerce
: ∀ e
A
s
, e
|-- A
-> A
: Srt_l
s
->
∀ B
, equiv
e
A
B
-> e
|-- A
>-> B
: s
.
Lemma
equiv_sym
: ∀ G
A
B
, equiv
G
A
B
-> equiv
G
B
A
.
Hint
Resolve
equiv_sym
: coc
.
Require
Import
Lambda.TPOSR.Thinning
.
Lemma
equiv_sort_weak
: ∀ G
s
s'
, equiv
G
s
s'
-> ∀ a
, tposr_wf
(a
:: G
) -> equiv
(a
:: G
) s
s'
.
Lemma
inv_llift_sort
: ∀ t
s
n
, llift
n
t
= Srt_l
s
-> t
= Srt_l
s
.
Lemma
inv_subst_sort
: ∀ t
t'
n
s
, lsubst_rec
t
t'
n
= Srt_l
s
->
t
= Srt_l
s
∨ t'
= Srt_l
s
.