{"id":9679,"date":"2015-11-26T23:29:50","date_gmt":"2015-11-26T23:29:50","guid":{"rendered":"http:\/\/www.lexicalscope.com\/blog\/?p=9679"},"modified":"2015-12-01T11:31:18","modified_gmt":"2015-12-01T11:31:18","slug":"calculations-in-dafny","status":"publish","type":"post","link":"https:\/\/www.lexicalscope.com\/blog\/2015\/11\/26\/calculations-in-dafny\/","title":{"rendered":"Calculations In Dafny"},"content":{"rendered":"<p>Here is an example of using <code>calc<\/code> in Dafny. <\/p>\n<p>Notes:<\/p>\n<ul>\n<li> Instead of using <code>==<\/code>, you can write another relational operator, for example implication <code>==&gt;<\/code><\/li>\n<li> I set the <code>Add<\/code> function to opaque, and disabled automatic induction, because otherwise Dafny will prove almost all of these lemmas automatically <\/li>\n<li> I wrote in the decreases clauses for didactic reasons. I wrote <code>decreases 0<\/code> where there is no recursive call <\/li>\n<li> I got the idea for this example <a href=\"http:\/\/www.doc.ic.ac.uk\/~scd\/Dafny%20support%20in%20Teaching%20--%20November%202013.pdf\">from this document by Sophia Drossopoulou<\/a> <\/li>\n<\/ul>\n<pre lang=\"Dafny\">\r\ndatatype Num = Zero | Succ(pred:Num)\r\n\r\nfunction {:opaque true} Add(x:Num, y:Num) : Num\r\n    decreases x;\r\n{\r\n    match x {\r\n        case Zero => y\r\n        case Succ(z) => Succ(Add(z, y))\r\n    }\r\n}\r\n\r\nlemma {:induction false} ZeroIdentity(x:Num)\r\n   decreases x;\r\n   ensures Add(x,Zero) == x\r\n{\r\n    match x {\r\n        case Zero =>\r\n            calc == {\r\n                Add(Zero,Zero);\r\n                    {reveal_Add();}\r\n                Zero;\r\n            }\r\n        case Succ(z) =>\r\n            calc == {\r\n                Add(x,Zero);\r\n                    {reveal_Add();}\r\n                Succ(Add(z,Zero));\r\n                    {ZeroIdentity(z);}\r\n                Succ(z);\r\n                    \/\/ definition of Num\r\n                x;\r\n            }\r\n    }\r\n}\r\n\r\nlemma {:induction false} SuccSymmetry(x:Num, y:Num)\r\n    decreases 0;\r\n    ensures Add(Succ(x),y) == Add(x,Succ(y))\r\n{\r\n    calc == {\r\n        Add(Succ(x),y);\r\n            {reveal_Add();}\r\n        Succ(Add(x,y));\r\n            {SuccLemmaFour(x, y);}\r\n        Add(x,Succ(y));\r\n    }\r\n}\r\n\r\nlemma {:induction false} SuccLemmaFour(x:Num, y:Num)\r\n    decreases x;\r\n    ensures Succ(Add(x, y)) == Add(x,Succ(y));\r\n{\r\n    match x {\r\n        case Zero =>\r\n            calc == {\r\n                Succ(Add(Zero, y));\r\n                    {reveal_Add();}\r\n                Succ(y);\r\n                    {reveal_Add();}\r\n                Add(Zero,Succ(y));\r\n            }\r\n        case Succ(z) =>\r\n            calc == {\r\n                Succ(Add(x, y));\r\n                    {reveal_Add();}\r\n                Succ(Succ(Add(z, y)));\r\n                    {SuccLemmaFour(z, y);}\r\n                Succ(Add(z, Succ(y)));\r\n                    {reveal_Add();}\r\n                Add(x,Succ(y));\r\n            }\r\n    }\r\n}\r\n\r\nlemma {:induction false} AddCommutative(x:Num, y:Num)\r\n    decreases x;\r\n    ensures Add(x, y) == Add(y, x)\r\n{\r\n    match x {\r\n        case Zero =>\r\n            calc == {\r\n                Add(Zero, y);\r\n                    {reveal_Add();}\r\n                y;\r\n                    {ZeroIdentity(y);}\r\n                Add(y, Zero);\r\n            }\r\n        case Succ(z) =>\r\n            calc == {\r\n                Add(x, y);\r\n                    {reveal_Add();}\r\n                Succ(Add(z, y));\r\n                    {AddCommutative(z, y);}\r\n                Succ(Add(y, z));\r\n                    {SuccLemmaFour(y, z);}\r\n                Add(y,Succ(z));\r\n                    \/\/ definition Num \r\n                Add(y, x);\r\n            }\r\n    }\r\n}\r\n\r\nlemma {:induction false} AddAssociative(x:Num, y:Num, z:Num)\r\n    decreases x;\r\n    ensures Add(Add(x,y),z) == Add(x,Add(y,z));\r\n{\r\n    match x {\r\n        case Zero =>\r\n            calc == {\r\n                Add(Add(Zero,y),z);\r\n                    {reveal_Add();}\r\n                Add(y,z);\r\n                    {reveal_Add();}\r\n                Add(Zero,Add(y,z));\r\n            }\r\n        case Succ(w) =>\r\n            calc == {\r\n                Add(Add(x,y),z);\r\n                    {reveal_Add();}\r\n                Add(Add(Succ(w),y),z);\r\n                    {SuccSymmetry(w,y);}\r\n                Add(Add(w,Succ(y)),z);\r\n                    {SuccLemmaFour(w, y);}\r\n                Add(Succ(Add(w,y)),z);\r\n                    {SuccSymmetry(Add(w,y),z);}\r\n                Add(Add(w,y),Succ(z));\r\n                    {SuccLemmaFour(Add(w,y), z);}\r\n                Succ(Add(Add(w,y),z));\r\n                    {AddAssociative(w,y,z);}\r\n                Succ(Add(w,Add(y,z)));\r\n                    {SuccLemmaFour(w, Add(y,z));}\r\n                Add(w,Succ(Add(y,z)));\r\n                    {SuccSymmetry(w,Add(y,z));}\r\n                Add(Succ(w),Add(y,z));\r\n                    {reveal_Add();}\r\n                Add(x,Add(y,z));\r\n            }\r\n    }\r\n}\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Here is an example of using calc in Dafny. Notes: Instead of using ==, you can write another relational operator, for example implication ==&gt; I set the Add function to opaque, and disabled automatic induction, because otherwise Dafny will prove &hellip; <a href=\"https:\/\/www.lexicalscope.com\/blog\/2015\/11\/26\/calculations-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-9679","post","type-post","status-publish","format-standard","hentry","category-dafny"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p2e3P7-2w7","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/9679","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=9679"}],"version-history":[{"count":5,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/9679\/revisions"}],"predecessor-version":[{"id":9721,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/9679\/revisions\/9721"}],"wp:attachment":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/media?parent=9679"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/categories?post=9679"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/tags?post=9679"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}