\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Extended pattern matching

Authors:

  Cristina Cornes and Hugo Herbelin

This section describes the full form of pattern matching in Rocq terms.

## Variants and extensions of `match`

### Multiple and nested pattern matching

The basic version of `match` allows pattern matching on simple patterns. As an extension, multiple nested patterns or disjunction of patterns are allowed, as in ML-like languages (cf. Multiple patterns and Nested patterns).

The extension is expanded during type inference into a sequence of match on simple patterns. Printing by default attempts to reconstruct the factorized syntax (see `Printing Matching`), but is often not successful and prints the expanded form.

### Pattern-matching on boolean values: the if expression

term_if`::=`if term as name? return term100? then term else term``

For inductive types with exactly two constructors and for pattern matching expressions that do not depend on the arguments of the constructors, it is possible to use a `if … then … else` notation. For instance, the definition

Definition not (b:bool) := match b with | true => false | false => true end.
  not is defined

can be alternatively written

Definition not (b:bool) := if b then false else true.
  not is defined

More generally, for an inductive type with constructors `ident1` and `ident2`, the following terms are equal:

`if term0 as name? return term? then term1 else term2`

`match term0 as name? return term? with | ident1 _* => term1 | ident2 _* => term2 end`

Example

Check (fun x (H:{x=0}+{x<>0}) => match H with | left _ => true | right _ => false end).
  fun (x : nat) (H : {x = 0} + {x <> 0}) => if H then true else false : forall x : nat, {x = 0} + {x <> 0} -> bool

Notice that the printing uses the `if` syntax because `sumbool` is declared as such (see Controlling pretty-printing of match expressions).

### Irrefutable patterns: the destructuring let variants

Pattern-matching where all cases are captured by a single pattern ("irrefutable pattern", typically for inductive types with a single constructor) can be alternatively written using `let … in …` constructions. There are two variants of them.

destructuring_let`::=`let ( name*, ) as name? return term100? := term in term`````|`let ' pattern in pattern? := term return term100? in term``

#### Let-tuple syntax

The expression `let ( identi*, ) := term0 in term1` performs case analysis on `term0` whose type must be an inductive type with exactly one constructor. The number of variables `identi` must correspond to the number of arguments of this constructor. Then, in `term1`, these variables are bound to the arguments of the constructor in `term0`. For instance, the definition

Definition fst (A B:Set) (H:A * B) := match H with | pair x y => x end.
  fst is defined

can be alternatively written

Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
  fst is defined

Notice that reduction is different from regular `let … in …` construction since it happens only if `term0` is in constructor form. Otherwise, the reduction is blocked.

The pretty-printing of a definition by matching on a irrefutable pattern can either be done using `match` or the `let` construction (see Section Controlling pretty-printing of match expressions).

If term inhabits an inductive type with one constructor `C`, we have an equivalence between

`let ( namei* ) as nameas? return termret? := term0 in term1`

and

`match term0 as nameas? return termret? with C namei* => term1 end`

(if the parameters of `C` are implicit arguments or `Asymmetric Patterns` is set).

In practice type inference may use slightly different heuristics for the different syntaxes.

#### Let-pattern syntax

Another destructuring let syntax is available by giving an arbitrary pattern (which must be irrefutable) instead of just a tuple for all the arguments. For example, the preceding example can be written:

Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
  fst is defined

This is useful to match deeper inside tuples and also to use notations for the pattern, as the syntax `let ’p := t in b` allows arbitrary patterns to do the deconstruction. For example:

Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := let '((a,b), (c, d)) := x in (a,b,c,d).
  deep_tuple is defined
Notation " x 'With' p " := (exist _ x p) (at level 20).
  Identifier 'With' now a keyword
Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := let 'x With p := t in x.
  proj1_sig' is defined

We can also match on multiple constructors:

Check fun A (x : A + A) => let '(inl y | inr y) := x in y.
  fun (A : Type) '(inl y | inr y) => y : forall A : Type, A + A -> A

When printing definitions which are written using this construct it takes precedence over let printing directives for the datatype under consideration (see Section Controlling pretty-printing of match expressions).

In general

`let ' pattern in patternin? := term0 return termret? in term1`

is desugared into

`match term0 as nameas? in patternin? return termret? with pattern => term1 end`

where if `pattern` is a name then it is used to provide `nameas`, otherwise the `as` annotation is left implicit.

Note

In the "let-tuple" syntax, `let (x, y) := ...` handles any inductive type with a unique constructor and 2 arguments.

In the "let-pattern" syntax, `let '(x, y) := ...` handles the inductive type whose constructor is produced by the `(_, _)` notation (by default `prod` whose constructor is `pair`).

