►CMSC 433:   Programming Language Technologies and Paradigms
▼Notes
►6 Inductive Proofs
On this page:
6.1 Proofs of functions
6.2 Lemma
6.3 Sum of Cubes
6.4 Fibonacci
6.5 Sum of Differences
6.6 Multiplication is Commutative
6.7 Postage Stamps
6.8 Reversing a Sequence
8.17
    contents    up   

6 Inductive Proofs🔗

    6.1 Proofs of functions

    6.2 Lemma

    6.3 Sum of Cubes

    6.4 Fibonacci

    6.5 Sum of Differences

    6.6 Multiplication is Commutative

    6.7 Postage Stamps

    6.8 Reversing a Sequence

6.1 Proofs of functions🔗

In this lecture, we will learn how to construct formal proofs to verify the correctness of functions.

As an example, consider a function that computes the sum of all numbers from 1 up to and including n—a sum commonly referred to as a triangular number.

Dafny

function TriangleNumber(n: int): int
  requires 0 <= n
{
  if n == 0 then 0 else TriangleNumber(n - 1) + n
}

Let’s write a method that does the same thing as this function, with a postcondition that says it does indeed return the same value as the function.

Dafny

method ComputeTriangleNumber(n: int) returns (s: int)
  requires 0 <= n  // omit this line; what happens?
  ensures s == TriangleNumber(n)
{
  if n == 0 {
    return 0;
  } else {
    s := ComputeTriangleNumber(n - 1);
    return s + n;
  }
}

For this method to be correct, every control path leading to the end of the method body must be shown to establish the postcondition.

Gauss used a closed form of triangle numbers. We can add that to the postcondition:

Dafny

method ComputeTriangleNumber2(n: int) returns (s: int)
  requires 0 <= n
  ensures s == TriangleNumber(n)
  ensures s == n * (n + 1) / 2
{
  if n == 0 {
    return 0;
  } else {
    s := ComputeTriangleNumber2(n - 1);
    return s + n;
  }
}

For this method to be correct, every control path leading to the end of the method body must be shown to establish both of these postconditions.

A consequence of the two postconditions 


s == TriangleNumber(n)
s == n * (n + 1) / 2

is that 
TriangleNumber(n) == n * (n + 1) / 2
Let’s change the postcondition to that:

Dafny

method ComputeTriangleNumber3(n: int) returns (s: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n == 0 {
    return 0;
  } else {
    s := ComputeTriangleNumber3(n - 1);
    return s + n;
  }
}

The out-parameter "s" is no longer mentioned in the postcondition. Let’s just remove it altogether.

Dafny

method ComputeTriangleNumber4(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n == 0 {
  } else {
    ComputeTriangleNumber4(n - 1);
  }
}

As before, correctness of this method means that every control path leading to the end establishes the postcondition. But why would anyone want to call such a method, since it does not return anything? By calling the method, the caller learns the postcondition. This is called a lemma!

6.2 Lemma🔗

A lemma in Dafny is like a method. The postcondition of the lemma is the statement of the lemma – the proof goal of the body of the lemma. The precondition of the lemma is the antecedent of the lemma – every caller must show the precondition in order to be allowed to call the lemma and obtain the information in the proof goal. Here is the same method but declared as a lemma and renamed "Gauss".

Dafny

lemma Gauss(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n == 0 {
  } else {
    Gauss(n - 1);
  }
}

The proof has the same structure as you may have encountered in previous classes or in high-school geometry. It is a proof by induction with the base case n == 0 and an induction step for n > 0. The induction hypothesis is obtained by calling the lemma recursively.

Lemmas in Dafny are proof artifacts, so they are ghost. All code inside a lemma must also be ghost (i.e., it cannot affect runtime behavior). Lemmas are not executable at runtime—they are erased.

In contrast, a method is executable and may have side effects. Because of this separation, a lemma generally cannot call a regular method, since that would mix ghost and non-ghost code.

Dafny

lemma Gauss'(n: int)
requires 0 <= n
{
var v := ComputeTriangleNumber(n);
// error: direct calls to methods are disallowed
// A lemma may call other lemmas, but not methods.
assert v == TriangleNumber(n);
}

If you want this construct to be executable, you can rewrite the lemma as a method:

Dafny

method Gauss'(n: int)
requires 0 <= n
{
var v := ComputeTriangleNumber(n);
assert v == TriangleNumber(n);
assert v == n * (n + 1) / 2 by { Gauss(n); }
}

