Аксиомы бесконечного множества Дафни и доказательство леммы НОД

Следующее, кажется, работает для бесконечных множеств.

   lemma WellOrderingPrinciple(s: iset<pos>)
        requires s != iset{}
        ensures exists min :: min in s && forall x | x in s && x != min :: min < x; 

    function iMin(s: iset<pos>): pos
        requires s != iset{}
        ensures forall x | x in s && x != iMin(s) :: iMin(s) in s ==> iMin(s) < x
    {
        WellOrderingPrinciple(s);
        var min :| min in s && forall x | x in s && x != min :: min < x; 
        min
    }

Я использовал nat вместо pos, но его легко портировать на pos.

lemma MinExist(s: set<nat>)
  requires s != {}
  ensures exists x :: x in s && forall y :: y in s ==> x <= y
{
    var x := FindMin(s);   
}

function FindMin(s: set<nat>): (min: nat)
  requires s != {}
  ensures min in s && forall y :: y in s ==> min <= y
{
  var x :| x in s;
  if s == {x} then
    x
  else
    var s' := s - {x};
    assert s == s' + {x};
    var y := FindMin(s');
    if x < y then x else y
}
 
function ISetMin(s: iset<nat>): nat
 requires s != iset{}
{
   ISetMinExists(s);
   var x :| x in s && forall y :: y in s ==> x <= y;
   x
}    

lemma ISetMinExists (s: iset<nat>)
  requires s != iset{}
  ensures exists x :: x in s && forall y :: y in s ==> x <= y
{
    var x :| x in s;
    var rs := s - iset{x};
    if rs == iset{}
    {
      forall i | i in s ensures x <= i {
         if i == x {}
         else {
          assert s == iset{x};
          assert i in iset{x};
          assert false;
         }
      }
    }
    else {
      var ss := set y | y < x ;
      var tt := set y | y in ss && y in s;
      if |tt| == 0 {
        forall i  | i in s ensures x <= i {
          if i < x {
            assert forall z :: z < x ==> z in ss;
            assert i in ss;
            assert i in tt;
          }
        }
      }
      else {
         var y := FindMin(tt);
         forall i | i in s ensures y <= i {
            if i < x {
               assert i in tt;
            }
         }
      }
    }
}

Я не закончил, но вот пробный набросок. Обратите внимание, что я усилил постусловие iMin, и есть несколько предположений, которые необходимо доказать. Надеюсь это поможет !

lemma WellOrderingPrinciple(s: iset<nat>)
    requires s != iset{}
    ensures exists min :: min in s && forall x | x in s && x != min :: min < x; 

function iMin(s: iset<nat>): nat
    requires s != iset{}
    // Change of the postcondition to be stronger
    ensures iMin(s) in s  && forall x | x in s && x != iMin(s) :: iMin(s) < x
{
    WellOrderingPrinciple(s);
    var min :| min in s && forall x | x in s && x != min :: min < x; 
    min
}

predicate IsGCD(a: nat, b: nat, g: nat) {
  g > 0 && (a % g) == 0 && (b % g) == 0 &&
  (forall x: nat | x > 0 && a % x == 0 && b % x == 0 ::
   x <= g
  )
}

function euclidianDivision(a: nat, d: nat): (result: (nat, nat))
  requires d > 0
  ensures result.0 == (a - (a % d))/d
  ensures result.1 == a % d
  ensures
    calc {
      result.0 * d + result.1;
      { assert result.0 == (a - (a % d))/d; }
      ((a - (a % d))/d)*d + result.1;
      ((a - (a % d))/d)*d + (a % d);
      { assume (a - (a % d)) % d == 0; } // TODO: Prove this
      a - (a % d) + (a % d);
      a;
    }
    result.0 * d + result.1 == a && 0 <= result.1 < d
{
  ((a - (a % d))/d, a % d)
}



lemma GcdLinearCombination(a: nat, b: nat, g: nat)
    requires IsGCD(a, b, g)
    requires a > 0 && b > 0
    ensures exists x,y :: g == a*x+b*y
{
  var allCombinations :=
    iset x: int, y: int | a*x+b*y > 0 :: var j: nat := a*x+b*y; j;
  assert allCombinations != iset{} by {
    var x := 1;
    var y := 1;
    assert a*x+b*y > 0;
    var j: nat := a*x+b*y;
    assert j in allCombinations;
  }
  var d := iMin(allCombinations);
  // Definition of d. Place where you need.
  //assert d in allCombinations && (forall x <- allCombinations | x != d :: d < x);

  assert d == g by {
    assert exists x: int, y: int :: a*x+b*y == d;
    var x, y :| a*x+b*y == d;
    assert forall x | x in allCombinations && x != d :: d in allCombinations ==> d < x;
    assert d > 0;
    
    if a % d != 0 {
      var (q, r) := euclidianDivision(a, d);
      assert r != 0;
      assert q * d + r == a;
      var x' := 1-q*x;
      var y': int := 0 - q*y;
      calc <==> {
        a == q * d + r;
        a == q * (a*x + b*y) + r;
        a - q * (a*x + b*y) == r;
        r == a - q * (a*x + b*y);
        r == a - q*(a*x) - q*(b*y);
        r == a - q*(x*a) - q*(y*b);
        r == a - (q*x)*a - (q*y)*b;
        r == (1 - (q*x))*a - (q*y)*b;
        r == x' * a + y' * b;
        r == a* x' + b * y';
      }
      var j: nat := a* x' + b * y';
      assert j in allCombinations;
      assert j == r;
      assert false;
    }
    if b % d != 0 {
      var (q, r) := euclidianDivision(b, d);
      assert r != 0;
      assert q * d + r == b;
      var y' := 1-q*y;
      var x': int := 0 - q*x;
      calc <==> {
        b == q * d + r;
        b == q * (a*x + b*y) + r;
        b == q * (b*y + a*x) + r;
        b - q * (b*y + a*x) == r;
        r == b - q * (b*y + a*x);
        r == b - q*(b*y) - q*(a*x);
        r == b - q*(b*y) - q*(a*x);
        r == b - (q*y)*b - (q*x)*a;
        r == (1 - (q*y))*b - (q*x)*a;
        r == y' * b + x' * a;
        r == b* y' + a * x';
        r == a * x' + b * y';
      }
      var j: nat := a* x' + b * y';
      assert j in allCombinations;
      assert j == r;
      assert false;
    }
    // Ok, so now we proved that d divides a and d divides b
    assert (a % d) == 0 && (b % d) == 0;
    var (x', r0) := euclidianDivision(a, d);
    var (y', r1) := euclidianDivision(b, d);
    assert x' * d == a;
    assert y' * d == b;
    // Now, is it the biggest?
    assert (forall x: nat | x > 0 && a % x == 0 && b % x == 0 :: x <= d) by {
      forall x: nat | x > 0 && a % x == 0 && b % x == 0 
        ensures x <= d
      {
        assume false; // TODO
      }
    } 
  }
  assert g in allCombinations;
}