
method m()
{
assert forall c:int,a:int :: c == a ==> exists z :: z == 1 && c * z == a;
}
I cannot guess how to help Dafny for proving this simple assert.



I don't know if this helps, but I got
this to verify:
method m()
{
assert forall c, a :: c == a ==> forall z :: true == if z == 1 && c * z == a then true else true;
}
This might not be exactly what you wanted, but there's one point to take away: existential quantifiers are problematic in current verification tools. You might need a lemma to verify statements with existential quantifiers. If possible, try and rewrite it as
a universal quantifier. Universal quantifiers (forall) are preferred over existential quantifiers.
Matt



Hi Matt,
Thank you for your answer.
I'm sorry but I'm not able to see the equivalence.
I mean that, as far as I know, "true == if B then true else true" for all boolean expression B, including when B is the constant false.
Hence, I cannot find any utility for this assert.
Best,
Paqui

