5.8. Pattern Matching🔗

Pattern matching is a way to recognize and destructure values using a syntax of patterns that are a subset of the terms. A pattern that recognizes and destructures a value is similar to the syntax that would be used to construct the value. One or more match discriminants are simultaneously compared to a series of match alternatives. Discriminants may be named. Each alternative contains one or more comma-separated sequences of patterns; all pattern sequences must contain the same number of patterns as there are discriminants. When a pattern sequence matches all of the discriminants, the term following the corresponding Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.=> is evaluated in an environment extended with values for each pattern variable as well as an equality hypothesis for each named discriminant. This term is called the right-hand side of the match alternative.

syntaxPattern Matching

term ::= ...
    | Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.

When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.

Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.

Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.

`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match
          ((generalizing := (trueVal | falseVal)))?
          ((motive := term))?
          `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. matchDiscr,*
        with
      (| (term,*)|* => term)*

syntaxMatch Discriminants

matchDiscr ::=
    `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. term

matchDiscr ::= ...
    | `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. ident : term

Pattern matching expressions may alternatively use quasiquotations as patterns, matching the corresponding Lean.Syntax values and treating the contents of antiquotations as ordinary patterns. Quotation patterns are compiled differently than other patterns, so if one pattern in a Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match is syntax, then all of them must be. Quotation patterns are described in the section on quotations.

Patterns are a subset of the terms. They consist of the following:

Catch-All Patterns: The hole syntax _ is a pattern that matches any value and binds no pattern variables. Catch-all patterns are not entirely equivalent to unused pattern variables. They can be used in positions where the pattern's typing would otherwise require a more specific inaccessible pattern, while variables cannot be used in these positions.
Identifiers: If an identifier is not bound in the current scope and is not applied to arguments, then it represents a pattern variable. Pattern variables match any value, and the values thus matched are bound to the pattern variable in the local environment in which the right-hand side is evaluated. If the identifier is bound, it is a pattern if it is bound to the constructor of an inductive type or if its definition has the match_pattern attribute.
Applications: Function applications are patterns if the function being applied is an identifier that is bound to a constructor or that has the match_pattern attribute and if all arguments are also patterns. If the identifier is a constructor, the pattern matches values built with that constructor if the argument patterns match the constructor's arguments. If it is a function with the match_pattern attribute, then the function application is unfolded and the resulting term's normal form is used as the pattern. Default arguments are inserted as usual, and their normal forms are used as patterns. Ellipses, however, result in all further arguments being treated as universal patterns, even those with associated default values or tactics.
Literals: Character literals and string literals are patterns that match the corresponding character or string. Raw string literals are allowed as patterns, but interpolated strings are not. Natural number literals in patterns are interpreted by synthesizing the corresponding OfNat instance and reducing the resulting term to normal form, which must be a pattern. Similarly, scientific literals are interpreted via the corresponding OfScientific instance. While Float has such an instance, Floats cannot be used as patterns because the instance relies on an opaque function that can't be reduced to a valid pattern.
Structure Instances: Structure instances may be used as patterns. They are interpreted as the corresponding structure constructor.
Quoted names: Quoted names, such as `x and ``plus, match the corresponding Lean.Name value.
Macros: Macros in patterns are expanded. They are patterns if the resulting expansions are patterns.
Inaccessible patterns: Inaccessible patterns are patterns that are forced to have a particular value by later typing constraints. Any term may be used as an inaccessible term. Inaccessible terms are parenthesized, with a preceding period (.).

syntaxInaccessible Patterns

term ::= ...
    | `.(e)` marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking.
In contrast to regular patterns, `e` may be an arbitrary term of the appropriate type.
.(term)

Inaccessible Patterns

A number's parity is whether it's even or odd:

inductive Parity : Nat → Type where
  | even (h : Nat) : Parity (h + h)
  | odd (h : Nat) : Parity ((h + h) + 1)

def Nat.parity (n : Nat) : Parity n :=
  match n with
  | 0 => .even 0
  | n' + 1 =>
    match n'.parity with
    | .even h => .odd h
    | .odd h =>
      have eq : (h + 1) + (h + 1) = (h + h + 1 + 1) :=
        byn:Nath:Nat⊢ h + 1 + (h + 1) = h + h + 1 + 1 omegaAll goals completed! 🐙
      eq ▸ .even (h + 1)

Because a value of type Parity contains half of a number (rounded down) as part of its representation of evenness or oddness, division by two can be implemented (in an unconventional manner) by finding a parity and then extracting the number.

def half (n : Nat) : Nat :=
  match n, n.parity with
  | .(h + h),     .even h => h
  | .(h + h + 1), .odd h  => h

Because the index structure of Parity.even and Parity.odd force the number to have a certain form that is not otherwise a valid pattern, patterns that match on it must use inaccessible patterns for the number being divided.

Patterns may additionally be named. Named patterns associate a name with a pattern; in subsequent patterns and on the right-hand side of the match alternative, the name refers to the part of the value that was matched by the given pattern. Named patterns are written with an @ between the name and the pattern. Just like discriminants, named patterns may also be provided with names for equality assumptions.

syntaxNamed Patterns

term ::= ...
    | `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
