{"id":527,"date":"2014-04-17T14:34:00","date_gmt":"2014-04-17T14:34:00","guid":{"rendered":"http:\/\/www.lexicalscope.com\/blog\/?p=527"},"modified":"2014-08-28T21:26:05","modified_gmt":"2014-08-28T21:26:05","slug":"inverting-maps-in-dafny","status":"publish","type":"post","link":"https:\/\/www.lexicalscope.com\/blog\/2014\/04\/17\/inverting-maps-in-dafny\/","title":{"rendered":"Inverting Maps in Dafny"},"content":{"rendered":"<p>I had cause to need to prove some things about <a href=\"http:\/\/rise4fun.com\/Dafny\/NINC\">injective maps and inverses<\/a>.<\/p>\n<pre lang=\"foo\">\r\n\/\/ union on maps does not seem to be defined in Dafny\r\nfunction union<U, V>(m: map<U,V>, m': map<U,V>): map<U,V>\r\n\trequires m !! m'; \/\/ disjoint\r\n\tensures forall i :: i in union(m, m') <==> i in m || i in m';\r\n\tensures forall i :: i in m ==> union(m, m')[i] == m[i];\r\n\tensures forall i :: i in m' ==> union(m, m')[i] == m'[i];\r\n{\r\n\tmap i | i in (domain(m) + domain(m')) :: if i in m then m[i] else m'[i]\r\n}\r\n\r\n\/\/ the domain of a map is the set of its keys  \r\nfunction domain<U,V>(m: map<U,V>) : set<U>\r\n\tensures domain(m) == set u : U | u in m :: u;\r\n\tensures forall u :: u in domain(m) ==> u in m;\r\n{\r\n\t\tset u : U | u in m :: u\r\n}\r\n\r\n\/\/ the domain of a map is the set of its values\r\nfunction range<U,V>(m: map<U,V>) : set<V>\r\n\tensures range(m) == set u : U | u in m :: m[u];\r\n\tensures forall v :: v in range(m) ==> exists u :: u in m && m[u] == v;\r\n{\r\n\tset u : U | u in m :: m[u]\r\n}\r\n\r\n\/\/ here a map m is smaller than m' if the domain of m is smaller than \r\n\/\/ the domain of m', and every key mapped in m' is mapped to the same \r\n\/\/ value that it is in m.   \r\npredicate mapSmaller<U,V>(m: map<U,V>, m': map<U,V>)\r\n\tensures mapSmaller(m,m') ==> \r\n\t\t(forall u :: u in domain(m) ==> u in domain(m'));\r\n{\r\n\tforall a :: a in m ==> a in m' && m[a] == m'[a]\r\n}\r\n\r\n\/\/ map m is the inverse of m' if for every key->value in m\r\n\/\/ there is value->key in m', and vice versa\r\npredicate mapsAreInverse<U,V>(m: map<U,V>, m': map<V,U>)\r\n{\r\n\t(forall a :: a in m ==> m[a] in m' && m'[m[a]] == a) &&\r\n\t(forall a :: a in m' ==> m'[a] in m && m[m'[a]] == a) \r\n}\r\n\r\n\/\/ map m is injective if no two keys map to the same value\t\r\npredicate mapInjective<U,V>(m: map<U,V>)\r\n{\r\n\tforall a,b :: a in m && b in m ==> a != b ==> m[a] != m[b]\r\n}\r\n\r\n\/\/ here we prove that injective map m has an inverse, we prove\r\n\/\/ this by calculating the inverse for an arbitrary injective map.\r\n\/\/ maps are finite in Dafny so we have no termination problem\r\nlemma invertMap<U,V>(m: map<U,V>) returns (m': map<V,U>)\r\n\trequires mapInjective(m);\r\n\tensures mapsAreInverse(m,m');\r\n{\r\n\tvar R := m;     \/\/ part of m left to invert\r\n\tvar S := map[]; \/\/ part of m already inverted\r\n\tvar I := map[]; \/\/ inverted S\r\n\r\n\twhile R != map[]       \/\/ while something left to invert\r\n\t\tdecreases R;   \/\/ each loop iteration makes R smaller\r\n\t\tinvariant mapSmaller(R, m);\r\n\t\tinvariant mapSmaller(S, m);\r\n\t\tinvariant R !! S; \/\/ disjoint\r\n\t\tinvariant m == union(R, S);\r\n\t\tinvariant mapsAreInverse(S,I);\r\n\t{\r\n\t\tvar a :| a in R;   \/\/ take something arbitrary in R\r\n\t\tvar v := R[a];\r\n\t\tvar r := map i | i in R && i != a :: R[i];  \/\/ remove a from R\r\n\t\tI := I[v:=a];\r\n\t\tS := S[a:=v];\r\n\t\tR := r;\r\n\t}\r\n\tm' := I;  \/\/ R is empty, S == m, I inverts S\r\n}\r\n\r\n\/\/ here we prove that every injective map has an inverse  \r\nlemma injectiveMapHasInverse<U,V>(m: map<U,V>)\r\n\trequires mapInjective(m);\r\n\tensures exists m' :: mapsAreInverse(m, m'); \r\n{\r\n    var m' := invertMap(m);\r\n}\r\n\r\n\/\/ here we prove that no non-injective map has an inverse  \r\nlemma nonInjectiveMapHasNoInverse<U,V>(m: map<U,V>)\r\n\trequires !mapInjective(m);\r\n\tensures !(exists m' :: mapsAreInverse(m, m')); \r\n{ }\r\n\r\n\/\/ here we prove that if m' is the inverse of m, then the domain of m\r\n\/\/ is the range of m', and vice versa  \r\nlemma invertingMapSwapsDomainAndRange<U,V>(m: map<U,V>, m': map<V,U>)\r\n\trequires mapsAreInverse(m, m');\r\n\tensures domain(m) == range(m') && domain(m') == range(m);\r\n{ }\r\n\r\n\/\/ a map m strictly smaller than map m' has fewer elements in its domain \r\nlemma strictlySmallerMapHasFewerElementsInItsDomain<U,V>(m: map<U,V>, m': map<U,V>)\r\n\trequires mapSmaller(m,m') && m != m';\r\n\tensures domain(m') - domain(m) != {};\r\n{\r\n\tvar R,R' := m,m';\r\n\twhile R != map[]\r\n\t\tdecreases R;\r\n\t\tinvariant mapSmaller(R,R');\r\n\t\tinvariant R != R';\r\n\t{\r\n\t\tvar a :| a in R && a in R';\r\n\t\tvar v := R[a];\r\n\r\n\t\tvar r := map i | i in R && i != a :: R[i];\r\n\t\tvar r' := map i | i in R' && i != a :: R'[i];\r\n\r\n\t\tR := r;\r\n\t\tR' := r';\r\n\t}\r\n\tassert R == map[];\r\n\tassert R' != map[];\r\n\r\n\tassert domain(R) == {};\r\n\tassert domain(R') != {};\r\n}\r\n\r\nfunction invert<U,V>(m:map<U,V>) : map<V,U>\r\n\trequires mapInjective(m); \r\n\tensures mapsAreInverse(m,invert(m));\r\n{\r\n\tinjectiveMapHasInverse(m);\r\n\t\t\r\n\tvar m' :| mapsAreInverse(m,m');\r\n\tm'\r\n}\t\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>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(m: map, m&#8217;: map): map requires m !! m&#8217;; \/\/ disjoint ensures forall &hellip; <a href=\"https:\/\/www.lexicalscope.com\/blog\/2014\/04\/17\/inverting-maps-in-dafny\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_feature_clip_id":0,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2},"jetpack_post_was_ever_published":false},"categories":[15],"tags":[],"class_list":["post-527","post","type-post","status-publish","format-standard","hentry","category-dafny"],"jetpack_publicize_connections":[],"jetpack_shortlink":"https:\/\/wp.me\/p2e3P7-8v","jetpack_sharing_enabled":true,"jetpack_featured_media_url":"","_links":{"self":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/527","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/comments?post=527"}],"version-history":[{"count":9,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/527\/revisions"}],"predecessor-version":[{"id":5897,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/527\/revisions\/5897"}],"wp:attachment":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/media?parent=527"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/categories?post=527"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/tags?post=527"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}