CODEWITHSUNDEEP
dafny
Snirka
Snirka

Reputation: 598

How to proof a subset product?

I am trying to write a program in dafny that finds all subsets of a given set of integers, whose product is a given number.

What i did is to implement the methods ComputeSubProduct, FindProductSets and GenerateAllIndexSubsets.

This is what i got so far:

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)
{}

I am getting assertion violation in the 'A' method:

  1. assert {} == AllIndexSubsets([])
  2. assert res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..])

Upvotes: 1

Views: 383

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Both of these assertions are false.

  1. The empty set is a member of AllIndexSubsets([]), since the empty set is a subset of any set.

  2. AllIndexSubsets(q) - AllIndexSubsets(q[1..]) consists of all subsets of {0, ..., |q|-1} that contain |q|-1. But res1 consists of all subsets of {0, ..., |q|-2} that contain index.

A few further comments.

You should be careful with the expression AllIndexSubsets(q[1..]), since it will return sets of indices into q[1..], which, when used in q will be "off by one". For example, q[1..][0] is q[1], not q[0]. In other words, indices into q[1..] are "shifted by one" from the corresponding indices into q. It looks to me like you currently don't handle this properly.

Your use of index is rather mysterious. It is a parameter to the method, and thus takes on arbitrary values (since it is not constrained by a precondition). But you use it as if (roughly speaking) it is equal to |q|-1. Something is fishy here as well.

Upvotes: 2

Related Questions