Monthly Archives: November 2015

Calculations In Dafny

Posted on by , Modified on December 1, 2015
Reply

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));
            }
    }
}