Dafny Power User:

Calling Lemmas Automatically

Calling Lemmas Automatically

**Abstract.** Some properties of a function are more useful than others. If you have proved such a
property as a lemma, you may want to have it be applied automatically. This note
considers ways to achieve something like that in Dafny.

On https://github.com/Microsoft/dafny/issues/231, a Dafny user asked:

Is there a way in Dafny to mark a lemma as “automatic” and add it to the knowledge base of z3 ?

For student homeworks, we often stumble on specifications that are just a bit too complex for Dafny to prove, and require some hand-crafted asserts or lemmas.

It would be nice if we could define those lemmas to augment boogie/z3 search space with domain-specific knowledge, avoiding the need to explain to our students how lemmas work, and the tedious and difficult task to find and use the required lemmas.

Is something like an {:auto} annotation feasible ? Can we augment the .bpl axiomatization ?

Here is an example that shows the issue. Suppose you declare a function and prove a property about it:

```
function FibFib(n: nat): nat {
if n == 0 then 0
else if n == 1 then 2
else FibFib(n-2) + FibFib(n-1)
}
lemma FibFibIsEven(n: nat)
ensures FibFib(n) % 2 == 0
{
// automatically proved by induction
}
```

For your application, it may be crucial that `FibFib`

always returns an even number. Using the declarations
above, you would then have to call the lemma `FibFibIsEven`

every time you use the function.
This is tedious. Is there some way to instruct Dafny to automatically apply `FibFibIsEven`

whenever
it's needed?

No, there's no such feature in Dafny. (VCC had such a feature, for example.) In some situations, such automation may work well. In other situations, it may cause the lemma to be invoked too many times (say, an infinite number of times), which is problematic.

If you have an interest in trying out some kind of `{:autoLemma}`

feature,
please feel free to play around with the open Dafny sources. In the present
state, I have four suggestions that you may try, and which may alleviate some
of the tedium you're experiencing.

One suggestion is to create an “uber lemma” that collects the statements of several other lemmas. For example, if you already have:

```
lemma Lemma0(x: X) ensures P0(x) { ... }
lemma Lemma1(x: X) ensures P1(x) { ... }
lemma Lemma2(x: X) ensures P2(x) { ... }
```

then you can combine them into one:

```
lemma Everything(x: X)
ensures P0(x) && P1(x) && P2(x)
{
Lemma0(x: X);
Lemma1(x: X);
Lemma2(x: X);
}
```

This lets you get all 3 properties by calling a single lemma.

Another suggestion is to invoke a lemma on many values at the same time. Given:

`lemma LemmaForOneX(x: X) ensures P(x) { ... }`

you can invoke this lemma for all values of `X`

simultaneously:

```
forall x {
LemmaForOneX(x);
}
```

By placing this `forall`

statement at the beginning of some code you're trying to prove, you have in effect called it for every imaginable value of `X`

. You can of course also tuck this statement into a lemma of its own and then call this one lemma:

```
lemma LemmaForEveryX()
ensures forall x :: P(x)
{
forall x {
LemmaForOneX(x);
}
}
```

In many cases, this will work fine. In other cases, the verifier may not realize that you have called the lemma on the value that needs the individual lemma, so you may still need to invoke `LemmaForOneX`

manually. Also, Dafny takes measure to avoid “matching loops” in the quantifiers generated for the lemma calls above (“matching loops” are what can cause an infinite number of uses of the lemmas). However, the mechanism is not perfect, so this added automation may in some cases cause degraded performance.

A third suggestion is to declare some of the most useful properties of a function in the postcondition of the function, rather than in a separate lemma. For example, instead of:

```
function F(x: X): int { ... }
lemma AboutF(x: X)
ensures F(x) % 2 == 0
{ ... }
```

you can declare:

```
function F(x: X): int
ensures F(x) % 2 == 0
{ ... }
```

To obtain the property stated by the lemma, you must call the lemma. In contrast, any property stated in the postcondition of a function is automatically applied every time you call the function.

As I've mentioned, more information can help the verifier do more things automatically, but too much information can also overwhelm and confuse the verifier. Therefore, my suggestion is to use function postconditions only for those properties that you think every user of the function will need. Properties needed more rarely are better off declared in lemmas that have to be manually invoked.

Also, there are limits to what you can write in a function postcondition. In particular, what you write must “terminate”. In practice, this means you may have problems mentioning the function applied to other arguments in the postcondition. For example,

```
predicate R(x: X, y: X)
// commutativity:
ensures R(x, y) <==> R(y, x)
// transitivity:
ensures forall z :: R(x, z) && R(z, y) ==> R(x, y)
```

is not admitted, because there are self-referential non-terminating (that is, infinitely recursive) calls in the postcondition. Thus, properties like commutativity and transitivity always need to be stated as separate lemmas.

A function postcondition conveniently provides all users of a function with
the property that it states, alleviating the need to call the lemma explicitly.
If the property is not interesting for all users, a fourth suggestion is to
declare two functions. The *basic* function gives the actual definition of
the function and an accompanying lemma states the property about it.
The *premium* function calls the basic function and states the property as
its postcondition, which is proved by a call to the lemma.

```
function F(x: X): int { ... }
lemma AboutF(x: X)
ensures F(x) % 2 == 0
{ ... }
function F_premium(x: X): int
ensures F_premium(x) % 2 == 0
{ AboutF(x); F(x) }
```

Users can now choose: a call to `F_premium`

obtains both the value of the
function and the proved property, whereas a call to `F`

obtains only the value.
If you expect the
premium version to be more popular than the basic version, you can of course
rename `F`

and `F_premium`

to `F_basic`

and `F`

, respectively.

Other than the postcondition, the two functions are synonyms. Semantically. A note of caution is that the mechanism the verifier uses as a guide to its use of quantifiers is syntactic. Therefore, which of the two functions you use in the body of a quantifier can make a difference in when the verifier decides to instantiate the quantifier. For this reason, I suggest you use the basic version of the function inside any quantifier you write.

Bryan Parno provided the fourth suggestion of wrapping a basic version of a function and its lemma into a premium version of the function.