如何证明Dafny中自然数乘除同一数的恒等性引理？

问题引理 #

你要证明的引理代码如下：

lemma MulDivIsId(a: nat, b: nat)
requires b > 0
ensures a * b / b == a
{
}

具体证明方法 #

你之前尝试的b/b=1和乘法结合律思路行不通，是因为Dafny的自然数截断除法不满足乘法对除法的分配律（即(x*y)/z ≠ x*(y/z)并非普遍成立）。正确的证明可以从除法的定义入手，或者用数学归纳法：

方法1：基于除法定义直接推导

Dafny中自然数截断除法的核心定义是：对于y>0，q = x/y当且仅当q*y ≤ x < (q+1)*y。利用这个定义可以直接完成证明：

lemma MulDivIsId(a: nat, b: nat)
requires b > 0
ensures a * b / b == a
{
  // 验证a满足除法定义的q条件
  assert a * b >= a * b;
  assert a * b < (a + 1) * b; // 因b>0，不等式两边乘b后方向不变
  // 根据定义，a*b /b 就是满足q*b ≤a*b <(q+1)*b的唯一q，即q=a
}

方法2：数学归纳法

针对自然数a做归纳，拆解问题为基础情况和归纳步骤：

lemma MulDivIsId(a: nat, b: nat)
requires b > 0
ensures a * b / b == a
{
  induction a {
    case 0 =>
      assert 0 * b == 0;
      assert 0 / b == 0; // 0除以任何正自然数都为0
    case a_prev =>
      calc {
        (a_prev + 1) * b / b;
        (a_prev * b + b) / b; // 乘法分配律展开
        a_prev * b / b + b / b; // 两个b的倍数相加后除以b，等于各自除以b的和
        a_prev + 1; // 应用归纳假设和b/b=1
      }
  }
}

自然数截断除法引理的通用证明步骤 #

1. 锚定除法定义：所有截断除法的推理都要基于核心定义——q = x/y当且仅当q*y ≤ x < (q+1)*y（y>0），这是验证器认可的最基础依据。
2. 优先使用数学归纳法：针对自然数类型的变量，归纳法能将复杂问题拆解为可验证的基础情况和递推步骤，Dafny对归纳法的支持非常友好。
3. 用calc块分步推导：把复杂表达式拆成多步转换，每一步用assert或已证引理验证转换的合法性，让验证器能逐步跟进你的推理逻辑。
4. 拆分情况讨论：如果引理涉及非倍数的情况，可拆分x = k*y + r（0 ≤ r < y）的形式，分别讨论余数为0和不为0的场景。
5. 调用内置引理：Dafny标准库中包含大量基础数论引理，比如Divides系列、MulDiv相关引理，可通过apply直接调用，减少重复证明。

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