Failure to Prove Existential with Subsequence

[whonore]

Dafny version

4.4.0

Code to produce this issue

lemma Test<T>(xs: seq<T>, n: nat, P: seq<T> -> bool)
  ensures exists idx: nat :: idx <= |xs| - n && P(xs[idx..idx + n])
{
  assume exists idx: nat :: idx <= |xs| - n && P(xs[idx..idx + n]);
}

Command to run and resulting output

$ dafny verify Test.dfy
Test.dfy(2,10): Warning: /!\ No terms found to trigger on.
  |
2 |   ensures exists idx: nat :: idx <= |xs| - n && P(xs[idx..idx + n])
  |           ^^^^^^

Test.dfy(4,9): Warning: /!\ No terms found to trigger on.
  |
4 |   assume exists idx: nat :: idx <= |xs| - n && P(xs[idx..idx + n]);
  |          ^^^^^^

Test.dfy(3,0): Error: a postcondition could not be proved on this return path
  |
3 | {
  | ^

Test.dfy(2,10): Related location: this is the postcondition that could not be proved
  |
2 |   ensures exists idx: nat :: idx <= |xs| - n && P(xs[idx..idx + n])
  |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 1 verified, 1 error

What happened?

While trying to prove the existence of a subsequence with some property, I found that Dafny couldn't verify the postcondition even when I assumed it. Of course, in the simplified example above, P may not hold for any subsequence, but it shouldn't matter since the body of the lemma assumes it does.

I tried several of the tricks with triggers suggested in #2721, but I couldn't find one that helped.

What type of operating system are you experiencing the problem on?

Linux

[MikaelMayer]

In general, it's better for dafny if anything after the "::" of an exists formula is inside a predicate. That way Dafny knows that, to prove the existence, it just needs to find values that satisfies this predicate application. A predicate application is an excellent trigger for Dafny as it's non ambiguous.

So the following works and is also usable and more deterministic because the trigger is obvious for Dafny

predicate BetterShape<T>(idx: nat, xs: seq<T>, n: nat, P: seq<T> -> bool)
{
  idx <= |xs| - n && P(xs[idx..idx + n])
}

lemma Test<T>(xs: seq<T>, n: nat, P: seq<T> -> bool)
  ensures exists idx: nat :: BetterShape(idx, xs, n, P)
{
  assume exists idx: nat :: BetterShape(idx, xs, n, P);
}

[whonore]

Thanks, that’s good to know. The predicate trick works for the thing I was actually trying to prove, but I’m still surprised that triggers matter at all in this example. Shouldn't assume X always be enough to prove ensures X regardless of what X is?

[keyboardDrummer]

A predicate application is an excellent trigger for Dafny as it's non ambiguous.

What do you mean by non-ambiguous on this context?

Shouldn't assume X always be enough to prove ensures X regardless of what X is?

That surprises me as well, but I guess for quantifiers this doesn't hold because I think quantifiers are only useable when their trigger is found, and in your problematic example, Dafny did not add any triggers to the quantifier in the assume clause so in effect it becomes unusable.

That said, I don't know how to add the right triggers to get your original example to work. I would have hoped this would work but it doesn't:

lemma Test<T>(xs: seq<T>, n: nat, P: seq<T> -> bool)
  ensures exists idx: nat :: idx <= |xs| - n && P(xs[idx..idx + n])
{
  assume exists idx: nat {:trigger P(xs[idx..idx + n])} :: idx <= |xs| - n && P(xs[idx..idx + n]);
  var idx: nat :| idx <= |xs| - n && P(xs[idx..idx + n]);
}

@MikaelMayer besides the predicate workaround you gave, could you explain why the original code, and the one with triggers added, does not work?

[MikaelMayer]

By non-ambiguous, I mean it's obvious what the trigger should be. Complex expressions can have non-trivial triggers which I call ambiguous, because there could be several possible triggers.
Let me try my best to answer your last question because it's a very interesting one.

Z3 has its own sets of triggers and, if Dafny does not specify triggers, Z3 might still be able to detect patterns and prove things. But Z3's mechanism is not dependable enough for Dafny's needs, so Dafny prefers to generate triggers when possible.

Originally the triggers were written by hand, but because triggers generally followed rules of thumb that were pretty straightforward, their detection is now mostly automatic.

• A trigger is a collection of expressions
• All bound variables must appear at least once in one expression of the trigger
• The matching can be done only on non-interpreted symbols besides bound variables (so + - don't make triggers unless arithmetic symbols are uninterpreted)

The expression xs[idx..idx + n] contains idx in a position that cannot be matched: idx + n because '+' is interpreted (meaning it's assigned a meaning immediately other than axioms Dafny provides). I don't know what it is preventing us really, looks like a z3 limitation.

Other solutions include:

• Introducing an auxiliary variable so that the trigger xs[idx..idxn] does not contain interpreted symbols:

lemma Test<T>(xs: seq<T>, n: nat, P: seq<T> -> bool)
  ensures exists idx: nat, idxn: nat :: idxn == idx + n <= |xs| && P(xs[idx..idxn])
{
  assume exists idx: nat, idxn: nat :: idxn == idx + n <= |xs| && P(xs[idx..idxn]);
  var idx: nat, idxn: nat :| idxn == idx + n && idx <= |xs| - n && P(xs[idx..idxn]);
}

• Adding an uninterpreted function that replaces the '+':

function plus(idx: nat, n: nat): nat { idx + n }

lemma Test<T>(xs: seq<T>, n: nat, P: seq<T> -> bool)
  ensures exists idx: nat :: idx <= |xs| - n && P(xs[idx..plus(idx, n)])
{
  assume exists idx: nat :: idx <= |xs| - n && P(xs[idx..plus(idx, n)]);
  var idx: nat :| idx <= |xs| - n && P(xs[idx..plus(idx, n)]);
}

Hope it helps!

[keyboardDrummer]

The expression xs[idx..idx + n] contains idx in a position that cannot be matched

That's good info and it answers my question. I made a related issue: #4958 could you check if that makes sense?

Other solutions include:

Thanks! These provide good clarifications.

[keyboardDrummer]

Thanks, that’s good to know. The predicate trick works for the thing I was actually trying to prove, but I’m still surprised that triggers matter at all in this example. Shouldn't assume X always be enough to prove ensures X regardless of what X is?

I think in the case of quantifiers, you should see

assume X as assume IfTriggerMatches => X

while assert X just remains that.

@RustanLeino would it be possible to automatically introduce names for quantifiers so that the expectation that assume X; assert X always works, holds?

[RustanLeino]

Shouldn't assume X always be enough to prove ensures X regardless of what X is?

This is true only if quantifiers in X have triggers. In the example, Dafny cannot find a good trigger, so it reports a warning about that.

The various alternative formulations that @MikaelMayer showed are good. Here is one more that works in this case (it works by removing the + from the only subexpression that mentions idx):

lemma Test<T>(xs: seq<T>, n: nat, P: seq<T> -> bool)
  ensures exists idx: nat :: idx <= |xs| - n && P(xs[idx..][..n])
{
  assume exists idx: nat :: idx <= |xs| - n && P(xs[idx..][..n]);
}

Rather than having an ensures exists idx ..., it is often better to return that idx from the lemma or method. This avoids the exists in the first place (and is usually easier for the caller of the lemma, anyhow; plus, it often does not make the proof of the lemma any more complicated, as long as there's an assignment to the out-parameter idx).

The strategy of introducing a name for the entire body (BetterShape above) is most likely to work. More specifically, using such a name may in some cases reduce automation, but it makes sure you can do a manual proof. Along the lines of what @keyboardDrummer suggests, I have many times wanted to have a facility to manually name the quantifier, so that I could get the effect of BetterShape, but without having to introduce a separate function. Perhaps something like BetterShape: exists idx .... (If such names were always introduced instead of current trigger selection, then I think many users would be disappointed, because the triggering patterns often pick up on other terms that are part of the verification context.) In addition to the syntax of such a feature, one needs to design what the "precondition" of such the function introduced by the name is.

[keyboardDrummer]

I've changed the bug label into enhancement. It seems there's an opportunity to improve either documentation or error reporting, although how exactly does not seem obvious.