Dafny GCD引理证明

Question

我想用dafny证明下面关于gcd的引理:对于所有k个自然数，如果k|a和k|b，则k|gcd(a，b)。到目前为止，我有以下代码：

// 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)
//k|a && k|b ==> k|gcd(a,b)
requires a > 0 && b > 0
    ensures gcd(a,b) > 0
    ensures forall k: nat :: divides(a,k) && divides(b,k) ==> divides(gcd(a,b),k)
{
    if(a == b) {
        assert a * 1 == gcd(a,b);
        assert b * 1 == gcd(a,b);
    } else if b > a {
        if(divides(a, b)) {
            assert divides(a,a);
            assert divides(a,b);
            assert divides(a, gcd(a,b));
        } else {
            dividesLemma(a, b - a);
        }
    } else {
        if(divides(b, a)) {
            assert divides(b,b);
            assert divides(b,a);
            assert divides(b, gcd(a,b));
        } else {
            dividesLemma(a, a - b);
        }
    }
}

我知道如何用手来做证明。我会考虑a和b的素数分解，并说gcd(a，b)是组合的素数分解，使得我们从每个素数分解中取最少的素数。例如，如果a=9，b= 15，9的素数分解= 3x3，15的素数分解= 3x5，所以gcd(9,5) =3，因为这是它们素数分解的最小组合。利用这一事实，应该很清楚，如果k|b和k|a，k一定包含这些最小素数。我怎么用dafny来表达呢？目前，我正在考虑基本情况if a=b和if a|b或b|a，但不确定如何合并a和b在素数分解中可能不共享公素数这一事实。

对此任何帮助都将不胜感激！

Answer 1

divides的调用方式有问题。我认为在确保条款中，你指的是divides(k, a)而不是divides(a, k)，类似于divides(b, k)和divides(gcd(a, b), k)。

在递归调用dividesLemma(a, b - a)之后，一种方法是使用方法的后置条件。这里我们知道，对于所有的k，k除以a，k除以b - a，这意味着k除以gcd(a, b-a)。使用此信息，我们尝试证明所需的后置条件(代码或证明简单易懂)

dividesLemma(a, b - a);
assert gcd(a, b) == gcd(a, b-a);
assert forall k : nat :: k > 0 && divides(k, a) && divides(k, b-a) ==> divides(k, gcd(a, b));
forall k : nat | k > 0 && divides(k, a) && divides(k, b) ensures divides(k, gcd(a, b)) {
    var m :| a == m * k;
    var n :| b == n * k;
    assert (b - a) == (n - m) * k;
    assume n >= m;
    assert divides(k, a);
    assert divides(k, b-a);
    // Implied from last assert forall
    assert divides(k, gcd(a, b)); 
}

这里我假设是n >= m，因为divides要求n-m为nat，这可以单独证明。

另外，第二个递归调用应该是dividesLemma(a - b, b)。

function gcd(a: nat, b: nat): nat
  requires a > 0 && b > 0
{
  if a == b
    then a
  else if a < b
    then gcd(a, b-a)
  else gcd(a-b, b)
}

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

lemma helper(a: nat, b: nat, k : nat)
  requires a > 0 && b > 0 && k > 0
  requires divides(k, a) && divides(k, b)
  requires b >= a
  ensures exists m, n :: a == m * k && b == n * k && m <= n;
{ }
    
lemma dividesLemma(a: nat, b: nat)
  decreases a + b
  requires a > 0 && b > 0
  ensures gcd(a, b) > 0
  ensures forall k: nat :: k > 0 && divides(k, a) && divides(k, b) ==> divides(k, gcd(a, b))
{
  if (a == b){
  }
  else if (b > a){
    dividesLemma(a, b - a);
    assert gcd(a, b) == gcd(a, b-a);
    assert forall k : nat :: k > 0 && divides(k, a) && divides(k, b-a) ==> divides(k, gcd(a, b));
    forall k : nat | k > 0 && divides(k, a) && divides(k, b) ensures divides(k, gcd(a, b)) {
      helper(a, b, k);
      var m, n :| a == m * k && b == n * k && m <= n;
      assert b - a == (n - m) * k;
      assert divides(k, b-a);
    }
  }
  else {
    dividesLemma(a - b, b);
    assert gcd(a, b) == gcd(a - b, b);
    assert forall k : nat :: k > 0 && divides(k, a-b) && divides(k, b) ==> divides(k, gcd(a, b));
    forall k : nat | k > 0 && divides(k, a) && divides(k, b) ensures divides(k, gcd(a, b)) {
      helper(b, a, k);
      var m, n :| b == m * k && a == n * k && m <= n;
      assert a - b == (n - m) * k;
      assert divides(k, a-b);
    }
  }
}