dafny infinite set axioms and proving gcd lemma

Question

Here is the goal. I am hoping to prove that given two numbers a and b, which are relatively prime I can show that there is some x and y such 1 = a*x+b*y. I copied implementation of GCD from KRML 279

lemma GcdLinearCombination(a: pos, b: pos)
    ensures exists x,y :: Gcd(a,b) == a*x+b*y
{

Looking at the standard proof of this fact in text books, the proof makes use of an infinite set, asserting that some smallest d in this set is a linear combination of a and b and it also is the gcd. It involves diving a by d and showing that the remainder r is also of the same form, a linear combination of a and b, but because d is the smallest combination of that form is is a contradiction so r must be 0. Can we really construct a proof like this in Dafny?

function combinationSet(a: pos, b: pos): set<pos> 
{
    set x: nat,y: nat | 0 <= x <= a && 0 <= y <= b && a*x+b*y > 0 :: a*x+b*y
}

function icombinationSet(a: pos, b: pos): iset<pos> 
{
    iset x: nat,y: nat | a*x+b*y > 0 :: a*x+b*y
}

They then call upon the well-ordering principle to assert that some smallest d exists in this infinite set after demonstrating that it is not empty. Do I need to create an axiom that in a set of only positive numbers that such a number exists or is there another mechanism I can call upon to deduce this?

Trying to implement Min for an infinite set fails because the iset is not decreasing.

  function iMin(s: iset<pos>): pos
        requires s != iset{}
        ensures forall x | x in s :: iMin(s) in s && iMin(s) <= x
    {
        var x :| x in s;
        if s == iset{x} then
            x
        else
            var y := iMin(s - iset{x}); //infinite set size is not decreasing as expected
            assert forall z | z in s :: z == x || (z in (s - iset{x}) && y <= z);
            if x < y then x else y
    }

Answer 1

I have used nat instead of pos, but should be easy to port to 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;
            }
         }
      }
    }
}