Two quantifiers in a specification

Let’s consider a Dafny lemma that involves two quantifiers in its specification. For example, we want to prove the following lemma:

// Test predicate
ghost predicate P(a: seq<int>, x: int, y: int)
{
    (0 <= x < |a| && 0 <= y < |a|) ==> a[x] < a[y]
}

lemma test1(a: seq<int>)
    requires forall x :: (exists y :: P(a, x, y))
    ensures forall x :: (exists y :: P(a, x, y))
{
    // not proved
    // Dafny can't find the trigger for `x`
}

lemma test2(a: seq<int>)
    requires exists x :: (forall y :: P(a, x, y))
    ensures exists x :: (forall y :: P(a, x, y))
{

    // not proved
    // same issue as test1
}

In both test1 and test2, Dafny fails to prove the lemmas because it cannot find appropriate triggers for the quantifiers.

And what is a trigger?

See Dafny Reference Manual on {:trigger}.

Trigger attributes are used on quantifiers and comprehensions.

The verifier instantiates the body of a quantified expression only when it can find an expression that matches the provided trigger.

predicate P(i: int)
predicate Q(i: int)

lemma {:axiom} PHoldEvenly()
  ensures  forall i {:trigger Q(i)} :: P(i) ==> P(i + 2) && Q(i)

lemma PHoldsForTwo()
  ensures forall i :: P(i) ==> P(i + 4)
{
  forall j: int
    ensures P(j) ==> P(j + 4)
  {
    if P(j) {
      assert P(j); // Trivial assertion
      
      PHoldEvenly();
      // Invoking the lemma assumes `forall i :: P(i) ==> P(i + 4)`,
      // but it's not instantiated yet
      
      // The verifier sees `Q(j)`, so it instantiates
      // `forall i :: P(i) ==> P(i + 4)` with `j`
      // and we get the axiom `P(j) ==> P(j + 2) && Q(j)`
      assert Q(j);     // hence it can prove `Q(j)`
      assert P(j + 2); //   and it can prove `P(j + 2)`
      assert P(j + 4); // But it cannot prove this
      // because it did not instantiate `forall i :: P(i) ==> P(i + 4)` with `j+2`
    }
  }
}

Here are ways one can prove assert P(j + 4);:

• Add assert Q(j + 2); just before assert P(j + 4);, so that the verifier sees the trigger.
• Change the trigger {:trigger Q(i)} to {:trigger P(i)} (replace the trigger).
• Change the trigger {:trigger Q(i)} to {:trigger Q(i)} {:trigger P(i)} (add a trigger).
• Remove {:trigger Q(i)} so that it will automatically determine all possible triggers thanks to the option /autoTriggers:1 which is the default.

Nested loops

See Dafny Reference Manual on Nested loops.

In the case of nested loops, the verifier might timeout sometimes because of inadequate or too much available information. One way to mitigate this problem, when it happens, is to isolate the inner loop by refactoring it into a separate method, with suitable pre and postconditions that will usually assume and prove the invariant again. For example,

while X
  invariant Y
{
    while X'
      invariant Y'
    {

    }
}

could be refactored as this:

while X
   invariant Y
 {
   innerLoop();
 }
...
method innerLoop()
  require Y'
  ensures Y'

My findings

I think the main issue can be the Skolemization of the quantifiers.

Skolemization: \(\forall x \exists y R(x,y) \Leftrightarrow \forall x R(x,f(x))\), here \(f\) is a Skolem function.

In test1, after Skolemization:

• the requirement becomes: \(\forall x P(a, x, f(x))\).
• the ensures becomes: \(\forall x P(a, x, g(x))\).
• Dafny cannot find the relation between f and g, so it cannot prove the lemma.

In test2, after Skolemization:

• the requirement becomes: \(P(a, h, y)\).
• the ensures becomes: \(P(a, k, y)\).
• Similarly, Dafny cannot find the relation between h and k, so it cannot prove the lemma.

And based on this understanding, I tried to prove two quantifers of \(\forall x \forall y\) and \(\exists x \exists y\), and Dafny can prove them successfully.

lemma test1(a: seq<int>)
    requires forall x :: (forall y :: P(a, x, y))
    ensures forall x :: (forall y :: P(a, x, y))
{
    // proved
}

lemma test2(a: seq<int>)
    requires exists x :: (exists y :: P(a, x, y))
    ensures exists x :: (exists y :: P(a, x, y))
{
    // proved
}