aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/addendum/extended-pattern-matching.rst
blob: c4f014772838e0867d9042b3e5c43f50b638f4bf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
.. include:: ../replaces.rst

.. _extendedpatternmatching:

Extended pattern-matching
=========================

:Authors: Cristina Cornes and Hugo Herbelin

.. TODO links to figures

This section describes the full form of pattern-matching in |Coq| terms.

.. |rhs| replace:: right hand side

Patterns
--------

The full syntax of match is presented in Figures 1.1 and 1.2.
Identifiers in patterns are either constructor names or variables. Any
identifier that is not the constructor of an inductive or co-inductive
type is considered to be a variable. A variable name cannot occur more
than once in a given pattern. It is recommended to start variable
names by a lowercase letter.

If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x
is a linear vector of (distinct) variables, it is called *simple*: it
is the kind of pattern recognized by the basic version of match. On
the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not
only made of variables, the pattern is called *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 bind anything. It may occur an
arbitrary number of times in a pattern. Alias patterns written
:n:`(@pattern as @identifier)` are also accepted. This pattern matches the
same values as ``pattern`` does and ``identifier`` is bound to the matched
value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
list of patterns separated with commas is also considered as a pattern
and is called *multiple pattern*. However multiple patterns can only
occur at the root of pattern-matching equations. Disjunctions of
*multiple pattern* are allowed though.