If present, the identifier `h` is bound to a proof of `x = e`. ident@term

term ::= ...
    | `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
If present, the identifier `h` is bound to a proof of `x = e`. ident@ident:term

5.8.1. Types

Each discriminant must be well typed. Because patterns are a subset of terms, their types can also be checked. Each pattern that matches a given discriminant must have the same type as the corresponding discriminant.

The right-hand side of each match alternative should have the same type as the overall Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match term. To support dependent types, matching a discriminant against a pattern refines the types that are expected within the scope of the pattern. In both subsequent patterns in the same match alternative and the right-hand side's type, occurrences of the discriminant are replaced by the pattern that it was matched against.

Type Refinement

This indexed family describes mostly-balanced trees, with the depth encoded in the type.

inductive BalancedTree (α : Type u) : Nat → Type u where
  | empty : BalancedTree α 0
  | branch (left : BalancedTree α n) (val : α) (right : BalancedTree α n) : BalancedTree α (n + 1)
  | lbranch (left : BalancedTree α (n + 1)) (val : α) (right : BalancedTree α n) : BalancedTree α (n + 2)
  | rbranch (left : BalancedTree α n) (val : α) (right : BalancedTree α (n + 1)) : BalancedTree α (n + 2)

To begin the implementation of a function to construct a perfectly balanced tree with some initial element and a given depth, a hole can be used for the definition.

def BalancedTree.filledWith (x : α) (depth : Nat) : BalancedTree α depth := don't know how to synthesize placeholder
context:
α : Type u
x : α
depth : Nat
⊢ BalancedTree α depth_

The error message demonstrates that the tree should have the indicated depth.

don't know how to synthesize placeholder
context:
α : Type u
x : α
depth : Nat
⊢ BalancedTree α depth

Matching on the expected depth and inserting holes results in an error message for each hole. These messages demonstrate that the expected type has been refined, with depth replaced by the matched values.

def BalancedTree.filledWith (x : α) (depth : Nat) : BalancedTree α depth :=
  match depth with
  | 0 => don't know how to synthesize placeholder
context:
α : Type u
x : α
depth : Nat
⊢ BalancedTree α 0_
  | n + 1 => don't know how to synthesize placeholder
context:
α : Type u
x : α
depth n : Nat
⊢ BalancedTree α (n + 1)_

The first hole yields the following message:

don't know how to synthesize placeholder
context:
α : Type u
x : α
depth : Nat
⊢ BalancedTree α 0

The second hole yields the following message:

don't know how to synthesize placeholder
context:
α : Type u
x : α
depth n : Nat
⊢ BalancedTree α (n + 1)

Matching on the depth of a tree and the tree itself leads to a refinement of the tree's type according to the depth's pattern. This means that certain combinations are not well-typed, such as 0 and branch, because refining the second discriminant's type yields BalancedTree α 0 which does not match the constructor's type.

def BalancedTree.isPerfectlyBalanced (n : Nat) (t : BalancedTree α n) : Bool :=
  match n, t with
  | 0, .empty => true
  | 0, type mismatch
  left.branch val right
has type
  BalancedTree ?m.53 (?m.50 + 1) : Type ?u.46
but is expected to have type
  BalancedTree α 0 : Type u.branch left val right => isPerfectlyBalanced left && isPerfectlyBalanced right
  | _, _ => false

type mismatch
  left.branch val right
has type
  BalancedTree ?m.53 (?m.50 + 1) : Type ?u.46
but is expected to have type
  BalancedTree α 0 : Type u

5.8.1.1. Pattern Equality Proofs

When a discriminant is named, Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match generates a proof that the pattern and discriminant are equal, binding it to the provided name in the right-hand side. This is useful to bridge the gap between dependent pattern matching on indexed families and APIs that expect explicit propositional arguments, and it can help tactics that make use of assumptions to succeed.

Pattern Equality Proofs

The function last?, which either throws an exception or returns the last element of its argument, uses the standard library function List.getLast. This function expects a proof that the list in question is nonempty. Naming the match on xs ensures that there's an assumption in scope that states that xs is equal to _ :: _, which simp_all uses to discharge the goal.

def last? (xs : List α) : Except String α :=
  match h : xs with
  | [] =>
    .error "Can't take first element of empty list"
  | _ :: _ =>
    .ok <| xs.getLast (show xs ≠ [] by intro h'α:Type ?u.7xs:List αhead✝:αtail✝:List αh:xs = head✝ :: tail✝h':xs = []⊢ False; simp_allAll goals completed! 🐙)

Without the name, simp_all is unable to find the contradiction.

def last?' (xs : List α) : Except String α :=
  match xs with
  | [] =>
    .error "Can't take first element of empty list"
  | _ :: _ =>
    .ok <| xs.getLast (show xs ≠ [] by intro h'α:Type ?u.7xs:List αhead✝:αtail✝:List αh':xs = []⊢ False; simp_all made no progresssimp_allα:Type ?u.7xs:List αhead✝:αtail✝:List αh':xs = []⊢ False)

simp_all made no progress

5.8.1.2. Explicit Motives

Pattern matching is not a built-in primitive of Lean. Instead, it is translated to applications of recursors via auxiliary matching functions. Both require a motive that explains the relationship between the discriminant and the resulting type. Generally, the Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match elaborator is capable of synthesizing an appropriate motive, and the refinement of types that occurs during pattern matching is a result of the motive that was selected. In some specialized circumstances, a different motive may be needed and may be provided explicitly using the (motive := …) syntax of Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match. This motive should be a function type that expects at least as many parameters as there are discriminants. The type that results from applying a function with this type to the discriminants in order is the type of the entire Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match term, and the type that results from applying a function with this type to all patterns in each alternative is the type of that alternative's right-hand side.

Matching with an Explicit Motive

An explicit motive can be used to provide type information that is otherwise unavailable from the surrounding context. Attempting to match on a number and a proof that it is in fact 5 is an error, because there's no reason to connect the number to the proof:

#eval
  match 5, rfl with
  invalid match-expression, pattern contains metavariables
  Eq.refl ?m.73| 5, rfl => "ok"

invalid match-expression, pattern contains metavariables
  Eq.refl ?m.73

An explicit motive explains the relationship between the discriminants:

"ok"#eval
  match (motive := (n : Nat) → n = 5 → String) 5, rfl with
  | 5, rfl => "ok"

"ok"

When matching on an indexed family, the indices must also be discriminants. Otherwise, the pattern would not be well typed: it is a type error if an index is just a variable but the type of a constructor requires a more specific value. However, a process called discriminant refinement automatically adds indices as additional discriminants.

Discriminant Refinement

In the definition of f, the equality proof is the only discriminant. However, equality is an indexed family, and the match is only valid when n is an additional discriminant.

def f (n : Nat) (p : n = 3) : String :=
  match p with
  | rfl => "ok"

Using Lean.Parser.Command.print : command#print demonstrates that the additional discriminant was added automatically.

def f : (n : Nat) → n = 3 → String :=
fun n p =>
  match 3, p with
  | .(n), ⋯ => "ok"#print f

def f : (n : Nat) → n = 3 → String :=
fun n p =>
  match 3, p with
  | .(n), ⋯ => "ok"

5.8.1.4. Generalization🔗

The pattern match elaborator automatically determines the motive by finding occurrences of the discriminants in the expected type, generalizing them in the types of subsequent discriminants so that the appropriate pattern can be substituted. Additionally, occurrences of the discriminants in the types of variables in the context are generalized and substituted by default. This latter behavior can be turned off by passing the (generalizing := false) flag to Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match.

Matching, With and Without Generalization

In this definition of boolCases, the assumption b is generalized in the type of h and then replaced with the actual pattern. This means that ifTrue and ifFalse have the types true = true → α and false = false → α in their respective cases, but h's type mentions the original discriminant.

def boolCases (b : Bool)
    (ifTrue : b = true → α)
    (ifFalse : b = false → α) :
    α :=
  match h : b with
  | true  => ifTrue application type mismatch
  ifTrue h
argument
  h
has type
  b = true : Prop
but is expected to have type
  true = true : Proph
  | false => ifFalse application type mismatch
  ifFalse h
argument
  h
has type
  b = false : Prop
but is expected to have type
  false = false : Proph

The error for the first case is typical of both:

application type mismatch
  ifTrue h
argument
  h
has type
  b = true : Prop
but is expected to have type
  true = true : Prop

Turning off generalization allows type checking to succeed, because b remains in the types of ifTrue and ifFalse.

def boolCases (b : Bool)
    (ifTrue : b = true → α)
    (ifFalse : b = false → α) :
    α :=
  match (generalizing := false) h : b with
  | true  => ifTrue h
  | false => ifFalse h

In the generalized version, rfl could have been used as the proof arguments as an alternative.

5.8.2. Custom Pattern Functions🔗

In patterns, defined constants with the match_pattern attribute are unfolded and normalized rather than rejected. This allows a more convenient syntax to be used for many patterns. In the standard library, Nat.add, HAdd.hAdd, Add.add, and Neg.neg all have this attribute, which allows patterns like n + 1 instead of Nat.succ n. Similarly, Unit and Unit.unit are definitions that set the respective universe parameters of PUnit and PUnit.unit to 0; the match_pattern attribute on Unit.unit allows it to be used in patterns, where it expands to PUnit.unit.{0}.

syntaxAttribute for Match Patterns

The match_pattern attribute indicates that a definition should be unfolded, rather than rejected, in a pattern.

attr ::= ...
    | match_pattern

Match Patterns Follow Reduction

The following function can't be compiled:

def nonzero (n : Nat) : Bool :=
  match n with
  | 0 => false
  invalid patterns, `k` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  .(Nat.add 1 k)| 1 + k => true

The error message on the pattern 1 + _ is:

invalid patterns, `k` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  .(Nat.add 1 k)

This is because Nat.add is defined by recursion on its second parameter, equivalently to:

def add : Nat → Nat → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

No ι-reduction is possible, because the value being matched is a variable, not a constructor. 1 + k gets stuck as Nat.add 1 k, which is not a valid pattern.

In the case of k + 1, that is, Nat.add k (.succ .zero), the second pattern matches, so it reduces to Nat.succ (Nat.add k .zero). The second pattern now matches, yielding Nat.succ k, which is a valid pattern.

5.8.3. Pattern Matching Functions🔗

syntax

Functions may be specified via pattern matching by writing a sequence of patterns after Lean.Parser.Term.fun : termfun, each preceded by a vertical bar (|).

term ::= ...
    | fun
        (| term,* => term)*

This desugars to a function that immediately pattern-matches on its arguments.

Pattern-Matching Functions

isZero is defined using a pattern-matching function abstraction, while isZero' is defined using a pattern match expression:

def isZero : Nat → Bool :=
  fun
    | 0 => true
    | _ => false

def isZero' : Nat → Bool :=
  fun n =>
    match n with
    | 0 => true
    | _ => false

Because the former is syntactic sugar for the latter, they are definitionally equal:

example : isZero = isZero' := rfl

The desugaring is visible in the output of Lean.Parser.Command.print : command#print:

def isZero : Nat → Bool :=
fun x =>
  match x with
  | 0 => true
  | x => false#print isZero

outputs

def isZero : Nat → Bool :=
fun x =>
  match x with
  | 0 => true
  | x => false

while

def isZero' : Nat → Bool :=
fun n =>
  match n with
  | 0 => true
  | x => false#print isZero'

outputs

def isZero' : Nat → Bool :=
fun n =>
  match n with
  | 0 => true
  | x => false

5.8.4. Other Pattern Matching Operators

In addition to Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match and termIfLet : term`if let pat := d then t else e` is a shorthand syntax for: ``` match d with | pat => t | _ => e ``` It matches `d` against the pattern `pat` and the bindings are available in `t`. If the pattern does not match, it returns `e` instead.if let, there are a few other operators that perform pattern matching.

syntax

The Lean.«term_Matches_|» : termmatches operator returns true if the term on the left matches the pattern on the right.

term ::= ...
    | term matches term

When branching on the result of Lean.«term_Matches_|» : termmatches, it's usually better to use termIfLet : term`if let pat := d then t else e` is a shorthand syntax for: ``` match d with | pat => t | _ => e ``` It matches `d` against the pattern `pat` and the bindings are available in `t`. If the pattern does not match, it returns `e` instead.if let, which can bind pattern variables in addition to checking whether a pattern matches.

If there are no constructor patterns that could match a discriminant or sequence of discriminants, then the code in question is unreachable, as there must be a false assumption in the local context. The Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if Lean can show that an empty set of patterns is exhaustive given `e`'s type, e.g. because it has no constructors.nomatch expression is a match with zero cases that can have any type whatsoever, so long as there are no possible cases that could match the discriminants.

syntaxCaseless Pattern Matches

term ::= ...
    | Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
nomatch term,*

Inconsistent Indices

There are no constructor patterns that can match both proofs in this example:

example (p1 : x = "Hello") (p2 : x = "world") : False :=
  nomatch p1, p2

This is because they separately refine the value of x to unequal strings. Thus, the Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if Lean can show that an empty set of patterns is exhaustive given `e`'s type, e.g. because it has no constructors.nomatch operator allows the example's body to prove False (or any other proposition or type).

When the expected type is a function type, Lean.Parser.Term.nofun : termnofun is shorthand for a function that takes as many parameters as the type indicates in which the body is Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if Lean can show that an empty set of patterns is exhaustive given `e`'s type, e.g. because it has no constructors.nomatch applied to all of the parameters.

syntaxCaseless Functions

term ::= ...
    | nofun

Impossible Functions

Instead of introducing arguments for both equality proofs and then using both in a Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if Lean can show that an empty set of patterns is exhaustive given `e`'s type, e.g. because it has no constructors.nomatch, it is possible to use Lean.Parser.Term.nofun : termnofun.

example : x = "Hello" → x = "world" → False := nofun

5.8.5. Elaborating Pattern Matching🔗

Planned Content

Specify the elaboration of pattern matching to auxiliary match functions.

Tracked at issue #209