如何证明子产品？

Question

我正在尝试用 dafny 编写一个程序，用于查找给定整数集的所有子集，其乘积为给定数字。

我所做的是实现方法 ComputeSubProduct、FindProductSets 和 GenerateAllIndexSubsets。

这是我目前得到的：

method Main() {
    var q := [2,3,4];
    var productSets := FindProductSets(q, 12);
    assert {1,2} in productSets by {
        calc {
            SubProduct(q, {1,2});
        == { LemmaSubProductsOrderIndifference(q, {1,2}, 1); }
            q[1]*q[2];
        ==
            3*4;
        ==
            12;
        }
    }
}

function SubProduct(q: seq<int>, indexSet: set<nat>): int
    requires InRange(q, indexSet)
{
    if |indexSet| == 0 then 1 else var i :| i in indexSet; q[i] * SubProduct(q, indexSet-{i})
}

predicate InRange<T>(q: seq<T>, indexSet: set<nat>)
{
    forall i :: i in indexSet ==> 0 <= i < |q|
}

function AllIndexSubsets<T>(q: seq<T>): (res: set<set<nat>>)
    ensures forall s :: s in res ==> InRange(q, s)
{
    AllSubsets(set i | P(i) && 0 <= i < |q|)
}

predicate P<T>(x: T) { true } // this is helpful only for avoiding a "no triggers found" warning by Dafny

function AllSubsets<T>(s: set<T>): set<set<T>>
{
    set subset: set<T> | P(subset) && subset <= s
}

method FindProductSets(q: seq<int>, num: int) returns (result: set<set<int>>)
    ensures forall indexSet :: indexSet in result <==> indexSet in AllIndexSubsets(q) && SubProduct(q, indexSet) == num


method GenerateAllIndexSubsets<T>(q: seq<T>) returns (res: set<set<nat>>)
    ensures res == AllIndexSubsets(q)
{
    res := A(q, 0);
}
method A<T>(q: seq<T>, index: nat) returns (res: set<set<nat>>)
    ensures res == AllIndexSubsets(q)
{
    if |q| == 0
        { 
        assert |q| == 0;// if's guard
        // ==>
        assert {} == AllIndexSubsets<nat>([]);
        assert q == [];
        assert {} == AllIndexSubsets(q);
        res := {};
        assert res == AllIndexSubsets(q); // postcondition
        }
    else
        { 
            assert |q| != 0; // !(if's guard)
            var res0 : set<set<nat>> := A(q[1..], index + 1);
            assert res0 == AllIndexSubsets(q[1..]);
            res := res0;    
            assert res ==  AllIndexSubsets(q[1..]); //GenerateAllIndexSubsets postcondition with q[1..]
            //var res1 : set<set<nat>> := AllIndexSubsetsIntersection(q, q[0], res0);
            var res1: set<set<nat>> := (set x | x in res0 :: x + {index});
            assert res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..]);
            assert res0 == AllIndexSubsets(q[1..]);
            assert res1 == AllIndexSubsets(q) - res0;
            // ==>
            assert res0 + res1 == AllIndexSubsets(q);
            res := res + res1;
            assert res == AllIndexSubsets(q); // postcondition
        }
    assert res == AllIndexSubsets(q); // postcondition
} 


method ComputeSubProduct(q: seq<int>, indexSet: set<nat>) returns (prod: int)
    requires InRange(q, indexSet)
    ensures prod == SubProduct(q, indexSet)

lemma {:verify false} LemmaSubProductsOrderIndifference(q: seq<int>, indexSet: set<nat>, i: nat)
    requires i in indexSet
    requires InRange(q, indexSet)
    ensures q[i] * SubProduct(q, indexSet-{i}) == SubProduct(q, indexSet)
{}

我在 'A' 方法中遇到断言冲突：

断言 {} == AllIndexSubsets([])
断言 res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..])

Answer 1

这两个断言都是错误的。

空集是AllIndexSubsets([])的成员，因为空集是任何集的子集。
AllIndexSubsets(q) - AllIndexSubsets(q[1..]) 由包含 |q|-1 的 {0, ..., |q|-1} 的所有子集组成。但是 res1 由包含 index 的 {0, ..., |q|-2} 的所有子集组成。

一些进一步的评论。

你应该小心表达式 AllIndexSubsets(q[1..])，因为它会将 return 组索引放入 q[1..]，当在 q 中使用时，它将是 "off by one"。例如，q[1..][0] 是 q[1]，而不是 q[0]。换句话说，q[1..] 中的索引是 "shifted by one" 中相应索引中的 q。在我看来你目前没有正确处理这个问题。

你对index的使用比较神秘。它是方法的一个参数，因此可以取任意值（因为它不受前提条件的约束）。但是你使用它就好像（粗略地说）它等于 |q|-1。这里也有可疑之处。

如何证明子产品？

How to proof a subset product?

dafny