13.3 Matching objects of dependent types
The previous examples illustrate pattern matching on objects of
non-dependent types, but we can also
use the expansion strategy to destructure objects of dependent type.
Consider the type listn of lists of a certain length:
Coq < Inductive listn : nat-> Set :=
Coq < niln : (listn O)
Coq < | consn : (n:nat)nat->(listn n) -> (listn (S n)).
listn_ind is defined
listn_rec is defined
listn_rect is defined
listn is defined
13.3.1 Understanding dependencies in patterns
We can define the function length over listn by:
Coq < Definition length := [n:nat][l:(listn n)] n.
length is defined
Just for illustrating pattern matching,
we can define it by case analysis:
Coq < Reset length.
Coq < Definition length := [n:nat][l:(listn n)]
Coq < Cases l of
Coq < niln => O
Coq < | (consn n _ _) => (S n)
Coq < end.
length is defined
We can understand the meaning of this definition using the
same notions of usual pattern matching.
Now suppose we split the second pattern of length into two
cases so to give an
alternative definition using nested patterns:
Coq < Definition length1:= [n:nat] [l:(listn n)]
Coq < Cases l of
Coq < niln => O
Coq < | (consn n _ niln) => (S n)
Coq < | (consn n _ (consn _ _ _)) => (S n)
Coq < end.
length1 is defined
It is obvious that length1 is another version of
length. We can also give the following definition:
Coq < Definition length2:= [n:nat] [l:(listn n)]
Coq < Cases l of
Coq < niln => O
Coq < | (consn n _ niln) => (S O)
Coq < | (consn n _ (consn m _ _)) => (S (S m))
Coq < end.
length2 is defined
If we forget that listn is a dependent type and we read these
definitions using the usual semantics of pattern matching, we can conclude
that length1
and length2 are different functions.
In fact, they are equivalent
because the pattern niln implies that n can only match
the value 0 and analogously the pattern consn determines that n can
only match values of the form (S v) where v is the value matched by
m.
The converse is also true. If
we destructure the length value with the pattern O then the list
value should be niln.
Thus, the following term length3 corresponds to the function
length but this time defined by case analysis on the dependencies instead of on the list:
Coq < Definition length3 := [n:nat] [l: (listn n)]
Coq < Cases l of
Coq < niln => O
Coq < | (consn O _ _) => (S O)
Coq < | (consn (S n) _ _) => (S (S n))
Coq < end.
Warning: This pattern matching may need dependent elimination to be compiled.
I will try, but if fails try again giving dependent elimination predicate.
length3 is defined
When we have nested patterns of dependent types, the semantics of
pattern matching becomes a little more difficult because
the set of values that are matched by a sub-pattern may be conditioned by the
values matched by another sub-pattern. Dependent nested patterns are
somehow constrained patterns.
In the examples, the expansion of
length1 and length2 yields exactly the same term
but the
expansion of length3 is completely different. length1 and
length2 are expanded into two nested case analysis on
listn while length3 is expanded into a case analysis on
listn containing a case analysis on natural numbers inside.
In practice the user can think about the patterns as independent and
it is the expansion algorithm that cares to relate them.
13.3.2 When the elimination predicate must be provided
The examples given so far do not need an explicit elimination predicate
between <> because all the rhs have the same type and the
strategy succeeds to synthesize it.
Unfortunately when dealing with dependent patterns it often happens
that we need to write cases where the type of the rhs are
different instances of the elimination predicate.
The function concat for listn
is an example where the branches have different type
and we need to provide the elimination predicate:
Coq < Fixpoint concat [n:nat; l:(listn n)]
Coq < : (m:nat) (listn m) -> (listn (plus n m))
Coq < := [m:nat][l':(listn m)]
Coq < <[n:nat](listn (plus n m))>Cases l of
Coq < niln => l'
Coq < | (consn n' a y) => (consn (plus n' m) a (concat n' y m l'))
Coq < end.
concat is recursively defined
Recall that a list of patterns is also a pattern. So, when
we destructure several terms at the same time and the branches have
different type we need to provide
the elimination predicate for this multiple pattern.
For example, an equivalent definition for concat (even though with a useless extra pattern) would have
been:
Coq < Reset concat.
Coq < Fixpoint concat [n:nat; l:(listn n)] : (m:nat) (listn m) -> (listn (plus n m))
Coq < := [m:nat][l':(listn m)]
Coq < <[n,_:nat](listn (plus n m))>Cases l l' of
Coq < niln x => x
Coq < | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
Coq < end.
concat is recursively defined
Note that this time, the predicate [n,_:nat](listn (plus n
m)) is binary because we
destructure both l and l' whose types have arity one.
In general, if we destructure the terms e1... en
the predicate will be of arity m where m is the sum of the
number of dependencies of the type of e1, e2,... en
(the l-abstractions
should correspond from left to right to each dependent argument of the
type of e1... en).
When the arity of the predicate (i.e. number of abstractions) is not
correct Coq rises an error message. For example:
Coq < Fixpoint concat [n:nat; l:(listn n)]
Coq < : (m:nat) (listn m) -> (listn (plus n m)) :=
Coq < [m:nat][l':(listn m)]
Coq < <[n:nat](listn (plus n m))>Cases l l' of
Coq < | niln x => x
Coq < | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
Coq < end.
Error during interpretation of command:
Fixpoint concat [n:nat; l:(listn n)]
: (m:nat) (listn m) -> (listn (plus n m)) :=
[m:nat][l':(listn m)]
<[n:nat](listn (plus n m))>Cases l l' of
| niln x => x
| (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
end.
Error: The elimination predicate [n:nat](listn (plus n m))
should be of arity 2 (for non dependent case) or 4 (for dependent case).