Theorem Proving in Lean 4

5. 策略（Tactics）

本章中，我们描述一种构建证明的替代方法，即使用策略（tactic）。证明项（proof term）是数学证明的一种表示；策略（tactic）是描述如何构建这样一条证明的命令或指令。非正式地说，你可能这样开始一个数学证明："为了证明正向方向，展开定义，应用（apply）前一条引理，然后化简。"正如这些是指示读者如何找到相关证明的指令一样，策略（tactic）是指示 Lean 如何构建证明项的指令。它们天然地支持一种增量式的证明编写风格，在这种风格中，你可以分解一个证明并逐步处理目标。

我们将由策略（tactic）序列组成的证明称为"策略风格"证明，以区别于我们目前所见到的编写证明项的方式，后者称为"项风格"证明。每种风格各有其优缺点。例如，策略风格的证明可能更难阅读，因为它们要求读者预测或猜测每条指令的结果。但它们也可能更短且更易编写。此外，策略（tactic）为使用 Lean 的自动化功能提供了途径，因为自动化过程本身就是策略（tactic）。

5.1. 进入策略模式（Entering Tactic Mode）🔗

概念上讲，陈述一个定理或引入一个 have 语句会创建一个目标（goal），即构建一个具有预期类型的项的目标。例如，下面创建了构建一个类型为 p ∧ q ∧ p 的项的目标，上下文中有常量 p q : Prop，hp : p 和 hq : q：

theorem declaration uses 'sorry'test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p All goals completed! 🐙

你可以将这个目标写作如下形式：

p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p

事实上，如果你将上面例子中的"sorry"替换为下划线，Lean 会报告这正是未被求解的目标。

通常情况下，你通过编写一个显式的项来满足这样的目标。但在任何期望项的地方，Lean 允许我们插入一个 by <tactics> 块，其中 <tactics> 是由分号或换行符分隔的一系列指令。你可以通过这种方式证明上面的定理：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

我们经常将 by 关键字放在前一行，并将上面的例子写成：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

apply 策略（apply tactic）应用（apply）一个表达式，将其视为一个具有零个或多个参数的函数。它将结论（conclusion）与当前目标中的表达式进行合一（unify），并为剩余的参数创建新的目标，前提是后面的参数不依赖于它们。在上面的例子中，指令 apply And.intro 产生两个子目标（subgoal）：

p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p

第一个目标由指令 exact hp 满足。exact 指令只是 apply 的一个变体，它指示给出的表达式应该精确地填充目标。在策略证明中使用它是一种好风格，因为它的失败表明出现了问题。它也比 apply 更健壮，因为精化器（elaborator）在处理被应用的表达式时会考虑由目标类型给定的预期类型。不过在此例中，apply 也完全可行。

你可以使用 #print 命令查看生成的证明项：

theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩#print test
theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

你可以增量式地编写策略脚本。在 VS Code 中，你可以按 CtrlShiftEnter 打开一个窗口来显示消息，当光标位于策略块中时，该窗口会显示当前目标。如果证明不完整，by 标记会带有红色波浪线，并且错误消息会包含剩余的目标。

策略指令可以接受复合表达式，而不仅仅是单个标识符。以下是前面证明的一个更短版本：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p All goals completed! 🐙

不出所料，它产生完全相同的证明项：

theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩#print test
theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

多个策略应用（apply）可以通过分号连接写在一行中。

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p; All goals completed! 🐙

可能产生多个子目标的策略（tactic）通常会为它们打上标签。例如，策略（tactic） apply And.intro 将第一个子目标标记为 leftp:Propq:Prophp:phq:q⊢ p，第二个子目标标记为 rightp:Propq:Prophp:phq:q⊢ q。对于 And.intro，标签是从声明中使用的参数名称推断出来的。你可以使用记号 case <tag> => <tactics> 来结构化你的策略（tactic）。以下是本章中第一个策略证明的结构化版本。

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p case left p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p case left p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

你可以使用 rightp:Propq:Prophp:phq:q⊢ q ∧ p 子目标，配合 case 记号：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p case right p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p case left p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 case left p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

注意，Lean 会在 case 块中隐藏其他目标。在 case left => 之后，证明状态为：

p:Propq:Prophp:phq:q⊢ q

我们说 case 正在"聚焦"所选目标。此外，如果在 case 块结束时所选目标没有完全求解，Lean 会标记一个错误。

对于简单的子目标，使用标签选择子目标可能不值得，但你仍然可能希望对证明进行结构化。Lean 也提供了"子弹"记号 . <tactics>（或 · <tactics>）来结构化证明：

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

5.2. 基本策略（Basic Tactics）🔗

除了 apply（应用）和 exact（精确提供）之外，另一个有用的策略（tactic）是 intro（引入），它引入一个假设。下面是一个命题逻辑中同一律的例子，我们在前一章中证明过，现在用策略（tactic）来证明。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ q → p ∧ q ∨ p ∧ rp:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ r → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ q → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ q p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ r → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ q → p ∧ (q ∨ r)p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ q → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ r All goals completed! 🐙

intro（引入）指令更一般地可以用于引入任何类型的变量：

example (α : Type) : α → α := α:Type⊢ α → α α:Typea:α⊢ α All goals completed! 🐙 example (α : Type) : ∀ x : α, x = x := α:Type⊢ ∀ (x : α), x = x α:Typex:α⊢ x = x All goals completed! 🐙

你可以使用它来引入多个变量：

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b intro a a:Natb:Nat⊢ ∀ (c : Nat), a = b → a = c → c = b a:Natb:Natc:Nat⊢ a = b → a = c → c = b a:Natb:Natc:Nath₁:a = b⊢ a = c → c = b a:Natb:Natc:Nath₁:a = bh₂:a = c⊢ c = b All goals completed! 🐙

正如 apply（应用）策略（tactic）是用于交互式构建函数应用的指令，intro（引入）策略（tactic）是用于交互式构建函数抽象（即形如 fun x => e 的项）的指令。与 lambda 抽象记号一样，intro（引入）策略（tactic）允许我们使用隐式的 match。

