Playing around with the example of Sum and SumMyWay from the dafny power user paper. I noticed that changing from addition to multiplication will work for sets. However, the lemma fails to verify for multisets. Why is this the case and how can it be fixed?
Verifies ok...
function Mul(s: set<int>): int {
if s == {} then 1 else
var x :| x in s; // this line takes the place of a call to Pick
x * Mul(s - {x})
}
lemma MulMyWay(s: set<int>, y: int)
requires y in s
ensures Mul(s) == y * Mul(s - {y})
{
var x :| x in s && Mul(s) == x * Mul(s - {x}); // this line takes the place of a call to Pick
if y == x { // error: postcondition might not hold on this path
} else {
calc {
Mul(s);
== // def. Mul // error: this step might not hold
x * Mul(s - {x});
== { MulMyWay(s - {x}, y); }
x * y * Mul(s - {x} - {y});
== { assert s - {x} - {y} == s - {y} - {x}; }
y * x * Mul(s - {y} - {x});
== { MulMyWay(s - {y}, x); }
y * Mul(s - {y});
}
}
}
endlessly spins and never verifies... I thought it was related to multiplication but since Mul verifies, it must be related to properties of multisets.
function Prod(s: multiset<int>): int {
if s == multiset{} then 1 else
var x :| x in s;
x * Prod(s - multiset{x})
}
lemma ProdMyWay(s: multiset<int>, y: int)
requires y in s
decreases s
ensures Prod(s) == y * Prod(s - multiset{y})
{
var x :| x in s && Prod(s) == x * Prod(s - multiset{x});
if y == x {
} else {
assert s == (s - multiset{x}) + multiset{x};
assert s == (s - multiset{x}- multiset{y}) + multiset{x} + multiset{x};
calc {
Prod(s);
==
x * Prod(s - multiset{x});
== { ProdMyWay(s - multiset{x}, y); }
x * y * Prod(s - multiset{x} - multiset{y});
== { assert s - multiset{x} - multiset{y} == s - multiset{y} - multiset{x}; }
y * x * Prod(s - multiset{y} - multiset{x});
== { ProdMyWay(s - multiset{y}, x); }
y * Prod(s - multiset{y});
}
}
}
I think you have a typo in your file. You are trying to prove
assert s == (s - multiset{x}- multiset{y}) + multiset{x} + multiset{x};
but what you probably want is
assert s == (s - multiset{x}- multiset{y}) + multiset{x} + multiset{y};
Second, Dafny and SMT solvers have a hard time with non-linearity. You can either remove the non-linear axioms and invoke them manually, or give Dafny more hints about each individual assertion.
calc {
Prod(s);
==
x * Prod(s - multiset{x});
== { ProdMyWay(s - multiset{x}, y); }
x * (y * Prod((s - multiset{x}) - multiset{y}));
==
(x * y) * Prod((s - multiset{x}) - multiset{y});
==
(y * x) * Prod((s - multiset{x}) - multiset{y});
== { assert s - multiset{x} - multiset{y} == s - multiset{y} - multiset{x}; }
(y * x) * Prod((s - multiset{y}) - multiset{x});
==
y * (x * Prod((s - multiset{y}) - multiset{x}));
== { ProdMyWay(s - multiset{y}, x); }
y * Prod(s - multiset{y});
}