Require
Import
Lambda.Utils
.
Require
Import
Lambda.Tactics
.
Require
Import
Lambda.MyList
.
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.Thinning
.
Require
Import
Lambda.TPOSR.LeftReflexivity
.
Require
Import
Lambda.TPOSR.Substitution
.
Require
Import
Lambda.TPOSR.SubstitutionTPOSR
.
Require
Import
Lambda.TPOSR.RightReflexivity
.
Require
Import
Lambda.TPOSR.CtxCoercion
.
Require
Import
Lambda.TPOSR.CtxConversion
.
Require
Import
Lambda.TPOSR.Equiv
.
Require
Import
Lambda.TPOSR.Generation
.
Require
Import
Lambda.TPOSR.Validity
.
Require
Import
Lambda.TPOSR.UnicityOfSorting
.
Require
Import
Lambda.TPOSR.TypesDepth
.
Require
Import
Lambda.TPOSR.TypesFunctionality
.
Require
Import
Lambda.TPOSR.UniquenessOfTypes
.
Require
Import
Lambda.TPOSR.ChurchRosserDepth
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: lterm
.
Corollary
church_rosser
: ∀ G
M
N
A
, G
|-- M
-> N
: A
-> ∀ P
B
, G
|-- M
-> P
: B
->
∃ Q
,
(G
|-- N
-> Q
: A
∧
G
|-- N
-> Q
: B
∧
G
|-- P
-> Q
: A
∧
G
|-- P
-> Q
: B
).
Inductive
tposrp_n
: lenv
-> lterm
-> lterm
-> lterm
-> nat
-> Prop
:=
| tposrp_n_tposr
: ∀ e
X
Y
Z
, e
|-- X
-> Y
: Z
-> tposrp_n
e
X
Y
Z
1
| tposrp_n_trans
: ∀ e
W
X
Z
, e
|-- W
-> X
: Z
-> ∀ Y
m
, tposrp_n
e
X
Y
Z
m
->
tposrp_n
e
W
Y
Z
(S
m
).
Lemma
tposrp_n_tposrp
: ∀ e
t
u
T
n
, tposrp_n
e
t
u
T
n
-> tposrp
e
t
u
T
.
Lemma
tposrp_n_cr
:
∀ n
m
e
A
B
T
, tposrp_n
e
A
B
T
n
-> ∀ C
, tposrp_n
e
A
C
T
m
->
∃ D
, tposrp_n
e
B
D
T
m
∧ tposrp_n
e
C
D
T
n
.
Lemma
tposrp_n_transitive
: ∀ e
t
u
T
n
, tposrp_n
e
t
u
T
n
->
∀ v
m
, tposrp_n
e
u
v
T
m
->
tposrp_n
e
t
v
T
(n
+ m
).
Lemma
tposrp_tposrp_n
: ∀ e
t
u
T
, tposrp
e
t
u
T
->
∃ n
, tposrp_n
e
t
u
T
n
.
Corollary
tposrp_cr
:
∀ e
A
B
T
, tposrp
e
A
B
T
-> ∀ C
, tposrp
e
A
C
T
->
∃ D
, tposrp
e
B
D
T
∧ tposrp
e
C
D
T
.
Corollary
tposr_eq_cr
: ∀ e
A
B
s
, e
|-- A
~= B
: s
->
∃ C
, tposrp
e
A
C
(Srt_l
s
) ∧ tposrp
e
B
C
(Srt_l
s
).
Lemma
tposr_sort_aux
: ∀ e
T
T'
Ts'
, tposr
e
T
T'
Ts'
-> ∀ s
, T
= Srt_l
s
-> T'
= Srt_l
s
.
Lemma
tposr_sort
: ∀ e
s
T'
Ts'
, tposr
e
(Srt_l
s
) T'
Ts'
-> T'
= Srt_l
s
.
Lemma
tposrp_sort_aux
: ∀ e
T
T'
Ts'
, tposrp
e
T
T'
Ts'
-> ∀ s
, T
= Srt_l
s
-> T'
= Srt_l
s
.
Lemma
tposrp_sort
: ∀ e
s
T'
Ts'
, tposrp
e
(Srt_l
s
) T'
Ts'
-> T'
= Srt_l
s
.
Lemma
tposr_eq_sort
: ∀ e
s
s0
s'
, tposr_eq
e
(Srt_l
s
) (Srt_l
s0
) s'
-> s
= s0
.
Lemma
tposr_sort_kinded_depth
: ∀ n
e
T
U
V
, e
|-- T
-> U
: V
[n
] ->
∀ s
, T
= Srt_l
s
-> V
= kind
.
Lemma
tposr_sort_kinded
: ∀ e
s
V
, e
|-- s
-> s
: V
-> V
= kind
.
Lemma
in_set_not_sort
: ∀ e
t
T
, e
|-- t
-> t
: T
->
T
= Srt_l
set
-> ∀ s
, t
≠ Srt_l
s
.
Lemma
tposr_sort_eq_aux
: ∀ e
t
u
T
, e
|-- t
-> u
: T
->
∀ s
, t
= Srt_l
s
-> u
= Srt_l
s
.
Lemma
tposr_sort_eq
: ∀ e
s
u
T
, e
|-- s
-> u
: T
-> u
= s
.
Lemma
tposrp_sort_eq_aux
: ∀ e
t
u
T
, e
|-- t
-+> u
: T
->
∀ s
, t
= Srt_l
s
-> u
= Srt_l
s
.
Lemma
tposrp_sort_eq
: ∀ e
s
u
T
, e
|-- s
-+> u
: T
-> u
= s
.
Lemma
tposr_eq_sort_tposrp_aux
: ∀ e
t
u
s
, e
|-- t
~= u
: s
->
∀ s'
, t
= Srt_l
s'
-> e
|-- u
-+> Srt_l
s'
: s
.
Lemma
tposr_eq_sort_tposrp
: ∀ e
s
u
s'
, e
|-- s
~= u
: s'
->
e
|-- u
-+> s
: s'
.
Lemma
tposr_prod_prod
: ∀ e
t
u
T
, e
|-- t
-> u
: T
->
∀ A
B
, t
= Prod_l
A
B
-> exists2
A'
B'
, u
= Prod_l
A'
B'
.
Lemma
tposr_sum_sum
: ∀ e
t
u
T
, e
|-- t
-> u
: T
->
∀ A
B
, t
= Sum_l
A
B
-> exists2
A'
B'
, u
= Sum_l
A'
B'
.
Lemma
tposr_subset_subset
: ∀ e
t
u
T
, e
|-- t
-> u
: T
->
∀ A
B
, t
= Subset_l
A
B
-> exists2
A'
B'
, u
= Subset_l
A'
B'
.
Lemma
tposrp_prod_prod_aux
: ∀ e
t
u
T
, e
|-- t
-+> u
: T
->
∀ A
B
, t
= Prod_l
A
B
-> exists2
A'
B'
, u
= Prod_l
A'
B'
.
Lemma
tposrp_sum_sum_aux
: ∀ e
t
u
T
, e
|-- t
-+> u
: T
->
∀ A
B
, t
= Sum_l
A
B
-> exists2
A'
B'
, u
= Sum_l
A'
B'
.
Lemma
tposrp_subset_subset_aux
: ∀ e
t
u
T
, e
|-- t
-+> u
: T
->
∀ A
B
, t
= Subset_l
A
B
-> exists2
A'
B'
, u
= Subset_l
A'
B'
.
Lemma
tposrp_prod_prod
: ∀ e
A
B
u
T
, e
|-- Prod_l
A
B
-+> u
: T
->
exists2
A'
B'
, u
= Prod_l
A'
B'
.
Lemma
tposrp_sum_sum
: ∀ e
A
B
u
T
, e
|-- Sum_l
A
B
-+> u
: T
->
exists2
A'
B'
, u
= Sum_l
A'
B'
.
Lemma
tposrp_subset_subset
: ∀ e
A
B
u
T
, e
|-- Subset_l
A
B
-+> u
: T
->
exists2
A'
B'
, u
= Subset_l
A'
B'
.
Lemma
tposr_eq_sort_prod
: ∀ e
s
t
u
s'
, ¬ e
|-- s
~= Prod_l
t
u
: s'
.
Lemma
tposr_eq_sort_sum
: ∀ e
s
t
u
s'
, ¬ e
|-- s
~= Sum_l
t
u
: s'
.
Lemma
tposr_eq_sort_subset
: ∀ e
s
t
u
s'
, ¬ e
|-- s
~= Subset_l
t
u
: s'
.
Lemma
tposr_eq_prod_sum
: ∀ e
t
u
t'
u'
s'
, ¬ e
|-- Prod_l
t
u
~= Sum_l
t'
u'
: s'
.
Lemma
tposr_eq_prod_subset
: ∀ e
t
u
t'
u'
s'
, ¬ e
|-- Prod_l
t
u
~= Subset_l
t'
u'
: s'
.
Lemma
tposr_eq_sum_subset
: ∀ e
t
u
t'
u'
s'
, ¬ e
|-- Sum_l
t
u
~= Subset_l
t'
u'
: s'
.
Lemma
tposr_coerce_sorts
: ∀ e
T
U
s'
, tposr_coerce
e
T
U
s'
->
∀ s
, (e
|-- T
~= (Srt_l
s
) : s'
-> e
|-- U
~= (Srt_l
s
) : s'
) ∧
(e
|-- U
~= (Srt_l
s
) : s'
-> e
|-- T
~= (Srt_l
s
) : s'
).
Lemma
tposr_coerce_sort_l
: ∀ e
s
u
s'
, e
|-- s
>-> u
: s'
-> e
|-- u
-+> s
: s'
.
Lemma
tposr_coerce_sort_r
: ∀ e
s
u
s'
, e
|-- u
>-> s
: s'
-> e
|-- u
-+> s
: s'
.
Lemma
tposr_coerce_eq_sort_aux
: ∀ e
T
U
s'
, tposr_coerce
e
T
U
s'
->
∀ s
s0
, T
= (Srt_l
s
) -> U
= (Srt_l
s0
) -> s
= s0
.
Lemma
tposr_coerce_eq_sort
: ∀ e
s
s0
s'
, e
|-- (Srt_l
s
) >-> (Srt_l
s0
) : s'
->
s
= s0
.
Lemma
equiv_eq_sort
: ∀ e
s
s0
, equiv
e
(Srt_l
s
) (Srt_l
s0
) -> s
= s0
.
Lemma
tposrp_conv_env
: ∀ e
A
B
T
, tposrp
e
A
B
T
->
∀ f
, conv_in_env
e
f
-> tposrp
f
A
B
T
.
Lemma
tposrp_tposr_eq_aux
: ∀ e
A
B
T
, tposrp
e
A
B
T
-> ∀ s
, T
= Srt_l
s
-> e
|-- A
~= B
: s
.
Lemma
tposrp_tposr_eq
: ∀ e
A
B
s
, tposrp
e
A
B
(Srt_l
s
) -> e
|-- A
~= B
: s
.
Lemma
tposrp_pi_aux
: ∀ e
T
T'
Ts
, tposrp
e
T
T'
Ts
->
∀ A
B
, T
= Prod_l
A
B
-> ∀ s
, Ts
= Srt_l
s
-> exists3
A'
B'
s1
, T'
= Prod_l
A'
B'
∧
tposrp
e
A
A'
(Srt_l
s1
) ∧ tposrp
(A
:: e
) B
B'
(Srt_l
s
).
Lemma
tposrp_pi
: ∀ e
A
B
T
s
, tposrp
e
(Prod_l
A
B
) T
(Srt_l
s
) ->
exists3
A'
B'
s1
, T
= Prod_l
A'
B'
∧
tposrp
e
A
A'
(Srt_l
s1
) ∧ tposrp
(A
:: e
) B
B'
(Srt_l
s
).
Corollary
injectivity_of_pi
: ∀ e
A
A'
B
B'
s
, e
|-- Prod_l
A
B
~= Prod_l
A'
B'
: s
->
∃ s1
, e
|-- A
~= A'
: s1
∧ A
:: e
|-- B
~= B'
: s
.
Lemma
tposrp_sum_aux
: ∀ e
T
T'
Ts
, tposrp
e
T
T'
Ts
->
∀ A
B
, T
= Sum_l
A
B
-> ∀ s
, Ts
= Srt_l
s
->
exists4
A'
B'
s1
s2
, T'
= Sum_l
A'
B'
∧
tposrp
e
A
A'
(Srt_l
s1
) ∧ tposrp
(A
:: e
) B
B'
(Srt_l
s2
) ∧
sum_sort
s1
s2
s
.
Lemma
tposrp_sum
: ∀ e
A
B
T
s
, tposrp
e
(Sum_l
A
B
) T
(Srt_l
s
) ->
exists4
A'
B'
s1
s2
, T
= Sum_l
A'
B'
∧
tposrp
e
A
A'
(Srt_l
s1
) ∧ tposrp
(A
:: e
) B
B'
(Srt_l
s2
) ∧
sum_sort
s1
s2
s
.
Corollary
injectivity_of_sum
: ∀ e
A
A'
B
B'
s
, e
|-- Sum_l
A
B
~= Sum_l
A'
B'
: s
->
exists2
s1
s2
, e
|-- A
~= A'
: s1
∧ A
:: e
|-- B
~= B'
: s2
∧ sum_sort
s1
s2
s
.
Lemma
tposrp_subset_aux
: ∀ e
T
T'
Ts
, tposrp
e
T
T'
Ts
->
∀ A
B
, T
= Subset_l
A
B
-> ∀ s
, Ts
= Srt_l
s
->
exists2
A'
B'
, T'
= Subset_l
A'
B'
∧
tposrp
e
A
A'
(Srt_l
set
) ∧ tposrp
(A
:: e
) B
B'
(Srt_l
prop
).
Lemma
tposrp_subset
: ∀ e
U
P
T'
(s
: sort
), e
|-- Subset_l
U
P
-+> T'
: s
->
exists2
U'
P'
, T'
= Subset_l
U'
P'
∧
e
|-- U
-+> U'
: set
∧ (U
:: e
) |-- P
-+> P'
: prop
.
Corollary
injectivity_of_subset
: ∀ e
U
P
U'
P'
s
, e
|-- Subset_l
U
P
~= Subset_l
U'
P'
: s
->
e
|-- U
~= U'
: set
∧ U
:: e
|-- P
~= P'
: prop
.