example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := α:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x α:Sort u_1p:α → Propq:α → Propw:αhpw:p whqw:q w⊢ ∃ x, q x ∧ p x All goals completed! 🐙

你也可以像在 match 表达式中一样提供多个分支。

example (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := α:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x intro α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:p w⊢ ∃ x, q x ∨ p x All goals completed! 🐙 α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:q w⊢ ∃ x, q x ∨ p x All goals completed! 🐙

intros（全部引入）策略（tactic）可以不带任何参数使用，在这种情况下，它会选择名称并尽可能多地引入变量。你马上就会看到一个例子。

assumption（假定）策略（tactic）会查看当前目标上下文中的假设，如果存在与结论匹配的假设，就应用它。

variable (x y z w : Nat) example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ z = w All goals completed! 🐙 -- applied h₃

如果有必要，它会合一结论中的元变量（metavariable）：

variable (x y z w : Nat) example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = ?bx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?b = wx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ Nat x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?b = w -- solves x = ?b with h₁ x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = ?h₂.bx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?h₂.b = wx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ Nat x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?h₂.b = w -- solves y = ?h₂.b with h₂ All goals completed! 🐙 -- solves z = w with h₃

下面的例子使用 intros（全部引入）指令自动引入三个变量和两个假设：

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = b✝ a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = ?ba✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = c✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝ All goals completed! 🐙

注意，由 Lean 自动生成的名称默认是不可访问的。这样做的动机是确保你的策略证明不依赖于自动生成的名称，从而更加健壮。然而，你可以使用组合子 unhygienic 来禁用这个限制。

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b unhygienic a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ c = b a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ c = ?ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ Nat a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ca:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ Nat a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = b All goals completed! 🐙

你也可以使用 rename_i（重命名）策略（tactic）来重命名上下文中最近的那些不可访问的名称。在下面的例子中，策略（tactic）rename_i h1 _ h2 重命名了你上下文中最后三个假设中的两个。

example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := ⊢ ∀ (a b c d : Nat), a = b → a = d → a = c → c = b a✝³:Natb✝:Natc✝:Natd✝:Nata✝²:a✝³ = b✝a✝¹:a✝³ = d✝a✝:a✝³ = c✝⊢ c✝ = b✝ a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ c✝ = b✝ a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ c✝ = ?ba✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b = b✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ Nat a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b = c✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b = b✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ Nat a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b = b✝ All goals completed! 🐙

rfl（自反性）策略（tactic）求解那些将自反关系应用于定义上相等的参数的目标。相等是自反的：

example (y : Nat) : (fun unused variable `x` Note: This linter can be disabled with `set_option linter.unusedVariables false`x : Nat => 0) y = 0 := y:Nat⊢ (fun x => 0) y = 0 All goals completed! 🐙

repeat（重复）组合子可以用于多次应用一个策略（tactic）：

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = b✝ a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = ?ba✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = c✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat repeat All goals completed! 🐙

另一个有时有用的策略（tactic）是 revert（撤回）策略（tactic），它在某种意义上与 intro（引入）相反：

example (x : Nat) : x = x := x:Nat⊢ x = x ⊢ ∀ (x : Nat), x = x y:Nat⊢ y = y All goals completed! 🐙

在 revert x 之后，证明状态为：

⊢ ∀ (x : Nat), x = x

在 intro y 之后，它为：

y:Nat⊢ y = y

将假设移到目标中会产生一个蕴含：

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x x:Naty:Nat⊢ x = y → y = x x:Naty:Nath₁:x = y⊢ y = x -- goal is x y : Nat, h₁ : x = y ⊢ y = x x:Naty:Nath₁:x = y⊢ x = y All goals completed! 🐙

在 revert h 之后，证明状态为：

x:Naty:Nat⊢ x = y → y = x

在 intro h₁ 之后，它为：

x:Naty:Nath₁:x = y⊢ y = x

但 revert（撤回）甚至更加聪明，因为它不仅会撤回上下文中的一个元素，还会撤回上下文中所有依赖于它的后续元素。例如，在上面例子中撤回 x 会同时带走 h：

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x y:Nat⊢ ∀ (x : Nat), x = y → y = x y:Natx✝:Nath✝:x✝ = y⊢ y = x✝ y:Natx✝:Nath✝:x✝ = y⊢ x✝ = y All goals completed! 🐙

在 revert x 之后，目标为：

y:Nat⊢ ∀ (x : Nat), x = y → y = x

你也可以一次性撤回上下文中的多个元素：

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x ⊢ ∀ (x y : Nat), x = y → y = x x✝:Naty✝:Nath✝:x✝ = y✝⊢ y✝ = x✝ x✝:Naty✝:Nath✝:x✝ = y✝⊢ x✝ = y✝ All goals completed! 🐙

在 revert x y 之后，目标为：

⊢ ∀ (x y : Nat), x = y → y = x

你只能 revert（撤回）局部上下文中的一个元素，即局部变量或假设。但是你可以使用 generalize（泛化）策略（tactic）将目标中的任意表达式替换为一个新变量：

example : 3 = 3 := ⊢ 3 = 3 x:Nat⊢ x = x ⊢ ∀ (x : Nat), x = x y:Nat⊢ y = y All goals completed! 🐙

具体来说，在 generalize 之后，目标为

x:Nat⊢ x = x

上面记号中的助记含义是：你通过将 3 设置为一个任意变量 x 来泛化目标。注意：并非所有泛化都保持目标的有效性。这里，generalize（泛化）将一个可以用 rfl 证明的目标替换为一个不可证明的目标：

declaration uses 'sorry'example : 2 + 3 = 5 := ⊢ 2 + 3 = 5 x:Nat⊢ 2 + x = 5 All goals completed! 🐙

在这个例子中，sorry（抱歉）策略（tactic）是 sorry 证明项的对等物。它关闭当前目标，产生通常的警告，表明 sorry 已被使用。为了保持前一个目标的有效性，generalize（泛化）策略（tactic）允许我们记录 3 已被替换为 x 这一事实。你只需要提供一个标签，generalize 就使用它来将赋值存储在局部上下文中：

example : 2 + 3 = 5 := ⊢ 2 + 3 = 5 x:Nath:3 = x⊢ 2 + x = 5 All goals completed! 🐙

在 generalize h : 3 = x 之后，h 是一个证明 3 = x：

x:Nath:3 = x⊢ 2 + x = 5

这里，重写策略（rewrite tactic）rw（重写）使用 h 再次将 x 替换为 3。rw（重写）策略（tactic）将在下面讨论。

5.3. 更多策略（More Tactics）🔗

一些额外的策略（tactic）对于构造和析构命题与数据很有用。例如，当应用于形式为 p ∨ q 的目标时，你可以使用诸如 apply Or.inl 和 apply Or.inr 这样的策略（tactic）。反过来，cases（情况分析）策略（tactic）可以用于分解一个析取：

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p cases h with p:Propq:Prophp:p⊢ q ∨ p p:Propq:Prophp:p⊢ p; All goals completed! 🐙 p:Propq:Prophq:q⊢ q ∨ p p:Propq:Prophq:q⊢ q; All goals completed! 🐙

注意其语法与 match 表达式中使用的语法类似。新的子目标可以按任意顺序求解：

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p cases h with p:Propq:Prophq:q⊢ q ∨ p p:Propq:Prophq:q⊢ q; All goals completed! 🐙 p:Propq:Prophp:p⊢ q ∨ p p:Propq:Prophp:p⊢ p; All goals completed! 🐙

你也可以使用（非结构化的）cases（情况分析），不带 with，并为每个分支提供一个策略（tactic）：

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:p⊢ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q All goals completed! 🐙

（非结构化的）cases（情况分析）在你可以用同一个策略（tactic）关闭多个子目标时特别有用：

example (p : Prop) : p ∨ p → p := p:Prop⊢ p ∨ p → p p:Proph:p ∨ p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p repeat All goals completed! 🐙

你也可以使用组合子 tac1 <;> tac2 将 tac2 应用于策略（tactic）tac1 产生的每个子目标：

example (p : Prop) : p ∨ p → p := p:Prop⊢ p ∨ p → p p:Proph:p ∨ p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p All goals completed! 🐙

你可以将非结构化的 cases（情况分析）策略（tactic）与 case（情况分析）和 . 记号结合使用：

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ p p:Propq:Proph✝:p⊢ p All goals completed! 🐙 p:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q All goals completed! 🐙 example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p case inr h p:Propq:Proph:q⊢ q ∨ p p:Propq:Proph:q⊢ q All goals completed! 🐙 case inl h p:Propq:Proph:p⊢ q ∨ p p:Propq:Proph:p⊢ p All goals completed! 🐙 example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p case inr h p:Propq:Proph:q⊢ q ∨ p p:Propq:Proph:q⊢ q All goals completed! 🐙 p:Propq:Proph✝:p⊢ q ∨ p p:Propq:Proph✝:p⊢ p All goals completed! 🐙

cases（情况分析）策略（tactic）也可以用于分解合取：

example (p q : Prop) : p ∧ q → q ∧ p := p:Propq:Prop⊢ p ∧ q → q ∧ p p:Propq:Proph:p ∧ q⊢ q ∧ p cases h with p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p; p:Propq:Prophp:phq:q⊢ p; All goals completed! 🐙

在这个例子中，应用 cases（情况分析）策略（tactic）后只有一个目标，其中 h : p ∧ q 被替换为一对假设 hp : p 和 hq : q：

p:Propq:Prophp:phq:q⊢ q ∧ p

constructor（构造）策略（tactic）应用合取唯一的构造子（constructor）And.intro。

利用这些策略（tactic），前一节中的一个例子可以重写如下：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h with p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q ∨ p ∧ rp:Propq:Propr:Prophp:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q; p:Propq:Propr:Prophp:ph✝:q⊢ pp:Propq:Propr:Prophp:ph✝:q⊢ q p:Propq:Propr:Prophp:ph✝:q⊢ pp:Propq:Propr:Prophp:ph✝:q⊢ q All goals completed! 🐙 p:Propq:Propr:Prophp:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:r⊢ p ∧ r; p:Propq:Propr:Prophp:ph✝:r⊢ pp:Propq:Propr:Prophp:ph✝:r⊢ r p:Propq:Propr:Prophp:ph✝:r⊢ pp:Propq:Propr:Prophp:ph✝:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) cases hpq with p:Propq:Propr:Prophp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophp:phq:q⊢ pp:Propq:Propr:Prophp:phq:q⊢ q ∨ r; p:Propq:Propr:Prophp:phq:q⊢ q ∨ r; p:Propq:Propr:Prophp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) cases hpr with p:Propq:Propr:Prophp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophp:phr:r⊢ pp:Propq:Propr:Prophp:phr:r⊢ q ∨ r; p:Propq:Propr:Prophp:phr:r⊢ q ∨ r; p:Propq:Propr:Prophp:phr:r⊢ r; All goals completed! 🐙

