17.3. 验证条件
mvcgen策略将以 SPred 和最弱先决条件表示的目标转换为一组不变量和验证条件，这些不变量和验证条件一起足以证明原始目标。
特别是，霍尔三元组是根据最弱前提条件定义的，因此可以使用 mvcgen 来证明它们。
目标的验证条件生成如下：
-
应用了许多简化和重写。
-
目标现在应该采用
P ⊢ₛ wp⟦e⟧ Q的形式（即，从一组有状态假设到暗示所需后置条件的最弱前提条件的蕴涵）。 -
如果表达式是 辅助匹配函数 或条件（
ite或dite）的应用，则首先对其进行简化。 每个匹配器的 判别式 被简化，并且整个项被减少以试图消除匹配器或条件。 如果失败，则会为每个分支生成一个新目标。 -
如果表达式是常量的应用，则按优先级顺序尝试标记为
@[spec]的适用引理。 Lean 包括常量的规范引理，例如bind、pure和ForIn.forIn，这些常量是由脱糖Lean.Parser.Term.do : termdo表示法产生的。 实例化引理有时会解除其前提，特别是由于与目标的定义等价而导致的示意性变量。 然而，Invariant类型的假设永远不会以这种方式实例化。 如果规范引理的前置条件或后置条件与目标的前置条件或后置条件不完全匹配，则创建新的元变量来证明必要的蕴涵。 如果这些不能使用简单的自动化立即释放，尝试使用局部假设并分解后置条件中的连词，那么它们仍然作为验证条件。 -
如果此过程创建的每个剩余目标的格式为
P ⊢ₛ wp⟦e⟧ Q，则将针对验证条件递归处理该目标。如果不是，则将其添加到不变量或验证条件集中。 -
由此产生的不变量和验证条件的子目标在证明状态中被分配了合适的名称。
-
根据策略的配置参数，在每个验证条件下尝试
mvcgen_trivial和mleave。
可以通过为库定义适当的 规范引理 来改进验证条件生成。 良好规范引理的存在会导致生成的验证条件更少。 此外，确保术语的 simp 范式 适用于模式匹配，并且默认 simp 集中有足够的引理来将每个可能的术语简化为该范式，可能会导致更多条件和模式匹配被消除。