term ::= ... |match ((generalizing := (trueVal | falseVal)))? ((motive := term))?matchDiscr,* with (| (term,*)|* => term)*
13.8. 模式匹配
模式匹配是一种使用模式语法识别值并解构值的方法；模式是项的一个子集。
用于识别并解构值的模式，其语法类似于构造该值时所使用的语法。
一个或多个匹配判别式会同时与一系列匹配分支进行比较。
判别式可以命名。
每个分支都包含一个或多个以逗号分隔的模式序列；所有模式序列所含的模式数都必须与判别式的数量相同。
当一个模式序列匹配全部判别式时，就在扩展后的环境中求值对应 Lean.Parser.Term.match : term=> 之后的项；该环境包含每个模式变量的值，以及每个具名判别式的一个相等性假设。
这个项称为匹配分支的右侧。
语法模式匹配
语法匹配判别式
matchDiscr ::=
matchDiscr ::= ...
|
模式匹配表达式也可以使用准引用作为模式：它匹配对应的 Lean.Syntax 值，并将反引用的内容视为普通模式。
引用模式的编译方式不同于其他模式，因此如果一个 Lean.Parser.Term.match : termmatch 中有一个模式是语法，那么所有模式都必须是语法。
引用模式见引用一节。
模式是项的一个子集。 模式由以下形式组成：
- 全匹配模式
空洞语法
_是一种匹配任意值且不绑定任何模式变量的模式。 全匹配模式并不完全等价于未使用的模式变量。 在模式的类型检查原本会要求更具体的不可访问模式的位置，可以使用全匹配模式，而变量不能用于这些位置。- 标识符
如果一个标识符未在当前作用域中绑定，也没有应用于实参，那么它表示一个模式变量。 模式变量匹配任意值；如此匹配到的值会绑定到模式变量，并加入求值右侧时所使用的局部环境。 如果标识符已绑定，那么当它绑定到某个归纳类型的构造器，或其定义带有
match_pattern属性时，它可以作为模式。- 应用
如果函数应用中的函数是绑定到构造器或带有
match_pattern属性的标识符，并且所有实参也都是模式，那么该函数应用就是模式。 如果该标识符是构造器，那么当实参模式与构造器的实参匹配时，此模式便匹配由该构造器构造的值。 如果它是带有match_pattern属性的函数，则展开该函数应用，并将所得项的范式用作模式。 默认实参会照常插入，并将其范式用作模式。 不过，省略号会使后续所有实参都被视为全匹配模式，即便这些实参带有相关的默认值或策略。- 字面量
字符字面量和字符串字面量是匹配相应字符或字符串的模式。 原始字符串字面量可以用作模式，但插值字符串不可以。 模式中的自然数字面量通过合成相应的
OfNat实例来解释，并将所得项归约为范式；该范式必须是模式。 类似地，科学计数字面量通过相应的OfScientific实例解释。- 结构体实例
结构体实例可以用作模式。 它们会被解释为相应的结构体构造器。
- 引用名称
`x和``none等引用名称会匹配相应的Lean.Name值。- 宏
模式中的宏会被展开。 如果展开结果是模式，那么这些宏就是模式。
- 不可访问模式
不可访问模式是因后续类型约束而被迫具有特定值的模式。 任何项都可以用作不可访问项。 不可访问项写在圆括号中，并以句点（
.）开头。
语法不可访问模式
term ::= ...
| 不可访问模式
一个数的奇偶性指它是偶数还是奇数：
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 类型的值在表示奇偶性时包含该数的一半（向下取整），因此可以先求奇偶性再提取其中的数，以一种非常规方式实现除以二。
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 的索引结构迫使该数具有某种原本不是合法模式的特定形式，因此匹配它的模式必须对被除数使用不可访问模式。
模式还可以命名。
具名模式把名称与模式关联起来；在后续模式和匹配分支的右侧中，该名称指代由给定模式匹配到的那部分值。
具名模式在名称与模式之间写一个 @。
与判别式一样，也可以为具名模式的相等性假设提供名称。
语法具名模式
term ::= ...
| term ::= ...
| 13.8.1. 类型
每个判别式都必须类型正确。 因为模式是项的一个子集，所以也可以检查它们的类型。 匹配某个判别式的每个模式，都必须与相应的判别式具有相同类型。
每个匹配分支的右侧都应与整个 Lean.Parser.Term.match : termmatch 项具有相同类型。
为支持依赖类型，将判别式与模式匹配会精化模式作用域内的预期类型。
在同一匹配分支的后续模式以及右侧的类型中，出现的判别式都会替换为与之匹配的模式。
类型精化
这个索引族描述近乎平衡的树，并将深度编码在类型中。
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 :=
_
错误消息表明树应具有指定的深度。
对预期深度进行匹配并插入空洞，会为每个空洞产生一条错误消息。
这些消息表明预期类型已经精化，其中 depth 被匹配到的值替换。
def BalancedTree.filledWith
(x : α) (depth : Nat) :
BalancedTree α depth :=
match depth with
| 0 => _
| n + 1 => _
第一个空洞产生以下消息：
第二个空洞产生以下消息：
同时匹配树的深度和树本身，会根据深度模式精化树的类型。
这意味着某些组合不是良类型的，例如 0 与 branch，因为精化第二个判别式的类型会得到 BalancedTree α 0，它与构造器的类型不匹配。
def BalancedTree.isPerfectlyBalanced
(n : Nat) (t : BalancedTree α n) : Bool :=
match n, t with
| 0, .empty => true
| 0, .branch left val right =>
isPerfectlyBalanced left &&
isPerfectlyBalanced right
| _, _ => false
13.8.1.1. 模式相等性证明
当判别式具名时，Lean.Parser.Term.match : termmatch 会生成模式与判别式相等的证明，并在右侧中把它绑定到所提供的名称。
这有助于衔接对索引族的依赖模式匹配与要求显式命题实参的 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 ≠ [] All goals completed! 🐙 α:Type ?u.3xs: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 ≠ [] α:Type ?u.3xs:List αhead✝:αtail✝:List αh':xs = []⊢ False α:Type ?u.3xs:List αhead✝:αtail✝:List αh':xs = []⊢ False; α:Type ?u.3xs:List αhead✝:αtail✝:List αh':xs = []⊢ False)
13.8.1.2. 显式动机
模式匹配并不是 Lean 的内建原语。
相反，它通过辅助匹配函数翻译成对递归器的应用。
二者都需要一个动机来说明判别式与结果类型之间的关系。
通常，Lean.Parser.Term.match : termmatch 精译器能够合成适当的动机，而模式匹配过程中发生的类型精化正是所选动机的结果。
在某些特殊情况下，可能需要不同的动机；可以使用 Lean.Parser.Term.match : termmatch 的 (motive := …) 语法显式提供它。
该动机应当是函数类型，并且至少接受与判别式数量相同的参数。
依次将这种类型的函数应用于各判别式所得的类型，就是整个 Lean.Parser.Term.match : termmatch 项的类型；将它应用于每个分支中的所有模式所得的类型，则是该分支右侧的类型。
13.8.1.3. 判别式精化
匹配索引族时，其索引也必须作为判别式。 否则模式将不是良类型的：如果某个索引只是变量，而构造器的类型要求更具体的值，就会产生类型错误。 不过，称为判别式精化的过程会自动把索引添加为额外的判别式。
13.8.1.4. 泛化
模式匹配精译器通过在预期类型中查找判别式的出现位置，自动确定动机；它在后续判别式的类型中泛化这些出现位置，以便代入相应的模式。
此外，默认情况下，上下文中变量类型里出现的判别式也会被泛化并替换。
向 Lean.Parser.Term.match : termmatch 传入 (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 h
| false => ifFalse h
第一个分支的错误是二者共有的典型错误：
关闭泛化后，类型检查能够成功，因为 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 作为证明实参。
13.8.2. 自定义模式函数
在模式中，带有 match_pattern 属性的已定义常量会被展开并规范化，而不是被拒绝。
这使许多模式可以使用更方便的语法。
标准库中的 Nat.add、HAdd.hAdd、Add.add 和 Neg.neg 都带有此属性，因此可以使用 n + 1 这样的模式，而不必写 Nat.succ n。
类似地，Unit 和 Unit.unit 是把 PUnit 和 PUnit.unit 各自的宇宙参数设为 0 的定义；Unit.unit 上的 match_pattern 属性使其可用于模式，并在其中展开为 PUnit.unit.{0}。
属性匹配模式属性
match_pattern 属性表示某个定义在模式中应被展开，而不是被拒绝。
attr ::= ... | match_pattern
匹配模式遵循归约
以下函数无法编译：
def nonzero (n : Nat) : Bool :=
match n with
| 0 => false
| 1 + k => true
模式 1 + _ 上的错误消息是：
这是因为 Nat.add 通过对第二个参数递归来定义，等价于：
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)，第二个模式匹配，因此它归约为 Nat.succ (Nat.add k .zero)。
此时第二个模式再次匹配，得到 Nat.succ k，这是一个合法模式。
13.8.3. 模式匹配函数
语法模式匹配函数
可以通过模式匹配指定函数：在 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
由于前者是后者的语法糖，两者在定义上相等：
example : isZero = isZero' := rfl
Lean.Parser.Command.print : command#print 的输出可显示脱糖结果：
#print isZero
输出
而
#print isZero'
输出
13.8.4. 其他模式匹配运算符
除 Lean.Parser.Term.match : termmatch 和 termIfLet : termif let 外，还有一些其他运算符会执行模式匹配。
语法
matches 运算符
根据 Lean.«term_Matches_|» : termmatches 的结果进行分支时，通常最好使用 termIfLet : termif let；它除了检查模式是否匹配外，还能绑定模式变量。
如果没有任何构造器模式能够匹配一个判别式或一组判别式，那么相关代码不可达，因为局部上下文中必然存在一个错误假设。
Lean.Parser.Term.nomatch : termnomatch 表达式是一个没有任何分支的匹配；只要不存在可能匹配判别式的分支，它就可以具有任意类型。
语法无分支模式匹配
term ::= ...
| 不一致的索引
当预期类型是函数类型时，Lean.Parser.Term.nofun : termnofun 是一种简写：它构造一个接受类型所指定数量参数的函数，并以应用于全部参数的 Lean.Parser.Term.nomatch : termnomatch 作为函数体。
语法无分支函数
term ::= ... | nofun