17.3. 验证条件🔗

mvcgen 策略把以 SPred 和最弱前置条件表示的目标转换为一组不变式和验证条件；它们共同足以证明原目标。 特别地，霍尔三元组以最弱前置条件定义，因此可以使用 mvcgen 来证明。

目标的验证条件按如下方式生成：

1. 应用若干简化和重写。

2. 此时目标应形如 P ⊢ₛ wp⟦e⟧ Q（即从一组有状态假设到蕴含所需后置条件之最弱前置条件的蕴涵）。

3. 展开表达式 e 中的可约常量以及标记了 @[spec] 的定义。

4. 若表达式是辅助匹配函数或条件式（ite 或 dite）的应用，则先对其化简。 化简每个匹配器的判别项，并归约整个项，尝试消除该匹配器或条件式。 若失败，则为每个分支生成一个新目标。

5. 若表达式是某个常量的应用，则按优先级顺序尝试适用的 @[spec] 引理。 Lean 为 Lean.Parser.Term.do : termdo 记法脱糖后产生的 bind、pure 和 ForIn.forIn 等常量提供了规约引理。 实例化引理有时会解决其前提，尤其是因与目标定义相等而确定的模式变量。 但 Invariant 类型的假设绝不会以这种方式实例化。 若规约引理的前置条件或后置条件与目标不完全匹配，则创建新的元变量来证明所需的蕴涵。 若尝试使用局部假设并分解后置条件中的合取之简单自动化无法立即解决它们，它们就会保留为验证条件。

6. 对该过程生成的每个剩余目标，若其形如 P ⊢ₛ wp⟦e⟧ Q，则递归生成验证条件；否则将其加入不变式或验证条件集合。

7. 为所得不变式和验证条件子目标在证明状态中赋予合适的名称。

8. 根据策略的配置参数，在每个验证条件上尝试 mvcgen_trivial 和 mleave。

为库定义合适的规约引理可以改善验证条件生成。 良好的规约引理能减少生成的验证条件数量。 此外，确保项的简化范式适合模式匹配，并确保默认 simp 集包含足够的引理，可将所有可能的项归约到该范式，便能消除更多条件式和模式匹配。