14. 策略样张
策略语言是一种用于构造证明的专用编程语言。 在 Lean 中，命题 由类型表示，证明是居住在这些类型中的术语。 关于命题的部分更详细地描述了命题。 虽然术语旨在方便地指示某个类型的特定居民，但策略的设计目的是方便地证明某个类型有人居住。 存在这种区别是因为定义挑选出感兴趣的精确对象并且程序返回预期结果很重要，但证明无关性意味着没有技术理由来选择一个证明项而不是另一个证明项。 例如，给定给定类型的两个假设，必须仔细编写程序才能使用正确的假设，而证明可以使用其中任何一个而不会产生任何后果。
策略是修改 proof state. 的命令式程序
证明状态由 goals 的有序序列组成，它们是局部假设以及要居住的类型的上下文；策略可能会通过可能为空的进一步目标序列（称为 subgoals）而“成功”，如果无法取得进展，则可能会“失败”。
如果策略成功且没有子目标，则证明完成。
如果它成功实现了一个或多个子目标，那么当这些子目标被证明时，它的一个或多个目标也将被证明。
证明状态中的第一个目标称为 main goal.
虽然大多数策略仅影响主要目标，但 <;> 和 all_goals 等运算符可用于将策略应用到许多目标，而子弹、next 或 case 等运算符可将后续策略的焦点缩小到仅一个目标目标处于证明状态。
策略在幕后构造 证明条款。 证明项是定理正确性的可独立检查的证据，以 Lean 的 类型论 形式编写。 每个证明都在 内核 中进行检查，并且可以使用独立实现的外部检查器进行验证，因此策略中的错误最糟糕的结果是令人困惑的错误消息，而不是不正确的证明。 策略证明中的每个目标对应于证明项的不完整部分。