Verus fails to verify sum additivity for Seq<i32>

[WeetHet]

I'm trying to prove that the subarray sum is additive, as in sum(a[l..m]) + sum(a[m..r]) == sum(a[l..r]), but verus fails to verify it:

use vstd::prelude::*;

verus! { fn main() {} }

verus! {

proof fn sum_is_additive(a: Seq<i32>) {
    assert(
        forall|l: int, m: int, r: int| #![auto] 0 <= l <= m <= r <= a.len() ==>
            a.subrange(l, m).fold_left(0, |s: int, v| s + v)
            + a.subrange(m, r).fold_left(0, |s: int, v| s + v)
            == a.subrange(l, r).fold_left(0, |s: int, v| s + v)
    );
}

}

2024-07-17-10-18-32.zip

[clemsys]

Hi, I think this property is too complex for the SMT solver to be able to figure out how to prove it automatically.

Here is a proof of your property. I took inspiration from the proofs of the file seq_lib.rs in the source code of Verus to help me.

use vstd::prelude::*;

verus! {

fn main() {}

pub open spec fn seq_sum(a: Seq<i32>) -> int {
    a.fold_left(0, |s: int, v| s + v)
}

proof fn sum_is_additive(a: Seq<i32>, l: int, m: int, r: int)
    requires
        0 <= l <= m <= r <= a.len(),
    ensures
        seq_sum(a.subrange(l, r)) == seq_sum(a.subrange(l, m)) + seq_sum(a.subrange(m, r))
    decreases r - m
{
    if m == r {
        // trivial base case
    } else if m == r - 1 {
        reveal_with_fuel(Seq::fold_left, 2);
        assert(a.subrange(l, r).drop_last() =~= a.subrange(l, r - 1));
    } else {
        sum_is_additive(a, l, m + 1, r);
        sum_is_additive(a, l, m, m + 1);
        sum_is_additive(a, m, m + 1, r);
    }
}

} // verus!

I hope this helps. If you have any question on the proof, don't hesitate!