5.1. 进入策略模式🔗

从概念上讲，陈述一个定理或引入一个 have 声明会产生一个目标， 即构造一个具有预期类型的项的目标。例如，下面创建的目标是构建一个类型为 p ∧ q ∧ p 的项， 上下文中有常量 p q : Prop，hp : p 和 hq : q：

写成目标如下：

事实上，如果你把上面的例子中的“sorry”换成下划线，Lean 会报告说，正是这个目标没有得到解决。

通常情况下，你会通过写一个明确的项来满足这样的目标。但在任何需要项的地方， Lean 允许我们插入一个 by <tactics> 块，其中 <tactics> 是一串命令， 用分号或换行符分开。你可以用下面这种方式来证明上面的定理：

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

apply 策略应用于一个表达式，被视为表示一个有零或多个参数的函数。 它将结论与当前目标中的表达式统一起来，并为剩余的参数创建新的目标， 只要后面的参数不依赖于它们。在上面的例子中，命令 apply And.intro 产生了两个子目标：

第一个目标是通过命令 exact hp 来实现的。exact 命令只是 apply 的一个变体， 它表示所给的表达式应该准确地填充目标。在策略证明中使用它很有益，因为它如果失败那么表明出了问题。 它也比 apply 更稳健，因为繁饰器在处理被应用的表达式时，会考虑到目标所预期的类型。 然而，在这种情况下，apply 也可以很好地工作。

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

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), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

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

可能产生多个子目标的策略通常对子目标进行标记。例如，策略 apply And.intro 将第一个子目标标记为 leftleftp:Propq:Prophp:phq:q⊢ p，将第二个标记为 rightrightp:Propq:Prophp:phq:q⊢ q ∧ p。在 apply 策略的情况下， 标签是从 And.intro 声明中使用的参数名称推断出来的。你可以使用符号 case <tag> => <tactics> 来结构化你的策略。下面是本章中第一个策略证明的结构化版本。

使用 case 标记，你也可以在 leftleftp:Propq:Prophp:phq:q⊢ p 之前先解决子目标 rightrightp:Propq:Prophp:phq:q⊢ q ∧ p：

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

我们说 case 是“专注”于选定的目标。 此外，如果所选目标在 case 块的末尾没有完全解决， Lean 会标记一个错误。

对于简单的子目标，可能不值得使用其标签来选择一个子目标，但你可能仍然想要结构化证明。 Lean 还提供了“子弹”符号 . <tactics>（或 · <tactics>）来结构化证明：

5.2. 基本策略🔗

除了 apply 和 exact 之外，另一个有用的策略是 intro， 它引入了一个假设。下面是我们在前一章中证明的命题逻辑中的一个等价性的例子，现在用策略来证明。

intro 命令可以更普遍地用于引入任何类型的变量：

你可以同时引入好几个变量：