Dafny 4.10对Leino《Program proofs》练习过强？求原因与解决办法

你遇到的情况确实是Dafny引擎版本迭代带来的变化。2023版《Program proofs》编写时，对应的Dafny版本（大概率是3.x或更早的4.x预览版）自动推理能力有限，这类基础代数等式化简、简单不等式证明需要手动展开推导步骤才能通过验证。但Dafny 4.10.0集成的SMT求解器（如Z3）优化了代数推理逻辑，能自动完成这类常规数学推导——而{:induction false}属性仅禁用归纳证明机制，完全不影响SMT求解器的常规代数化简能力，所以对你提到的习题无效。

既然你需要保留验证功能，但希望强制自己完成手动推导步骤，有两种实用方法：

1. 手动拆解证明步骤，添加中间断言 #

把原有的大目标拆分成多个小的、需要手动推导的子步骤，用assert语句明确写出每一步的推导结果，让Dafny仅验证这些子步骤的正确性，而非直接跳过推导过程。比如针对习题5.4a，可以改写为：

lemma {:induction false} ex_5_4_a(x: int, y: int)
ensures 5*x - 3*(y+x) == 2*x-3*y
{
  // 手动展开分配律
  assert 5*x - 3*(y+x) == 5*x - 3*y - 3*x;
  // 手动合并同类项
  assert 5*x - 3*x == 2*x;
  // 最终结论由上述两步自然推导得出
}

这种方法完全贴合书籍的练习初衷，既能让你练习手动推导逻辑，又能通过Dafny验证每一步的正确性。

2. 限制SMT求解器的自动推理能力 #

如果希望从工具层面限制自动推导，可以通过调整Dafny的求解器参数实现：

• 切换到推理能力较弱的SMT求解器，比如给lemma添加{:smt-solver "cvc4"}属性，CVC4在部分简单代数推导上的自动能力弱于Z3；
• 设置极短的SMT超时时间，比如{:smt-timeout 1}，让求解器没时间完成自动推导（注意：这种方法可能会误杀正常的验证需求，需谨慎使用）。

不过更推荐第一种方法，因为它直接聚焦练习核心——掌握手动证明逻辑，而非单纯限制工具能力。

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