Properties of < on unary numbers in Dafny

Question

I haven't been able to prove the following, using Dafny: S(x) < S(y) ==> x < y for the datatype of unary numbers with constructors Z and S (here I am only using S).

I tried forms of induction and I can suspect the reason lies in the generality of the < relation, but still I am wondering whether there could be a way out.

Answer 1

The built-in < operator on datatypes probably doesn't do what you want here. I would recommend defining your own notion of "less than" on your type. Then you should be able to use induction on it normally.

---

See the reference manual for how the built-in < operator is defined for datatypes:

The operator < is defined for two operands of the same datataype. It means is properly contained in. For example, in the code

datatype X = T(t: X) | I(i: int)
method comp() {
  var x := T(I(0));
  var y := I(0);
  var z := I(1);
  assert x.t < x;
  assert y < x;
  assert !(x < x);
  assert z < x; // FAILS
}

x is a datatype value that holds a T variant, which holds a I variant, which holds an integer 0. The value x.t is a portion of the datatype structure denoted by x, so x.t < x is true. Datatype values are immutable mathematical values, so the value of y is identical to the value of x.t, so y < x is true also, even though y is constructed from the ground up, rather than as a portion of x. However, z is different than either y or x.t and consequently z < x is not provable. Furthermore, < does not include ==, so x < x is false.

Note that only < is defined; not <= or > or >=.

Also, < is underspecified. With the above code, one can prove neither z < x nor !(z < x) and neither z < y nor !(z < y). In each pair, though, one or the other is true, so (z < x) || !(z < x) is provable.

Answer 2

The reason is that, when you compare two datatypes like in

S(x) < S(y)

internally, for verification, this condition is rewritten to

Dtrank(S(x)) < Dtrank(S(y))

where Dtrank is a function that can convert sequences and datatypes to integers, supposedly representing a kind of height. This function only contains two axioms for your case:

• Dtrank(x) < DtRank(S(x)) for all x

What you want is this lemma:

lemma MeaningOfLess(x: Un, y: Un) 
  requires x < y
  ensures y.S? && (x == y.tail || x < y.tail)
{}

and the case requiring attention is this one:

• Assumption: dtrank(x) < dtrank(S(y))
• Assumption: dtrank(y) < dtrank(S(y))
• Assumption: x != y
• Proof obligation: dtrank(x) < dtrank(y)

Now, what prevents the following to hold: dtrank(y) < dtrank(x) < dtrank(S(y)) ? Thinking about it carefully. You got two instances of datatypes. In your head, it's clear that they are ordered. For the solver, it's not, and just from the axioms above, you cannot immediately obtain that x must be included in y if it's included in S(y) and is not y.

I leave it there because I don't know how to prove more at this point, and indeed you might be better off defining your own axioms than relying on <.

I obtained all information by running dafny verify --bprint ltdatatype.bpl <myfile.dfy>