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 e₁... e_n the predicate will be of arity m where m is the sum of the number of dependencies of the type of e₁, e₂,... e_n (the l-abstractions should correspond from left to right to each dependent argument of the type of e₁... e_n). 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 term
  [n:nat]
   [l:(listn n)]
    [m:nat]
     [l':(listn m)]
      <[n0:nat](listn (plus n0 m))>
        Cases l l' of
          niln dum_x => dum_x
        | (consn dum_n' dum_a dum_y) dum_x =>
              (consn (plus dum_n' m) dum_a
                (concat dum_n' dum_y m dum_x))
        end failed to typecheck:
The elimination predicate [n0:nat](listn (plus n0 m))
should be of arity 2 (for non dependent case)  or 4 (for dependent case).

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.2.2.html at 8/10/98