Simple assertion that is not proved

Feb 26, 2014 at 1:28 PM
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.
Feb 26, 2014 at 6:59 PM
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
Feb 27, 2014 at 1:35 PM
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