6.8. パターンマッチ（Pattern Matching）🔗

パターンマッチ （pattern matching）は項のサブセットである パターン （pattern）の構文を使用して、値を認識・分解するための手段です。値を認識して分解するパターンは、値を構成するために使用される構文に似ています。1つ以上の マッチ判別子 （match discriminant）が一連の マッチ選択肢 （match alternative）と同時に比較されます。判別子には名前を付けることができます。各選択肢は、カンマで区切られた1つ以上のパターン列を含んでいます；すべてのパターン列は、識別子の数と同じ数のパターンを含んでいなければなりません。パターン列がすべての判別子にマッチすると、対応する 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. => に続く項が、各 パターン変数 の値と各名前付き判別子に対する等式の仮定が追加された環境で評価されます。この項はマッチ選択肢の 右辺 （right-hand side）と呼ばれます。

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

パターンマッチ式は代わりに quasiquotations をパターンとして使用することができ、対応する Lean.Syntax 値にマッチし、 antiquotations の内容は通常のパターンとして扱われます。quotation のパターンはその他のパターンとは異なるコンパイルをされるため、 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 の中のどれか1つのパターンが構文であれば、すべてのパターンも構文でなければなりません。quotation パターンは quotation の節 で説明されています。

パターンは項のサブセットです。これらは以下から構成されます：

Catch-All パターン

ホールの構文 _ は任意の値にマッチし、パターン変数を束縛しないパターンです。Catch-All パターンは未使用のパターン変数を完全に同等ではありません。Catch-All パターンはパターンの型付けがより具体的な アクセス不能パターン を必要とするような位置で使用することができますが、変数はこのような位置では使用できません。

識別子

識別子が現在のスコープで束縛されず、引数にも適用されない場合、これはパターン変数を表します。 パターン変数 （pattern variable）は任意の値にマッチし、こうしてマッチした値は 右辺 が評価されるローカル環境でパターン変数に束縛されます。識別子が束縛される場合、 帰納型 の コンストラクタ に束縛されるか、その定義に match_pattern 属性があれば、それはパターンです。

適用

関数適用はパターンになります。これは適用される関数がコンストラクタに束縛されている識別子であるか、 match_pattern 属性を持ち、すべての引数もパターンである場合です。識別子がコンストラクタの場合、引数のパターンがコンストラクタの引数にマッチすると、パターンはそのコンストラクタで構築された値にマッチします。 match_pattern 属性を持つ関数である場合、関数適用は展開され、結果の項の 正規形 がパターンとして使用されます。デフォルト引数は通常通り挿入され、その正規形がパターンとして使用されます。しかし、ellipsis は関連するデフォルト値やタクティクを持つものであっても、それ以降のすべての引数がユニバーサルパターンとして扱われてしまいます。

リテラル

文字リテラル と 文字列リテラル は、対応する文字または文字列にマッチするパターンです。 生文字列リテラル はパターンとして許容されますが、 補間文字列 は許容されません。パターン内の 自然数リテラル は、対応する OfNat インスタンスを統合し、その結果の項を 正規形 に簡約することで解釈されます。同様に、 科学的リテラル は対応する OfScientific インスタンスを介して解釈されます。 Float にはそのようなインスタンスがありますが、そのインスタンスは有効なパターンに簡約できない不透明な関数に依存しているため、 Float をパターンとして使用することはできません。

構造体インスタンス

構造体インスタンス はパターンとして使用することができます。それらは対応する構造体インスタンスとして解釈されます。

quote された名前

