The Hilbert epsilon operator

Question

Why you can use the Hilbert epsilon operator in a method and in a function, but not in a "function method"?

method choose<T>(s:set<T>) returns (x:T)
	requires s != {}
{
var z :| z in s;
return z;
}

function choose'<T>(s:set<T>):T
// function method choose'<T>(s:set<T>):T // Activate this line and comment the previous line to see the error
	requires s != {}
{
var z :| z in s;
z
}

Answer 1

In order for the Hilbert epsilon operator, also known in Dafny as the let-such-that expression,

var z :| P; E

to be compilable, the constraint P must determine z uniquely. In your case, the constraint P is z in s, which does not determine z uniquely except for singleton sets.

If s were of type set<int>, you can (inefficiently) live up to this requirement by changing your choose' function to:

function method choose'<T>(s:set<int>):int
  requires s != {}
{
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

Almost. You need to convince Dafny there is such a z. You can do that in a lemma. Here's a probably-longer-than-necessary-but-the-first-thing-I-got-working lemma that does that. Note that the lemma also uses the Hilbert operator, but in a statement context, so the uniqueness requirement does not apply.

function method choose'<T>(s:set<int>):int
  requires s != {}
{
  HasMinimum(s);
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

lemma HasMinimum(s: set<int>)
  requires s != {}
  ensures exists z :: z in s && forall y :: y in s ==> z <= y
{
  var z :| z in s;
  if s == {z} {
    // the mimimum of a singleton set is its only element
  } else if forall y :: y in s ==> z <= y {
    // we happened to pick the minimum of s
  } else {
    // s-{z} is a smaller, nonempty set and it has a minimum
    var s' := s - {z};
    HasMinimum(s');
    var z' :| z' in s' && forall y :: y in s' ==> z' <= y;
    // the minimum of s' is the same as the miminum of s
    forall y | y in s
      ensures z' <= y
    {
      if
      case y in s' =>
        assert z' <= y;  // because z' in minimum in s'
      case y == z =>
        var k :| k in s && k < z;  // because z is not minimum in s
        assert k in s';  // because k != z
    }
  }
}

Unfortunately, the type of your s is not set<int>. I don't know how to get a unique value from a general set. :(

For information about why the uniqueness requirement is important in compiled expressions see this paper.

Rustan