class IntegerInduction {
  // This class considers different ways of proving, for any natural n:
  //   (SUM i in [0, n] :: i^3) == (SUM i in [0, n] :: i)^2

  // In terms of Dafny functions, the theorem to be proved is:
  //   SumOfCubes(n) == Gauss(n) * Gauss(n)

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

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

  // Here is one proof.  It uses a lemma, which is proved separately.

  ghost method Theorem0(n: int)
    requires 0 <= n;
    ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
  {
    if (n != 0) {
      call Theorem0(n-1);
      call Lemma(n-1);
    }
  }

  ghost method Lemma(n: int)
    requires 0 <= n;
    ensures 2 * Gauss(n) == n*(n+1);
  {
    if (n != 0) { call Lemma(n-1); }
  }

  // Here is another proof.  It states the lemma as part of the theorem, and
  // thus proves the two together.

  ghost method Theorem1(n: int)
    requires 0 <= n;
    ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
    ensures 2 * Gauss(n) == n*(n+1);
  {
    if (n != 0) {
      call Theorem1(n-1);
    }
  }

  ghost method DoItAllInOneGo()
    ensures (forall n :: 0 <= n ==>
                SumOfCubes(n) == Gauss(n) * Gauss(n) &&
                2 * Gauss(n) == n*(n+1));
  {
  }

  // Here is another proof.  It makes use of Dafny's induction heuristics to
  // prove the lemma.

  ghost method Theorem2(n: int)
    requires 0 <= n;
    ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
  {
    if (n != 0) {
      call Theorem2(n-1);

      assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
    }
  }

  ghost method M(n: int)
    requires 0 <= n;
  {
    assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1));  // manually assume the induction hypothesis
    assert 2 * Gauss(n) == n*(n+1);
  }

  // Another way to prove the lemma is to supply a postcondition on the Gauss function

  ghost method Theorem3(n: int)
    requires 0 <= n;
    ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
  {
    if (n != 0) {
      call Theorem3(n-1);
    }
  }

  function GaussWithPost(n: int): int
    requires 0 <= n;
    ensures 2 * GaussWithPost(n) == n*(n+1);
  {
    if n == 0 then 0 else GaussWithPost(n-1) + n
  }

  // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction

  ghost method Theorem4()
    ensures (forall n :: 0 <= n ==>
        SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));
  {
    // look ma, no hints!
  }

  ghost method Theorem5(n: int)
    requires 0 <= n;
    ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
  {
    // the postcondition is a simple consequence of these quantified versions of the theorem:
    if (*) {
      assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
    } else {
      call Theorem4();
    }
  }

  // The body of this function method gives a single quantifier, which leads to an efficient
  // way to check sortedness at run time.  However, an alternative, and ostensibly more general,
  // way to express sortedness is given in the function's postcondition.  The alternative
  // formulation may be easier to understand for a human and may also be more readily applicable
  // for the program verifier.  Dafny will show that postcondition holds, which ensures the
  // equivalence of the two formulations.
  // The proof of the postcondition requires induction.  It would have been nicer to state it
  // as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the
  // possibility of applying induction.  Instead, the "==>" and "<==" cases are given separately.
  // Proving the "<==" case is simple; it's the "==>" case that requires induction.
  // The example uses an attribute that requests induction on just "j".  However, the proof also
  // goes through by applying induction on both bound variables.
  function method IsSorted(s: seq<int>): bool
    ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
    ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
  {
    (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
  }
}

datatype Tree<T> {
  Leaf(T);
  Branch(Tree<T>, Tree<T>);
}

class DatatypeInduction<T> {
  function LeafCount<T>(tree: Tree<T>): int
  {
    match tree
    case Leaf(t) => 1
    case Branch(left, right) => LeafCount(left) + LeafCount(right)
  }

  method Theorem0(tree: Tree<T>)
    ensures 1 <= LeafCount(tree);
  {
    assert (forall t: Tree<T> :: 1 <= LeafCount(t));
  }

  // see also Test/dafny0/DTypes.dfy for more variations of this example
}

// ----------------------- Induction and case splits -----------------
// This is a simple example where the induction hypothesis and the
// case splits are decoupled.

datatype D = Nothing | Something(D);

function FooD(n: nat, d: D): int
  ensures 10 <= FooD(n, d);
{
  match d
  case Nothing =>
    if n == 0 then 10 else FooD(n-1, #D.Something(d))
  case Something(next) =>
    if n < 100 then n + 12 else FooD(n-13, next)
}