New test file: dafny4/NumberRepresentations.dfy

1 files changed, 304 insertions, 0 deletions

diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
new file mode 100644
index 00000000..2f31c006
--- /dev/null
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -0,0 +1,304 @@
+// We consider a number representation that consists of a sequence of digits.  The least

+// significant digit is stored at index 0.

+// For a given base, function eval gives the number that is represented.  Note

+// that eval can be defined without regard to the sign or magnitude of the digits.

+

+function eval(digits: seq<int>, base: int): int

+  requires 2 <= base;

+{

+  if |digits| == 0 then 0 else digits[0] + base * eval(digits[1..], base)

+}

+

+lemma test_eval()

+{

+  assert forall base :: 2 <= base ==> eval([], base) == 0;

+  assert forall base :: 2 <= base ==> eval([0], base) == 0;

+  forall base | 2 <= base {

+    calc {

+      eval([0, 0], base);

+      0;

+    }

+  }

+

+  calc {

+    eval([3, 2], 10);

+    3 + 10 * eval([2], 10);

+    23;

+  }

+  var oct, dec := 8, 10;

+  calc {

+    eval([1, 3], oct);

+    1 + oct * eval([3], oct);

+    5 + dec * eval([2], dec);

+    eval([5, 2], dec);

+  }

+

+  assert eval([29], 420) == 29;

+  assert eval([29], 8) == 29;

+

+  calc {

+    eval([-2, 1, -3], 5);

+    -2 + 5 * eval([1, -3], 5);

+    -2 + 5 * 1 + 25 * eval([-3], 5);

+    -2 + 5 * 1 + 25 * (-3);

+    -72;

+  }

+}

+

+// To achieve a unique (except for leading zeros) representation of each number, we

+// consider digits that are drawn from a consecutive range of "base" integers

+// including 0.  That is, each digit lies in the half-open interval [lowDigit..lowDigit+base].

+

+predicate IsSkewNumber(digits: seq<int>, lowDigit: int, base: nat)

+{

+  2 <= base &&  // there must be at least two digits

+  lowDigit <= 0 < lowDigit + base &&  // digits must include 0

+  forall d :: d in digits ==> lowDigit <= d < lowDigit + base  // every digit is in this range

+}

+

+// The following theorem says that any natural number is representable as a sequence

+// of digits in the range [0..base].

+

+lemma CompleteNat(n: nat, base: nat) returns (digits: seq<int>)

+  requires 2 <= base;

+  ensures IsSkewNumber(digits, 0, base) && eval(digits, base) == n;

+{

+  if n < base {

+    digits := [n];

+  } else {

+    var d, m := n / base, n % base;

+    assert base * d + m == n;

+    if n <= d {

+      calc {

+        base * d + m == n;

+      ==> { assert 0 <= m; }

+        base * d <= n;

+      ==> { assert n <= d; }

+        base * n <= n;

+        (base - 1) * n + n <= n;

+        (base - 1) * n <= 0;

+      ==> { MulSign(base - 1, n); }

+        (base - 1) <= 0 || n <= 0;

+        { assert 0 < n; }

+        (base - 1) <= 0;

+        { assert 2 <= base; }

+        false;

+      }

+      assert false;

+    }

+    assert d < n && 0 <= m;

+    digits := CompleteNat(d, base);

+    digits := [m] + digits;

+  }

+}

+

+// we used the following lemma to prove the theorem above

+lemma MulSign(x: int, y: int)

+  requires x * y <= 0;

+  ensures x <= 0 || y <= 0;

+{

+}

+

+// The following theorem says that, provided there's some digit with the same sign as "n",

+// then "n" can be represented.

+

+lemma Complete(n: int, lowDigit: int, base: nat) returns (digits: seq<int>)

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base;

+  requires 0 <= lowDigit ==> 0 <= n;  // without negative digits, only non-negative numbers can be formed

+  requires lowDigit + base <= 1 ==> n <= 0;  // without positive digits, only positive numbers can be formed

+  ensures IsSkewNumber(digits, lowDigit, base) && eval(digits, base) == n;

+  decreases if 0 <= n then n else -n;

+{

+  if lowDigit <= n < lowDigit + base{

+    digits := [n];

+  } else if 0 < n {

+    digits := Complete(n - 1, lowDigit, base);

+    digits := inc(digits, lowDigit, base);

+  } else {

+    digits := Complete(n + 1, lowDigit, base);

+    digits := dec(digits, lowDigit, base);

+  }

+}

+

+ghost method inc(a: seq<int>, lowDigit: int, base: nat) returns (b: seq<int>)

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base;

+  requires IsSkewNumber(a, lowDigit, base);

+  requires eval(a, base) == 0 ==> 1 < lowDigit + base;

+  ensures IsSkewNumber(b, lowDigit, base) && eval(b, base) == eval(a, base) + 1;

+{

+  if a == [] {

+    b := [1];

+  } else if a[0] + 1 < lowDigit + base {

+    b := a[0 := a[0] + 1];

+  } else {

+    b := inc(a[1..], lowDigit, base);

+    b := [lowDigit] + b;

+  }

+}

+

+ghost method dec(a: seq<int>, lowDigit: int, base: nat) returns (b: seq<int>)

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base;

+  requires IsSkewNumber(a, lowDigit, base);

+  requires eval(a, base) == 0 ==> lowDigit < 0;

+  ensures IsSkewNumber(b, lowDigit, base) && eval(b, base) == eval(a, base) - 1;

+{

+  if a == [] {

+    b := [-1];

+  } else if lowDigit <= a[0] - 1 {

+    b := a[0 := a[0] - 1];

+  } else {

+    b := dec(a[1..], lowDigit, base);

+    b := [lowDigit + base - 1] + b;

+  }

+}

