Difference between map<U,V> and map<int,int>

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 (d|d 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 (d|d in m) 
    { 
        a3(m,m',d); 
        assert exists d' :: d' in m' && m'[d'] == d;
    }
}