forall and proving universals

May 4, 2015 at 10:04 AM
Edited May 4, 2015 at 10:06 AM
I am trying to understand how to persuade Dafny of
universal statements that it is unable to prove.
I would have thought that the following should
work, but it does not. When I leave the ensures clause off
Dafny suggests that I should add the ensures clause, but
even with that in place it fails to accept what should be
a perfectly good proof.
lemma alltest(A:seq<int>)
  {forall (q:nat) 
      ensures forall q:nat :: q<|A| ==> A[q] ==1;
      {assume q<|A| ==> A[q]==1;}
   assert forall q:nat :: q<|A| ==> A[q] ==1;
    }
Part of my problem is that there is no real documentation that
I can find for the forall loop statement. It would be good if the
lemmas section of the tutorial could be expanded to include that.
At the moment the focus is entirely on induction.

I can get the proof to go through through using a while loop and an invariant,
but that seems like a using a sledgehammer to crack a nut, and it
becomes particularly cumbersome when dealing with quantifications
over more than one variable.

Ron
May 4, 2015 at 11:30 AM

http://www.lexicalscope.com/blog/2014/07/31/dafny-proving-forall-x-px-qx/

May 5, 2015 at 8:02 PM
Hi Ron,

The problem is that your ensures clause introduces yet another q. Without it, everything verifies:
lemma alltest(A:seq<int>)
{
  forall q:nat
    ensures q<|A| ==> A[q] ==1
  {
    assume q<|A| ==> A[q]==1;
  }
  assert forall q:nat :: q<|A| ==> A[q] ==1;
}
We are writing a comprehensive reference manual for Dafny. For now, here are some notes on the forall statement.

The forall statement is a aggregate statement. As such, it performs its body for each of values specified by the bound variables. The body instantiations are performed simultaneously; more precisely, all reads precede writes. The syntax is as follows (shown here with two bound variables):
forall x: T, y: U | R(x,y,z)
  ensures P(x,y,z)
{
  Body
}
The types T and U can be omitted if they can be inferred. R(x,y,z) is a boolean expression; if | R(x,y,z) is omitted, the expression defaults to true. Optionally, x: T, y: U | R(x,y,z) can be enclosed in parentheses. As a degenerate case, the statement allows no bound variables (and, in that case, no | R(x,y,z)), which is sometimes useful to hide the proof of the ensures condition (in the future, I plan to introduce a version of the assert statement that does this instead). P(x,y,z) is a boolean expression. Multiple ensures clauses have the same effect as conjoining their conditions. Body is a list of statements.

There are two basic version of the forall statement, one executable and one ghost.

In the executable version of the forall statement, ensures clauses are not allowed and the Body must be one assignment statement. Note that the forall statement is not a loop. In particular, no loop invariant is required to reason about it. However, the forall statement can perform the duties of simple loops. For example, the following forall statement initializes all elements of a real matrix:
forall i, j | 0 <= i < m.Length0 && 0 <= j < m.Length1 {
  m[i,j] := 0.0;
}
Reads are performed before writes, so the following forall statement rotates the elements of an array:
forall i | 0 <= i < a.Length {
  a[i] := a[(i + 1) % a.Length];
}
Just like in multiple-assignment statements, the left-hand sides of the various body instantiations must denote different l-values (unless the corresponding right-hand sides are equal). In the executable version of the forall statement, range expression R(x,y,z) combined with the types of the bound variables must be within a finite range, thus ensuring that the forall statement will terminate.

The ghost version of the forall statement corresponds to the logic rule of "universal introduction": by proving a property P(x) for an arbitrary x, one obtains the universally quantified fact forall x :: P(x). Here, the Body can be any list of (ghost) statements that lead to the verification of the given ensures conditions. If the Body consists of a single lemma call and the ensures clause of the forall statement is omitted, then Dafny automatically uses the lemma's ensures clauses as the ensures clauses of the forall statement. Similarly, if Body consists of a single calc statement and the ensures clause is omitted, then Dafny will use the conclusion of the calc statement (that is, its first line connected with its last line) as the ensures condition.

I hope this explanation will help.

Program safely,
Rustan
May 11, 2015 at 4:58 AM
Thanks, thats very helpful!