Why is Dafny not able to prove this lemma by induction?

[Meijster]

Hi, we (CS programme at university of Groningen, Netherlands) have decided to use Dafny in our education, and I am busy making exercises for our students.

I stumbled into the following. I wanted to prove the simple property that n^3 + 2*n is divisible by 3 for all natural numbers n.

I wrote the following:

lemma {:induction false} manualDiv3property(n: nat) 
  ensures (n*n*n + 2*n) % 3 == 0
{
    if (n==0) {
        // No body needed, Dafny is able to proof this automatically
    } else {
       manualDiv3property(n-1);
       calc {
        n*n*n + 2*n;
        (n-1)*(n-1)*(n-1) + 3*n*n - n + 1;
        (n-1)*(n-1)*(n-1) + 2*(n-1) + 3*n*n - 3*n + 3;
        (n-1)*(n-1)*(n-1) + 2*(n-1) + 3*(n*n - n + 1);
       }
    }
}

So, basically I wrote the majority of the proof by hand , and used Dafny to make sure I did not make calculational mistakes. That works perfectly!

However, I expected the following to work too (removed induction:false):

lemma autoDiv3property(n: nat) 
  ensures (n*n*n + 2*n) % 3 == 0
{
    if (n==0) {
        // No body needed, Dafny is able to proof this automatically
    } else {
       // autoDiv3property(n-1);
       calc {
        n*n*n + 2*n;
        (n-1)*(n-1)*(n-1) + 3*n*n - n + 1;
        (n-1)*(n-1)*(n-1) + 2*(n-1) + 3*n*n - 3*n + 3;
        (n-1)*(n-1)*(n-1) + 2*(n-1) + 3*(n*n - n + 1);
       }
    }
}

Now, it turns out that Dafny cannot prove the lemma. However, if I uncomment the line // autoDiv3property(n-1); it works again. Isn't that the default induction that Dafny should perform in automatic mode?

BTW: I am using Dafny 4.2 (but I don't think that matters).

[MikaelMayer]

I'm not very satisfied by my answer, but I looked at the generated boogie code using --bprint:file.bpl, and what I can tell you is that it emits the recurrence hypothesis if it can find in the lemma's body an instance of the predicate to prove with a value potentially less than the current argument. So the following can be proven:

predicate property(n: nat) {
  (n*n*n + 2*n) % 3 == 0 &&
  if n == 0 then
    true
  else
    property(n - 1)
}

lemma autoDiv3property(n: nat) 
  ensures property(n)
{
    if (n==0) {
        // No body needed, Dafny is able to proof this automatically
    } else {
       var _ := property(n-1); // Just mentioning this term makes it works.
       calc {
        n*n*n + 2*n;
        (n-1)*(n-1)*(n-1) + 3*n*n - n + 1;
        (n-1)*(n-1)*(n-1) + 2*(n-1) + 3*n*n - 3*n + 3;
        (n-1)*(n-1)*(n-1) + 2*(n-1) + 3*(n*n - n + 1);
       }
    }
}

I'm not totally satisfied by this answer because for other functions it works just because the function itself contains a recursive call and there it works. but I thought I would share with you this insight, as it's quite time-consuming to make experiments. Hope it helps.