I had cause to need to prove some things about injective maps and inverses.
// union on maps does not seem to be defined in Dafny
function union<U, V>(m: map<U,V>, m': map<U,V>): map<U,V>
requires m !! m'; // disjoint
ensures forall i :: i in union(m, m') <==> i in m || i in m';
ensures forall i :: i in m ==> union(m, m')[i] == m[i];
ensures forall i :: i in m' ==> union(m, m')[i] == m'[i];
{
map i | i in (domain(m) + domain(m')) :: if i in m then m[i] else m'[i]
}
// the domain of a map is the set of its keys
function domain<U,V>(m: map<U,V>) : set<U>
ensures domain(m) == set u : U | u in m :: u;
ensures forall u :: u in domain(m) ==> u in m;
{
set u : U | u in m :: u
}
// the domain of a map is the set of its values
function range<U,V>(m: map<U,V>) : set<V>
ensures range(m) == set u : U | u in m :: m[u];
ensures forall v :: v in range(m) ==> exists u :: u in m && m[u] == v;
{
set u : U | u in m :: m[u]
}
// here a map m is smaller than m' if the domain of m is smaller than
// the domain of m', and every key mapped in m' is mapped to the same
// value that it is in m.
predicate mapSmaller<U,V>(m: map<U,V>, m': map<U,V>)
ensures mapSmaller(m,m') ==>
(forall u :: u in domain(m) ==> u in domain(m'));
{
forall a :: a in m ==> a in m' && m[a] == m'[a]
}
// map m is the inverse of m' if for every key->value in m
// there is value->key in m', and vice versa
predicate mapsAreInverse<U,V>(m: map<U,V>, m': map<V,U>)
{
(forall a :: a in m ==> m[a] in m' && m'[m[a]] == a) &&
(forall a :: a in m' ==> m'[a] in m && m[m'[a]] == a)
}
// map m is injective if no two keys map to the same value
predicate mapInjective<U,V>(m: map<U,V>)
{
forall a,b :: a in m && b in m ==> a != b ==> m[a] != m[b]
}
// here we prove that injective map m has an inverse, we prove
// this by calculating the inverse for an arbitrary injective map.
// maps are finite in Dafny so we have no termination problem
lemma invertMap<U,V>(m: map<U,V>) returns (m': map<V,U>)
requires mapInjective(m);
ensures mapsAreInverse(m,m');
{
var R := m; // part of m left to invert
var S := map[]; // part of m already inverted
var I := map[]; // inverted S
while R != map[] // while something left to invert
decreases R; // each loop iteration makes R smaller
invariant mapSmaller(R, m);
invariant mapSmaller(S, m);
invariant R !! S; // disjoint
invariant m == union(R, S);
invariant mapsAreInverse(S,I);
{
var a :| a in R; // take something arbitrary in R
var v := R[a];
var r := map i | i in R && i != a :: R[i]; // remove a from R
I := I[v:=a];
S := S[a:=v];
R := r;
}
m' := I; // R is empty, S == m, I inverts S
}
// here we prove that every injective map has an inverse
lemma injectiveMapHasInverse<U,V>(m: map<U,V>)
requires mapInjective(m);
ensures exists m' :: mapsAreInverse(m, m');
{
var m' := invertMap(m);
}
// here we prove that no non-injective map has an inverse
lemma nonInjectiveMapHasNoInverse<U,V>(m: map<U,V>)
requires !mapInjective(m);
ensures !(exists m' :: mapsAreInverse(m, m'));
{ }
// here we prove that if m' is the inverse of m, then the domain of m
// is the range of m', and vice versa
lemma invertingMapSwapsDomainAndRange<U,V>(m: map<U,V>, m': map<V,U>)
requires mapsAreInverse(m, m');
ensures domain(m) == range(m') && domain(m') == range(m);
{ }
// a map m strictly smaller than map m' has fewer elements in its domain
lemma strictlySmallerMapHasFewerElementsInItsDomain<U,V>(m: map<U,V>, m': map<U,V>)
requires mapSmaller(m,m') && m != m';
ensures domain(m') - domain(m) != {};
{
var R,R' := m,m';
while R != map[]
decreases R;
invariant mapSmaller(R,R');
invariant R != R';
{
var a :| a in R && a in R';
var v := R[a];
var r := map i | i in R && i != a :: R[i];
var r' := map i | i in R' && i != a :: R'[i];
R := r;
R' := r';
}
assert R == map[];
assert R' != map[];
assert domain(R) == {};
assert domain(R') != {};
}
function invert<U,V>(m:map<U,V>) : map<V,U>
requires mapInjective(m);
ensures mapsAreInverse(m,invert(m));
{
injectiveMapHasInverse(m);
var m' :| mapsAreInverse(m,m');
m'
} |
