Library Lambda.CCSum.Inversion
Require
Import
Lambda.Terms
.
Require
Import
Lambda.Reduction
.
Require
Import
Lambda.Conv
.
Require
Import
Lambda.LiftSubst
.
Require
Import
Lambda.CCSum.Types
.
Implicit
Types
i
k
m
n
p
: nat
.
Implicit
Type
s
: sort
.
Implicit
Types
A
B
M
N
T
t
u
v
: term
.
Definition
inv_type
(P
: Prop
) e
t
T
: Prop
:=
match
t
with
| Srt
prop
⇒ conv
T
(Srt
kind
) → P
| Srt
set
⇒ conv
T
(Srt
kind
) → P
| Srt
kind
⇒ True
| Ref
n
⇒ ∀ x
: term
, item
_
x
e
n
→ conv
T
(lift
(S
n
) x
) → P
| Abs
A
M
⇒
∀ s1
s2
(U
: term
),
typ
e
A
(Srt
s1
) →
typ
(A
:: e
) M
U
→ typ
(A
:: e
) U
(Srt
s2
) → conv
T
(Prod
A
U
) → P
| App
u
v
⇒
∀ Ur
V
: term
,
typ
e
v
V
→ typ
e
u
(Prod
V
Ur
) → conv
T
(subst
v
Ur
) → P
| Pair
T'
u
v
⇒
∀ U
s1
, typ
e
U
(Srt
s1
) →
typ
e
u
U
→
∀ V
s2
, typ
(U
:: e
) V
(Srt
s2
) →
typ
e
v
(subst
u
V
) → T'
= (Sum
U
V
) → conv
T
(Sum
U
V
) → P
| Prod
A
B
⇒
∀ s1
s2
,
typ
e
A
(Srt
s1
) → typ
(A
:: e
) B
(Srt
s2
) → conv
T
(Srt
s2
) → P
| Sum
A
B
⇒
∀ s1
s2
,
typ
e
A
(Srt
s1
) → typ
(A
:: e
) B
(Srt
s2
) → conv
T
(Srt
s2
) → P
| Subset
A
B
⇒
∀ s1
s2
,
typ
e
A
(Srt
set
) → typ
(A
:: e
) B
(Srt
prop
) → conv
T
(Srt
set
) → P
| Pi1
t
⇒
∀ U
V
,
typ
e
t
(Sum
U
V
) → conv
T
U
→ P
| Pi2
t
⇒
∀ U
V
,
typ
e
t
(Sum
U
V
) → conv
T
(subst
(Pi1
t
) V
) → P
end
.
Lemma
inv_type_conv
:
∀ (P
: Prop
) e
t
(U
V
: term
),
conv
U
V
→ inv_type
P
e
t
U
→ inv_type
P
e
t
V
.
Theorem
typ_inversion
:
∀ (P
: Prop
) e
t
T
, typ
e
t
T
→ inv_type
P
e
t
T
→ P
.
Lemma
inv_typ_kind
: ∀ e
t
, ¬ typ
e
(Srt
kind
) t
.
Lemma
inv_typ_prop
: ∀ e
T
, typ
e
(Srt
prop
) T
→ conv
T
(Srt
kind
).
Lemma
inv_typ_set
: ∀ e
T
, typ
e
(Srt
set
) T
→ conv
T
(Srt
kind
).
Lemma
inv_typ_ref
:
∀ (P
: Prop
) e
T
n
,
typ
e
(Ref
n
) T
→
(∀ U
: term
, item
_
U
e
n
→ conv
T
(lift
(S
n
) U
) → P
) → P
.
Lemma
inv_typ_abs
:
∀ (P
: Prop
) e
A
M
(U
: term
),
typ
e
(Abs
A
M
) U
→
(∀ s1
s2
T
,
typ
e
A
(Srt
s1
) →
typ
(A
:: e
) M
T
→ typ
(A
:: e
) T
(Srt
s2
) → conv
(Prod
A
T
) U
→ P
) →
P
.
Lemma
inv_typ_app
:
∀ (P
: Prop
) e
u
v
T
,
typ
e
(App
u
v
) T
→
(∀ V
Ur
: term
,
typ
e
u
(Prod
V
Ur
) → typ
e
v
V
→ conv
T
(subst
v
Ur
) → P
) → P
.
Lemma
inv_typ_pair
:
∀ (P
: Prop
) e
T
u
v
T'
,
typ
e
(Pair
T
u
v
) T'
→
(∀ T
U
V
: term
, ∀ s1
s2
,
typ
e
U
(Srt
s1
) →
typ
e
u
U
→ typ
(U
:: e
) V
(Srt
s2
) → typ
e
v
(subst
u
V
) →
T
= (Sum
U
V
) → conv
T'
(Sum
U
V
) → P
) → P
.
Lemma
inv_typ_prod
:
∀ (P
: Prop
) e
T
(U
s
: term
),
typ
e
(Prod
T
U
) s
→
(∀ s1
s2
,
typ
e
T
(Srt
s1
) → typ
(T
:: e
) U
(Srt
s2
) → conv
(Srt
s2
) s
→ P
) → P
.
Lemma
inv_typ_sum
:
∀ (P
: Prop
) e
T
(U
s
: term
),
typ
e
(Sum
T
U
) s
→
(∀ s1
s2
,
typ
e
T
(Srt
s1
) → typ
(T
:: e
) U
(Srt
s2
) → conv
(Srt
s2
) s
→ P
) → P
.
Lemma
inv_typ_subset
:
∀ (P
: Prop
) e
T
(U
s
: term
),
typ
e
(Subset
T
U
) s
→
(typ
e
T
(Srt
set
) → typ
(T
:: e
) U
(Srt
prop
) → conv
(Srt
set
) s
→ P
) → P
.
Lemma
inv_typ_pi1
:
∀ (P
: Prop
) e
t
T
,
typ
e
(Pi1
t
) T
→
(∀ U
V
, typ
e
t
(Sum
U
V
) → conv
U
T
→ P
) → P
.
Lemma
inv_typ_pi2
:
∀ (P
: Prop
) e
t
T
,
typ
e
(Pi2
t
) T
→
(∀ U
V
, typ
e
t
(Sum
U
V
) → conv
(subst
(Pi1
t
) V
) T
→ P
) → P
.
Lemma
typ_mem_kind
: ∀ e
t
T
, mem_sort
kind
t
→ ¬ typ
e
t
T
.
Lemma
inv_typ_conv_kind
: ∀ e
t
T
, conv
t
(Srt
kind
) → ¬ typ
e
t
T
.
Lemma
type_pair_unique
: ∀ e
t
T
, typ
e
t
T
→ ∀ U
V
u
v
, t
= (Pair
(Sum
U
V
) u
v
) →
conv
T
(Sum
U
V
).
Lemma
type_pair_unique2
: ∀ e
t
T
, typ
e
t
T
→
∀ T'
u
v
, t
= (Pair
T'
u
v
) → ∃ U
, ∃ V
, T'
= Sum
U
V
∧ conv
T
(Sum
U
V
).