// We now consider proving that programs terminate. As it turns out, Dafny has
// proved termination all along, but so far our examples have been simple
// enough that we (mostly) haven't needed to do anything ourselves. In this next
// pair of classes, we'll learn the general technique to specify and verify the
// absence of infinite recursion. In a few weeks, we'll apply the same ideas to prevent
// infinite loops.

// Why is it necessary to prove termination?
// If we ignored termination, then we would accept a method like

predicate P(x: int)

method M(x: int)
  ensures P(x)
{
  M(x); // bad: infinite recursion
}

// for any predicate `P`. This is bad, because a call to `M` would never return.
// In a running program, you may be able to detect this behavior, because the
// program may be running for a suspiciously long time, or it may crash with a
// stack overflow.

// The situation for a lemma is arguably worse. Since a lemma is not compiled,
// infinite recursion in a lemma does not by itself lead to long execution times
// or stack overflows, but the presence of such a lemma can give us incorrect
// information. For example, the postcondition of the following lemma tells us
// that `P(x)` holds in `LCaller`. This can lead to missed errors in a caller.

lemma L(x: int)
  ensures P(x)
{
  L(x); // bad: infinite recursion
}

method LCaller(x: int) returns (y: int)
  ensures 0 <= y
{
  L(x);
  if P(x) {
    return 2;
  } else {
    // According to the lemma's postcondition, this is dead code.
    return 100 - x;
  }
}

// Infinite recursion for a function also leads to trouble. Not only would such
// a function have the same undesirable run-time behavior as infinite methods, but
// admitting a function with infinite recursion may in a subtle way introduce
// mathematical inconsistencies. For example, consider a function defined to
// return a value that's larger than the function result itself:

function F(x: int): int {
  1 + F(x) // bad: infinite recursion
}

// Such a function would allow a method to prove contradictory assertions.

method FCaller() returns (y: int)
  ensures 0 <= y
{
  assert F(5) == 1 + F(5);
  assert false;
  return -19;
}

// There are several ways to avoid mathematical inconsistencies in function
// definitions, but checking for termination is the most straightforward and
// most commonly used way to do so.

// How to establish termination. See SLIDES.
//   - Diagrams/animations in slides.
//   - Well-founded orders
//   - `decreases` clauses

// Here are some simple examples that we've seen variations of already:

function Factorial(n: nat): nat
  decreases n
{
  if n > 0 then n * Factorial(n - 1) else 1
}

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

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

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

// When we saw these before, we didn't have to write `decreases` specifications.
// How come? For every recursive (or mutually recursive) function/lemma/method,
// Dafny defines a default `decreases` clause, which is used if the
// function/lemma/method does not declare an explicit `decreases` clause. For a
// function/lemma/method with a parameter `x`, the default is `decreases x`. For
// lots of functions, lemmas, and methods, including the examples above, this simple
// default is correct, so the verifier uses it and proves termination without having
// to bother us about it at all.

// Here's another function and proof we saw before:

function Pow(n: nat): int
  decreases n
{
  if n == 0 then 1 else 2 * Pow(n - 1)
}

lemma PowPlusDist(m: nat, n: nat)
  ensures Pow(m + n) == Pow(m) * Pow(n)
  decreases m
{
  if m == 0 {
  } else {
    calc {
      Pow(m) * Pow(n);
      2 * Pow(m - 1) * Pow(n);
      2 * (Pow(m - 1) * Pow(n));
      { PowPlusDist(m - 1, n); } // here is the recursive call; notice that our termination metric goes down
      2 * Pow(m + n - 1);
      Pow(m + n);
    }
  }
}