+

+// Finally, we prove that number representations are unique, except for leading zeros.

+// Recall, a "leading" zero is one at the end of the sequence.

+

+// The trim function removes any leading zeros.

+

+function trim(digits: seq<int>): seq<int>

+{

+  if |digits| != 0 && digits[|digits| - 1] == 0 then trim(digits[..|digits|-1]) else digits

+}

+

+// Here follow a number of lemmas about trim

+

+lemma TrimResult(digits: seq<int>)

+  ensures var last := |trim(digits)| - 1;

+    0 <= last ==> trim(digits)[last] != 0;

+{

+}

+

+lemma TrimProperty(a: seq<int>)

+  requires a == trim(a);

+  ensures a == [] || a[1..] == trim(a[1..]);

+{

+  assert forall b :: |trim(b)| <= |b|;

+}

+

+lemma TrimPreservesValue(digits: seq<int>, base: nat)

+  requires 2 <= base;

+  ensures eval(digits, base) == eval(trim(digits), base);

+{

+  var last := |digits| - 1;

+  if |digits| != 0 && digits[last] == 0 {

+    assert digits == digits[..last] + [0];

+    LeadingZeroInsignificant(digits[..last], base);

+  }

+}

+

+lemma LeadingZeroInsignificant(digits: seq<int>, base: nat)

+  requires 2 <= base;

+  ensures eval(digits, base) == eval(digits + [0], base);

+{

+  if |digits| != 0 {

+    var d := digits[0];

+    assert [d] + digits[1..] == digits;

+    calc {

+      eval(digits, base);

+      eval([d] + digits[1..], base);

+      d + base * eval(digits[1..], base);

+      { LeadingZeroInsignificant(digits[1..], base); }

+      d + base * eval(digits[1..] + [0], base);

+      eval([d] + (digits[1..] + [0]), base);

+      { assert [d] + (digits[1..] + [0]) == ([d] + digits[1..]) + [0]; }

+      eval(([d] + digits[1..]) + [0], base);

+      eval(digits + [0], base);

+    }

+  }

+}

+

+// We now get on with proving the uniqueness of the representation

+

+lemma UniqueRepresentation(a: seq<int>, b: seq<int>, lowDigit: int, base: nat)

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base;

+  requires a == trim(a) && b == trim(b);

+  requires IsSkewNumber(a, lowDigit, base) && IsSkewNumber(b, lowDigit, base);

+  requires eval(a, base) == eval(b, base);

+  ensures a == b;

+{

+  if eval(a, base) == 0 {

+    ZeroIsUnique(a, lowDigit, base);

+    ZeroIsUnique(b, lowDigit, base);

+  } else {

+    var aa, bb := eval(a, base), eval(b, base);

+    var arest, brest := a[1..], b[1..];

+    var ma, mb := aa % base, bb % base;

+

+    assert 0 <= ma < base && 0 <= mb < base;

+    LeastSignificantDigitIsAlmostMod(a, lowDigit, base);

+    LeastSignificantDigitIsAlmostMod(b, lowDigit, base);

+    assert ma == mb && a[0] == b[0];

+    var y := a[0];

+

+    assert aa == base * eval(arest, base) + y;

+    assert bb == base * eval(brest, base) + y;

+    MulInverse(base, eval(arest, base), eval(brest, base), y);

+    assert eval(arest, base) == eval(brest, base);

+

+    TrimProperty(a);

+    TrimProperty(b);

+    UniqueRepresentation(arest, brest, lowDigit, base);

+    assert [y] + arest == a && [y] + brest == b;

+  }

+}

+

+lemma ZeroIsUnique(a: seq<int>, lowDigit: int, base: nat)

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base;

+  requires a == trim(a);

+  requires IsSkewNumber(a, lowDigit, base);

+  requires eval(a, base) == 0;

+  ensures a == [];

+{

+  if a != [] {

+    assert eval(a, base) == a[0] + base * eval(a[1..], base);

+    if eval(a[1..], base) == 0 {

+      TrimProperty(a);

+      ZeroIsUnique(a[1..], lowDigit, base);

+    }

+    assert false;

+  }

+}

+

+lemma LeastSignificantDigitIsAlmostMod(a: seq<int>, lowDigit: int, base: nat)

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base && IsSkewNumber(a, lowDigit, base);

+  requires a != [];

+  ensures var mod := eval(a, base) % base; a[0] == mod || a[0] == mod - base;

+{

+  var n := eval(a, base);

+  var d, m := n / base, n % base;

+  assert base * d + m == n;

+  assert 0 <= m < base;

+

+  assert lowDigit <= a[0] < lowDigit + base;

+  var arest := a[1..];

+  var nrest := eval(arest, base);

+  assert base * nrest + a[0] == n;

+

+  var p := MulProperty(base, d, m, nrest, a[0]);

+  assert -1 * base <= a[0] - m < 1 * base;

+  if {

+    case p == -1 =>  assert a[0] == m - base;

+    case p == 0 =>  assert a[0] == m;

+  }

+}

+

+lemma MulProperty(k: int, a: int, x: int, b: int, y: int) returns (p: int)

+  requires 0 < k;

+  requires k * a + x == k * b + y;

+  ensures y - x == k * p;

+{

+  calc {

+    k * a + x == k * b + y;

+    k * a - k * b == y - x;

+    k * (a - b) == y - x;

+  }

+  p := a - b;

+}

+

+lemma MulInverse(x: int, a: int, b: int, y: int)

+  requires x != 0 && x * a + y == x * b + y;

+  ensures a == b;

+{

+}