In practice, to reason about methods, you specify their behavior using functions or predicates. Lemmas can then call those functions (or other lemmas) to establish properties about the method’s specification. For example, we used a function 

ensures s == TriangleNumber(n)
in the specification of ComputeTriangleNumber.

Let’s apply the rules from Lecture 3 (here, going in the forward direction) and add assert statements to show this in more detail.

Dafny

lemma Gauss2(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n == 0 {
    assert TriangleNumber(n) == 0; // by definition of TriangleNumber
    assert n * (n + 1) / 2 == 0; // by arithmetic
    // Therefore:
    assert TriangleNumber(n) == n * (n + 1) / 2;
  } else {
    var n' := n - 1;
    Gauss2(n');
    assert TriangleNumber(n') == n' * (n' + 1) / 2;
    // we get this information from the postcondition of the
    // call Gauss(n')

    assert TriangleNumber(n) == TriangleNumber(n') + n;
    // by definition of TriangleNumber

    // Therefore:
    assert TriangleNumber(n) == n' * (n' + 1) / 2 + n;

    // We also have:
    assert n' * (n' + 1) / 2 + n == (n - 1) * n / 2 + n;
    assert (n - 1) * n / 2 + n == (n - 1) * n / 2 + 2 * n / 2;
    assert (n - 1) * n / 2 + 2 * n / 2 == (n - 1 + 2) * n / 2;
    assert (n - 1 + 2) * n / 2 == n * (n + 1) / 2;
    assert TriangleNumber(n) == n * (n + 1) / 2;
  }
}

Sometimes, you may have to write out proofs in a lot of detail, maybe to figure out what’s missing in a proof that does not go through automatically or maybe to give the verifier enough hints about the proof structure so that it can complete the proof. When you do, long sequences of assert statements (like in Gauss2 above) are hard to read. Here are two structuring devices you can use to make proofs easier to read, assert by and calc.

Dafny

  lemma Gauss3(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n == 0 {
    assert TriangleNumber(n) == n * (n + 1) / 2 by {
      assert TriangleNumber(n) == 0; // by definition of TriangleNumber
      assert n * (n + 1) / 2 == 0; // by arithmetic
    }

  } else {
    assert TriangleNumber(n - 1) == (n - 1) * n / 2 by {
      var n' := n - 1;
      Gauss3(n');
      assert TriangleNumber(n') == n' * (n' + 1) / 2;
    }

    calc {
      // Note the semi-colon at the end of each line
      // it can be easy to forget
      TriangleNumber(n);
    ==  // by definition of TriangleNumber
      TriangleNumber(n - 1) + n;
    ==  // from the "assert by" above
      (n - 1) * n / 2 + n;
    ==  // arithmetic
      (n - 1) * n / 2 + 2 * n / 2;
    ==  // distribute * and +
      ((n - 1) + 2) * n / 2;
    ==  // arithmetic
      (n * (n + 1)) / 2;
    }
  }
}

Instead of just giving natural-language comments for the steps, you can add a pair of curly braces and justify a step by adding some code inside.

Dafny

lemma Gauss4(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n == 0 {
    // easy
  } else {
    calc {
      TriangleNumber(n);
    ==  // by definition of TriangleNumber
      TriangleNumber(n - 1) + n;
    ==  { Gauss4(n - 1); }  // this recursive call to the lemma
                            // obtains the induction hypothesis
      (n - 1) * n / 2 + n;
    ==  { assert n == 2 * n / 2; }
      (n - 1) * n / 2 + 2 * n / 2;
    ==  // arithmetic
      (n * (n + 1)) / 2;
    }
  }
}

The calc statement above is easy to read, but you don’t have to supply all the information to make the verifier happy. For example, the "==" between each line is the default operator and can be omitted. Here’s the same proof – shorter, but more cryptic.

Dafny

lemma Gauss5(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  if n != 0 { // to make things shorter, the "if" condition was
              // negated and one branch omitted
    calc {
      TriangleNumber(n);
      TriangleNumber(n - 1) + n;
      { Gauss5(n - 1); }
      (n - 1) * n / 2 + n;
      { assert n == 2 * n / 2; }
      (n - 1) * n / 2 + 2 * n / 2;
      (n * (n + 1)) / 2;
    }
  }
}

Often, much of the proof is carried out automatically, so you don’t need to provide many details. For example, consider the first Gauss lemma above. For simple cases like this, Dafny even performs a small amount of automatic induction. In effect, it implicitly inserts 
if n > 0 { Gauss(n - 1); }
into each lemma body. Thus, the following is also accepted as a valid proof:

Dafny

lemma Gauss6(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
}

But where’s the fun in that? You wouldn’t really learn anything. In fact, for Project 1 you’ll be required to disable automatic induction. Here’s how to do that for a lemma:

Dafny

lemma {:induction false} Gauss7(n: int)
  requires 0 <= n
  ensures TriangleNumber(n) == n * (n + 1) / 2
{
  // error is reported here, saying the verifier
  // cannot find the proof
}

Now that we understand what lemmas are, know that they can be called recursively (which, for a lemma, gives us the usual induction hypothesis), and have seen two basic proof-structuring constructs—assert by and calc—let’s start writing some proofs.

6.3 Sum of Cubes🔗

Let’s prove that the square of the sum of the first n positive numbers equals the sum of the first n positive cubes.

13+23+33+ ... +n3=(1+2+3+... +n)2

Rather than declaring the parameter to be of type "int" and using a precondition that says the parameter is non-negative, we can use the type "nat".

Dafny

function SumCubesThrough(n: nat): nat {
  if n == 0 then 0 else SumCubesThrough(n - 1) + n * n * n
}

lemma Sums(n: nat)
  ensures TriangleNumber(n) * TriangleNumber(n) ==
          SumCubesThrough(n)
{
  if n == 0 {
  } else {
    // For brevity, here are names for things with long names
    var tn := TriangleNumber(n);
    var tn' := TriangleNumber(n - 1);
    var s' := SumCubesThrough(n - 1);
    // Working with non-linear arithmetic can require a lot of
    // patience with the verifier. Sometimes, it can help to name
    // subexpressions, so we introduce the name "nn" here.
    var nn := n * n;
    calc {
      tn * tn;
      (tn' + n) * (tn' + n);
      tn' * tn' + 2 * tn' * n + nn;
      { Sums(n - 1); }
      s' + 2 * tn' * n + nn;
      { Gauss(n - 1); }
      s' + (n - 1) * nn + nn;
      s' + n * nn;
      SumCubesThrough(n);
    }
  }
}

6.4 Fibonacci🔗

Here’s the recursive (and very inefficient) implementation of Fibonacci.

Dafny

function Fib(n: nat): nat {
  if n < 2 then n else Fib(n - 2) + Fib(n - 1)
}

The example below shows that a calc doesn’t need to use == at every step—here, two of the steps use >= instead.

Dafny

lemma {:induction false} FibGetsLarger(n: nat)
  requires n >= 5
  ensures Fib(n) >= n
{
  if n == 5 {
    assert Fib(5) == 5;
  } else if n == 6 {
    assert Fib(6) == 8;
  } else {
    calc {
      Fib(n);
      Fib(n - 2) + Fib(n - 1);
    >=  { FibGetsLarger(n - 2); FibGetsLarger(n - 1); }
      n - 2 + n - 1;
    >=  { assert n >= 3; }
      n;
    }
  }
}

Note that the assert n >= 3; above is mostly for human readers. The verifier will still check that the assertion holds. However, if the verifier can finish the proof without relying on it, the assertion may seem misleading to a human. For instance, if you replace it with assert n >= 0; or assert 20 > 9;, the verifier will prove the condition, but it won’t actually aid the proof of the calc step.

6.5 Sum of Differences🔗

The next two lemmas demonstrate variations in proof style.

Here is a function that sums the elements of a given sequence.

Dafny

function Sum(s: seq<int>): int {
  if |s| == 0 then 0 else s[0] + Sum(s[1..])
}

This function computes the element-wise differences of two given sequences and sums up these differences.

Dafny

function SumOfDifferences(s: seq<int>, t: seq<int>): int
  requires |s| == |t|
{
  if |s| == 0 then
    0
  else s[0] - t[0] + SumOfDifferences(s[1..], t[1..])
}

We prove that a SumOfDifferences can also be computed by calling Sum. Like many other similar lemmas, the proof of can be written with a calc statement (as we’ll do in an example below). But to show a different way to approach a proof obligation, here is an alternative proof style where we start by writing down some things we know or believe to be true. Each such thing is written down with an assertion, which the verifier checks. Then, we hope that looking at these facts will give us an idea of how to use the induction hypothesis to compute the proof.

Dafny

lemma {:induction false} SequenceMinus(s: seq<int>, t: seq<int>)
  requires |s| == |t|
  ensures SumOfDifferences(s, t) == Sum(s) - Sum(t)
{
  if |s| == 0 {
  } else {
    // Here are some things we know:
    assert SumOfDifferences(s, t) ==
           s[0] - t[0] + SumOfDifferences(s[1..], t[1..]);
    assert Sum(s) == s[0] + Sum(s[1..]);
    assert Sum(t) == t[0] + Sum(t[1..]);
    // By calling the lemma recursively, we can obtain a property
    // that relates the Sum(_[1..]) terms on the previous two lines.
    assert SumOfDifferences(s[1..], t[1..]) ==
           Sum(s[1..]) - Sum(t[1..])
           by {SequenceMinus(s[1..], t[1..]);
    }
  }
}

We can turn the previous proof into a proof calculation. When the proof goal of the lemma is an equality, then a typical way to write a proof calculation is to start from the "more complicated" side of the equality. Sometimes, we may need to start from both ends to see if we can connect the pieces. Which do you find easier to read or write?

Dafny

lemma {:induction false} SequenceMinus'(s: seq<int>, t: seq<int>)
  requires |s| == |t|
  ensures SumOfDifferences(s, t) == Sum(s) - Sum(t)
{
  if |s| == 0 {
  } else {
    calc {
      // Here, we start from the LHS of the proof goal
      SumOfDifferences(s, t);
      // apply the definition of `SumOfDifferences`
      s[0] - t[0] + SumOfDifferences(s[1..], t[1..]);
      // In the line above, we have something that looks
      // like a smaller version of the proof goal,
      // so let's call the lemma recursively
      { SequenceMinus'(s[1..], t[1..]); }
      s[0] - t[0] + Sum(s[1..]) - Sum(t[1..]);

      // From the definition of `Sum(s)`
      s[0] + Sum(s[1..]) - t[0] - Sum(t[1..]);

      Sum(s) - Sum(t);
    }
  }
}

6.6 Multiplication is Commutative🔗

In the following example, we will establish the commutativity of multiplication.

Dafny

function Mult(x:nat, y:nat):nat{
  if y == 0 then 0 else x + Mult(x, y-1)
}

We now proceed to formally prove the commutativity of multiplication.

Dafny

lemma MultiComm (x:nat, y:nat)
  ensures Mult(x,y) == Mult(y,x)
{
  if y==0{
  }else{
    calc{
      Mult(x,y);
    ==
      x + Mult(x, y-1);
    ==
      x + Mult(y-1,x);
    }
  }
}

lemma {:induction false} MultiComm2 (x:nat, y:nat)
  ensures Mult(x,y) == Mult(y,x)
{
  if x == y {
  }else if x == 0{
    {MultiComm2(x,y-1);}
  }else if y==0{
    MultiComm2(x-1, y);
  }
  else{
    calc{
      Mult(x,y);
    ==
      x + Mult(x, y-1);
    ==
       {MultiComm2(x,y-1);}
      x + Mult(y-1,x);
    ==
      x + y-1 + Mult(y-1,x-1);
    ==
       {MultiComm2(x-1,y-1);}
      x + y-1 + Mult(x-1,y-1);
    ==
      y + Mult(x-1,y);
    == {MultiComm2(x-1, y);}
      y + Mult(y,x-1);
    ==
      Mult(y,x);
    }
  }
}

lemma {:induction false} MultiComm3 (x:nat, y:nat)
  ensures Mult(x,y) == Mult(y,x)
{
  if x == y {
  }else if x == 0{
    {MultiComm3(x,y-1);}
  }else if y==0{
    MultiComm3(x-1, y);
  }
  else{
      assert Mult(x,y)  == x + Mult(x, y-1);
      assert x + Mult(x, y-1)== x + Mult(y-1,x)
          by  {MultiComm3(x,y-1);}
      assert x + Mult(y-1,x) == x + Mult(y-1,x);
      assert  x + Mult(y-1,x) ==  x + y-1 + Mult(y-1,x-1);
     assert x + y-1 + Mult(y-1,x-1) ==  x + y-1 + Mult(x-1,y-1)
          by {MultiComm3(x-1,y-1);}
     assert x + y-1 + Mult(x-1,y-1) ==  y + Mult(x-1,y);
     assert y + Mult(x-1,y) ==  y + Mult(y,x-1)
            by {MultiComm3(x-1, y);}
     assert y + Mult(y,x-1) == Mult(y,x);
    }
  }

6.7 Postage Stamps🔗

Consider the following problem: every amount of postage that is at least 12 cents can be made from 3-cent and 4-cent stamps We can try to prove that using a lemma like this:

Dafny

lemma PostageStampsExists(amount: int)
  requires 12 <= amount
  ensures exists threes, fours :: 0 <= threes
          && 0 <= fours && 3 * threes + 4 * fours == amount

The existential quantifier in the postcondition may look frightening. But there is another way to express the property. Very often when you have to prove the existence of something (here, nonnegative values for threes and fours), you end up constructing those somethings. That means you can write a method that computes the somethings and returns the somethings in out-parameters. In fact, you can do the same for lemmas, because lemmas can have out-parameter, too! So, here is a logically equivalent way of stating the lemma, but one that is more straightforward to work with.

Dafny

lemma PostageStamps(amount: int) returns (threes: nat, fours: nat)
  requires 12 <= amount
  ensures 3 * threes + 4 * fours == amount
{
  if amount == 12 {
    threes, fours := 0, 3;
  } else {
    threes, fours := PostageStamps(amount - 1);
    if threes == 0 {
      assert 3 <= fours;
      fours := fours - 3;
      threes := threes + 4;
    }
    assert 3 * threes + 4 * fours == amount - 1;
    threes := threes - 1;
    fours := fours + 1;
  }
}

Now, let us change the problem slightly: every amount of postage that is at least 12 cents can be made from 3-cent and 7-cent stamps. We will prove it using regular induction in PostageStamps2 and strong induction in PostageStamps3.

Dafny

lemma PostageStamps2(amount: int) returns (threes: nat, sevens: nat)
  requires 12 <= amount
  ensures 3 * threes + 7 * sevens == amount
{
  if amount ==12{
    threes := 4;
    sevens := 0;
  }else{
    threes, sevens := PostageStamps2(amount - 1);
    assert threes >= 2 || sevens >= 2;
    if threes >= 2{
      threes := threes - 2 ;
      sevens := sevens + 1;
    }else if sevens >= 2{
      sevens := sevens -2;
      threes := threes +5 ;
    }
    assert 3 * threes + 7 * sevens == amount;
  }
}

lemma PostageStamps3(amount: int) returns (threes: nat, sevens: nat)
  requires 12 <= amount
  ensures 3 * threes + 7 * sevens == amount
{
  if amount ==12{
    threes := 4;
    sevens := 0;
  }else if amount == 13{
    threes := 2;
    sevens := 1;
  }else if amount == 14{
    threes := 0;
    sevens := 2;
  }else{
    threes, sevens := PostageStamps3(amount - 3);
    threes := threes + 1;
    assert 3 * threes + 7 * sevens == amount;
  }
}

6.8 Reversing a Sequence🔗

Dafny

function Reverse(s: seq<int>): seq<int> {
  if s == [] then [] else Reverse(s[1..]) + [s[0]]
}

lemma ReverseShuffle(s: seq<int>, x: int)
  ensures Reverse(s + [x]) == [x] + Reverse(s)
{
  if s == [] {
    // let's write out simplifications of the various subexpressions
    assert s + [x] == [x];
    assert Reverse([x]) == [x];
    assert Reverse(s) == [];
    assert [x] + Reverse(s) == [x];
  } else {
    var s' := s + [x];
    calc {
      Reverse(s');
      // definition of Reverse
      Reverse(s'[1..]) + [s'[0]];
      { assert s'[1..] == s[1..] + [x]; }
      Reverse(s[1..] + [x]) + [s'[0]];
      { ReverseShuffle(s[1..], x); }
      [x] + Reverse(s[1..]) + [s'[0]];
      { assert s'[0] == s[0]; }
      [x] + Reverse(s[1..]) + [s[0]];
      // definition of Reverse
      [x] + Reverse(s);
    }
  }
}

lemma ReverseIsItsOwnInverse(s: seq<int>)
  ensures Reverse(Reverse(s)) == s
{
  if s == [] {
  } else {
    calc {
      Reverse(Reverse(s));
      Reverse(Reverse(s[1..]) + [s[0]]);
      { ReverseShuffle(Reverse(s[1..]), s[0]); }
      [s[0]] + Reverse(Reverse(s[1..]));
      { ReverseIsItsOwnInverse(s[1..]); }
      [s[0]] + s[1..];
      s;
    }
  }
}

In this example, we’ll use a pair of integers ‘(x, y)‘ to represent an interval from ‘x‘ to, but not including, ‘y‘. For such a pair ‘p‘, its two components are denoted ‘p.0‘ and ‘p.1‘.

Dafny

function InInterval(i: int, p: (int, int)): bool {
  p.0 <= i < p.1
}

A number is in an interval sequence if it is in any of its intervals.

Dafny

function InIntervalSequence(i: int, s: seq<(int, int)>): bool {
  if |s| == 0 then
    false
  else if InInterval(i, s[0]) then
    true
  else
    InIntervalSequence(i, s[1..])
}

Before we continue, let’s consider an alternative definition of InIntervalSequence.

Dafny

function InIntervalSequence'(i: int, s: seq<(int, int)>): bool {
  |s| != 0 && (InInterval(i, s[0]) ||
     InIntervalSequence'(i, s[1..]))
}

Are these two the same definition? Let’s prove that they are.

Dafny

lemma {:induction false} SameIntervalDefinitions(i: int, s: seq<(int, int)>)
  ensures InIntervalSequence(i, s) == InIntervalSequence'(i, s)
{
  // Let's divide up the proof into three cases
  if |s| == 0 {
    assert !InIntervalSequence(i, s);
    assert !InIntervalSequence'(i, s);
  } else if InInterval(i, s[0]) {
    assert InIntervalSequence(i, s);
    assert InIntervalSequence'(i, s);
  } else {
    assert InIntervalSequence(i, s) == InIntervalSequence(i, s[1..]);
    assert InIntervalSequence'(i, s) == InIntervalSequence'(i, s[1..]);
    SameIntervalDefinitions(i, s[1..]);
  }
}

Here is an even simpler proof:

Dafny


lemma {:induction false} SameIntervalDefinitions2(i: int, s: seq<(int, int)>)
  ensures InIntervalSequence(i, s) == InIntervalSequence'(i, s)
{
  if |s| == 0 {
    assert InIntervalSequence(i, s) ==  InIntervalSequence'(i, s);
  }else{
    calc{
      InIntervalSequence(i, s);
      InInterval(i, s[0]) || InIntervalSequence(i, s[1..]);
      InIntervalSequence'(i, [s[0]]) || InIntervalSequence(i, s[1..]);
      {SameIntervalDefinitions2(i, s[1..]);}
      InIntervalSequence'(i, [s[0]]) || InIntervalSequence'(i, s[1..]);
       InIntervalSequence'(i, s);
    }
  }
}

lemma {:induction false} SameIntervalDefinitions3(i: int, s: seq<(int, int)>)
  ensures InIntervalSequence(i, s) == InIntervalSequence'(i, s)
{
  if |s| == 0 || InInterval(i, s[0]) {
  }else{
      assert InIntervalSequence(i, s) == InIntervalSequence(i, s[1..]);
      assert InIntervalSequence'(i, s) == InIntervalSequence'(i, s[1..]);
      SameIntervalDefinitions3(i, s[1..]);
  }
}

Let’s consider a function that optimizes interval sequences. We won’t be terribly inventive here, just enough to show a flavor of proving that an optimized version of a data structure represents the same numbers as the original.

Dafny

function Optimize(s: seq<(int, int)>): seq<(int, int)> {
  if s == [] then
    []
  else if s[0].1 <= s[0].0 then
    // interval s[0] is empty, so let's omit it
    Optimize(s[1..])
  else
    [s[0]] + Optimize(s[1..])
}

Dafny

lemma {:induction false} OptimizationIsCorrect(i: int, s: seq<(int, int)>)
  ensures InIntervalSequence(i, Optimize(s)) == InIntervalSequence(i, s)
{
  // We consider the same three cases as in the Optimize function.
  if s == [] {
    // easy
  } else if s[0].1 <= s[0].0 {
    assert !InInterval(i, s[0]);
    OptimizationIsCorrect(i, s[1..]);
  } else {
    // This is almost too easy.
    // Once we figure out how to apply the induction hypothesis,
    // the automated verifier does all of the heavy lifting.
    OptimizationIsCorrect(i, s[1..]);
  }
}

    contents    up