你将在 归纳类型（Inductive Types） 中看到这些策略（tactic）是相当通用的。cases（情况分析）策略（tactic）可以用于分解任何归纳定义类型的元素；constructor（构造）总是应用归纳定义类型的第一个可应用构造子（constructor）。例如，你可以将 cases（情况分析）和 constructor（构造）用于存在量词：

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x) → ∃ x, p x ∨ q x p:Nat → Propq:Nat → Proph:∃ x, p x⊢ ∃ x, p x ∨ q x cases h with p:Nat → Propq:Nat → Propx:Natpx:p x⊢ ∃ x, p x ∨ q x p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p ?intro.w ∨ q ?intro.wp:Nat → Propq:Nat → Propx:Natpx:p x⊢ Nat; p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p ?intro.wp:Nat → Propq:Nat → Propx:Natpx:p x⊢ Nat; All goals completed! 🐙

这里，constructor（构造）策略（tactic）将存在断言的第一部分，即 x 的值，保持为隐式。它由一个元变量表示，应该稍后实例化。在前面的例子中，元变量的正确值由策略（tactic）exact px 确定，因为 px 的类型是 p x。如果你想显式地指定存在量词的一个见证（witness），可以使用 exists 策略（tactic）：

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x) → ∃ x, p x ∨ q x p:Nat → Propq:Nat → Proph:∃ x, p x⊢ ∃ x, p x ∨ q x cases h with p:Nat → Propq:Nat → Propx:Natpx:p x⊢ ∃ x, p x ∨ q x p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p x ∨ q x; p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p x; All goals completed! 🐙

