[SOLVED] Why this dafny post-condition is not inferred?

Why this dafny post-condition is not inferred?

I have proved some purely existential lemmas (with no out-results) in a similar constructive way to this one:

lemma DivModExistsUnique_Lemma (x:nat, y:nat)  
requires y != 0
ensures exists q:nat, r:nat :: x == y*q + r &&  r < y 
{
var q:nat, r:nat := 0, x;
while r >= y 
  invariant x == y*q + r
  {
  q := q + 1;
  r := r - y;
  }
assert x == y*q + r &&  r < y;
}

I can’t think why this post-condition is not inferred from the last assertion in the proof.

There is some additional hint that can be given to Dafny?

Solution

Nice proof! The problem is that the quantifier in the postcondition has no "matching pattern" (also known as "trigger") that involves r. Dafny gives a warning about this. So what does that mean?

To prove an existential quantifier, the verifier attempts to find a witness. In searching for a witness, the verifier is not going to try every possible term in mathematics, and it's not even going to try every term that appears elsewhere in your program. Instead, the verifier limits its attention to terms that both appear elsewhere in the proof context and have the shape of a "matching pattern" for the quantifier. In the Dafny IDE (VS Code or Emacs), you can place the cursor over the quantifier and the IDE will show you the triggers that Dafny selected. (Again, in your case, it will instead say "No triggers".)

There are certain rules about what triggers can and cannot be (see the Dafny FAQ or many answered questions on StackOverflow). For q, the verifier will select the term y*q as the trigger. It is allowed, because Dafny allows * to appear in triggers. However, the only possibly useful triggers for r would be ... + r and r < ..., neither of which is allowed because triggers are not allowed to mention + or <. Therefore, Dafny finds no trigger for the quantifier, which essentially means that it will never find witnesses that prove the existential quantifier.

To work around this problem, you can introduce a function that involves the quantified variables. For example,

function MulAdd(a: nat, b: nat, c: nat): nat {
  a*b + c
}

lemma DivModExistsUnique_Lemma(x:nat, y:nat)  
  requires y != 0
  ensures exists q:nat, r:nat :: x == MulAdd(y, q, r) && r < y
{
  var q:nat, r:nat := 0, x;
  while r >= y 
    invariant x == MulAdd(y, q, r)
  {
    q := q + 1;
    r := r - y;
  }
}

will prove your program. The IDE will then also show you that Mul(y, q, r) is selected as a trigger.

Quantifiers without triggers tend to be ones that only use "built-in symbols" like + and < and &&. When your problems have other functions, the verifier can usually find triggers.

For your proof, the most elegant solution to my taste is to use lemma out-parameters. That means the lemma can just "return" the q and r it computes. It also makes the lemma easier to use, because the caller of the lemma would otherwise typically need to Skolemize the quantifier (which you do in Dafny with the assign-such-that operator :| -- which also involves triggers, by the way). But you said you're (for some reason) trying to avoid out-parameters. If so, then the MulAdd function will do the trick.