Lean 语言参考手册

关于：inductionWithNoAlts🔗

Error code: lean.inductionWithNoAlts

Induction pattern with nontactic in natural-number-game-style `with` clause.

Severity: ErrorSince: 4.26.0

在 Lean 中使用归纳的策略证明需要用类似模式匹配的记法描述证明的各个情形。 不过，Mathlib 中的 induction' 策略以及自然数游戏使用的专用 induction 策略遵循不同的模式。

示例🔗

为归纳证明添加显式情形
theorem zero_mul (m : Nat) : 0 * m = 0 := by induction m Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.with n n_ih rw [Nat.mul_zero] rw [Nat.mul_succ] rw [Nat.add_zero] rw [n_ih] 
Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
theorem zero_mul (m : Nat) : 0 * m = 0 := by induction m with | zero => rw [Nat.mul_zero] | succ n n_ih => rw [Nat.mul_succ] rw [Nat.add_zero] rw [n_ih]

这个错误例子具有自然数游戏中正确证明的结构；如果 import Mathlib 并将 induction 替换为 induction'， 该证明就能工作。基础 Lean 中的归纳策略要求 with 关键字后跟一系列情形， 归纳情形的名称应在 succ 情形中提供，而不是预先提供。