Trying for a little Dafny proof about "touching" integers

Question

I'd like to prove that if integer a is less than integer b and they are touching, then a+1==b. I define touching as there not being an integer i between a and b.

Can this work? (If not, I can beg the question and just define touching as a+1==b.)

Code:

predicate Touching(a: int, b:int)
  requires a < b
{
  !(exists i :: a < i < b)
}

method IntThing(a: int, b:int)
  requires a < b
  requires Touching(a,b)
{
 // Error: assertion might not hold
  assert a+1==b;
}

Answer 1

Here is a generalization using a different definition of touching. It shows that if two integers are "touching" then their difference is -1,0, or 1.

We now define two integer ranges as "touching" (which may including overlapping) if the set of points in their union is exactly equal to the set of points in their bounding range. I think this is intuitive.

predicate Touching(pair0: (int,int), pair1: (int,int))
  requires ValidPair(pair0)
  requires ValidPair(pair1)
{
  var pair2 := BoundingRange(pair0, pair1);
  RangeToSet(pair2) == RangeToSet(pair0) + RangeToSet(pair1)
}
// This is just a definition. We don't prove any interesting properties about it.
function BoundingRange(pair0: (int,int), pair1: (int,int)): (int,int)
  requires ValidPair(pair0)
  requires ValidPair(pair1)
  ensures ValidPair(BoundingRange(pair0, pair1))
{
  var start := if pair0.0 < pair1.0 then pair0.0 else pair1.0;
  var end := if pair0.1 > pair1.1 then pair0.1 else pair1.1;
  (start, end)
}

I'm interested in inclusive ranges, so ...

// *inclusive* range to set
function RangeToSet(pair: (int,int)): set<int>
  requires ValidPair(pair)
{
  set i | pair.0 <= i <= pair.1 :: i
}
predicate ValidPair(pair: (int,int)) {
  pair.0 <= pair.1
}

We need a lemma, defined inductively, that the size of an integer range's set of points is just the difference between its endpoints (adjusted for being inclusive).

lemma RangeToSetSize(pair: (int,int)) returns (r: int)
  decreases pair.1-pair.0
  requires ValidPair(pair)
  ensures |RangeToSet(pair)| == r
  ensures r == pair.1-pair.0+1
{
  if pair.0 == pair.1 {
    assert RangeToSet(pair) == {pair.0};
    r := 1;
  }
  else
  {
    assert RangeToSet((pair.0+1, pair.1)) + {pair.0} == RangeToSet(pair);
    var s2 := RangeToSetSize((pair.0+1, pair.1));
    r := 1 + s2;
  }
}

Now we can prove that two touching points are within 1 of each other:

method IntThing(a: int, b:int)
  requires Touching((a,a), (b,b))
  ensures -1 <= a-b <= 1
{
  var range := BoundingRange((a,a),(b,b));
  assert RangeToSet(range) == {a}+{b};
  var len := RangeToSetSize(range);
}