Dafny中Nat类型构造函数顺序不同导致验证结果差异问题

两个Nat定义的语义说明 #

你给出的两个Nat类型定义在逻辑语义上完全等价，仅构造子的声明顺序不同，不存在逻辑表达能力或者含义层面的差异。

// 定义1：S在前
datatype Nat = S(Nat) | Z
// 定义2：Z在前
datatype Nat = Z | S(Nat)

验证差异的核心原因 #

验证结果不同完全是Dafny自动验证器的启发式策略特性导致的，和类型本身的语义无关，具体原因如下：

• Dafny的{:induction n}自动归纳策略会按照构造子的声明顺序生成归纳分支、分配搜索优先级：
  第一种定义S(Nat)在前，自动归纳时优先对S构造的项应用归纳假设，刚好匹配natToDay函数的递归结构：函数优先匹配多层S包裹的项，递归调用时剥离7层S后传入参数k，归纳假设很容易被自动应用到k上完成证明。
  第二种定义Z在前，自动归纳时优先穷尽Z的基础分支，再逐层展开S的分支，默认的启发式搜索深度不足以自动匹配到7层S的递归结构，无法自动应用归纳假设完成证明，因此会报后置条件可能不成立的错误。这并不代表后置条件逻辑上不成立，只是自动验证器在默认配置下没有找到证明路径。
• 你可以通过手动补充归纳提示、调整搜索深度、或者手动拆分case的方式，让第二种定义的代码也正常通过验证。

内容的提问来源于stack exchange，提问作者Boro Sitnikovski