Since extended ``match`` 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. Re-nesting of
pattern is performed at printing time. An easy way to see the result
of the expansion is to toggle off the nesting performed at printing
(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print`
if the term is a constant, or using the command :cmd:`Check`.

The extended ``match`` still accepts an optional *elimination predicate*
given after the keyword ``return``. Given a pattern matching expression,
if all the right-hand-sides of ``=>`` have the same
type, then this type can be sometimes synthesized, and so we can omit
the return part. Otherwise the predicate after return has to be
provided, like for the basicmatch.

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:

.. coqtop:: in undo

   Fixpoint max (n m:nat) {struct m} : nat :=
     match n with
     | O => m
     | S n' => match m with
               | O => S n'
               | S m' => S (max n' m')
               end
     end.

Multiple patterns
-----------------

Using multiple patterns in the definition of ``max`` lets us write:

.. coqtop:: in undo

   Fixpoint max (n m:nat) {struct m} : nat :=
       match n, m with
       | O, _ => m
       | S n', O => S n'
       | S n', S m' => S (max n' m')
       end.

which will be compiled into the previous form.

The pattern-matching compilation strategy examines patterns from left
to right. A match expression is generated **only** when there is at least
one constructor in the column of patterns. E.g. the following example
does not build a match expression.

.. coqtop:: all

   Check (fun x:nat => match x return nat with
                       | y => y
                       end).


Aliasing subpatterns
--------------------

We can also use :n:`as @ident` to associate a name to a sub-pattern:

.. coqtop:: in undo

   Fixpoint max (n m:nat) {struct n} : nat :=
     match n, m with
     | O, _ => m
     | S n' as p, O => p
     | S n', S m' => S (max n' m')
     end.

Nested patterns
---------------

Here is now an example of nested patterns:

.. coqtop:: in

   Fixpoint even (n:nat) : bool :=
     match n with
     | O => true
     | S O => false
     | S (S n') => even n'
     end.

This is compiled into:

.. coqtop:: all undo

   Unset Printing Matching.
   Print even.

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

.. coqtop:: in undo

   Fixpoint lef (n m:nat) {struct m} : bool :=
     match n, m with
     | O, x => true
     | x, O => false
     | S n, S m => lef n m
     end.

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 it is
not matched by some pattern of a previous row. Thus in the example,O O
is matched by the first pattern, and so :g:`(lef O O)` yields true.

Another way to write this function is:

.. coqtop:: in

   Fixpoint lef (n m:nat) {struct m} : bool :=
     match n, m with
     | O, x => true
     | S n, S m => lef n m
     | _, _ => false
     end.

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 not accepted by the system. Here is an
example:

.. coqtop:: all

   Fail Check (fun x:nat =>
                 match x with
                 | O => true
                 | S _ => false
                 | x => true
                 end).


Disjunctive patterns
--------------------

Multiple patterns that share the same right-hand-side can be
factorized using the notation :n:`{+| @mult_pattern}`. For
instance, :g:`max` can be rewritten as follows:

.. coqtop:: in undo

   Fixpoint max (n m:nat) {struct m} : nat :=
     match n, m with
     | S n', S m' => S (max n' m')
     | 0, p | p, 0 => p
     end.

Similarly, factorization of (non necessary multiple) patterns that
share the same variables is possible by using the notation :n:`{+| @pattern}`.
Here is an example:

.. coqtop:: in

   Definition filter_2_4 (n:nat) : nat :=
     match n with
     | 2 as m | 4 as m => m
     | _ => 0
     end.


Here is another example using disjunctive subpatterns.

.. coqtop:: in

   Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
     match p with
     | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
     | _ => (0,0)
     end.

About patterns of parametric types
----------------------------------

Parameters in patterns
~~~~~~~~~~~~~~~~~~~~~~

When matching objects of a parametric type, parameters do not bind in
patterns. They must be substituted by “``_``”. Consider for example the
type of polymorphic lists:

.. coqtop:: in

   Inductive List (A:Set) : Set :=
   | nil : List A
   | cons : A -> List A -> List A.

We can check the function *tail*:

.. coqtop:: all

   Check
     (fun l:List nat =>
        match l with
        | nil _ => nil nat
        | cons _ _ l' => l'
        end).

When we use parameters in patterns there is an error message:

.. coqtop:: all

   Fail Check
     (fun l:List nat =>
        match l with
        | nil A => nil nat
        | cons A _ l' => l'
        end).

.. opt:: Asymmetric Patterns

This option (off by default) removes parameters from constructors in patterns:

.. coqtop:: all

   Set Asymmetric Patterns.
   Check (fun l:List nat =>
     match l with
     | nil => nil
     | cons _ l' => l'
     end).
   Unset Asymmetric Patterns.

Implicit arguments in patterns
------------------------------

By default, implicit arguments are omitted in patterns. So we write:

.. coqtop:: all

   Arguments nil [A].
   Arguments cons [A] _ _.
   Check
     (fun l:List nat =>
        match l with
        | nil => nil
        | cons _ l' => l'
        end).

But the possibility to use all the arguments is given by “``@``” implicit
explicitations (as for terms 2.7.11).

.. coqtop:: all

   Check
     (fun l:List nat =>
        match l with
        | @nil _ => @nil nat
        | @cons _ _ l' => l'
        end).


.. _matching-dependent:

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 :g:`listn` of
lists of a certain length:

.. coqtop:: in reset

   Inductive listn : nat -> Set :=
   | niln : listn 0
   | consn : forall n:nat, nat -> listn n -> listn (S n).


Understanding dependencies in patterns
--------------------------------------

We can define the function length over :g:`listn` by:

.. coqtop:: in

   Definition length (n:nat) (l:listn n) := n.

Just for illustrating pattern matching, we can define it by case
analysis:

.. coqtop:: in

   Definition length (n:nat) (l:listn n) :=
     match l with
     | niln => 0
     | consn n _ _ => S n
     end.

We can understand the meaning of this definition using the same
notions of usual pattern matching.


When the elimination predicate must be provided
-----------------------------------------------

Dependent pattern matching
~~~~~~~~~~~~~~~~~~~~~~~~~~

The examples given so far do not need an explicit elimination
predicate 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:

.. coqtop:: in

   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
    listn (n + m) :=
     match l in listn n return listn (n + m) with
     | niln => l'
     | consn n' a y => consn (n' + m) a (concat n' y m l')
     end.

The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`.
In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr`
are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`.

In the concrete syntax, it should be written :
``match m as x in (I _ … _ y1 … ys) return Q with … end``
The variables which appear in the ``in`` and ``as`` clause are new and bounded
in the property :g:`Q` in the return clause. The parameters of the
inductive definitions should not be mentioned and are replaced by ``_``.

Multiple dependent pattern matching
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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 types we need to provide the elimination predicate for this
multiple pattern. It is done using the same scheme, each term may be
associated to an as and in clause in order to introduce a dependent
product.

For example, an equivalent definition for :g:`concat` (even though the
matching on the second term is trivial) would have been:

.. coqtop:: in

   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
    listn (n + m) :=
     match l in listn n, l' return listn (n + m) with
     | niln, x => x
     | consn n' a y, x => consn (n' + m) a (concat n' y m x)
     end.

Even without real matching over the second term, this construction can
be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same
length, by writing

.. coqtop:: in

   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
    listn (n + m) :=
     match l in listn n, l' return listn (n + m) with
     | niln, x => x
     | consn n' a y, x => consn (n' + m) a (concat n' y m x)
     end.

I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`.

.. _match-in-patterns:

Patterns in ``in``
~~~~~~~~~~~~~~~~~~

If the type of the matched term is more precise than an inductive
applied to variables, arguments of the inductive in the ``in`` branch can
be more complicated patterns than a variable.

Moreover, constructors whose type do not follow the same pattern will
become impossible branches. In an impossible branch, you can answer
anything but False_rect unit has the advantage to be subterm of
anything.

To be concrete: the ``tail`` function can be written:

.. coqtop:: in

   Definition tail n (v: listn (S n)) :=
     match v in listn (S m) return listn m with
     | niln => False_rect unit
     | consn n' a y => y
     end.

and :g:`tail n v` will be subterm of :g:`v`.

Using pattern matching to write proofs
--------------------------------------

In all the previous examples the elimination predicate does not depend
on the object(s) matched. But it may depend and the typical case is
when we write a proof by induction or a function that yields an object
of dependent type. An example of proof using match in given in Section
8.2.3.

For example, we can write the function :g:`buildlist` that given a natural
number :g:`n` builds a list of length :g:`n` containing zeros as follows:

.. coqtop:: in

   Fixpoint buildlist (n:nat) : listn n :=
     match n return listn n with
     | O => niln
     | S n => consn n 0 (buildlist n)
     end.

We can also use multiple patterns. Consider the following definition
of the predicate less-equal :g:`Le`:

.. coqtop:: in

   Inductive LE : nat -> nat -> Prop :=
     | LEO : forall n:nat, LE 0 n
     | LES : forall n m:nat, LE n m -> LE (S n) (S m).

We can use multiple patterns to write the proof of the lemma
:g:`forall (n m:nat), (LE n m) \/ (LE m n)`:

.. coqtop:: in

   Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
     match n, m return LE n m \/ LE m n with
     | O, x => or_introl (LE x 0) (LEO x)
     | x, O => or_intror (LE x 0) (LEO x)
     | S n as n', S m as m' =>
         match dec n m with
         | or_introl h => or_introl (LE m' n') (LES n m h)
         | or_intror h => or_intror (LE n' m') (LES m n h)
         end
     end.

In the example of :g:`dec`, the first match is dependent while the second
is not.

The user can also use match in combination with the tactic :tacn:`refine` (see
Section 8.2.3) to build incomplete proofs beginning with a match
construction.


Pattern-matching on inductive objects involving local definitions
-----------------------------------------------------------------

If local definitions occur in the type of a constructor, then there
are two ways to match on this constructor. Either the local
definitions are skipped and matching is done only on the true
arguments of the constructors, or the bindings for local definitions
can also be caught in the matching.

.. example::

   .. coqtop:: in

      Inductive list : nat -> Set :=
      | nil : list 0
      | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)).

   In the next example, the local definition is not caught.

   .. coqtop:: in

      Fixpoint length n (l:list n) {struct l} : nat :=
        match l with
        | nil => 0
        | cons n l0 => S (length (2 * n) l0)
        end.

   But in this example, it is.

   .. coqtop:: in

      Fixpoint length' n (l:list n) {struct l} : nat :=
        match l with
        | nil => 0
        | @cons _ m l0 => S (length' m l0)
        end.

.. note:: For a given matching clause, either none of the local
          definitions or all of them can be caught.

.. note:: You can only catch let bindings in mode where you bind all
          variables and so you have to use ``@`` syntax.

.. note:: this feature is incoherent with the fact that parameters
          cannot be caught and consequently is somehow hidden. For example,
          there is no mention of it in error messages.

Pattern-matching and coercions
------------------------------

If a mismatch occurs between the expected type of a pattern and its
actual type, a coercion made from constructors is sought. If such a
coercion can be found, it is automatically inserted around the
pattern.

.. example::

   .. coqtop:: in

      Inductive I : Set :=
        | C1 : nat -> I
        | C2 : I -> I.

      Coercion C1 : nat >-> I.

   .. coqtop:: all

      Check (fun x => match x with
                      | C2 O => 0
                      | _ => 0
                      end).


When does the expansion strategy fail?
--------------------------------------

The strategy works very like in ML languages when treating patterns of
non-dependent type. But there are new cases of failure that are due to
the presence of dependencies.

The error messages of the current implementation may be sometimes
confusing. When the tactic fails because patterns are somehow
incorrect then error messages refer to the initial expression. But the
strategy may succeed to build an expression whose sub-expressions are
well typed when the whole expression is not. In this situation the
message makes reference to the expanded expression. We encourage
users, when they have patterns with the same outer constructor in
different equations, to name the variable patterns in the same
positions with the same name. E.g. to write ``(cons n O x) => e1`` and
``(cons n _ x) => e2`` instead of ``(cons n O x) => e1`` and
``(cons n' _ x') => e2``. This helps to maintain certain name correspondence between the
generated expression and the original.

Here is a summary of the error messages corresponding to each
situation:

.. exn:: The constructor @ident expects @num arguments.

   The variable ident is bound several times in pattern termFound a constructor
   of inductive type term while a constructor of term is expectedPatterns are
   incorrect (because constructors are not applied to the correct number of the
   arguments, because they are not linear or they are wrongly typed).

.. exn:: Non exhaustive pattern-matching.

   The pattern matching is not exhaustive.

.. exn:: The elimination predicate term should be of arity @num (for non \
         dependent case) or @num (for dependent case).

   The elimination predicate provided to match has not the expected arity.

.. exn:: Unable to infer a match predicate
         Either there is a type incompatibility or the problem involves dependencies.

   There is a type mismatch between the different branches. The user should
   provide an elimination predicate.