关于整数“相邻”特性的Dafny证明可行性问询

你的证明方案无法直接通过Dafny自动验证，核心原因是：Dafny的整数理论虽基于皮亚诺算术，但不会自动调用“整数离散性”的隐含规则——即对任意整数a，不存在整数i满足a < i < a+1，且a+1是大于a的最小整数。要完成证明，有两种可选方案：

方案1：补充整数离散性引理 #

先证明一个辅助引理明确整数的离散特性，再用它推导出目标结论：

// 证明整数a和a+1之间不存在其他整数
lemma IntDiscreteness(a: int)
  ensures !(exists i: int :: a < i < a+1)
{} // Dafny可自动验证该引理

predicate Touching(a: int, b:int)
  requires a < b
{
  !(exists i :: a < i < b)
}

method IntThing(a: int, b:int)
  requires a < b
  requires Touching(a,b)
{
  // 反证法：假设a+1 < b，推出矛盾
  if a+1 < b {
    assert exists i :: a < i < b; // i=a+1就是满足条件的整数，与Touching定义冲突
    assert false;
  }
  // 结合前提a < b，可推导出a+1 == b
  assert a+1 == b;
}

方案2：直接修改Touching的定义 #

如果不想额外编写引理，直接将“相邻”定义为a+1 == b是最简洁的方式，此时断言可直接通过验证：

predicate Touching(a: int, b:int)
  requires a < b
{
  a+1 == b
}

method IntThing(a: int, b:int)
  requires a < b
  requires Touching(a,b)
{
  assert a+1 == b; // 无验证错误，直接成立
}

总结：若坚持用“无中间整数”的相邻定义，需补充离散性引理完成证明；若追求简洁高效，直接用a+1 == b定义相邻更合适。

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