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 is defined
listn_rect is defined
listn_ind is defined
listn_rec 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.

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 the matching on the second term is trivial) would have been:

Coq < Reset concat.

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.
concat is recursively defined

Notice 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 raises 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.
Toplevel input, characters 119-120
>    <[n:nat](listn (plus n m))>Cases l l' of 
>      ^
Error: The elimination predicate 
[n:nat](listn (plus n m))
should be of arity nat->nat->Type (for non dependent case) or
(n:nat)(listn n)->(n0:nat)(listn n0)->Type (for dependent case).