Union: elimination forms for union and iexistsTo assist in typechecking code that operates on a union, we have
unpack and its dependently typed analogue unpack_dep:
unpack : intersect (i : level) (a : U i) (b : a -> U i) (c : U i) .
(union (x : a) . b x) -> (intersect (x : a) . b x -> c) -> c
= fn u f . f u
unpack_dep : intersect (i : level) (a : U i) (b : a -> U i) .
forall (c : intersect (x : a) . b x -> U i) (u : union (x : a) . b x) .
(intersect (x : a) . forall (y : b x) . c y) -> c u
= fn c u f . f u
The syntactic sugar unpack x = u in m is accepted for
`unpack u (fn x . m).
Since unions are, at least in part, for managing situations in which
some variables are hidden, everything in this module takes every
argument invisibly (i.e., using a intersect) that can be taken
that way.
Beyond that, observe that in the body of unpack and unpack_dep,
the union’s hidden witness (x) is bound using intersection, which
means that the body cannot use that variable.
This is essential, due to the nature of union types. Nevertheless,
that limitation can be problematic when defining a type based on a
union, so we have a variation on unpack for defining types:
unpackt : intersect (i : level) .
forall (a : U i) (b : a -> U i) .
(forall (x : a) . b x -> U i) -> (union (x : a) . b x) -> U i
= fn a b c u .
union (x : a) . exists (y : b x) . y = u : (union (x1 : a) . b x1) & c x y
The syntactic sugar unpackt (x , y) = u in b is accepted for
`unpackt _ _ (fn x y . b) u.
The unpackt type has an introduction and elimination form:
unpackt_intro : intersect
(i : level)
(a : U i)
(b : a -> U i)
(c : forall (x : a) . b x -> U i)
(x : a) .
forall (y : b x) . c x y -> `unpackt a b c y
= fn y z . (y, (), z)
unpackt_elim : intersect
(i : level)
(a : U i)
(b : a -> U i)
(c : forall (x : a) . b x -> U i)
(d : (union (x : a) . b x) -> U i)
(u : union (x : a) . b x) .
`unpackt a b c u
-> (intersect (x : a) . forall (y : b x) . c x y -> d y)
-> d u
= fn w f . f (w #1) (w #2 #2)
Again, observe that the continuation in unpackt_elim (i.e., its
final argument) cannot refer to the union’s hidden witness (x).
The intro and elim forms reduce in the expected manner:
unpackt_elim (unpackt_intro y z) f --> f y z
To use an unpackt, it is generally just a matter of destructing it
and exploiting its equality. Suppose:
i : level
a : U i
b : a -> U i
c : forall (x : a) . b x -> U i
d : forall (x : a) . b x -> U i
u : union (x : a) . b x
H : unpackt (x , y) = u in c x y
Then destruct /H/ /x y Heq Hy/ >> reduce /Hy/ produces:
x (hidden) : a
y : b x
Heq : y = u : (union (x1 : a) . b x1)
Hy : c x y
Now (assuming u is always used in a manner consistent with the type
union (x : a) . b x) you can use subst /u/ to replace u with y
and proceed from there.
A similar set of definitions is available for iexists:
iunpack : intersect (i : level) (a : Kind i) (b : a -> U i) (c : U i) .
(iexists (x : a) . b x) -> (intersect (x : a) . b x -> c) -> c
= fn u f . f u
iunpack_dep : intersect (i : level) (a : Kind i) (b : a -> U i) .
forall (c : intersect (x : a) . b x -> U i) (u : iexists (x : a) . b x) .
(intersect (x : a) . forall (y : b x) . c y) -> c u
= fn c u f . f u
The syntactic sugar iunpack x = u in m is accepted for
`iunpack u (fn x . m).
iunpackt : forall (i : level) (a : Kind i) (b : a -> U i) .
(forall (x : a) . b x -> U i) -> (iexists (x : a) . b x) -> U i
= fn i a b c u .
iexists (x : a) . exists (y : b x) . y = u : (iexists (x1 : a) . b x1) & c x y
The syntactic sugar iunpackt (x , y) = u in b is accepted for
`iunpackt _ _ _ (fn x y . b) u.
iunpackt_intro : intersect
(i : level)
(a : Kind i)
(b : a -> U i)
(c : forall (x : a) . b x -> U i)
(x : a) .
forall (y : b x) . c x y -> `iunpackt i a b c y
= fn y z . (y, (), z)
iunpackt_elim : intersect
(i : level)
(a : Kind i)
(b : a -> U i)
(c : forall (x : a) . b x -> U i)
(d : (iexists (x : a) . b x) -> U i)
(u : iexists (x : a) . b x) .
`iunpackt i a b c u
-> (intersect (x : a) . forall (y : b x) . c x y -> d y)
-> d u
= fn w f . f (w #1) (w #2 #2)
iunpackt_elim (iunpackt_intro y z) f --> f y z