这里是另一个例子：

example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x p:Nat → Propq:Nat → Proph:∃ x, p x ∧ q x⊢ ∃ x, q x ∧ p x cases h with p:Nat → Propq:Nat → Propx:Nathpq:p x ∧ q x⊢ ∃ x, q x ∧ p x cases hpq with p:Nat → Propq:Nat → Propx:Nathp:p xhq:q x⊢ ∃ x, q x ∧ p x All goals completed! 🐙

这些策略（tactic）可以同样好地用于数据和命题。在下一个例子中，它们被用来定义交换积类型和和类型分量的函数：

def swap_pair : α × β → β × α := α:Type ?u.18β:Type ?u.17⊢ α × β → β × α α:Type ?u.18β:Type ?u.17p:α × β⊢ β × α α:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ β × α α:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ βα:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ α α:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ βα:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ α All goals completed! 🐙 def swap_sum : Sum α β → Sum β α := α:Type ?u.196β:Type ?u.195⊢ α ⊕ β → β ⊕ α α:Type ?u.196β:Type ?u.195p:α ⊕ β⊢ β ⊕ α α:Type ?u.196β:Type ?u.195val✝:α⊢ β ⊕ αα:Type ?u.196β:Type ?u.195val✝:β⊢ β ⊕ α α:Type ?u.196β:Type ?u.195val✝:α⊢ β ⊕ α α:Type ?u.196β:Type ?u.195val✝:α⊢ α; All goals completed! 🐙 α:Type ?u.196β:Type ?u.195val✝:β⊢ β ⊕ α α:Type ?u.196β:Type ?u.195val✝:β⊢ β; All goals completed! 🐙

注意，除了我们为变量选择的名称外，这些定义与合取和析取的类似命题的证明完全相同。cases（情况分析）策略（tactic）也可以对自然数进行情况区分：

open Nat example (P : Nat → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : Nat) : P m := P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succm:Nat⊢ P m cases m with P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succ⊢ P 0 All goals completed! 🐙 P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succm':Nat⊢ P (m' + 1) All goals completed! 🐙

cases（情况分析）策略（tactic）及其伴生策略（tactic）induction（归纳），在 归纳类型的策略（Tactics for Inductive Types） 一节中有更详细的讨论。

contradiction（矛盾）策略（tactic）在当前目标的假设中搜索矛盾：

example (p q : Prop) : p ∧ ¬ p → q := p:Propq:Prop⊢ p ∧ ¬p → q p:Propq:Proph:p ∧ ¬p⊢ q p:Propq:Propleft✝:pright✝:¬p⊢ q All goals completed! 🐙

你也可以在策略块中使用 match。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r match h with p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ p ∧ q; p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ q p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) match h with p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ r; All goals completed! 🐙

你可以将 intro（引入）与 match "结合"，并将前面的例子写成如下形式：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r intro p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q; p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ q p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ q All goals completed! 🐙 p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ r; p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) intro p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ r; All goals completed! 🐙

5.4. 结构化策略证明（Structuring Tactic Proofs）🔗

策略（tactic）通常提供了一种构建证明的有效方式，但长序列的指令可能掩盖论证的结构。在本节中，我们描述一些有助于为策略风格的证明提供结构的方法，使这类证明更易读且更健壮。

Lean 的证明编写语法的一个优点是可以混合项风格和策略风格的证明，并在这两者之间自由转换。例如，策略（tactic）apply（应用）和 exact（精确提供）期望任意项，你可以使用 have（拥有）、show（展示）等来编写这些项。反过来，在编写任意 Lean 项时，你总是可以通过插入一个 by 块来调用策略模式。下面是一个有些玩具性质的例子：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r exact have hp : p := h.left have hqr : q ∨ r := h.right show (p ∧ q) ∨ (p ∧ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Proph:p ∧ (q ∨ r)hp:p := h.lefthq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hp:p := h.lefthr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙

下面是一个更自然的例子：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) All goals completed! 🐙

事实上，还有一个 show（展示）策略（tactic），它类似于证明项中的 show 表达式。它只是声明将要求解的目标的类型，同时保持在策略模式中。

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) All goals completed! 🐙

show（展示）策略（tactic）实际上可以用于将目标重写为定义上等价的形式：

example (n : Nat) : n + 1 = Nat.succ n := n:Nat⊢ n + 1 = n.succ n:Nat⊢ n.succ = n.succ All goals completed! 🐙

还有一个 have（拥有）策略（tactic），它引入一个新的子目标，就像在编写证明项时一样：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qhpq:p ∧ q := ⟨hp, hq⟩⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qhpq:p ∧ q := ⟨hp, hq⟩⊢ p ∧ q All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rhpr:p ∧ r := ⟨hp, hr⟩⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rhpr:p ∧ r := ⟨hp, hr⟩⊢ p ∧ r All goals completed! 🐙

与证明项一样，你可以在 have（拥有）策略（tactic）中省略标签，此时会使用默认标签 this：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q := ⟨hp, hq⟩⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q := ⟨hp, hq⟩⊢ p ∧ q All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r := ⟨hp, hr⟩⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r := ⟨hp, hr⟩⊢ p ∧ r All goals completed! 🐙

have（拥有）策略（tactic）中的类型可以省略，所以你可以写 have hp := h.left 和 have hqr := h.right。事实上，使用这种记号，你甚至可以同时省略类型和标签，此时新的事实会以标签 this 引入：

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q := ⟨hp, hq⟩⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q := ⟨hp, hq⟩⊢ p ∧ q; All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r := ⟨hp, hr⟩⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r := ⟨hp, hr⟩⊢ p ∧ r; All goals completed! 🐙