### Controlling pretty-printing of match expressions

The following commands give some control over the pretty-printing of `match` expressions.

#### Printing nested patterns

Flag Printing Matching

  The Calculus of Inductive Constructions knows pattern matching only over simple patterns. It is however convenient to re-factorize nested pattern matching into a single pattern matching over a nested pattern.

  When this flag is on (default), Coq’s printer tries to do such limited re-factorization. Turning it off tells Rocq to print only simple pattern matching problems in the same way as the Rocq kernel handles them.

#### Factorization of clauses with same right-hand side

Flag Printing Factorizable Match Patterns

  When several patterns share the same right-hand side, it is additionally possible to share the clauses using disjunctive patterns. Assuming that the `Printing Matching` mode is on, this flag (on by default) tells Rocq's printer to try to do this kind of factorization.

#### Use of a default clause

Flag Printing Allow Match Default Clause

  When several patterns share the same right-hand side which do not depend on the arguments of the patterns, yet an extra factorization is possible: the disjunction of patterns can be replaced with a `_` default clause. Assuming that the printing matching mode and the factorization mode are on, this flag (on by default) tells Rocq's printer to use a default clause when relevant.

#### Printing of wildcard patterns

Flag Printing Wildcard

  Some variables in a pattern may not occur in the right-hand side of the pattern matching clause. When this flag is on (default), the variables having no occurrences in the right-hand side of the pattern matching clause are just printed using the wildcard symbol “_”.

#### Printing of the elimination predicate

Flag Printing Synth

  In most of the cases, the type of the result of a matched term is mechanically synthesizable. Especially, if the result type does not depend of the matched term. When this flag is on (default), the result type is not printed when Rocq knows that it can re- synthesize it.

#### Printing of hidden subterms

Flag Printing Match All Subterms

  In order to be able to cheaply reconstruct the types of the variables bound by `in` and `as`, `match` terms contain the polymorphic universe instance and the parameters of the inductive which is being matched. When this flag is on (it is off by default), this information is displayed as a volatile cast around the match discriminee.

  When the match relies on `Definitional UIP`, the indices are also subterms of the `match` term and are displayed when this flag is on. Otherwise they are not subterms and are displayed as holes (`_`) when this flag is on.

  Example

  Polymorphic Inductive eqT@{u} {A:Type@{u}} (a:A) : A -> Type@{u} := reflT : eqT a a.
    eqT is defined eqT_rect is defined eqT_ind is defined eqT_rec is defined eqT_sind is defined
  Set Definitional UIP.
  Inductive seq {A} (a:A) : A -> SProp := srefl : seq a a.
    seq is defined seq_rect is defined seq_ind is defined seq_rec is defined seq_sind is defined
  Print eqT_rect.
    eqT_rect@{u u0} = fun (A : Type) (a : A) (P : forall a0 : A, eqT a a0 -> Type) (reflT : P a (reflT a)) (a0 : A) (e : eqT a a0) => match e as e0 in eqT _ a1 return P a1 e0 with | Top.reflT _ => reflT end : forall (A : Type) (a : A) (P : forall a0 : A, eqT a a0 -> Type), P a (reflT a) -> forall (a0 : A) (e : eqT a a0), P a0 e Arguments eqT_rect A%_type_scope a P%_function_scope reflT a0 e
  Print seq_rect.
    seq_rect = fun (A : Type) (a : A) (P : forall a0 : A, seq a a0 -> Type) (srefl : P a (srefl a)) (a0 : A) (s : seq a a0) => match s as s0 in seq _ a1 return P a1 s0 with | Top.srefl _ => srefl end : forall (A : Type) (a : A) (P : forall a0 : A, seq a a0 -> Type), P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s Arguments seq_rect A%_type_scope a P%_function_scope srefl a0 s
  Set Printing Match All Subterms.
  Set Printing Universes.
  Print eqT_rect.
    eqT_rect@{u u0} = fun (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}) (reflT : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) => match e :> eqT@{u} a _ as e0 in eqT _ a1 return P a1 e0 with | Top.reflT _ => reflT end : forall (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}), P a (reflT@{u} a) -> forall (a0 : A) (e : eqT@{u} a a0), P a0 e (* u u0 |= *) Arguments eqT_rect A%_type_scope a P%_function_scope reflT a0 e
  Print seq_rect.
    seq_rect = fun (A : Type@{seq_rect.u1}) (a : A) (P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}) (srefl : P a (srefl a)) (a0 : A) (s : seq a a0) => match s :> seq a a0 as s0 in seq _ a1 return P a1 s0 with | Top.srefl _ => srefl end : forall (A : Type@{seq_rect.u1}) (a : A) (P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}), P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s Arguments seq_rect A%_type_scope a P%_function_scope srefl a0 s

