The problem is that the quantifier
forall i:int:: a!=i*c
has no matching trigger. A matching trigger is a term (that is, an expression) that gives the verifier a clue that a universal quantifier should be instantiated. For example, if (in
a precondition, say) you write a quantifier like
requires forall i :: 0 <= i ==> f(i) < 100
then you will be able to verify
assert f(20) + f(22) < 200;
This is because the verifier will use
f(_)
as the matching trigger for the quantifier, and then the presence of the terms
f(20)
and
f(22)
in the assertion will cause the quantifier to be instantiated with
i:=20
and with
i:=22
. As another example, if you tried to prove
assert f(-18) + f(22) < 200;
then the verifier will instantiate the quantifier with
i:=-18
and with
i:=22
, but the instantiation
i:=-18
does not give any information about
f(22)
, so the verifier will complain about not being able to verify the assertion.
Consider an example that involves another quantifier:
assert forall a,b :: 0 <= a && 0 <= b ==> f(a) + f(b) < 200;
Here, the verifier will consider an arbitrary
a
and
b
, and will be able to verify the body of the quantifier because it will instantiate the quantifier in the precondition with
i:=a
and with
i:=b
.
How did the verifier come up with the trigger
f(_)
in the first place? It looks in the body of the quantifier and tries to find expressions that involve the bound variable of the quantifier, like
f(i)
above. There are certain rules about what can be a trigger. Triggers cannot contain interpreted symbols, that is, boolean and arithmetic operators with a predefined meaning, like
+
,
&&
,
<=
, and
==
. In your example, the quantifier:
forall i :: a != i*c
has no subexpression that makes an allowable trigger. Therefore, you can’t even prove something as obvious as:
lemma Test0(a: int, c: int)
requires forall i :: a != i*c
{
assert forall i :: a != i*c; // error reported here
}
This is a problem with trying to prove properties that involve only built-in arithmetic and no user-defined functions. The solution is to introduce a(n uninterpreted) synonym for the built-in operation, here
*
. The following verifies:
function Mul(x: int, y: int): int { x * y }
lemma Test1(a: int, c: int)
requires forall i :: a != Mul(i,c)
{
assert forall i :: a != Mul(i,c);
}
In this example,
Mul(_,c)
gets picked as the matching trigger for the quantifier in the precondition, so when trying to prove
a != Mul(i,c)
for an arbitrary
I
in the assertion, the desired instantiation of the quantifier in the precondition takes places.
(There is actually a command-line option in Dafny that does this for you, namely
/noNLarith
. However, using this mode also disables more of non-linear arithmetic than you might like.)
I hope this explanation helps a bit. Do you mind if I post it on the Discussion board on dafny.codeplex.com?
Rustan
PS. There are other, more cryptic, workarounds, including the following:
function Id(x: int): int { x }
lemma Test2(a: int, c: int)
requires forall i :: a != Id(i)*c
{
assert forall i :: a != Id(i)*c;
}
predicate LookHere(i: int) { true }
lemma Test3(a: int, c: int)
requires forall i :: LookHere(i) && a != i*c
{
assert forall i :: LookHere(i) && a != i*c;
}