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

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

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

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

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

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.