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
Addfunction 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 0where 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));
}
}
} |