#### Printing matching on irrefutable patterns

If an inductive type has just one constructor, pattern matching can be written using the let-tuple syntax.

Table Printing Let qualid

  This table specifies a set of qualids for which pattern matching is displayed using a let expression. Note that this only applies to pattern matching instances entered with `match`. It doesn't affect pattern matching explicitly entered with a destructuring `let`. Use the `Add` and `Remove` commands to update this set.

#### Printing matching on booleans

If an inductive type is isomorphic to the boolean type, pattern matching can be written using `if` … `then` … `else` …. This table controls which types are written this way:

Table Printing If qualid

  This table specifies a set of qualids for which pattern matching is displayed using `if` … `then` … `else` …. Use the `Add` and `Remove` commands to update this set.

This example emphasizes what the printing settings offer.

Example

Definition snd (A B:Set) (H:A * B) := match H with | pair x y => y end.
  snd is defined
Test Printing Let for prod.
  Cases on elements of prod are printed using a `let' form
Print snd.
  snd = fun (A B : Set) (H : A * B) => let (_, y) := H :> A * B in y : forall A B : Set, A * B -> B Arguments snd (A B)%_type_scope H
Remove Printing Let prod.
Unset Printing Synth.
Unset Printing Wildcard.
Print snd.
  snd = fun (A B : Set) (H : A * B) => match H :> A * B return B with | (x, y) => y end : forall A B : Set, A * B -> B Arguments snd (A B)%_type_scope H

### Conventions about unused pattern-matching variables

Pattern-matching variables that are not used on the right-hand side of `=>` are considered the sign of a potential error. For instance, it could result from an undetected misspelled constant constructor. By default, a warning is issued in such situations.

Warning Unused variable ident might be a misspelled constructor. Use _ or _ident to silence this warning.

  This indicates that an unused pattern variable `ident` occurs in a pattern-matching clause.

  The warning can be deactivated by using a variable name starting with `_` or by setting `Set Warnings "-unused-pattern-matching-variable"`.

  Here is an example where the warning is activated.

  Example

  Definition is_zero (o : option nat) := match o with | Some _ => true | x => false end.
    Toplevel input, characters 71-72: > Definition is_zero (o : option nat) := match o with | Some _ => true | x => false end. > ^ Warning: Unused variable x might be a misspelled constructor. Use _ or _x to silence this warning. [unused-pattern-matching-variable,default] is_zero is defined

## Patterns

The full syntax of `match` is presented in Definition by cases: match. 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. 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 `(pattern as ident)` are also accepted. This pattern matches the same values as `pattern` does and `ident` is bound to the matched value. A pattern of the form `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 patterns are allowed though.

