Express relations and their properties

Apr 18, 2016 at 6:56 PM
Hello:

I want to represent some relations in Dafny and state that they follow certain properties like transitivity, antisymmetry or totalness.

For example, suppose we want to declare a binary relation on a type T which is a total preorder relation. We may write the following predicate along with its three properties (Reflexive is superfluous because Total is harder, unless == does something strange, I think).
predicate Leq<T>(x : T, y : T)
    // Reflexive
    ensures x == y ==> Leq(x, y)

    // Transitive
    ensures forall z : T :: Leq(x, z) && Leq(z, y) ==> Leq(x, y)

    // Total
    ensures Leq(x, y) || Leq(y, x)


method Main()
{
    var a : int, b : int, c : int;

    assume Leq(a, b);
    assume Leq(b, c);

    // Transitivity
    assert Leq(a, c);

    // Reflexivity
    assert Leq(a, a);

    var x : int, y : int;

    assume !Leq(x, y);

    // Totalness
    assert Leq(y, x);
}
This function can be used in any other function or method taking advantage of its properties, as in this example. But the function verification itself fails and Dafny complains about termination in the second and third postconditions.

A lemma might be used instead but it seems to be quite uncomfortable. I want to abstract from the particular relation definition. What is the better way to represent that in Dafny?

Thanks in advance.
Apr 19, 2016 at 2:27 PM
I don't see immediately how you can do this. You need to prove that the predicate is defined. The terminiation error means that Dafny can't prove it is defined.

Here are some random thoughts:

To show termination you would somehow have to show that the predicate terminiates in a finite number of steps. The fact that T has no ordering makes it difficult. Could you provide a witness to the number of recursive steps required for Leq?


The lemma version would look like the following:
predicate Leq<T>(x : T, y : T)

lemma LeqTotalPreorder<T>(x : T, y : T)
    // Reflexive
    ensures x == y ==> Leq(x, y)

    // Transitive
    ensures forall z : T :: Leq(x, z) && Leq(z, y) ==> Leq(x, y)

    // Total
    ensures Leq(x, y) || Leq(y, x)


method Main()
{
    var a : int, b : int, c : int;

    assume Leq(a, b);
    assume Leq(b, c);

    // Transitivity
    LeqTotalPreorder(a,c);
    assert Leq(a, c);

    // Reflexivity
    LeqTotalPreorder(a,a);
    assert Leq(a, a);

    var x : int, y : int;

    assume !Leq(x, y);

    // Totalness
    LeqTotalPreorder(x,y);
    assert Leq(y, x);
}
Developer
Apr 19, 2016 at 5:12 PM
One option would be to write your predicate without any ensures initially, write a lemma ensuring its properties, and then write a wrapper around the original predicate. It can provide ensures about the original predicate without running into termination errors, and it can call the lemma to make proving those properties easier.

Another option, which might be more what you're looking for, is to use Dafny's support for higher-order functions. For example, you could write something like this:
method Test(ghost R:(int,int)->bool)
    requires forall x, y :: R.requires(x,y);
    requires forall x, y :: x == y ==> R(x, y);
    requires forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z);
    requires forall x, y :: R(x, y) || R(y, x);

predicate Leq(x:int, y:int)
{
    x <= y
}

method Main()
{
    Test(Leq);
}
If you want to talk about lots of relations that have those properties, you could abstract the requires on Test into a predicate of its own.

Hope this helps.
Marked as answer by ruvus on 4/23/2016 at 1:58 PM
Apr 23, 2016 at 9:55 PM
Edited Apr 23, 2016 at 9:56 PM
Thanks! The use of higher-order functions is what I was looking for and it seems to work ok.

For the sake of completeness, I will briefly write what I have tried following parno's suggestions. The predicate "the argument is a total preorder relation" may be written like that:
predicate TotalPreorder(R : (T, T) -> bool)
    reads R.reads
{
       (forall x, y :: R.requires(x, y))
    && (forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z))
    && (forall x, y :: R(x, y) || R(y, x))
}
The wrapper method has also worked, but I find it less convenient.
predicate LeqDef(x : int, y : int)
{
    x <= y
}

lemma LeqIsTotal(x : int, y : int)
    ensures LeqDef(x, y) || LeqDef(y, x)
{
}

predicate Leq(x : int, y : int)
    ensures LeqDef(x, y) || LeqDef(y, x)
{
    LeqIsTotal(x, y); LeqDef(x, y)
}
And in response to lexicalscope, in the following example it is clear that the predicate ends in a finite number of steps but Dafny keeps complaining about termination errors:
predicate Leq(x : nat, y : nat)
    ensures Leq(x, y) || Leq(y, x)
    // decreases 0
{
    true
}