Apr 29, 2014 at 5:30 PM
Edited Apr 29, 2014 at 5:31 PM

http://rise4fun.com/Dafny/3tne
Sorry if this is a silly question, but I am missing something about how Dafny works I think. I am able to prove something for generic maps of type map<U,V> but I seem to then be unable to use this fact for maps of type map<int,int>.
Dafny can prove the following lemma a1:
lemma a1<U(==),V(==)> (m:map<U,V>, m':map<V,U>)
requires mapsAreInverse(m,m');
ensures forall d :: d in m ==> exists d' :: d' in m' && m'[d'] == d;
{ }
But I can not use a1 to prove a2 due to "A postcondition might not hold on this return path":
lemma a2(m:map<int,int>, m':map<int,int>)
requires mapsAreInverse(m,m');
ensures forall d :: d in m ==> exists d' :: d' in m' && m'[d'] == d;
{
a1(m,m');
}
Any advice appreciated.
Cheers,
Tim


May 7, 2014 at 10:50 AM
Edited May 7, 2014 at 10:52 AM

I have bumped into another strange thing whilst working on this lemma. I guess this all has something to do with instantiation of the "forall d" quantifier.
http://rise4fun.com/Dafny/uQKy
This lemma Dafny can prove:
static lemma {:verify true} a3(m:map<int,int>, m':map<int,int>, d:int)
requires d in m;
requires mapsAreInverse(m,m');
ensures exists d' :: d' in m' && m'[d'] == d;
{
var d' := m[d];
assert m'[d'] == d;
}
And I can use a3 to prove this related Lemma:
static lemma {:verify true} a4(m:map<int,int>, m':map<int,int>)
requires mapsAreInverse(m,m');
ensures forall d :: d in m ==> exists d' :: d' in m' && m'[d'] == d;
{
forall (dd in m)
{
a3(m,m',d);
}
}
However, if I assert the post condition of a4 just before the end of the forall, then Dafny can no longer prove the lemma!
// postcondition might not hold
static lemma {:verify true} a5(m:map<int,int>, m':map<int,int>)
requires mapsAreInverse(m,m');
ensures forall d :: d in m ==> exists d' :: d' in m' && m'[d'] == d;
{
forall (dd in m)
{
a3(m,m',d);
assert exists d' :: d' in m' && m'[d'] == d;
}
}

