Sequence membership versus sequence indexing

[RustanLeino]

Given that every element in a sequence s is 3, Dafny is able to automatically prove s[k] == 3, right?

Not always. 😒

If you express the 3-everywhere property by a quantifier over the index, then it works:

method M0(s: seq<int>, k: int)
  requires forall i :: 0 <= i < |s| ==> s[i] == 3
  requires 0 <= k < |s|
{
  assert s[k] == 3;
}

But if you don't care about the index and you just want to express the 3-everywhere property in terms of each member of the sequence, then Dafny won't prove the property automatically:

method M1(s: seq<int>, k: int)
  requires forall x :: x in s ==> x == 3
  requires 0 <= k < |s|
{
  assert s[k] == 3; // error: not proved automatically
}

The reason is that the expression x in s is represented this way in the verifier, and Dafny's axioms (can construct a s[_] term from a _ in s term, but) never construct a _ in s term from a s[_] term. Dafny picks x in s as the trigger for the quantifier in M1's precondition. But the rest of M1 does not have any _ in s expressions, and therefore the quantifier never gets used.

There are two ways around this in Dafny today. One is to rewrite the quantifier in M1 into the logically equivalent quantifier used by M0. This is slightly annoying, because it forces the program to mention the index i, which in this example is not otherwise needed. The other way around the problem is to give the verifier the hint s[k] in s:

method M2(s: seq<int>, k: int)
  requires forall x :: x in s ==> x == 3
  requires 0 <= k < |s|
{
  assert s[k] in s; // with this hint, the next line verifies
  assert s[k] == 3;
}

This works, because, if asked, Dafny can prove that s[k] in s holds, and then the s[k] in the final assertion is known to be in s, so the quantifier in the precondition will trigger. But this is also annoying, because the property s[k] is s seems so trivial.

I think we should fix this problem, because many users are running into it and it's annoying.

Candidate solution

There are several possible solutions. Determining which one works best may require some exprimentation. My hunch is that the following may be a good solution:

For any given quantifier

forall x :: ...x...

if Dafny picks out a trigger x in s for some expression s denoting a sequence, then Dafny will automatically replace the given quantifier by the rewrite

forall i :: 0 <= i < |s| ==> ...s[i]...

and will then recompute triggers for this quantifier.

Notes:

• An implementation detail: I explained the suggested solution above as a Dafny-expression rewrite. However, if formulated as such, the rewrite may not be legal Dafny. To illustrate, consider

  function PId(s: seq<int>): seq<int>  // partial identity function
    requires |s| == 100
  {
    s
  }
  method R(s: seq<int>)
    requires forall x :: |s| == 100 && x in PId(s) ==> x == 3

  For this quantifier, Dafny picks out the trigger x in PId(s). Taking my suggestion above literally, the rewrite would then turn the precondition into

  requires forall i :: 0 <= i < |PId(s)| ==> |s| == 100 && PId(s)[i] in PId(s) ==> PId(s)[i] == 3

  But this Dafny expression is not well-formed -- the first occurrence of PId(s) violates the precondition of PId.

  So, the rewrite should be done in such a way that antecedent 0 <= i < |s| is admitted without well-formedness checks. (This can be done by calling TrExpr on the expression s and then wrapping the result in a BoogieWrapper node, or by introducing some other kind of wrapping mechanism.)

• An analogous rewrite would be done for existential quantifiers and (set and map) comprehensions.

• A decision decision should be made about whether to always apply this rewrite if x in s is a trigger of the original expression or to apply it only when x in s is the only trigger.

[cpitclaudel]

The proposed rewrite makes sense to me, but it's a bit scary to introduce explicit indices where there were none. Would it break lots of stuff to add an axiom for this?

That is, maybe we could change this:

axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
  Seq#Contains(s,x) <==>
    (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));

to something like this?

axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
  Seq#Contains(s,x) ==>
    (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
axiom (forall<T> s: Seq T, i: int :: { Seq#Index(s,i) }
  (0 <= i && i < Seq#Length(s)) ==>
  Seq#Contains(s, Seq#Index(s,i)));