Question

A function seems to work just once. How do I get it to apply a bunch of times? Here is an example:

function Sum(s: seq<nat>): nat {
  if |s| == 0 then 0
  else s[0] + Sum(s[1..])
}

lemma Sum1(s: seq<nat>)
  requires |s| == 1
  ensures Sum(s) == s[0]
{
  // trivial
}

lemma Sum2(s: seq<nat>)
  requires |s| == 2
  ensures Sum(s) == s[0] + s[1]
{
  // Doesn't work.  I need...
  // Sum1(s[1..]);
}

lemma Sum3(s: seq<nat>)
  requires |s| == 3
  ensures Sum(s) == s[0] + s[1] + s[2]
{
  // Doesn't work.  I need...
  // Sum2(s[1..]);
}

The latter two lemmas will not prove without uncommenting the application of the lemma for one less iteration. How can I get this to prove automatically?

Answer

Function bodies are transparent. That is, when there is a call to a function in Dafny code, the body of the function is available for reasoning about the effect of the function. But for recursive functions, it generally only does this once or twice, as that is usually sufficient to form an inductive proof. And always unrolling multiple times can reduce performance.

You can request that Dafny unroll a function multiple times by using the {:fuel} attribute. The value of the attribute is the number of times the function will be unrolled. This is still a fixed upper limit, but it does the trick in this case:

function {:fuel 10} Sum(s: seq<nat>): nat {
  if |s| == 0 then 0
  else s[0] + Sum(s[1..])
}

lemma Sum1(s: seq<nat>)
  requires |s| == 1
  ensures Sum(s) == s[0]
{
  // trivial
}

lemma Sum2(s: seq<nat>)
  requires |s| == 2
  ensures Sum(s) == s[0] + s[1]
{
  // Doesn't work.  I need...
  // Sum1(s[1..]);
}

lemma Sum3(s: seq<nat>)
  requires |s| == 3
  ensures Sum(s) == s[0] + s[1] + s[2]
{
  // Doesn't work.  I need...
  // Sum2(s[1..]);
}

A function will also keep unrolling if it has an argument that is a literal and that argument decreases on each recursive call. So for this example we can write a helper function that takes a nat argument and give it a literal value that tells it how much to unroll.

function Sum(s: seq<nat>): nat {
  if |s| == 0 then 0
  else s[0] + Sum(s[1..])
}

function Sum_(s: seq<nat>, n: nat): nat
  ensures Sum(s) == Sum_(s,n)
  ensures |s| > 0 && n > 0 ==> Sum_(s,n) == s[0] + Sum_(s[1..], n-1)
{
  if |s| == 0 || n == 0 then Sum(s)
  else s[0] + Sum_(s[1..], n-1)
}

lemma Sum1(s: seq<nat>)
  requires |s| == 1
  ensures Sum(s) == s[0]
{
  // trivial
}

lemma Sum3(s: seq<nat>)
  requires |s| == 3
  ensures Sum(s) == s[0] + s[1] + s[2]
{
  var _ := Sum_(s, 3);
}

lemma Sum9(s: seq<nat>)
  requires |s| == 9
  ensures Sum(s) == s[0] + s[1] + s[2] + s[3] + s[4] + s[5] + s[6] + s[7] + s[8]
{
  var _ := Sum_(s, 9);
}

With this solution, the number of unrollings can be set at the call site, rather than in the function definition.

This paper gives some technical insight into how recursive functions are handled in situations like these examples.