Requiring to assert a[0] in a

Question

I'm currently learning dafny and ran into a really odd assertion requirement:

method M (a : seq<int>, acc : seq<int>) 
  requires |a| > 0
  requires forall va, vacc :: va in a && vacc in acc ==> vacc <= va
{
  assert forall vacc :: vacc in acc ==> vacc <= a[0];
}

The above code fails on the assertion, however if I add assert a[0] in a it verifies?

Why is this the case, surely in all circumstances that |a| > 0 a[0] in a holds since seq is immutable?

(also any style guide recommendations would be appreciated :) )

score 1 · Accepted Answer · answered Nov 12 '20 at 17:29

1

This has to do with "triggers".

The short answer is that until you manually "mention" a[0], Dafny will not be able to take advantage of the quantified requires clause. It does not matter how you mention a[0], just that you mention it. That is why your trivial assertion works even though it doesn't seem to add anything logically: it's just because it mentions a[0].

For more information, see:

the FAQ qustion
this answer "what are triggers?"
this answer about "no terms found to trigger on"

answered Nov 12 '20 at 17:29

James Wilcox

5,307
16
25

Brilliant thanks! Are there any good herustics for when this may be an issue? – Cjen1 Nov 12 '20 at 20:07
1

It will basically always be an issue whenever you have a `forall` fact that you need to take advantage of. It also happens any time you're trying to *prove* an `exists` fact. – James Wilcox Nov 13 '20 at 00:19

Requiring to assert a[0] in a

1 Answers1