本章我们将描述另一种构建证明的方法， 即策略 Tactic。 每个证明项 proof term 都代表一个数学证明，而 策略则是描述如何构建证明的命令或指令。 非正式地说，你可以以下述语句开始一段数学证明： “为了证明条件的必要性，需要 展开定义 应用前面的定理 并进行简化。” 正如这些指令会告诉读者该如何重建证明， 策略也是一系列指令，它们会告诉 Lean 该如何构建证明。 它们自然支持增量式书写证明， 在这种写作方式中，你将分解一个证明 并一步步地实现目标。
由策略序列构成的证明将被称作“策略风格 Tactic-Style”证明， 以此区别于之前介绍的证明项 proof term 写法， 即“项风格 Term-Style”证明。 每种风格都有优缺点，比如： 策略风格证明可能更难阅读，因为这需要读者预测或猜测每条指令的结果， 但它们通常更简短且更容易书写。 此外策略为使用 Lean 的自动化提供了一条途径，因为自动化过程本身就是策略。
5.1. 进入策略模式 Entering Tactic Mode
从概念上讲，陈述一个定理或引入一个 have 声明都会产生一个目标，
即构造一个具有预期类型的项。例如下面创建的目标便是
在带有常量
p q : Prop，
hp : p 和
hq : q 的语境中
构建一个类型为 p ∧ q ∧ p 的项：
| |
目标如下：
| |
事实上，如果你把上面的例子中的“sorry”换成下划线，
Lean 会报告说这就是未解决的目标。
通常情况下我们可以通过构造一个明确的项来满足这样的目标，
但在任何需要项的地方 Lean 都允许我们插入一个 by <tactics> 块——
其中 <tactics> 是一串命令，用分号或换行符分开。
因此你可以用下面这种方式来证明上面的定理：
| |
我们经常会
把关键字 by放在前一行并
把上面的例子写成如下形式：
| |
apply 策略
会应用一个表达式，后者可被视为一个接受零或多个参数的函数。
apply 会将结论与当前目标中的表达式统一起来，并
为剩余的参数创建新的目标，前提是后面的参数不会依赖于它们。
在上面的例子中，命令 apply And.intro 会产生两个子目标：
| |
| |
第一个目标是通过命令 exact hp 来实现的。
exact 命令只是 apply 的一个变体，它表示
所给的表达式应该准确地填充目标。
它在策略风格证明中会很有益，
因为一旦它失败就意味着有问题。
它也比 apply 更稳健，
因为繁饰器在处理被应用的表达式时
会考虑到目标所预期的类型——
尽管 apply 在这种情况下也可以很好地工作。
你可以用 #print 命令查看所产生的证明项：
| |
你可以循序渐进地写一个策略脚本。在 VS Code 中可以通过按
Ctrl + Shift + Enter 打开一个窗口来显示信息，并且
只要光标在策略块中当前目标就会在该窗口中显示。如果证明是不完整的，
标记 by 会被装饰成一条红色的波浪线，错误信息中会指明剩余的目标。
策略命令不仅能接受单一标识符，还可以接受复合表达式。 下面是前面的证明的一个简短版本：
| |
毫不意外它生成了完全相同的证明项：
| |
| |
如果策略可能产生多个子目标，
那么它们通常会对子目标进行标记。
例如，策略 apply And.intro
将第一个子目标标记为 left 并
将第二个子目标标记为 right。
对于 apply 策略，
标签是从 And.intro 声明中使用的参数名称推断出来的。
你可以使用符号 case <tag> => <tactics>来结构化你的策略。
下面是本章中第一个策略证明的结构化版本。
| |
在 case 语句中你也可以
在解决子目标 left 之前
先解决子目标 right：
| |
注意到 Lean 会在 case 区块中隐藏其他的目标。
在 case left => 后我们的证明状态会变成
| |
可见 case 会“专注于”选定的目标；此外
如果所选目标在 case 区块的末尾仍未解决，
那么 Lean 便会标记一个错误。
简单的子目标完全没必要用标签去选择，
但你可能仍想要对证明进行结构化。
Lean 还提供了“子弹”符号 . <tactics>（或 · <tactics>）
来重构证明：
| |
5.2. 基本策略 Basic Tactics
除 apply 和 exact 之外还有一个有用的策略 intro：
它用于引入一个假设。下面是我们在第 3 章中证明的命题逻辑中的一个等价性的例子，现在换用策略来证明：
| |
intro 命令还可以推广到任意类型的变量：
| |
你甚至可以一次性引入多个变量：
| |
正如
apply 策略用于交互式地构造函数应用，
intro 策略用于交互式地构造函数抽象。
（即形如 fun x => e 的项）。
正如
Lambda 抽象符号允许我们使用隐式的模式匹配
一样，
intro 策略也允许我们使用隐式的模式匹配。
| |
也可以像 match 表达式那样提供多个选项。
| |
intros 策略
可以在没有任何参数的情况下使用，
在此情况下它会选择名字并尽可能多地引入变量。
稍后你会看到一个例子。
assumption 策略
会在当前目标对应的语境下查看假设：
如果存在与结论匹配的假设，
那么它就会被 assumption 应用。
| |
若有必要它会在结论中统一元变量：
| |
下面的例子使用 intros 命令来自动引入三个变量和两个假设：
| |
注意 Lean 自动生成的名称在默认情况下是不可访问的。
这么做的动机是确保你的策略证明
不依赖于自动生成的名字并
因此而更加稳健；
然而你可以使用组合器
unhygienic 来禁用这一限制。
| |
你也可以使用 rename_i 策略
来重命名所处语境中最近的几个无法访问的名字。
策略 rename_i h1 _ h2 会重命名语境中最近的三个假设中的两个：
| |
rfl 策略
会解决那些形如自反关系应用在定义相等的参数的目标。
等号就是自反的：
| |
| |
还有一个很有用的策略是 revert 策略。
从某种意义上说，它是对 intro 的逆：
| |
revert x 后证明状态变成
| |
intro y 后则会变成
| |
将一个假设还原到目标中会产生一个蕴含：
| |
revert h 后证明状态变成
| |
intro h₁ 之后则变成
| |
但是 revert 更聪明，因为它
不仅会还原语境中的一个元素，
且还会还原语境中所有依赖它的后续元素。
例如在上面的例子中，还原 x 会带来 h。
| |
revert x 后证明状态变成
| |
你还可以一次性还原多个元素：
| |
revert x y 之后证明状态变成
| |
你只能 revert 局部语境中的一个元素，也就是一个局部变量或假设；不过
你可以通过 generalize 策略
将目标中的任意表达式替换为新的变量：
| |
特别地，在 generalize 之后，证明状态变成
| |
上述符号的记忆法是，你通过将 3 设定为任意变量 x 来泛化目标。
注意并不是所有泛化都能保留目标的有效性：这里
generalize 将一个可以用 rfl 证明的目标
替换为了一个无法被证明的目标：
| |
在这个例子中 sorry 策略是 sorry 证明项的类似物。
它结束当前的目标并警告 sorry 被使用。
为保持之前目标的有效性，generalize 策略允许我们记录“3 已经被 x 所取代”的事实。
你所要做的就是提供一个标签，这样 generalize 会用它来存储局部语境中的赋值：
| |
在 generalize h : 3 = x 之后，h 是 3 = x 的证明：
| |
这里重写策略 rw 使用 h 再次将 x 替换为 3。
rw 策略下文将继续讨论。
5.3. 更多策略 More Tactics
一些额外的策略会对建构和解构命题/数据很有用。例如
在处理形为 p ∨ q 的证明目标时，我们可以使用 apply Or.inl 和 apply Or.inr 等策略；
但是 cases 策略可以用来解构一个析取：
| |
注意到其语法与 match 表达式中使用的语法类似。
新的子目标可按任何顺序解决：
| |
你也可以使用一个不带有 with 的（非结构化的）cases
并为每个备选情况制定一个策略：
| |
如果可以用同一个策略来解决子任务，
那么（非结构化的）cases 会非常有用：
| |
你也可以使用组合器 tac1 <;> tac2
将 tac2 应用于策略 tac1 产生的每个子目标：
| |
你还可以结合 . 符号
使用非结构化的 cases 策略：
| |
cases 策略也可以被用来分解一个合取：
| |
在这个例子中，应用 cases 策略后目标只剩下一个，伴随着
h : p ∧ q 被一对假设 hp : p 和 hq : q 所取代：
| |
constructor 策略
应用了合取的唯一一个构造子 And.intro。
有了这些策略，上一节的一个例子便可改写为如下：
| |
在归纳类型一章中你将看到这些策略是相当通用的：
cases 策略可用来解构递归定义类型下的任何元素，而
constructor 策略总会应用递归定义类型第一个适用的构造子。例如，
你可以将 cases 和 constructor 与一个存在量词一起使用：
| |
这里 constructor 策略将存在性命题的第一个组成部分（即 x 的值）保留为隐式的。
它由一个元变量表示，这个元变量未来会被实例化。在前面的例子中，
元变量的正确值是由策略 exact px 决定的，因为 px 的类型是 p x。
如果想明确指定存在量词的存在者，那么可以使用exists 策略：
| |
另一个例子如下：
| |
这些策略既能用于命题也能用于数据类型。 在下面的两个例子中，它们被用来定义类型加乘法的交换子：
| |
注意到：不考虑我们为变量分配的名字，上述两条定义完全等同于合取析取交换律单侧方向的证明。
cases 策略也会对自然数进行逐情况区分：
| |
cases 策略及其同伴 induction 策略将在归纳类型的策略一节中详细介绍。
contradiction 策略
则搜索当前目标的假设中的矛盾：
| |
你也可以在策略块中使用 match：
| |
你还可以将 intro 与 match 结合起来，
然后上例就可以写成如下形式：
| |
5.4. 结构化策略证明 Structuring Tactic Proofs
策略通常能提供构建证明的有效方法，但一长串指令会掩盖论证的结构。 本节我们将描述一些有助于为策略式证明提供结构的方法， 以让证明变得更易读且更稳健
Lean 的证明写作语法的一个优点是
它可以混合项风格和策略风格证明，并在两者之间自由转换。例如，
策略 apply 和 exact 允许传入任意的项，
这些项你可以用 have，show 等来写。反之，
在写一个任意的 Lean 项时，你总是可以通过插入一个 by 块来启用策略模式。
下面是一个简单的例子：
| |
更自然一点
| |
事实上确实存在一个 show 策略，类似于证明项中的 show 表达式。
它只会简单地声明即将被解决的目标的类型并保持策略模式。
| |
show 策略其实可以被用来重写一些定义等价的目标：
| |
此外还有 have 策略，它会引入一个新的子目标，就像写证明项时一样：
| |
与证明项一样，你也可以省略 have 策略中的标签，
这种情况下将会使用默认标签 this：
| |
由于 have 策略中的类型可以省略，所以你可以写
have hp := h.left 和
have hqr := h.right。事实上，利用这种符号
你甚至还可以同时省略类型和标签，此时新的事实需要通过标签 this 引入：
| |
Lean 还有一个 let 策略，它类似于 have 策略，
但用于引入局部定义而非辅助事实。它是策略风格对证明项中的 let 的模拟：
| |
与 have 一样，你可以通过写 let a := 3 * 2 来让类型变成隐式的。
let 和 have 的区别在于 let 在语境中引入了一个局部定义，
这样局部声明的定义就可以在证明中展开。
我们已用 . 创建过嵌套的策略块。在嵌套块中，Lean 会聚焦于第一个目标：
如果该目标在块结束时还没有被完全解决，就会产生一个错误。
这有助于指示由一个策略引入的多个子目标的独立证明。
符号 . 是空格敏感的，其依靠缩进来检测策略块是否结束。
或者你也可以用花括号和分号来定义策略块：
| |
使用缩进来排版证明是很有用的：
每当一个策略留下一个以上的子目标时，
我们就通过将剩余的子目标封闭在块中并缩进来分离它们。因此，
假如定理 foo 被应用到一个单一的目标后产生了四个子目标，
那么证明看起来可能会像这样：
| |
或者像这样
| |
或者像这样
| |
5.5. 策略组合子 Tactic Combinators
策略组合子 Tactic combinator
是从旧策略形成新策略的操作。by 块中已经隐含了一个顺序组合子：
| |
这里 apply Or.inl; assumption 在功能上等同于一个单一的策略：它
首先应用 apply Or.inl，
然后应用 assumption。
在 t₁ <;> t₂ 中，<;> 操作符提供了顺序操作的一个并行版本：
首先 t₁ 被应用于当前的目标，
然后 t₂ 被应用于所有生成的子目标：
| |
这 在产生的目标可以统一方式完成——或者至少是 能在所有目标上统一取得进展时会特别有用。
first | t₁ | t₂ | ... | tₙ 会应用每个 tᵢ
直到其中一个成功，否则失败：
| |
在第一个例子中，左边的分支成功了，而 在第二个例子中，右边的分支成功了。 在接下来的三个例子中，同样的复合策略在每种情况下都成功了：
| |
该策略尝试立即通过 assumption 解决左边的析取项；
如果失败了，它尝试聚焦于右边的析取项；
如果这也不起作用，就会调用 assumption 策略。
毫无疑问，你现在已经注意到策略会失败。事实上，
正是“失败”状态导致了 first 组合子回溯并尝试下一个策略。
try 组合子建立了一个总是成功的策略，尽管可能是以一种平凡的方式：
try t 执行 t 并报告成功，即使 t 失败。它等同于 first | t | skip，
其中 skip 是一个什么都不做的策略（并且成功地做到了）。在下一个例子中，第二个 constructor
在右边的合取项 q ∧ r 上成功了（记住析取和合取是向右结合的），但
在第一个合取项上失败了。
try 策略确保了顺序组合的成功：
| |
小心：repeat (try t) 将永远循环下去，
因为内部策略永远不会失败。
证明中经常会有多个未完成的目标。
并行顺序只是安排将单一策略应用于多个目标的一种方式，还有其他方式也可以做到这一点。例如，
all_goals t 将 t 应用于所有开启的目标：
| |
在这种情况下，any_goals 策略提供了一个更稳健的解决方案。
它类似于 all_goals，只是如果它的参数在至少一个目标上成功，它就成功：
| |
下方 by 块中的第一个策略会重复地拆分合取项：
| |
事实上我们完全可以把完整的策略压缩成一行：
| |
组合子 focus t 则确保 t 只影响当前的目标，
并将其他目标暂时从作用域中隐藏。因此
如果 t 通常只影响当前的目标，
那么 focus (all_goals t) 与 t 有同样的效果。
5.6. 重写 Rewriting
rw 策略和 simp 策略在计算式证明一节中有简要介绍过。
我们将在本节和下一节中更详细地讨论它们。
rw 策略
提供了一个对目标和假设应用等号代换性的基本机制，
允许我们以一种方便和有效的方法来处理等式。
该策略最基本的形式是 rw [t]，其中 t 是一个类型为等式的项。例如 t
可以是上下文中的一个假设，如 h : x = y；t 也
可以是一个具有普适性的引理，如 add_comm : ∀ x y, x + y = y + x——其中
重写策略试图找到 x 和 y 的合适实例；或者 t 也
可以是任何断言具体或普适性定理的复合项。
在下面的例子我们将使用这种基本形式，利用一个假设来重写目标。
| |
在上面的例子中，
第一次使用 rw 会将目标 f k = 0 中的 k 替换为 0。然后，
第二次使用 rw 会将目标 f 0 替换为 0。
该策略会自动解决任何形如 t = t 的目标。
下面是一个使用复合表达式重写的例子：
| |
这里 h hq 构建了等式 x = y。
多个重写的组合可以通过 rw [t_1, ..., t_n] 实现，
这不过是 rw[t_1]; ...; rw [t_n] 的简写；
因此前面的例子可以写成如下形式：
| |
默认情况下 rw 将正向套用等式 —— 即
先将等号左侧与一个表达式进行匹配，再用等号右侧进行替换。
←t 符号可用来指示 rw 策略反向套用等式 t。
| |
在这个例子中，项 ←h₁ 指示重写器将 b 替换为 a。在编辑器中，
你可以把反向的箭头输入为 \l。
也可以使用等效的 ASCII 符号 <-。
有时恒等式的左手边可以匹配模式中的多个子项，
此时 rw 策略会选择它在遍历该项时发现的第一个匹配。
如果那不是你想要的，你还可以使用额外的参数来指定合适的子项。
| |
在上面的第一个例子中，
第一步会将 a + b + c 重写为 a + (b + c)。
下一步则对 b + c 项应用交换律；若不指定参数，该策略会将 a + (b + c) 重写为 (b + c) + a。
最后一步会在反方向应用结合律，将 a + (c + b) 重写为 a + c + b。
接下来的两个例子则是应用结合律，
先将两边的括号移到右边，
然后再交换 b 和 c。
请注意，最后一个例子通过指定 Nat.add_comm 的第二个参数，
指定了重写应该发生在右手边。
默认情况下 rw 策略只影响目标。
rw[t] at h 会将重写应用于假设 h。
| |
第一步 rw [Nat.add_zero] at h 会将假设 a + 0 = 0 重写为 a = 0；
接着新的假设 a = 0 会被用来将目标重写为 f 0 = f 0。
rw 策略并不仅仅局限于命题；在下面的例子中，
我们使用 rw[h] at t 来将假设 t : Tuple α n 重写为 t : Tuple α 0：
| |
5.7. 使用简化器 Using the Simplifier
尽管 rw 被设计成操作目标的“手术刀”，
但简化器 Simplifier 提供了一种更强大的自动化形式：
Lean 库中有不少被 [simp] 属性标记的恒等式，
它们会被 simp 用来迭代地重写表达式中的子项。
| |
第一个例子中目标等式的左侧部分会根据涉及 0 和 1 的常用恒等式进行简化，
如此便将目标归约为 x * y = x * y，然后 simp 会应用自反性完成证明；
第二个例子中则是先用 simp 将目标归约为 p (x * y)，
然后再用假设 h 完成证明。下面是一些关于列表的例子：
| |
与 rw 一样，你也可以使用关键字 at 来简化一个假设：
As with rw, you can use the keyword at to simplify a hypothesis:
| |
此外你可以使用“通配符”星号来简化所有的假设和目标：
Moreover, you can use a “wildcard” asterisk to simplify all the hypotheses and the goal:
| |
对于可交换和可结合的操作，如自然数上的乘法，
简化器使用这两个事实来重写表达式，以及左交换律（Left commutativity）。
在乘法的情况下，后者表示如下：x * (y * z) = y * (x * z)。
local 修饰符告诉简化器在当前文件（或章节或命名空间，视情况而定）中使用这些规则。
看起来交换律和左交换律是有问题的，因为重复应用其中任何一个都会导致循环。但简化器
会检测置换其参数的恒等式，并
使用一种被称为有序重写 Ordered rewriting 的技术。
这意味着系统维持着项的内部排序，并且
只有在这样做会降低排序的情况下才应用恒等式。
有了上面提到的三个恒等式，其效果是表达式中的所有括号都向右结合，
并且表达式以一种规范的（虽然有些随意）方式排序。
在结合律和交换律下等价的两个表达式会被重写为相同的规范形式。
For operations that are commutative and associative,
like multiplication on the natural numbers,
the simplifier uses these two facts to rewrite an expression,
as well as left commutativity. In the case of multiplication
the latter is expressed as follows: x * (y * z) = y * (x * z).
The local modifier tells the simplifier to use these rules
in the current file (or section or namespace, as the case may be). It may seem that
commutativity and left-commutativity are problematic,
in that repeated application of either causes looping. But the simplifier
detects identities that permute their arguments, and
uses a technique known as ordered rewriting. This means that the system
maintains an internal ordering of terms, and
only applies the identity if doing so decreases the order.
With the three identities mentioned above, this has the effect that
all the parentheses in an expression are associated to the right, and
the expressions are ordered in a canonical (though somewhat arbitrary) way.
Two expressions that are equivalent up to associativity and commutativity
are then rewritten to the same canonical form.
| |
与 rw 一样，你可以向 simp 发送一个要使用的列表，包括
一般的引理、局部假设、要展开的定义和复合表达式。
simp 策略也能识别 rewrite 所能识别的 ←t 语法。在任何情况下，
额外的规则都会被添加到用于简化项的恒等式集合中。
As with rw, you can send simp a list of facts to use, including
general lemmas, local hypotheses, definitions to unfold, and compound expressions.
The simp tactic also recognizes the ←t syntax that rewrite does. In any case,
the additional rules are added to the collection of identities
that are used to simplify a term.
| |
一个常见的习惯用法是使用局部假设来简化目标：
A common idiom is to simplify a goal using local hypotheses:
| |
为了在简化时使用局部上下文中存在的所有假设，
我们可以使用通配符 *：
To use all the hypotheses present in the local context when simplifying,
we can use the wildcard symbol, *:
| |
这里有另一个例子：
Here is another example:
| |
简化器也会做命题重写。例如，使用假设 p，它
将 p ∧ q 重写为 q，将 p ∨ q 重写为 True，
然后它平凡地证明了这一点。
迭代这样的重写会产生非平凡的命题推理。
The simplifier will also do propositional rewriting. For example,
using the hypothesis p, it rewrites p ∧ q to q and p ∨ q to True,
which it then proves trivially. Iterating such rewrites
produces nontrivial propositional reasoning.
| |
下一个例子 简化了所有的假设，然后 用它们来证明目标。
The next example simplifies all the hypotheses, and then uses them to prove the goal.
| |
使简化器特别有用的一点是，它的能力可以随着库的发展而增长。例如， 假设我们定义了一个列表操作，通过附加其反转来使其输入对称：
One thing that makes the simplifier especially useful is that its capabilities can grow as a library develops. For example, suppose we define a list operation that symmetrizes its input by appending its reversal:
| |
那么对于任何列表 xs，
(mk_symm xs).reverse 等于 mk_symm xs，
这可以通过展开定义轻松证明：
Then for any list xs, (mk_symm xs).reverse is equal to mk_symm xs,
which can easily be proved by unfolding the definition:
| |
我们现在可以用这个定理来证明新的结果：
We can now use this theorem to prove new results:
| |
但是使用 reverse_mk_symm 通常是正确的做法，
如果用户不必显式地调用它，那就更好了。
你可以在定义定理时将其标记为简化规则来实现：
But using reverse_mk_symm
is generally the right thing to do, and it
would be nice if users did not have to invoke it explicitly.
You can achieve that
by marking it as a simplification rule
when the theorem is defined:
| |
符号 @[simp] 声明 reverse_mk_symm 具有 [simp] 属性，
可以更明确地拼写出来：
The notation @[simp] declares reverse_mk_symm
to have the [simp] attribute, and
can be spelled out more explicitly:
| |
该属性也可以在定理声明后的任何时间应用：
The attribute can also be applied any time after the theorem is declared:
| |
然而，一旦应用了该属性，就没有办法永久地删除它；
它在任何导入了分配该属性的文件中都会持续存在。正如我们将在属性中进一步讨论的那样，
我们可以使用 local 修饰符将属性的范围限制在当前文件或章节中：
Once the attribute is applied, however,
there is no way to permanently remove it; it persists in any file
that imports the one where the attribute is assigned.
As we will discuss further in Attributes, one can limit the scope of an attribute
to the current file or section using the local modifier:
| |
在 section 之外，化简器默认将不再使用 reverse_mk_symm。
Outside the section, the simplifier
will no longer use reverse_mk_symm by default.
注意，我们讨论过的各种 simp 选项，即给出显式的规则列表，
以及使用 at 指定位置，可以组合使用，但它们列出的顺序是固定的。
你可以在编辑器中通过将光标放在 simp 标识符上，
查看与其关联的文档字符串，从而看到正确的顺序。
Note that the various simp options we have discussed—
giving an explicit list of rules, and
using at to specify the location—can be combined, but
the order they are listed is rigid. You can see the correct order in an editor
by placing the cursor on the simp identifier to see the documentation string
that is associated with it.
There are two additional modifiers that are useful. By default,
simp includes all theorems that have been marked with the attribute [simp].
Writing simp only excludes these defaults, allowing you to use a more explicitly crafted list of rules. In the examples below, the minus sign and only are used to block the application of reverse_mk_symm.
| |
simp 策略有许多配置选项。例如，
我们可以按如下方式启用上下文相关的化简：
The simp tactic has many configuration options. For example,
we can enable contextual simplifications as follows:
| |
使用 +contextual 时，simp 策略在化简 y + x = y 时会使用 x = 0 这一事实，
而在化简另一个分支时会使用 x ≠ 0。这里有另一个例子：
With +contextual, the simp tactic uses the fact that
x = 0 when simplifying y + x = y, and
x ≠ 0 when simplifying the other branch.
Here is another example:
| |
Another useful configuration option is +arith
which enables arithmetical simplifications.
| |
索引 Index
术语
ID 使用 term:<中文术语>。
语法
ID 使用 synt:<关键字>。
- 语法
by ... - 策略
apply ... - 策略
exact ... - 语法
; - 策略
case ... - 策略
. ...或者· ... - 策略
intro ... - 策略
intros ... - 策略
assumption - 策略
unhygienic - 策略
rename_i ... - 策略
rfl - 策略
repeat ... - 策略
revert ... - 策略
generalize ... - 策略
cases ... with ... - 策略
<;> - 策略
constructor - 策略
exists ... - 策略
induction - 策略
contradiction - 策略
show ... - 策略
have ... := ... - 语法
this - 策略
let ... := ... - 策略
first|...|... - 策略
try ... - 策略
skip - 策略
all_goals ... - 策略
any_goals ... - 策略
focus ... - 策略
rw[...] - 语法
rw[←...] - 语法
rw[...] at ...
代码块
ID 使用 S<小节>.code<编号>。
S05-01-code01.lean：创建定理test : p → q → p ∧ q ∧ p（证明待完成）S05-01-code02.lean：创建定理test : p → q → p ∧ q ∧ p（利用by开启策略风格）S05-01-code03.lean：创建定理test : p → q → p ∧ q ∧ p（调整by的位置）S05-01-code04.lean：打印定理test以显示项风格证明S05-01-code05.lean：创建定理test : p → q → p ∧ q ∧ p（简化代码至三行）S05-01-code06.lean：打印定理test以显示项风格证明S05-01-code07.lean：创建定理test : p → q → p ∧ q ∧ p（利用;将策略写在同一行）S05-01-code08.lean：创建定理test : p → q → p ∧ q ∧ p（利用case结构化证明）S05-01-code09.lean：创建定理test : p → q → p ∧ q ∧ p（利用case结构化证明，调整子目标顺序）S05-01-code10.lean：创建定理test : p → q → p ∧ q ∧ p（利用./·结构化证明）S05-02-code01.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)S05-02-code02.lean：创建例子α → α和∀ x : α, x = x（利用intro引入任意变量）S05-02-code03.lean：创建例子∀ a b c : Nat, a = b → a = c → c = b（利用intro引入多个变量）S05-02-code04.lean：创建例子(∃ x, p x ∧ q x) → ∃ x, q x ∧ p x（利用intro模式匹配（隐式））S05-02-code05.lean：创建例子(∃ x, p x ∨ q x) → ∃ x, q x ∨ p x（利用intro模式匹配（多分支））S05-02-code06.lean：创建例子x = y → y = z → z = w → x = w（利用assumption）S05-02-code07.lean：创建例子x = y → y = z → z = w → x = w（利用assumption统一元变量）S05-02-code08.lean：创建例子∀ a b c : Nat, a = b → a = c → c = b（利用intros自动引入三个变量和两个假设）S05-02-code09.lean：创建例子∀ a b c : Nat, a = b → a = c → c = b（利用unhygienic访问intros自动生成的名称）S05-02-code10.lean：创建例子∀ a b c : Nat, a = b → a = c → c = b（利用rename_i重命名最近的intros引入的名字）S05-02-code11.lean：创建例子∀ y : Nat, (fun x : Nat => 0) y = 0（利用rfl证明自反关系）S05-02-code12.lean：创建例子∀ a b c : Nat, a = b → a = c → c = b（利用repeat重复策略）S05-02-code13.lean：创建例子∀ x : Nat, x = x（利用revert还原全称量词）S05-02-code14.lean：创建例子∀ x y : Nat, x = y → y = x（利用revert还原假设）S05-02-code15.lean：创建例子∀ x y : Nat, x = y → y = x（利用revert还原全称量词及相关假设）S05-02-code16.lean：创建例子∀ x y : Nat, x = y → y = x（利用revert还原多个全称量词及相关假设）S05-02-code17.lean：创建例子3 = 3（利用generalize泛化目标中的表达式）S05-02-code18.lean：创建例子2 + 3 = 5（利用generalize泛化目标中的表达式，证明待完成）S05-02-code19.lean：创建例子2 + 3 = 5（利用generalize泛化目标中的表达式，记录赋值）S05-03-code01.lean：创建例子p ∨ q → q ∨ p（利用cases解构析取）S05-03-code02.lean：创建例子p ∨ q → q ∨ p（利用cases解构析取，调整子目标顺序）S05-03-code03.lean：创建例子p ∨ q → q ∨ p（利用cases（无with）解构析取）S05-03-code04.lean：创建例子p ∨ p → p（利用cases（无with）解构析取，利用repeat重复策略）S05-03-code05.lean：创建例子p ∨ p → p（利用<;>组合器将策略应用于所有子目标）S05-03-code06.lean：创建例子p ∨ q → q ∨ p（利用cases（无with）结合case或.结构化证明）S05-03-code07.lean：创建例子p ∧ q → q ∧ p（利用cases解构合取）S05-03-code08.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)（利用cases和constructor）S05-03-code09.lean：创建例子(∃ x, p x ∧ q x) → ∃ x, q x ∧ p x（利用cases和constructor）S05-03-code10.lean：创建例子(∃ x, p x) → ∃ x, p x ∨ q x（利用cases和exists）S05-03-code11.lean：创建例子(∃ x, p x ∧ q x) → ∃ x, q x ∧ p x（利用cases和exists）S05-03-code12.lean：定义函数 类型加法乘法运算的交换律（利用cases、constructor及<;>）S05-03-code13.lean：创建例子 数学归纳法的合理性（利用cases对自然数分类讨论）S05-03-code14.lean：创建例子p ∧ ¬p → q（利用contradiction搜索矛盾）S05-03-code15.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)（利用intro和match）S05-03-code16.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)（利用intro（隐式match））S05-04-code01.lean：创建例子p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)（利用have声明子证明，利用show显示目标）S05-04-code02.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)（利用case）S05-04-code03.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)（利用show显示目标）S05-04-code04.lean：创建例子n + 1 = Nat.succ n（利用show显示目标）S05-04-code05.lean：创建例子p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)（利用have声明子证明，利用show显示目标）S05-04-code06.lean：创建例子p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)（利用have声明子证明（匿名）并用this调用）S05-04-code07.lean：创建例子p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)（利用have声明子证明（匿名）并用this调用）S05-04-code08.lean：创建例子∃ x, x + 2 = 8（利用let声明局部定义）S05-04-code09.lean：创建例子p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)（利用花括号和分号结构化证明）S05-05-code01.lean：创建例子p → p ∨ q（利用;组合子）S05-05-code02.lean：创建例子p → p ∨ q（利用<;>组合子）S05-05-code03.lean：创建例子p → p ∨ q（利用first组合子）S05-05-code04.lean：创建例子p → p ∨ q ∨ r（利用first组合子和repeat）S05-05-code05.lean：创建例子p → q → r → p ∧ q ∧ r（利用try组合子）S05-05-code06.lean：创建例子p → q → r → p ∧ q ∧ r（利用all_goals组合子）S05-05-code07.lean：创建例子p → q → r → p ∧ q ∧ r（利用any_goals组合子）S05-05-code08.lean：创建例子p → q → r → p ∧ q ∧ r（利用all_goals组合子和repeat）S05-05-code09.lean：创建例子p → q → r → p ∧ q ∧ r（利用all_goals组合子和repeat，写成一行）S05-06-code01.lean：创建例子f 0 = 0 → k = 0 → f k = 0（利用rw）S05-06-code02.lean：创建例子∀ x y : Nat, (q → x = y) → q → p y → p x（利用rw（合并多次rw））S05-06-code03.lean：创建例子f 0 = 0 → k = 0 → f k = 0（利用rw（合并多次rw））S05-06-code04.lean：创建例子∀ a b : Nat, a = b → f a = 0 → f b = 0（利用rw（通过←反方向套等式）S05-06-code05.lean：创建例子∀ a b c : Nat, a + b + c = a + c + b（利用rw（通过提供定理的额外参数来指定匹配项））S05-06-code06.lean：创建例子∀ a : Nat, a + 0 = 0 → f a = f 0（利用rw（通过at指定被重写的等式））S05-07-code01.lean：创建例子∀ a : Nat, n = 0 → Tuple a n → Tuple a 0（利用rw）
练习
微信