Lean 还有一个 let（let）策略（tactic），它类似于 have（拥有）策略（tactic），但用于引入局部定义而不是辅助事实。它是证明项中 let 的策略对应物：

example : ∃ x, x + 2 = 8 := ⊢ ∃ x, x + 2 = 8 a:Nat := 3 * 2⊢ ∃ x, x + 2 = 8 All goals completed! 🐙

与 have（拥有）一样，你可以通过写 let a := 3 * 2 来隐式保留类型。let（let）和 have（拥有）的区别在于，let（let）在上下文中引入一个局部定义，因此局部声明的定义可以在证明中展开。

我们已经使用 . 来创建嵌套的策略块。在嵌套块中，Lean 聚焦于第一个目标，如果在块结束时它没有完全求解，则生成一个错误。这有助于指示由策略（tactic）引入的多个子目标的单独证明。记号 . 对空白敏感，并依靠缩进来检测策略块何时结束。或者，你可以使用花括号和分号来定义策略块：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ rp:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ r; All goals completed! 🐙 } p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r; All goals completed! 🐙 } } p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r)p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r); p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r); All goals completed! 🐙 } p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r); All goals completed! 🐙 } }

使用缩进来结构化证明是很有用的：每当一个策略（tactic）留下多个子目标时，我们通过将它们封闭在块中并缩进来分隔剩余的子目标。因此，如果定理 foo 应用于一个目标产生四个子目标，我们会期望证明看起来像这样：

  apply foo
  . <proof of first goal>
  . <proof of second goal>
  . <proof of third goal>
  . <proof of final goal>

或

  apply foo
  case <tag of first goal>  => <proof of first goal>
  case <tag of second goal> => <proof of second goal>
  case <tag of third goal>  => <proof of third goal>
  case <tag of final goal>  => <proof of final goal>

或

  apply foo
  { <proof of first goal>  }
  { <proof of second goal> }
  { <proof of third goal>  }
  { <proof of final goal>  }

5.5. 策略组合子（Tactic Combinators）🔗

策略组合子（Tactic combinator）是从已有策略（tactic）形成新策略（tactic）的操作。顺序组合子在 by 块中已经是隐式的：

example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q p:Propq:Prophp:p⊢ p; All goals completed! 🐙

这里，apply Or.inl; assumption 在功能上等价于一个先应用 apply Or.inl 然后应用 assumption（假定）的单个策略（tactic）。

在 t₁ <;> t₂ 中，<;> 操作符提供了顺序操作的并行版本：t₁ 应用于当前目标，然后 t₂ 应用于所有生成的子目标：

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q All goals completed! 🐙

当生成的目标可以以统一的方式完成，或者至少可以在所有目标上统一地取得进展时，这尤其有用。

first | t₁ | t₂ | ... | tₙ（首个）依次应用每个 tᵢ，直到其中一个成功，否则失败：

example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q first | p:Propq:Prophp:p⊢ p; All goals completed! 🐙 | apply Or.inr; assumption example (p q : Prop) (hq : q) : p ∨ q := p:Propq:Prophq:q⊢ p ∨ q first | p:Propq:Prophq:q⊢ p; p:Propq:Prophq:q⊢ p | p:Propq:Prophq:q⊢ q; All goals completed! 🐙

在第一个例子中，左分支成功，而在第二个例子中，右分支成功。在接下来的三个例子中，相同的复合策略（tactic）在每个情况下都成功：

example (p q r : Prop) (hp : p) : p ∨ q ∨ r := p:Propq:Propr:Prophp:p⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophp:p⊢ p; All goals completed! 🐙 | apply Or.inr | assumption) example (p q r : Prop) (hq : q) : p ∨ q ∨ r := p:Propq:Propr:Prophq:q⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophq:q⊢ q; All goals completed! 🐙 | p:Propq:Propr:Prophq:q⊢ q ∨ r | assumption) example (p q r : Prop) (hr : r) : p ∨ q ∨ r := p:Propq:Propr:Prophr:r⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophr:r⊢ r; p:Propq:Propr:Prophr:r⊢ q | p:Propq:Propr:Prophr:r⊢ r | All goals completed! 🐙)

该策略（tactic）首先尝试通过假定（assumption）来求解左侧的析取项；如果失败，则尝试聚焦于右侧的析取项；如果那也不奏效，则调用 assumption（假定）策略（tactic）。

毫无疑问，你现在已经注意到策略（tactic）可能会失败。实际上，正是"失败"状态导致 first（首个）组合子回溯并尝试下一个策略（tactic）。try（尝试）组合子构建一个总是成功的策略（tactic），尽管可能是以平凡的方式：try t 执行 t 并报告成功，即使 t 失败了。它等价于 first| t |skip，其中 skip 是一个什么都不做的策略（tactic）（并且成功地做到了）。在下一个例子中，第二个 constructor（构造）在右侧的合取项 q ∧ r 上成功（记住析取和合取是右结合的），但在第一个上失败。try（尝试）策略（tactic）确保了顺序组合的成功：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r (try p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r) p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r All goals completed! 🐙

小心：repeat (try t) 会永远循环下去，因为内部的策略（tactic）永远不会失败。

在证明中，通常有多个未完成的目标。并行顺序是安排单个策略（tactic）应用于多个目标的一种方式，但还有其它方式。例如，all_goals t（全部目标）将 t 应用于所有开放的目标：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r all_goals (try p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r) all_goals All goals completed! 🐙

在这种情况下，any_goals（任一目标）策略（tactic）提供了更健壮的解决方案。它类似于 all_goals（全部目标），但只要它的参数至少在其中一个目标上成功时，它就算成功：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r any_goals p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r any_goals All goals completed! 🐙

下面 by 块中的第一个策略（tactic）反复拆分合取：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ ((p ∧ q) ∧ r) ∧ q ∧ r ∧ p repeat (any_goals p:Propq:Propr:Prophp:phq:qhr:r⊢ p) all_goals All goals completed! 🐙

