DEV Community

Aaron Elligsen
Aaron Elligsen

Posted on

2

Writing lemmas in Dafny

Lemmas

Quite often you need to explain various mathematical facts to Dafny. The way you do this is by writing lemmas, which are basically ghost methods. Like any other function or method they can have input parameters, return values, preconditions, and postconditions. However, lemmas only exist in the specification context and do not compile to executable code.

There is a guide to writing lemmas here.

Direct Proof: An example on Relations

A Relation is a set of order pairs of objects of some other set. The most common example is the integer ordering relation, like less than or equal to. If we limit ourselves to just the integers 1-3 we can encode the it like so.

var lessThanEqual := {
(1,1),
(1,2),
(1,3),
(2,2),
(2,3),
(3,3)
};
Enter fullscreen mode Exit fullscreen mode

We can say that 1 is less than or equal to 3 if the pair (1,3) is in the lessThanEqual set.

There are many types of relations. We can define these types in Dafny using predicate functions. We can create generic functions by parameterizing the input type as a type variable T.

predicate relationOnASet<T>(R: set<(T,T)>, S: set<T>) {
    forall ts :: ts in R ==> ts.0 in S && ts.1 in S
}

predicate reflexive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall s :: s in S ==> (s,s) in R
}

predicate symmetric<T>(R: set<(T,T)>, S: set<T>)
    requires relationOnASet(R, S)
{
    forall x: T, y:T :: x in S && y in S && (x,y) in R ==> (y, x) in R
}

predicate transitive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall a,b,c :: a in S && b in S && c in S && (a,b) in R && (b,c) in R ==> (a,c) in R
}

predicate equivalenceRelation<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    reflexive(R, S) && symmetric(R, S) && transitive(R, S)
}
Enter fullscreen mode Exit fullscreen mode

Union of relations?

Since a relation is just a set and we can combine sets using set union, what can we say about the union of certain kinds of relations? Dafny overloads + to mean set union when working with sets.

If we union two symmetric relations is the result still symmetric?We can prove it in Dafny like so.

lemma symmetricUnion<T>(R_1: set<(T,T)>, S_1: set<T>, R_2: set<(T,T)>, S_2: set<T>)
    requires |R_1| > 0
    requires |R_2| > 0
    requires |S_1| > 0
    requires |S_2| > 0
    requires relationOnASet(R_1, S_1)
    requires relationOnASet(R_2, S_2)
    requires symmetric(R_1, S_1)
    requires symmetric(R_2, S_2)
    ensures symmetric(R_1+R_2, S_1+S_2)
{
    forall x,y | x in S_1+S_2 && y in S_1+S_2 && (x,y) in R_1+R_2
        ensures (y,x) in R_1+R_2
    {
        if  x in S_1 && y in S_1 && (x,y) in R_1 {
            assert (y,x) in R_1+R_2;
        }else if  x in S_2 && y in S_2 && (x,y) in R_2 {
            assert (y,x) in R_1+R_2;
        }
    }
}
Enter fullscreen mode Exit fullscreen mode

However, if we ask the same question about transitive relations we run into trouble. We can create a counter example.

lemma transitiveUnionCounterExample<T>()
  returns (
  R1: set<(T, T)>, S1: set<T>,
  R2: set<(T, T)>, S2: set<T>)
  ensures relationOnASet(R1, S1)
  ensures relationOnASet(R2, S2)
  ensures transitive(R1, S1)
  ensures transitive(R2, S2)
  ensures ! transitive(R1 + R2, S1 + S2)
{
  var a : T :| assume true;
  var b : T :| assume a != b;
  var c : T :| assume a != c && b != c;
  S1 := {a, b};
  S2 := {b, c};
  R1 := {(a, b)};
  R2 := {(b, c)};
}

lemma transitiveUnionNotAlwaysTransitive<T>()
  ensures !
  (forall S1 : set<T>, S2 : set<T>, R1 : set<(T,T)>, R2 : set<(T, T)> ::
  relationOnASet(R1, S1) &&
  relationOnASet(R2, S2) &&
  transitive(R1, S1) &&
  transitive(R2, S2)  ==> transitive(R1 + R2, S1 + S2)
  )
{
  var a, b, c, d := transitiveUnionCounterExample<T>();
}
Enter fullscreen mode Exit fullscreen mode

Proofs by contradiction in Dafny

The creator of Dafny recommends the following template for a proof by contradiction.

lemma L(...)
  requires P
  ensures Q
{
  if !Q {
    ...
    assert !P;
    assert false;
  }
}
Enter fullscreen mode Exit fullscreen mode

The goal here is that if we assume !Q for some proposition, then through some calculations or assertions we can show that implies !P, which is assumed to be true by the require precondition, then we have reached a contradiction.

Asserting false is an additional step which makes it clear we expect this branch to end in contradiction.

Image of AssemblyAI tool

Challenge Submission: SpeechCraft - AI-Powered Speech Analysis for Better Communication

SpeechCraft is an advanced real-time speech analytics platform that transforms spoken words into actionable insights. Using cutting-edge AI technology from AssemblyAI, it provides instant transcription while analyzing multiple dimensions of speech performance.

Read full post

Top comments (0)

AWS Security LIVE!

Tune in for AWS Security LIVE!

Join AWS Security LIVE! for expert insights and actionable tips to protect your organization and keep security teams prepared.

Learn More

👋 Kindness is contagious

Dive into an ocean of knowledge with this thought-provoking post, revered deeply within the supportive DEV Community. Developers of all levels are welcome to join and enhance our collective intelligence.

Saying a simple "thank you" can brighten someone's day. Share your gratitude in the comments below!

On DEV, sharing ideas eases our path and fortifies our community connections. Found this helpful? Sending a quick thanks to the author can be profoundly valued.

Okay