13.1 Patterns

The full syntax of Cases is presented in figure 13.1. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or coinductive type is considered to be a variable. A variable name cannot occur more than once in a given pattern.

If a pattern has the form (c vec(x)) where c is a constructor symbol and vec(x) is a linear vector of variables, it is called simple: it is the kind of pattern recognized by the basic version of Cases. If a pattern is not simple we call it nested.

A variable pattern matches any value, and the identifier is bound to that value. The pattern ``_'' (called ``don't care'' or ``wildcard'' symbol) also matches any value, but does not binds anything. It may occur an arbitrary number of times in a pattern. Alias patterns written (pattern as identifier) are also accepted. This pattern matches the same values as pattern does and identifier is bound to the matched value. A list of patterns is also considered as a pattern and is called multiple pattern.

Note also the annotation is mandatory when the sequence of equation is empty.

nested_pattern := ident

| _

| ( ident nested_pattern ... nested_pattern )

| ( nested_pattern as ident )

| ( nested_pattern , nested_pattern )

| ( nested_pattern )

mult_pattern := nested_pattern ... nested_pattern

ext_eqn := mult_pattern => term

term := [annotation] Cases term ... term of [ext_eqn | ... | ext_eqn] end

Figure 13.1:Extended Cases syntax

Since extended Cases expressions are compiled into the primitive ones, the expressiveness of the theory remains the same. Once the stage of parsing has finished only simple patterns remain. An easy way to see the result of the expansion is by printing the term with Print if the term is a constant, or using the command Check.

The extended Cases still accepts an optional elimination predicate enclosed between brackets <>. Given a pattern matching expression, if all the right hand sides of => (rhs in short) have the same type, then this term can be sometimes synthesized, and so we can omit the <>. Otherwise we have toprovide the predicate between <> as for the basic Cases.

Let us illustrate through examples the different aspects of extended pattern matching. Consider for example the function that computes the maximum of two natural numbers. We can write it in primitive syntax by:

Coq < Fixpoint max [n,m:nat] : nat :=
Coq < Cases n of
Coq < O => m
Coq < | (S n') => Cases m of
Coq < O => (S n')
Coq < | (S m') => (S (max n' m'))
Coq < end
Coq < end.
max is recursively defined

Using multiple patterns in the definition allows to write:

Coq < Reset max.

Coq < Fixpoint max [n,m:nat] : nat :=
Coq < Cases n m of
Coq < O _ => m
Coq < | (S n') O => (S n')
Coq < | (S n') (S m') => (S (max n' m'))
Coq < end.
max is recursively defined

which will be compiled into the previous form.

The strategy examines patterns from left to right. A Cases expression is generated only when there is at least one constructor in the column of patterns. For example:

Coq < Check [x:nat]<nat>Cases x of y => y end.
[x:nat]x
: nat->nat

We can also use ``as patterns'' to associate a name to a sub-pattern:

Coq < Reset max.

Coq < Fixpoint max [n:nat] : nat -> nat :=
Coq < [m:nat] Cases n m of
Coq < O _ => m
Coq < | ((S n') as N) O => N
Coq < | (S n') (S m') => (S (max n' m'))
Coq < end.
Warning: the variable N starts with upper case in a pattern
max is recursively defined

Here is now an example of nested patterns:

Coq < Fixpoint even [n:nat] : bool :=
Coq < Cases n of
Coq < O => true
Coq < | (S O) => false
Coq < | (S (S n')) => (even n')
Coq < end.
even is recursively defined

This is compiled into:

Coq < Print even.
even =
Fix even{even [n:nat] : bool :=
           Cases n of
             O => true
           | (S a) => Cases a of
                        O => false
                      | (S n') => (even n')
                      end
           end}
     : nat->bool

In the previous examples patterns do not conflict with, but sometimes it is comfortable to write patterns that admits a non trivial superposition. Consider the boolean function lef that given two natural numbers yields true if the first one is less or equal than the second one and false otherwise. We can write it as follows:

Coq < Fixpoint lef [n,m:nat] : bool :=
Coq < Cases n m of
Coq < O x => true
Coq < | x O => false
Coq < | (S n) (S m) => (lef n m)
Coq < end.
lef is recursively defined

Note that the first and the second multiple pattern superpose because the couple of values O O matches both. Thus, what is the result of the function on those values? To eliminate ambiguity we use the textual priority rule: we consider patterns ordered from top to bottom, then a value is matched by the pattern at the ith row if and only if is not matched by some pattern of a previous row. Thus in the example, O O is matched by the first pattern, and so (lef O O) yields true.

Another way to write this function is:

Coq < Reset lef.

Coq < Fixpoint lef [n,m:nat] : bool :=
Coq < Cases n m of
Coq < O x => true
Coq < | (S n) (S m) => (lef n m)
Coq < | _ _ => false
Coq < end.
lef is recursively defined

Here the last pattern superposes with the first two. Because of the priority rule, the last pattern will be used only for values that do not match neither the first nor the second one.

Terms with useless patterns are accepted by the system. For example,

Coq < Check [x:nat]Cases x of O => true | (S _) => false | x => true end.
[x:nat]Cases x of
         O => true
       | (S _) => false
       end
     : nat->bool

is accepted even though the last pattern is never used. Beware, the current implementation rises no warning message when there are unused patterns in a term.

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