// The PowPlusDist lemma looks at parameter `m`. Here's an alternative version that
// instead looks at parameter `n`.
lemma PowPlusDist'(m: nat, n: nat)
  ensures Pow(m + n) == Pow(m) * Pow(n)
  decreases n
{
  if n == 0 {
  } else {
    calc {
      Pow(m) * Pow(n);
      Pow(m) * (2 * Pow(n - 1));
      2 * (Pow(m) * Pow(n - 1));
      { PowPlusDist'(m, n - 1); } // here is the recursive call; notice that our termination metric goes down
      2 * Pow(m + n - 1);
      Pow(m + n);
    }
  }
}

function FastPow(n: nat): int
  decreases n
{
  if n == 0 then
    1
  else
    var half := n / 2;
    var p := FastPow(half); // How do we know `half < n`? Because `0 < n`.
    if n % 2 == 0 then
      p * p
    else
      2 * p * p
}

// Note that Pow and FastPow have the same `decreases` specification, even though their recursive
// patterns are different. That's fine. Here's another example that uses both recursion patterns:

function AlsoFastPow(n: nat): int
  decreases n
{
  if n == 0 then
    1
  else if n % 2 == 1 then
    2 * AlsoFastPow(n - 1)
  else
    var p := AlsoFastPow(n / 2);
    p * p
}

// A lemma can do that, too:

lemma {:induction false} FastPowsAreTheSame(n: nat)
  ensures FastPow(n) == AlsoFastPow(n)
  decreases n
{
  if n == 0 {
  } else if n % 2 == 1 {
    FastPowsAreTheSame(n - 1);
  } else {
    FastPowsAreTheSame(n / 2);
  }
}

// A `decreases` clause doesn't have to list just a parameter. Any expression is allowed.
// The value of the expression is evaluated on entry to the function/lemma/method.
// As a silly example,

function Fib2(n: nat): nat
  decreases 2 * n + 15
{
  if n < 2 then n else Fib2(n - 2) + Fib2(n - 1)
}

// Let's do some more examples, where the default `decreases` clause does not let
// us prove termination, and we have to supply a better `decreases` clause ourselves.

function SumRange(s: seq<int>, lo: int, hi: int): int
  requires 0 <= lo <= hi <= |s|
  decreases hi
{
  if hi == lo then 0 else SumRange(s, lo, hi - 1) + s[hi - 1]
}

function SumRange'(s: seq<int>, lo: int, hi: int): int
  requires 0 <= lo <= hi <= |s|
  decreases hi - lo
{
  if hi == lo then 0 else s[lo] + SumRange'(s, lo + 1, hi)
}

// Here are some examples that perform merges.

function MergeLists(xs: List<int>, ys: List<int>): List<int>
  decreases Length(xs) + Length(ys)
{
  match (xs, ys)
  case (Nil, _) => ys
  case (_, Nil) => xs
  case (Cons(x, xs'), Cons(y, ys')) =>
    if x <= y then
      Cons(x, MergeLists(xs', ys))
    else
      Cons(y, MergeLists(xs, ys'))
}

function MergeSequences(a: seq<int>, b: seq<int>): seq<int>
  decreases |a| + |b|
{
  if a == [] then
    b
  else if b == [] then
    a
  else if a[0] <= b[0] then
    [a[0]] + MergeSequences(a[1..], b)
  else
    [b[0]] + MergeSequences(a, b[1..])
}

function MergeSequencesFrom(a: seq<int>, b: seq<int>, i: nat, j: nat): seq<int>
  requires i <= |a| && j <= |b|
  decreases |a| + |b| - i - j
{
  if i == |a| then
    b[j..]
  else if j == |b| then
    a[i..]
  else if a[i] <= b[j] then
    [a[i]] + MergeSequencesFrom(a, b, i + 1, j)
  else
    [b[j]] + MergeSequencesFrom(a, b, i, j + 1)
}

// In our examples so far, the `decreases` clause always used a natural number (that is, a non-negative
// integer). That's just a special (but common) case. We're going to build up to more complicated types.
// The next one to consider, and which also we have tacitly seen before, are datatypes.

// A fancier (and more precise) name for the algebraic datatypes that we use throughout this class is
// _inductive_ datatypes. Essentially, this means that the datatype values are constructed "bottom up".
// For example, if you want to construct a `List` of length 5, you first "construct" the value `Nil`,
// and then you construct longer and longer lists by using `Cons` 5 times. If you go the other direction,
// the process of deconstructing (or dismantling, or "destructing") datatype values always comes to an
// end. More formally, there is a well-founded order on datatype values such that deconstruction gives
// you smaller values. This well-founded order (or, in all fairness, one such well-founded order) is
// known as _structural inclusion_. Using `>` to denote this order, here are some examples:

datatype List<X> = Nil | Cons(head: X, tail: List<X>)
  
lemma ListExamples(xs: List<int>) {
  assert Cons(728, Cons(1500, Cons(-50, xs)))
      > Cons(1500, Cons(-50, xs))
      > Cons(-50, xs)
      > xs;
}

// Note that the `head` value of these examples does not play a role in the ordering, because they
// are not datatypes. If `head` is a datatype, then the same rules apply across the different types.

datatype Color = Red | Green | Blue

lemma ColorListExamples(c: Color, d: Color) {
  assert Cons(c, Cons(d, Nil)) > Cons(d, Nil) > d;
}
  
// Here are more examples, using a different datatype.

datatype Tree = Leaf | Node(left: Tree, right: Tree)

lemma TreeExamples(a: Tree, b: Tree) {
  assert Node(a, b) > a;
  assert Node(a, b) > b;
  assert Node(a, Leaf) > Leaf;
  assert Node(Leaf, b) > Leaf;
}

// Here are two List functions and a lemma that we've seen before, but now
// showing the `decreases` clauses explicitly.

function Length<X>(xs: List<X>): nat
  decreases xs
{
  match xs
  case Nil => 0
  case Cons(_, tail) => 1 + Length(tail)
}

function Append<X>(xs: List<X>, ys: List<X>): List<X>
  decreases xs
{
  match xs
  case Nil => ys
  case Cons(x, tail) => Cons(x, Append(tail, ys))
}

lemma AppendLength<X>(xs: List<X>, ys: List<X>)
  ensures Length(Append(xs, ys)) == Length(xs) + Length(ys)
  decreases xs
{
  match xs
  case Nil =>
  case Cons(x, tail) =>
    calc {
      Length(Append(xs, ys));
      Length(Append(Cons(x, tail), ys));
      Length(Cons(x, Append(tail, ys)));
      1 + Length(Append(tail, ys));
      { AppendLength(tail, ys); } // induction hypothesis; note that xs > tail
      1 + Length(tail) + Length(ys);
      Length(Cons(x, tail)) + Length(ys);
      Length(xs) + Length(ys);
    }
}

// Finally, here is an example that uses mutual recursion.

datatype Expr =
  | Const(c: int)
  | Var(name: string)
  | NAry(op: Operator, args: List<Expr>)
type Operator

function Subst(e: Expr, name: string, x: int): Expr
  decreases e
{
  match e
  case Const(_) => e
  case Var(n) => if n == name then Const(x) else e
  case NAry(op, args) => NAry(op, SubstList(args, name, x))
}

function SubstList(es: List<Expr>, name: string, x: int): List<Expr>
  decreases es
{
  match es
  case Nil => Nil
  case Cons(e, tail) => Cons(Subst(e, name, x), SubstList(tail, name, x))
}

lemma SubstIdempotent(e: Expr, name: string, x: int)
  ensures Subst(Subst(e, name, x), name, x) == Subst(e, name, x)
  decreases e
{
  match e
  case Const(_) =>
  case Var(_) =>
  case NAry(op, args) =>
    SubstListIdempotent(args, name, x);
}

lemma SubstListIdempotent(es: List<Expr>, v: string, c: int)
  ensures SubstList(SubstList(es, v, c), v, c) == SubstList(es, v, c)
  decreases es
{
  match es
  case Nil =>
  case Cons(e, tail) =>
    calc {
      SubstList(SubstList(es, v, c), v, c);
    ==  // def. inner SubstList
      SubstList(Cons(Subst(e, v, c), SubstList(tail, v, c)), v, c);
    ==  // def. outer SubstList
      Cons(Subst(Subst(e, v, c), v, c), SubstList(SubstList(tail, v, c), v, c));
    ==  { SubstIdempotent(e, v, c); }
      Cons(Subst(e, v, c), SubstList(SubstList(tail, v, c), v, c));
    ==  { SubstListIdempotent(tail, v, c); }
      Cons(Subst(e, v, c), SubstList(tail, v, c));
    ==  // def. SubstList
      SubstList(es, v, c);
    }
}