# Calculations In Dafny

Here is an example of using `calc` in Dafny.

Notes:

• Instead of using `==`, you can write another relational operator, for example implication `==>`
• I set the `Add` function to opaque, and disabled automatic induction, because otherwise Dafny will prove almost all of these lemmas automatically
• I wrote in the decreases clauses for didactic reasons. I wrote `decreases 0` where there is no recursive call
• I got the idea for this example from this document by Sophia Drossopoulou
```datatype Num = Zero | Succ(pred:Num)   function {:opaque true} Add(x:Num, y:Num) : Num decreases x; { match x { case Zero => y case Succ(z) => Succ(Add(z, y)) } }   lemma {:induction false} ZeroIdentity(x:Num) decreases x; ensures Add(x,Zero) == x { match x { case Zero => calc == { Add(Zero,Zero); {reveal_Add();} Zero; } case Succ(z) => calc == { Add(x,Zero); {reveal_Add();} Succ(Add(z,Zero)); {ZeroIdentity(z);} Succ(z); // definition of Num x; } } }   lemma {:induction false} SuccSymmetry(x:Num, y:Num) decreases 0; ensures Add(Succ(x),y) == Add(x,Succ(y)) { calc == { Add(Succ(x),y); {reveal_Add();} Succ(Add(x,y)); {SuccLemmaFour(x, y);} Add(x,Succ(y)); } }   lemma {:induction false} SuccLemmaFour(x:Num, y:Num) decreases x; ensures Succ(Add(x, y)) == Add(x,Succ(y)); { match x { case Zero => calc == { Succ(Add(Zero, y)); {reveal_Add();} Succ(y); {reveal_Add();} Add(Zero,Succ(y)); } case Succ(z) => calc == { Succ(Add(x, y)); {reveal_Add();} Succ(Succ(Add(z, y))); {SuccLemmaFour(z, y);} Succ(Add(z, Succ(y))); {reveal_Add();} Add(x,Succ(y)); } } }   lemma {:induction false} AddCommutative(x:Num, y:Num) decreases x; ensures Add(x, y) == Add(y, x) { match x { case Zero => calc == { Add(Zero, y); {reveal_Add();} y; {ZeroIdentity(y);} Add(y, Zero); } case Succ(z) => calc == { Add(x, y); {reveal_Add();} Succ(Add(z, y)); {AddCommutative(z, y);} Succ(Add(y, z)); {SuccLemmaFour(y, z);} Add(y,Succ(z)); // definition Num Add(y, x); } } }   lemma {:induction false} AddAssociative(x:Num, y:Num, z:Num) decreases x; ensures Add(Add(x,y),z) == Add(x,Add(y,z)); { match x { case Zero => calc == { Add(Add(Zero,y),z); {reveal_Add();} Add(y,z); {reveal_Add();} Add(Zero,Add(y,z)); } case Succ(w) => calc == { Add(Add(x,y),z); {reveal_Add();} Add(Add(Succ(w),y),z); {SuccSymmetry(w,y);} Add(Add(w,Succ(y)),z); {SuccLemmaFour(w, y);} Add(Succ(Add(w,y)),z); {SuccSymmetry(Add(w,y),z);} Add(Add(w,y),Succ(z)); {SuccLemmaFour(Add(w,y), z);} Succ(Add(Add(w,y),z)); {AddAssociative(w,y,z);} Succ(Add(w,Add(y,z))); {SuccLemmaFour(w, Add(y,z));} Add(w,Succ(Add(y,z))); {SuccSymmetry(w,Add(y,z));} Add(Succ(w),Add(y,z)); {reveal_Add();} Add(x,Add(y,z)); } } }```

# Dafny Proof by Contradiction

The general method in Dafny for proving something by contradiction is:

```lemma X() ensures Q(x) { if !Q(x) { // derive contradiction assert false; } }```