// This file defines some functions that we ask you to prove lemmas about.
// Please don't modify it or turn it in.

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

  function Fib3(n: int): int {
    if n < 3 then n else Fib3(n - 3) + Fib3(n - 2) + Fib3(n - 1)
  }

  function Fibly(n: int): int {
    if n < 2 then n else Fibly(n - 2) - Fibly(n - 1)
  }

  function IterativeAdding(k: int, a: int, b: int): int
    requires 0 <= k
  {
    if k == 0 then a else IterativeAdding(k - 1, b, a + b)
  }

  // Function `Pow(n)` computes `2^n` (that is, 2 to the power of `n`).
  function Pow(n: nat): int
  {
    if n == 0 then 1 else 2 * Pow(n - 1)
  }

  // A quicker way to compute `2^n` squares intermediate results.
  function FastPow(n: nat): int
  {
    if n == 0 then
      1
    else
      var half := n / 2;
      var p := FastPow(half);
      if n % 2 == 0 then
        p * p
      else
        2 * p * p
  }

  // A given, arbitrary (that is, body-less) function.
  function F(x: int): int

  // The next two functions repeatedly apply `F` `n` times to a
  // given value `x`. Function `IterApply` first recurses to apply
  // the function `n - 1` times and then applies `F` once more.
  function IterApply(n: nat, x: int): int
  {
    if n == 0 then x else F(IterApply(n - 1, x))
  }

  // Function `IterApply'` does it by first applying `F` to the given
  // value `x` and then applying `F` `n - 1` times to the result.
  function IterApply'(n: nat, x: int): int
  {
    if n == 0 then x else IterApply'(n - 1, F(x))
  }

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

  // This function triples each number in the given sequence and
  // sums these up.
  function SumTriples(s: seq<int>): int {
    if |s| == 0 then 0 else 3 * s[0] + SumTriples(s[1..])
  }

  // The tuple type `(int, int)` denotes pairs of integers.
  // To create a pair, use parentheses, like `(34, 55)`.
  // Given a pair `p`, you can refer to its two components as `p.0` and `p.1`.
  //
  // Note: Because we have specifications, we can limit use of this
  // function to sequences of the same length. You've probably written
  // similar programs in other classes and wondered what how to handle
  // the case where `s` and `t` have different lengths. Here, we don't
  // have to handle other cases.
  function Zip(s: seq<int>, t: seq<int>): seq<(int, int)>
    requires |s| == |t|
  {
    if |s| == 0 then [] else [(s[0], t[0])] + Zip(s[1..], t[1..])
  }

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

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