事实上，我们可以将整个策略（tactic）压缩到一行：

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ ((p ∧ q) ∧ r) ∧ q ∧ r ∧ p repeat (any_goals (first | p:Propq:Propr:Prophp:phq:qhr:r⊢ p | All goals completed! 🐙))

组合子 focus t（聚焦）确保 t 只作用于当前目标，临时将其他目标从作用域中隐藏。因此，如果 t 通常只作用于当前目标，那么 focus (all_goals t) 与 t 有相同的效果。

5.6. 重写（Rewriting）🔗

rw（重写）策略（tactic）和 simp（化简）策略（tactic）在 计算证明（Calculational Proofs） 中简要介绍过。在本节和下一节中，我们将更详细地讨论它们。

rw（重写）策略（tactic）提供了一种将代入应用于目标和假设的基本机制，提供了一种方便且高效的处理等式的方式。该策略（tactic）最基本的形式是 rw [t]，其中 t 是一个项，其类型断言了一个等式。例如，t 可以是上下文中的假设 h : x = y；可以是一个通用引理，如 add_comm : ∀ x y, x + y = y + x，此时重写策略（tactic）会尝试找到 x 和 y 的合适实例；或者可以是任何断言具体或通用等式的复合项。在下面的例子中，我们使用这种基本形式通过一个假设来重写目标。

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f 0 = 0 -- replace k with 0 All goals completed! 🐙 -- replace f 0 with 0

在上面的例子中，第一次使用 rw（重写）将目标 f k = 0 中的 k 替换为 0。然后，第二次替换将 f 0 替换为 0。该策略（tactic）会自动关闭任何形式为 t = t 的目标。下面是一个使用复合表达式进行重写的例子：

example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y) (h' : p y) (hq : q) : p x := x:Naty:Natp:Nat → Propq:Proph:q → x = yh':p yhq:q⊢ p x x:Naty:Natp:Nat → Propq:Proph:q → x = yh':p yhq:q⊢ p y; All goals completed! 🐙

这里，h hq 建立了等式 x = y。

多个重写可以用记号 rw [t_1, ..., t_n] 组合，这不过是 rw[t_1]; ...;rw [t_n] 的简写。前面的例子可以写成如下形式：

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

默认情况下，rw（重写）沿着正向使用等式，将左侧与表达式匹配，并将其替换为右侧。记号 ←t 可用于指示策略（tactic）沿反向使用等式 t。

variable (a b : Nat) (f : Nat → Nat) example (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := a:Natb:Natf:Nat → Nath₁:a = bh₂:f a = 0⊢ f b = 0 All goals completed! 🐙

在这个例子中，项 ←h₁ 指示重写器将 b 替换为 a。在编辑器中，你可以输入反向箭头为 \l。你也可以使用 ASCII 等价形式 <-。

有时一个等式的左侧可能在模式中匹配到多个子项，此时 rw（重写）策略（tactic）会选择在遍历项时找到的第一个匹配。如果那不是你想要的，你可以使用额外的参数来指定适当的子项。

example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙 example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙 example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙

在上面的第一个例子中，第一步将 a + b + c 重写为 a + (b + c)。下一步对 b + c 应用交换律；如果不指定参数，该策略（tactic）会转而将 a + (b + c) 重写为 (b + c) + a。最后一步沿反向应用结合律，将 a + (c + b) 重写为 a + c + b。接下来的两个例子则在两边应用结合律将括号移到右边，然后交换 b 和 c。注意最后一个例子通过指定 Nat.add_comm 的第二个参数来指明重写应该在右侧进行。

默认情况下，rw（重写）策略（tactic）只影响目标。记号 rw [t] at h 将重写应用于

example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := f:Nat → Nata:Nath:a + 0 = 0⊢ f a = f 0 f:Nat → Nata:Nath:a = 0⊢ f a = f 0 All goals completed! 🐙

第一步，rw [Nat.add_zero] at h，将假设 a + 0 = 0 重写为 a = 0。然后新的假设 a = 0 用于将目标重写为 f 0 = f 0。

rw（重写）策略（tactic）不限于命题。在下面的例子中，我们使用 rw [h] at t 将假设 t : Tuple α n 重写为 t : Tuple α 0。

def Tuple (α : Type) (n : Nat) := { as : List α // as.length = n } example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := α:Typen:Nath:n = 0t:Tuple α n⊢ Tuple α 0 α:Typen:Nath:n = 0t:Tuple α 0⊢ Tuple α 0 All goals completed! 🐙

5.7. 使用化简器（Using the Simplifier）🔗

如果说 rw（重写）被设计为一种操控目标的手术工具，那么化简器（simplifier）则提供了更强大的自动化形式。Lean 库中的许多等式已经被标记了 [simp] 属性，simp（化简）策略（tactic）使用它们来迭代地重写表达式中的子项。

example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := x:Naty:Natz:Nat⊢ (x + 0) * (0 + y * 1 + z * 0) = x * y All goals completed! 🐙 example (x y z : Nat) (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p ((x + 0) * (0 + y * 1 + z * 0)) x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p (x * y); All goals completed! 🐙

在第一个例子中，目标中等号左侧使用常见的涉及 0 和 1 的恒等式进行化简，将目标简化为 x * y = x * y。此时，simp（化简）应用自反性来完成它。在第二个例子中，simp（化简）将目标简化为 p (x * y)，此时假设 h 完成它。下面是一些关于列表的例子：

open List example (xs : List Nat) : reverse (xs ++ [1, 2, 3]) = [3, 2, 1] ++ reverse xs := xs:List Nat⊢ (xs ++ [1, 2, 3]).reverse = [3, 2, 1] ++ xs.reverse All goals completed! 🐙 example (xs ys : List α) : length (reverse (xs ++ ys)) = length xs + length ys := α:Type u_1xs:List αys:List α⊢ (xs ++ ys).reverse.length = xs.length + ys.length All goals completed! 🐙

与 rw（重写）一样，你可以使用关键字 at 来化简一个假设：

example (x y z : Nat) (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := x:Naty:Natz:Natp:Nat → Proph:p ((x + 0) * (0 + y * 1 + z * 0))⊢ p (x * y) x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p (x * y); All goals completed! 🐙

此外，你可以使用"通配符"星号来化简所有假设和目标：

attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * w * z + y * x) w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + w * (x * z))⊢ p (x * y + w * (x * z)); All goals completed! 🐙 example (x y z : Nat) (p : Nat → Prop) (h₁ : p (1 * x + y)) (h₂ : p (x * z * 1)) : p (y + 0 + x) ∧ p (z * x) := x:Naty:Natz:Natp:Nat → Proph₁:p (1 * x + y)h₂:p (x * z * 1)⊢ p (y + 0 + x) ∧ p (z * x) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y) ∧ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y) ∧ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y)x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y)x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x * z) All goals completed! 🐙