`x や ``plus などの quote された名前は、対応する Lean.Name 値をマッチします。

マクロ

パターン内のマクロは展開されます。展開の結果がパターンであれば、それらはパターンです。

アクセス不能パターン

アクセス不能パターン （inaccessible pattern）は、後の型付け制約によって特定の値を持つことを強制されるパターンです。任意の項をアクセス不能な項として使用することができます。アクセス不能項は括弧でくくられ、その前にピリオド（.）が付きます。

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)
アクセス不能パターン

数値の パリティ （parity）とはその値が偶か奇かを指します：

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) := n:Nath:Nat⊢ h + 1 + (h + 1) = h + h + 1 + 1 All goals completed! 🐙 eq ▸ .even (h + 1)

Parity 型の値は、偶数または奇数の表現の一部として、数の半分（切り捨て）を含むため、パリティを判定してから数を抽出することで、（一般的ではないですが）2による除算を実装することができます。

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

Parity.even と Parity.odd のインデックス構造は、それ以外の有効なパターンではない特定の形式を持つ数を強制するため、これにマッチするパターンは割られる数に対してアクセス不能パターンを使用しなければなりません。

パターンはさらに名前を付けることができます。 名前付きパターン （named pattern）はパターンに名前を付けます；後続のパターンとマッチ選択肢の右側では、名前は指定されたパターンにマッチした値の部分を指します。名前付きパターンは名前とパターンの間に @ を付けて記述します。判別子と同じように、名前付きパターンによって等価性の仮定にも名前を与えることができます。

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

6.8.1. 型（Types）

各判別子は適切に型付けされていなければなりません。パターンは項のサブセットであるため、その型もチェックできます。与えられた判別子にマッチする各パターンは、対応する判別子と同じ型を持っていなければなりません。

各マッチ選択肢の 右辺 は、 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 項全体と同じ型を持つ必要があります。依存型をサポートするために、判別子をパターンにマッチさせると、パターンの範囲内で期待される型が絞り込まれます。同じマッチ選択肢の後続パターンと右辺の型の両方において、判別子の出現はそれがマッチされたパターンに置き換えられます。

型の絞り込み

この 添字付けられた型の族 は深さが型にエンコードされた平衡に近い木を記述します。

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)

ある初期要素と与えられた深さに対して完全な平衡木を構成する関数の実装を始めるには、定義に ホール を使います。

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

エラーメッセージはその木が指定された深さを持つべきであることを示しています。

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

期待される深さに対してマッチしてホールを挿入すると、それぞれのホールに対してエラーメッセージが表示されます。これらのメッセージは depth がマッチした値で置き換えられ、期待される型が絞り込まれたことを示します。

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)_

一つ目のホールは以下のメッセージを生成します：

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

二つ目のホールは以下のメッセージを生成します：

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

木の深さと木自体でマッチすると、深さのパターンに従って木の型が絞り込まれます。これは 0 と branch のような特定の組み合わせが well-typed ではないことを意味します。なぜなら、2番目の判別子の型を絞り込むと BalancedTree α 0 が生成され、コンストラクタの型と一致しないからです。

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

6.8.1.1. パターンの等価性の証明（Pattern Equality Proofs）

判別子の名前が指定されると、 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 はパターンと判別子が等しいという証明を生成し、 右辺 で指定された名前に束縛します。これは添字付けられた型の族に対する依存パターンマッチと明示的な命題引数を期待する API とのギャップを埋めるにあたって便利であり、仮定を利用するタクティクを成功させるために役立ちます。

パターンの等価性の証明

関数 last? は例外を投げるか、引数の最後の要素を返す関数です。これは標準ライブラリの関数 List.getLast を使用しています。この関数は当該リストが空でないことの証明を期待します。xs にマッチする名前を付けることで、xs が _ :: _ に等しいことを記述する仮定がスコープに含まれることが保証されます。この仮定は simp_all がゴールを達成するために使用されます。

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 α:Type ?u.7xs:List αhead✝:αtail✝:List αh:xs = head✝ :: tail✝h':xs = []⊢ False; All goals completed! 🐙)

名前がない場合、 simp_all は矛盾を見つけることができません。

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

6.8.1.2. 明示的な動機（Explicit Motives）

パターンマッチは Lean の組み込みのプリミティブではありません。これは 補助マッチ関数 を介して 再帰子 の適用に変換されます。どちらも、判別子と結果の型の関係を説明する 動機 （motive）を必要とします。一般的に、 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 エラボレータは適切な動機を統合することができ、パターンマッチ中に発生する型の絞り込みは選択された動機の結果です。特殊な状況化では別の動機が必要になることがあり、その場合は 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 の (motive := …) 構文を使用して明示的に提供することができます。この動機は、少なくとも識別子の数と同じ数のパラメータを必要とする関数型でなければなりません。この型を持つ関数を判別子に順番に適用した結果の型は 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 項全体の型であり、この型を持つ関数を各選択肢のすべてのパターンに適用した結果の型はその選択肢の 右辺 の型です。

明示的な動機によるマッチ

明示的な動機は、周囲の文脈からは得られない型情報を提供するために使用することができます。ある数字とそれが実際には 5 であるという証明のマッチを試みると、数字と証明を結び付ける推論ができないためエラーとなります：

#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

明示的な動機は、判別子の間の関係を説明します：

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

6.8.1.3. 判別子の絞り込み（Discriminant Refinement）

添字付けられた型の族にマッチする場合、添字も判別子でなければなりません。一方で、パターンは正しく型付けされない可能性があります：添字が単なる変数であるにもかかわらず、コンストラクタの型がより具体的な値を必要とする場合は型エラーとなります。しかし、 判別子の絞り込み （discriminant refinement）と呼ばれる処理によって自動的に添字が追加の判別子として追加されます。

判別子の絞り込み

f の定義では、等式の証明が唯一の判別子です。しかし、等式は添字付けられた型の族であり、マッチは n が追加の判別子である場合にのみ有効です。

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

Lean.Parser.Command.print : command#print を使用することで、追加の判別子が自動的に追加されたことを確認できます。

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"

6.8.1.4. 一般化（Generalization）🔗

パターンマッチのエラボレータは、適切なパターンを代入できるように、期待される型で判別子の出現を見つけ、後続の判別子の型でそれらを一般化することによって動機を自動的に決定します。さらに、コンテキスト中の変数の型に判別子が出現した場合は、デフォルトで一般化・置換されます。この後者の動作は 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 にフラグ (generalizing := false) を渡すことでオフにすることができます。

一般化の有無によるマッチ

この boolCases の定義では、仮定 b は h の型で一般化され、実際のパターンに置き換えられます。つまり、 ifTrue と ifFalse はそれぞれのケースで true = true → α と false = false → α の型を持ちますが、h の型はもとの判別子に言及しています。

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

最初のケースのエラーが両者に典型的なものです：

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

一般化をオフにすると b は ifTrue と ifFalse の型のままであるため、型チェックが成功します。

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

一般化されたバージョンでは、選択肢として rfl を証明引数として使うこともできます。

6.8.2. カスタムのパターン関数（Custom Pattern Functions）🔗

パターンでは、 match_pattern 属性で定義された定数は拒否されずに展開・正規化されます。これにより、多くのパターンでより便利な構文を使用することができます。標準ライブラリでは、 Nat.add ・ HAdd.hAdd ・ Add.add ・ Neg.neg はすべてこの属性を持っており、 Nat.succ n の代わりに n + 1 のようなパターンを使用できます。同様に、 Unit と Unit.unit は PUnit と PUnit.unit のそれぞれの 宇宙パラメータ を0に設定したものに対する定義です； Unit.unit の match_pattern 属性により、 PUnit.unit.{0} に展開されるパターンで使用することができます。

syntaxAttribute for Match Patterns

match_pattern 属性は、定義がパターンで拒否されるのではなく、展開されるべきであることを示します。

attr ::= ...
    | match_pattern
マッチパターンが簡約に従う

次の関数はコンパイルできません：

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

パターン 1 + _ に対するエラーメッセージは次の通りです：

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

これは、 Nat.add が2番目のパラメータに対して再帰的に定義されているからです：

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

マッチする値はコンストラクタではなく変数であるため、 ι簡約 はできません。 1 + k は Nat.add 1 k という有効でないパターンとして引っかかります。

k + 1 の場合、つまり Nat.add k (.succ .zero) の場合、2番目のパターンがマッチするため、 Nat.succ (Nat.add k .zero) に簡約されます。再度2番目のパターンがマッチし、有効なパターン Nat.succ k が得られます。

6.8.3. パターンマッチ関数（Pattern Matching Functions）🔗

syntax

関数は Lean.Parser.Term.fun : termfun の後に縦棒（|）で始まる一連のパターンを書くことで、パターンマッチとして指定をすることができます。

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

これは引数を即座にパターンマッチする関数に脱糖されます。

パターンマッチ関数

isZero はパターンマッチ関数抽象を使って定義される一方、 isZero' はパターンマッチ式を使って定義されています：

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

前者は後者のための構文糖衣であるため definitionally equal です：

example : isZero = isZero' := rfl

脱糖は Lean.Parser.Command.print : command#print の出力で見ることができます：

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

上記は以下を出力し、

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

一方で、

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

上記は以下を出力します。

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

6.8.4. その他のパターンマッチ演算子（Other Pattern Matching Operators）

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 と 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 に加え、パターンマッチを行う演算子がいくつかあります。

syntax

Lean.«term_Matches_|» : termmatches 演算子は左側の項が右側の項にマッチする場合に true を返します。

term ::= ...
    | term matches term

Lean.«term_Matches_|» : termmatches の結果で分岐するような場合、通常は 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 を使う方が良いです。こちらではパターンがマッチしたかどうかに加え、パターン変数を束縛することができます。

判別子または判別子の列にマッチするコンストラクタのパターンが無い場合、ローカルコンテキストに誤った仮定が存在するはずであるため、問題のコードは到達不可能です。 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 式は、判別子にマッチする可能性のあるケースが存在しない限り、任意の型を持つことができるゼロケースとのマッチです。

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,*
一貫性のない添字

この例では、両方の証明にマッチするコンストラクタのパターンはありません：

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

これは x の値を別々に等しくない文字列に絞り込むためです。したがって、 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 演算子によって、この例の本体は False （またはその他の命題や型）を証明することができます。

期待される型が関数型である場合、 Lean.Parser.Term.nofun : termnofun はその型が示す数だけパラメータを取る関数の省略形であり、その関数の本体は全てのパラメータに適用された 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 です。

syntaxCaseless Functions
term ::= ...
    | nofun
不可能な関数

両方の等式証明の引数を導入し、 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 で両方を使用する代わりに、 Lean.Parser.Term.nofun : termnofun を使用することができます。

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

6.8.5. Elaborating Pattern Matching🔗

Planned Content

Specify the elaboration of pattern matching to auxiliary match functions.

Tracked at issue #209