如何用Dafny证明「k整除a且k整除b则k整除gcd(a,b)」引理

首先你当前的代码存在两个核心问题：

1. 后置条件写反了：你定义的divides(a,b)表示a整除b，你要证明的「若k整除a且k整除b，则k整除gcd(a,b)」对应的逻辑写反了，同时漏了k必须为正的前置约束。
2. 缺少核心辅助引理：欧几里得算法的递归步骤依赖「若k整除两个数，则k整除两数的差」的性质，你需要先证明这个辅助引理才能完成递归分支的推导。

第一步：实现辅助引理 #

先证明差的整除性质，为递归步骤做铺垫：

lemma divides_sub(k: nat, x: nat, y: nat)
  requires k > 0
  requires divides(k, x) && divides(k, y)
  requires x >= y
  ensures divides(k, x - y)
{
  // 从divides的定义取出两个系数
  var (k1, k2) :| x == k1 * k && y == k2 * k;
  assert x - y == (k1 - k2) * k;
}

第二步：修正原引理的定义与实现 #

修正后置条件，对齐gcd函数的递归逻辑，补充归纳推导步骤：

// Euclid's algorithm for computing the greatest common divisor
function gcd(a: nat, b: nat): nat
    requires a > 0 && b > 0
{
    if a == b then a else 
    if b > a then gcd(a, b - a) else 
    gcd(a - b, b) 
}

predicate divides(a: nat, b:nat)
    requires a > 0
{
exists k: nat :: b == k * a
}

lemma dividesLemma(a: nat, b: nat)
requires a > 0 && b > 0
    ensures gcd(a,b) > 0
    // 修正后的后置条件：对任意正整数k，若k整除a且k整除b，则k整除gcd(a,b)
    ensures forall k: nat :: k > 0 && divides(k,a) && divides(k,b) ==> divides(k, gcd(a,b))
{
    if(a == b) {
        // 基础情况：a==b时gcd就是a，自然成立
    } else if b > a {
        // 递归调用对齐gcd的逻辑：gcd(a,b) = gcd(a, b-a)
        dividesLemma(a, b - a);
        // 对任意满足条件的k，先证k整除b-a
        forall k | k>0 && divides(k,a) && divides(k,b) 
        ensures divides(k, gcd(a,b))
        {
            divides_sub(k, b, a);
            // 用归纳假设得到k整除gcd(a, b-a)，也就是gcd(a,b)
        }
    } else {
        // 递归调用对齐gcd的逻辑：gcd(a,b) = gcd(a-b, b)
        dividesLemma(a - b, b);
        forall k | k>0 && divides(k,a) && divides(k,b) 
        ensures divides(k, gcd(a,b))
        {
            divides_sub(k, a, b);
        }
    }
}

说明 #

你不需要用质因数分解的思路来证明，沿着你定义的欧几里得gcd函数的递归结构做归纳证明是最直接的方案：

• 基础情况a==b时结论显然成立
• 递归步骤中，两数的公因子必然同时整除两数的差，因此公因子集合和递归调用的公因子集合完全一致，通过归纳假设就能推导出原命题成立

上述代码可以直接在Dafny中验证通过。

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