14. 策略证明
策略语言是一种用于构造证明的专用编程语言。 在 Lean 中，命题由类型表示，而证明则是这些类型的项。 命题一节更详细地介绍了命题。 项的设计目标是便于指出类型的某个特定元素，而策略的设计目标则是便于证明某个类型存在元素。 之所以作此区分，是因为定义必须精确地选出所关注的对象、程序必须返回预期结果；但证明无关性意味着，从技术上说，并没有理由偏好某个证明项而非另一个。 例如，给定同一类型的两个假设时，程序必须仔细编写以使用正确的那个，而证明使用任一个都不会造成影响。
策略是修改证明状态的命令式程序。
证明状态由一列有序的目标组成；每个目标都是局部假设的上下文以及一个需要构造元素的类型。策略可能成功并产生一列可能为空的后续目标（称为子目标），也可能因无法取得进展而失败。
如果策略成功且没有子目标，证明就完成了。
如果策略成功并产生一个或多个子目标，那么当这些子目标都得到证明时，原目标也就得到证明。
证明状态中的第一个目标称为主目标。
大多数策略只影响主目标，但可以用 <;> 和 all_goals 等运算符将策略应用到多个目标；也可以用项目符号、next 或 case 等运算符，将后续策略的焦点缩小到证明状态中的单个目标。
在幕后，策略会构造证明项。 证明项是以 Lean 类型论书写、可独立检查的定理成立证据。 每个证明都会由内核检查，也可由独立实现的外部检查器验证；因此，策略中的缺陷最坏只会导致令人困惑的错误消息，而不会产生错误的证明。 策略证明中的每个目标都对应证明项中尚未完成的一部分。