Since extended `match` expressions are compiled into the primitive ones, the expressiveness of the theory remains the same. Once parsing has finished only simple patterns remain. The original nesting of the `match` expressions is recovered at printing time. An easy way to see the result of the expansion is to toggle off the nesting performed at printing (use here `Printing Matching`), then by printing the term with `Print` if the term is a constant, or using the command `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:

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.
  max is defined max is recursively defined (guarded on 2nd argument)

## Multiple patterns

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

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.
  max is defined max is recursively defined (guarded on 2nd argument)

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.

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

## Aliasing subpatterns

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

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.
  max is defined max is recursively defined (guarded on 1st argument)

## Nested patterns

Here is now an example of nested patterns:

Fixpoint even (n:nat) : bool := match n with | O => true | S O => false | S (S n') => even n' end.
  even is defined even is recursively defined (guarded on 1st argument)

This is compiled into:

Unset Printing Matching.
Print even.
  even = fix even (n : nat) : bool := match n with | 0 => true | S n0 => match n0 with | 0 => false | S n' => even n' end end : nat -> bool Arguments even n%_nat_scope

Set Printing Matching.

In the previous examples patterns do not conflict with, but sometimes it is comfortable to write patterns that admit a nontrivial 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:

Fixpoint lef (n m:nat) {struct m} : bool := match n, m with | O, _ => true | _, O => false | S n, S m => lef n m end.
  lef is defined lef is recursively defined (guarded on 2nd argument)

Note that the first and the second multiple pattern overlap 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 to be ordered from top to bottom. A value is matched by the pattern at the ith row if and only if it is not matched by some pattern from 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:

Fixpoint lef (n m:nat) {struct m} : bool := match n, m with | O, _ => true | S n, S m => lef n m | _, _ => false end.
  lef is defined lef is recursively defined (guarded on 2nd argument)

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:

Fail Check (fun x:nat => match x with | O => true | S _ => false | x => true end).
  The command has indeed failed with message: Pattern "x" is redundant in this clause.

## Disjunctive patterns

Multiple patterns that share the same right-hand-side can be factorized using the notation `pattern+,+|`. For instance, `max` can be rewritten as follows:

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.
  max is defined max is recursively defined (guarded on 2nd argument)

Similarly, factorization of (not necessarily multiple) patterns that share the same variables is possible by using the notation `pattern+|`. Here is an example:

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

Nested disjunctive patterns are allowed, inside parentheses, with the notation `(pattern+|)`, as 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.
  filter_some_square_corners is defined

## 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:

Inductive List (A:Set) : Set := | nil : List A | cons : A -> List A -> List A.
  List is defined List_rect is defined List_ind is defined List_rec is defined List_sind is defined

We can check the function tail:

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

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

Fail Check (fun l:List nat => match l with | nil A => nil nat | cons A _ l' => l' end).
  The command has indeed failed with message: The parameters do not bind in patterns; they must be replaced by '_'.

Flag Asymmetric Patterns

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

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

## Implicit arguments in patterns

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

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

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

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

## 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 types. Consider the type `listn` of lists of a certain length:

Inductive listn : nat -> Set := | niln : listn 0 | consn : forall n:nat, nat -> listn n -> listn (S n).
  listn is defined listn_rect is defined listn_ind is defined listn_rec is defined listn_sind is defined

## Understanding dependencies in patterns

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

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

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

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

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 right hand sides have the same type and Rocq succeeds to synthesize it. Unfortunately when dealing with dependent patterns it often happens that we need to write cases where the types of the right hand sides are different instances of the elimination predicate. The function `concat` for `listn` is an example where the branches have different types and we need to provide the elimination predicate:

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.
  concat is defined concat is recursively defined (guarded on 2nd argument)

Reset concat.

The elimination predicate is `fun (n:nat) (l:listn n) => listn (n+m)`. In general if `m` has type `(I q1 … qr t1 … ts)` where `q1, …, qr` are parameters, the elimination predicate should be of the form `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 `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 with an `as` clause and an `in` clause in order to introduce a dependent product.

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

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.
  concat is defined concat is recursively defined (guarded on 2nd argument)

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

Check (fun n (a b: listn n) => match a, b with | niln, b0 => tt | consn n' a y, bS => tt end).
  fun (n : nat) (a _ : listn n) => match a with | niln | _ => tt end : forall n : nat, listn n -> listn n -> unit

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

### 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 types 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:

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.
  tail is defined

and `tail n v` will be subterm of `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 a dependent type. An example of a proof written using `match` is given in the description of the tactic `refine`.

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

Fixpoint buildlist (n:nat) : listn n := match n return listn n with | O => niln | S n => consn n 0 (buildlist n) end.
  buildlist is defined buildlist is recursively defined (guarded on 1st argument)

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

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).
  LE is defined LE_ind is defined LE_sind is defined

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

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.
  dec is defined dec is recursively defined (guarded on 1st argument)

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

The user can also use match in combination with the tactic `refine` to build incomplete proofs beginning with a `match` construction.

## Pattern-matching on inductive objects involving local definitions

If local definitions (`let :=`) 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

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

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

Fixpoint length n (l:list n) {struct l} : nat := match l with | nil => 0 | cons n l0 => S (length (2 * n) l0) end.
  length is defined length is recursively defined (guarded on 2nd argument)

But in this example, it is.

Fixpoint length' n (l:list n) {struct l} : nat := match l with | nil => 0 | @cons _ m l0 => S (length' m l0) end.
  length' is defined length' is recursively defined (guarded on 2nd argument)

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

Inductive I : Set := | C1 : nat -> I | C2 : I -> I.
  I is defined I_rect is defined I_ind is defined I_rec is defined I_sind is defined
Coercion C1 : nat >-> I.
  C1 is now a coercion

Check (fun x => match x with | C2 O => 0 | _ => 0 end).
  fun x : I => match x with | C1 _ | _ => 0 end : I -> nat

## When does the expansion strategy fail?

The strategy works very like in ML languages when treating patterns of non-dependent types. 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:

Error The constructor ident expects natural arguments.
Error The variable ident is bound several times in pattern term
Error Found a constructor of inductive type term while a constructor of term is expected

  Patterns are incorrect (because constructors are not applied to the correct number of arguments, because they are not linear or they are wrongly typed).

Error Non exhaustive pattern matching.

  The pattern matching is not exhaustive.

Error The elimination predicate term should be of arity natural (for non dependent case) or natural (for dependent case).

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

Error Unable to infer a match predicate
Error 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.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF