Have trouble understand the use of reveal_with_fuel in the fibo example

[KaminariOS]

use builtin::*;
use builtin_macros::*;
use vstd::{prelude::*, *};

verus! {

spec fn fibo(n: nat) -> nat
    decreases n,
{
    if n == 0 {
        0
    } else if n == 1 {
        1
    } else {
        fibo((n - 2) as nat) + fibo((n - 1) as nat)
    }
}

proof fn lemma_fibo_is_monotonic(i: nat, j: nat)
    requires
        i <= j,
    ensures
        fibo(i) <= fibo(j),
    decreases j - i,
{
    if i < 2 && j < 2 {
    } else if i == j {
    } else if i == j - 1 {
        reveal_with_fuel(fibo, 2);
        lemma_fibo_is_monotonic(i, (j - 1) as nat);
    } else {
        lemma_fibo_is_monotonic(i, (j - 1) as nat);
        lemma_fibo_is_monotonic(i, (j - 2) as nat);
    }
}

spec fn fibo_fits_u64(n: nat) -> bool {
    fibo(n) <= 0xffff_ffff_ffff_ffff
}

exec fn fibo_impl(n: u64) -> (result: u64)
    requires
        fibo_fits_u64(n as nat),
    ensures
        result == fibo(n as nat),
{
    if n == 0 {
        return 0;
    }
    let mut prev: u64 = 0;
    let mut cur: u64 = 1;
    let mut i: u64 = 1;
    while i < n
        invariant
            0 < i <= n,
            fibo_fits_u64(n as nat),
            fibo_fits_u64(i as nat),
            cur == fibo(i as nat),
            prev == fibo((i - 1) as nat),
    {
        i = i + 1;
        proof {
            lemma_fibo_is_monotonic(i as nat, n as nat);
        }
        let new_cur = cur + prev;
        prev = cur;
        cur = new_cur;
    }
    cur
}

fn main() {
}

}

Why reveal_with_fuel 2? Unfolding f(j) once gives f(j) = f(j - 1) + f(j - 2). How does unfolding help?

[utaal]

Dear @KaminariOS I recommend asking on Zulip for quicker responses: https://verus-lang.zulipchat.com/

[tjhance]

I recall discussing this same question before.

Verus proves this case as follows:

• From lemma_fibo_is_monotonic(i, (j - 1) as nat); we get that fibo(i) <= fibo(j-1).
• By a single unfolding, we also get fibo(j) == fibo(j-1) + fibo(j-2).
• By a second unfolding, we learn that fibo(j-2) is a nat, thus fibo(j-2) >= 0.

Putting these all together, we get fibo(i) <= fibo(j). Presumably, the confusing thing is the third bullet point; most people do not expect that an "unfolding" is required to deduce that fibo(j-2) is a nat.

We could consider changing this behavior; I don't think it's intentional.

[parno]

You don't actually need induction at all for this case. The proof also goes through if you replace

        reveal_with_fuel(fibo, 2);
        lemma_fibo_is_monotonic(i, (j - 1) as nat);

with

  assert(fibo(j) == fibo((j - 2) as nat) + fibo((j - 1) as nat)

which also seems magical (not in a good way). Since we have i == j - 1, substitution gives:

  assert(fibo(j) == fibo((j - 2) as nat) + fibo(i as nat)

and presumably having fibo((j - 2) as nat) to trigger on tells us that the result is a nat; it does seem like that should come in automatically though.