expressing properties of inductive datatypes in Dafny

Question

I defined a sigma algebra datatype in Dafny, as shown below:

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)

class test {

    var S : set<int>

    function eval(X: Alg) : set<int>  // evaluates an algebra
        reads this;
        decreases X;
    {
        match X
        case Empty => {}
        case Complement(a) => S - eval(X.a)
        case Union(b,c) => eval(X.b) + eval(X.c)
        case Set(s) => X.s
    }
}

I want to state properties that quantify over the inductive datatype. Is it possible to express properties like this?

Here is an example of what I have tried:

lemma algebra()
    ensures exists x :: x in Alg ==> eval(x) == {};
    ensures forall x :: x in Alg ==> eval(x) <= S;
    ensures forall x :: x in Alg ==> exists y :: y in Alg && eval(y) == S - eval(x);
    ensures forall b,c :: b in Alg && c in Alg ==> exists d :: d in Alg && eval(d) == eval(b) + eval(c);

But I get the error message:

second argument to "in" must be a set, multiset, or sequence with elements of type Alg, or a map with domain Alg

I want to state properties like: "there exists an algebra such that ...", or "for all algebras ...".

Answer 1

A type is not the same as a set in Dafny. You want to express the quantifiers in your lemmas as follows:

lemma algebra()
  ensures exists x: Alg :: eval(x) == {}
  ensures forall x: Alg :: eval(x) <= S
  ensures forall x: Alg :: exists y: Alg :: eval(y) == S - eval(x)
  ensures forall b: Alg, c: Alg :: exists d: Alg :: eval(d) == eval(b) + eval(c)

In the same way, you can declare a variable x to have type int, but you don't write x in int.

Because of type inference, you don't have to write : Alg explicitly. You can just write:

lemma algebra()
  ensures exists x :: eval(x) == {}
  ensures forall x :: eval(x) <= S
  ensures forall x :: exists y :: eval(y) == S - eval(x)
  ensures forall b, c :: exists d :: eval(d) == eval(b) + eval(c)

Another comment on the example: You're defining mathematics here. When you do, it's usually a good idea to stay away from the imperative features like classes, methods, and mutable fields. You don't need such features and they just complicate the mathematics. Instead, I suggest removing the class, changing the declaration of S to be a const, and removing the reads clause. That gives you:

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)

const S: set<int>

function eval(X: Alg): set<int>  // evaluates an algebra
  decreases X
{
  match X
  case Empty => {}
  case Complement(a) => S - eval(X.a)
  case Union(b,c) => eval(X.b) + eval(X.c)
  case Set(s) => X.s
}

lemma algebra()
  ensures exists x :: eval(x) == {}
  ensures forall x :: eval(x) <= S
  ensures forall x :: exists y :: eval(y) == S - eval(x)
  ensures forall b, c :: exists d :: eval(d) == eval(b) + eval(c)

Rustan