[WIP] task013

[ahuoguo]

Been able to prove in dafny: (several lemma relies on dafny being able to use non-linearity, see the failed ones by --disable-nonlinear-arithmetic flag).

module gcd {

  method gcd_exec(a: nat, b: nat) returns (res: nat)
    requires a > 0 && b > 0
    ensures res > 0
    ensures divides(res, a) && divides(res, b)
    ensures forall k: nat :: k > 0 && divides(k, a) && divides(k, b) ==> divides(k, res)
    ensures res == gcd(a, b)
  {
    if a == b {
      res := a;
    }
    else if a < b {
      res := gcd_exec(a, b-a);
    }
    else {
      res := gcd_exec(a-b, b);
    }
    dividesLemma(a, 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)
  }

  ghost predicate divides(a: nat, b: nat)
    requires a > 0 && b > 0
  {
    exists k :: 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 dividesLemma2(a:nat, b:nat, c:nat)
    requires a > 0 && b > 0 && c > 0
    requires divides(a, b) && divides(a, c)
    ensures divides (a, b + c)
  {
    var m, n :| b == m * a && c == n * a;
    assert b + c == (m + n) * a;
  }


  lemma dividesLemma(a: nat, b: nat)
    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))
    ensures divides(gcd(a, b), a) && divides(gcd(a, b), b)
  {
    if (a == b){
      assert divides(a, a) by {
        assert a == 1 * a;
      }
    }
    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);
      }
      assert divides(gcd(a, b), b) by {
        dividesLemma2(gcd(a, b), a, 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);
      }
      dividesLemma2(gcd(a, b), a - b, b);
    }

  }
}

I used recursion, rather than using a while loop. Rustin Leino has a case study on a fancy way to prove it in dafny https://leino.science/papers/krml279.html.