对于像自然数上乘法这样可交换且可结合的操作，化简器使用这两个事实以及左交换律来重写表达式。在乘法的情况下，左交换律的表达如下：x * (y * z) = y * (x * z)。local 修饰符告诉化简器在当前文件（或 section，或 namespace，视情况而定）中使用这些规则。交换律和左交换律似乎存在问题，因为反复应用任一法则都会导致循环。但化简器能够检测到对其参数进行置换的等式，并使用一种称为有序重写的技术。这意味着系统维护一个项的内部顺序，并且只在这样做会降低顺序时才应用该等式。有了上述三个等式，所有表达式中的括号都关联到右侧，并且表达式按某种规范（虽然有些任意）的方式排序。这样，在结合律和交换律下等价的表达式会被重写为相同的规范形式。

example (w x y z : Nat) (unused variable `p` Note: This linter can be disabled with `set_option linter.unusedVariables false`p : Nat → Prop) : x * y + z * w * x = x * w * z + y * x := w:Natx:Naty:Natz:Natp:Nat → Prop⊢ x * y + z * w * x = x * w * z + y * x All goals completed! 🐙 example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * w * z + y * x) w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * y + w * (x * z)); w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + w * (x * z))⊢ p (x * y + w * (x * z)); All goals completed! 🐙

与 rw（重写）一样，你可以向 simp（化简）提供一组要使用的事实，包括通用引理、局部假设、要展开的定义和复合表达式。simp（化简）策略（tactic）也识别 ←t 语法，就像 rewrite（重写）所做的那样。无论如何，额外的规则会被添加到用于化简项的等式集合中。

