使用递归函数验证Dafny迭代算法：唯一元素乘积验证受阻

我实现了一个计算整数数组中唯一元素乘积的Dafny迭代算法，同时定义了对应的递归ghost函数ProductOfUniques和Multiply。目前算法中的所有独立断言与循环不变式均能通过验证，但方法的后置条件始终无法通过验证。我尝试添加断言p == ProductOfUniques(a[..i])以及编写辅助引理，均未解决问题，恳请提供帮助。

迭代算法代码 #

method UniqueProduct(a: array<int>) returns (product: int)
    requires a.Length > 0
    ensures product == ProductOfUniques(a[..])
{
    var p := 1;
    var seen: seq<int> := [];
    
    for i := 0 to a.Length
        invariant 0 <= i <= a.Length
        invariant forall x :: x in seen ==> x in a[..i]
        invariant forall k :: 0 <= k < i && a[k] !in seen ==> seen == a[..i]
        invariant forall k :: 0 <= k < i && a[k] !in seen ==> p == ProductOfUniques(a[..i])
//        invariant p == ProductOfUniques(a[..i])
    {
        if !(a[i] in seen) {
            seen := seen + [a[i]];
            p := p * a[i];
        }
        assert a[..i+1][..i] == a[..i];
        assert forall k :: 0 <= k < |seen| ==> seen[k] in a[..i+1];
        assert a[i] !in seen ==> p == ProductOfUniques(a[..i+1]) == ProductOfUniques(a[..i]+[a[i]]);
        assert a[i] in seen <== p == ProductOfUniques(a[..i]);
    }
    assert a[..a.Length] == a[..];
    assert a[a.Length-1] !in seen ==> p == ProductOfUniques(a[..a.Length]) == ProductOfUniques(a[..a.Length-1]+[a[a.Length-1]]);

    assert a[a.Length-1] in seen <== p == ProductOfUniques(a[..a.Length-1]+[a[a.Length-1]]);

//    assert p == ProductOfUniques(a[..]);
    product := p;
}

递归Ghost函数代码 #

ghost function ProductOfUniques(a: seq<int>) : int
{
    if |a| == 0 then 1 
    else Multiply(a, [])
}

ghost function Multiply(numbers: seq<int>, seen: seq<int>) : int
    requires |numbers| > 0
{
    var tail := numbers[|numbers|-1];
    if |numbers| == 1 then 
        if tail in seen then 1 else tail 
    else 
        Multiply(numbers[..|numbers|-1], seen + [tail]) * (if tail in seen then 1 else tail) 
}

尝试的辅助引理 #

lemma X(a: seq<int>, i: int, n: int)
    requires |a| > 0
    requires 0 < i < |a|
    ensures n in a[..i] ==> ProductOfUniques(a[..i]) == ProductOfUniques(a[..i] + [n])

内容的提问来源于stack exchange，提问作者cvl