def f (m n : Nat) : Nat := m + n + m example {m n : Nat} (h : n = 1) (h' : 0 = m) : (f m n) = n := m:Natn:Nath:n = 1h':0 = m⊢ f m n = n All goals completed! 🐙

一个常见的用法是使用局部假设来化简目标：

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

要在化简时使用局部上下文中存在的所有假设，我们可以使用通配符 *：

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

这是另一个例子：

example (u w x y z : Nat) (h₁ : x = y + z) (h₂ : w = u + x) : w = z + y + u := u:Natw:Natx:Naty:Natz:Nath₁:x = y + zh₂:w = u + x⊢ w = z + y + u All goals completed! 🐙

化简器也会进行命题重写。例如，使用假设 p，它将 p ∧ q 重写为 q，将 p ∨ q 重写为 True，然后平凡地证明它。迭代这样的重写可以产生不平凡的命题推理。

example (p q : Prop) (hp : p) : p ∧ q ↔ q := p:Propq:Prophp:p⊢ p ∧ q ↔ q All goals completed! 🐙 example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q All goals completed! 🐙 example (p q r : Prop) (hp : p) (hq : q) : p ∧ (q ∨ r) := p:Propq:Propr:Prophp:phq:q⊢ p ∧ (q ∨ r) All goals completed! 🐙

下一个例子化简所有假设，然后使用它们来证明目标。

example (u w x x' y y' z : Nat) (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y') : x + y + 0 = x' + y' := u:Natw:Natx:Natx':Naty:Naty':Natz:Natp:Nat → Proph₁:x + 0 = x'h₂:y + 0 = y'⊢ x + y + 0 = x' + y' u:Natw:Natx:Natx':Naty:Naty':Natz:Natp:Nat → Proph₁:x = x'h₂:y = y'⊢ x + y = x' + y' All goals completed! 🐙

使得化简器特别有用的一个方面是，它的能力可以随着库的发展而增长。例如，假设我们定义了一个列表操作，通过追加其反转来对称化输入：

def mk_symm (xs : List α) := xs ++ xs.reverse

那么对于任何列表 xs，(mk_symm xs).reverse 等于 mk_symm xs，这可以通过展开定义来轻松证明：

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙

我们现在可以使用这个定理来证明新的结果：

example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

但使用 reverse_mk_symm 通常是正确的做法，如果用户不必显式调用它就太好了。你可以在定义定理时将其标记为化简规则来实现这一点：

@[simp] theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

记号 @[simp] 声明 reverse_mk_symm 具有 [simp] 属性，也可以更明确地写成：

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 attribute [simp] reverse_mk_symm example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

该属性也可以在定理声明之后的任何时间应用：

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 attribute [simp] reverse_mk_symm example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

但是，一旦属性被应用，就没有办法永久移除它；它会持续存在于任何导入分配了该属性的文件的文件中。正如我们将在 属性（Attributes） 中进一步讨论的，你可以使用 local 修饰符将属性的作用域限制在当前文件或 section 中：

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 section attribute [local simp] reverse_mk_symm example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙 end

在 section 外部，化简器默认将不再使用 reverse_mk_symm。

注意，我们讨论过的各种 simp（化简）选项——给出显式的规则列表，以及使用 at 指定位置——可以组合使用，但它们的列出顺序是固定的。你可以通过在编辑器中把光标放在 simp 标识符上来查看与之关联的文档字符串，以了解正确的顺序。

还有两个有用的修饰符。默认情况下，simp（化简）包含所有已被标记了 [simp] 属性的定理。写 simp only 排除这些默认规则，允许你使用更显式地编写的规则列表。在下面的例子中，减号和 only 用于阻止应用 reverse_mk_symm。

def mk_symm (xs : List α) := xs ++ xs.reverse @[simp] theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p ((mk_symm ys).reverse ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p ((mk_symm ys).reverse ++ xs.reverse)⊢ p ((mk_symm ys).reverse ++ xs.reverse); All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p ((mk_symm ys).reverse ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p ((mk_symm ys).reverse ++ xs.reverse)⊢ p ((mk_symm ys).reverse ++ xs.reverse); All goals completed! 🐙

simp（化简）策略（tactic）有许多配置选项。例如，我们可以如下启用上下文化简：

example : if x = 0 then y + x = y else x ≠ 0 := x:Naty:Nat⊢ if x = 0 then y + x = y else x ≠ 0 All goals completed! 🐙

使用 +contextual（上下文），simp（化简）策略（tactic）在化简 y + x 时会利用 x = 0 这一事实，并在化简另一个分支时利用 x ≠ 0。这是另一个例子：

example : ∀ (x : Nat) (unused variable `h` Note: This linter can be disabled with `set_option linter.unusedVariables false`h : x = 0), y + x = y := y:Nat⊢ ∀ (x : Nat), x = 0 → y + x = y All goals completed! 🐙

另一个有用的配置选项是 +arith，它启用算术化简。

example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := x:Naty:Nat⊢ 0 < 1 + x ∧ x + y + 2 ≥ y + 1 All goals completed! 🐙

5.8. 分裂策略（Split Tactic）🔗

split（分裂）策略（tactic）对于将嵌套的 if-then-else 和 match 表达式分解为各种情况很有用。对于一个具有 n 种情况的 match 表达式，split（分裂）策略（tactic）最多产生 n 个子目标。这里有一个例子：

def f (x y z : Nat) : Nat := match x, y, z with | 5, _, _ => y | _, 5, _ => y | _, _, 5 => y | _, _, _ => 1 example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := w:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1 All goals completed! 🐙 w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1 All goals completed! 🐙 x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1 All goals completed! 🐙 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 All goals completed! 🐙

我们可以将上面的策略证明压缩如下。

example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := w:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1; w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1; w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 first | w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 | All goals completed! 🐙

策略（tactic）split <;> first | contradiction | rfl 首先应用 split（分裂）策略（tactic），然后对生成的每个目标依次尝试 contradiction（矛盾），如果 contradiction（矛盾）失败则尝试 rfl（自反性）。与 simp（化简）一样，我们可以将 split（分裂）应用于特定的假设：

def g (xs ys : List Nat) : Nat := match xs, ys with | [a, b], _ => a+b+1 | _, [b, _] => b+1 | _, _ => 1 example (xs ys : List Nat) (h : g xs ys = 0) : False := xs:List Natys:List Nath:g xs ys = 0⊢ False xs:List Natys:List Nath:(match xs, ys with | [a, b], x => a + b + 1 | x, [b, head] => b + 1 | x, x_1 => 1) = 0⊢ False; ys:List Natxs✝:List Natys✝:List Nata✝:Natb✝:Nath:a✝ + b✝ + 1 = 0⊢ Falsexs:List Natxs✝:List Natys✝:List Natb✝:Nathead✝:Natx✝:∀ (a b : Nat), xs = [a, b] → Falseh:b✝ + 1 = 0⊢ Falsexs:List Natys:List Natxs✝:List Natys✝:List Natx✝¹:∀ (a b : Nat), xs = [a, b] → Falsex✝:∀ (b head : Nat), ys = [b, head] → Falseh:1 = 0⊢ False ys:List Natxs✝:List Natys✝:List Nata✝:Natb✝:Nath:a✝ + b✝ + 1 = 0⊢ Falsexs:List Natxs✝:List Natys✝:List Natb✝:Nathead✝:Natx✝:∀ (a b : Nat), xs = [a, b] → Falseh:b✝ + 1 = 0⊢ Falsexs:List Natys:List Natxs✝:List Natys✝:List Natx✝¹:∀ (a b : Nat), xs = [a, b] → Falsex✝:∀ (b head : Nat), ys = [b, head] → Falseh:1 = 0⊢ False All goals completed! 🐙

5.9. 可扩展策略（Extensible Tactics）🔗

在下面的例子中，我们使用指令 syntax 定义记号 triv。然后，我们使用指令 macro_rules 来指定当使用 triv 时应执行的操作。你可以提供不同的展开，策略解释器会尝试所有展开，直到其中一个成功：

-- Define a new tactic notation syntax "triv" : tactic macro_rules | `(tactic| triv) => `(tactic| assumption) example (h : p) : p := p:Sort ?u.2129h:p⊢ p All goals completed! 🐙 -- You cannot prove the following theorem using `triv` -- example (x : α) : x = x := by -- triv -- Let's extend `triv`. The tactic interpreter -- tries all possible macro extensions for `triv` until one succeeds macro_rules | `(tactic| triv) => `(tactic| rfl) example (x : α) : x = x := α:Sort u_1x:α⊢ x = x All goals completed! 🐙 example (x : α) (h : p) : x = x ∧ p := α:Sort u_1p:Propx:αh:p⊢ x = x ∧ p α:Sort u_1p:Propx:αh:p⊢ x = xα:Sort u_1p:Propx:αh:p⊢ p α:Sort u_1p:Propx:αh:p⊢ x = xα:Sort u_1p:Propx:αh:p⊢ p All goals completed! 🐙 -- We now add a (recursive) extension macro_rules | `(tactic| triv) => `(tactic| apply And.intro <;> triv) example (x : α) (h : p) : x = x ∧ p := α:Sort u_1p:Propx:αh:p⊢ x = x ∧ p All goals completed! 🐙

5.10. 练习（Exercises）

  1. 回到 命题与证明（Propositions and Proofs） 和 量词与等式（Quantifiers and Equality） 中的练习，现在尽可能多地用策略证明重新做一遍，并适当使用 rw（重写）和 simp（化简）。

  2. 使用策略组合子来获得以下命题的一行证明：

declaration uses 'sorry'example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := p:Propq:Propr:Prophp:p⊢ (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) All goals completed! 🐙