// Do NOT use automatic induction anywhere in this assignment. Dafny turns
// on automatic induction by default, so each lemma has to explicitly disable
// it. This is done by using the attribute `{:induction false}`.

include "pset02_definitions.dfy"

module Pset2 {
  // A module is a unit of related definitions in Dafny. The following line
  // makes all of the functions we have defined in the Defs module in
  // `pset02_definitions.dfy` available here, using their same names:
  import opened Defs
  // (This is convenient, but can make it harder to keep track of where
  // everything is defined!)

  // Prove the following lemma. That is, write a body for it that verifies.
  // You are to complete the proof without Dafny's automatic induction, so
  // keep the `{:induction false}` attribute.
  lemma {:induction false} Fib3GetsLarger(n: int)
    ensures n <= Fib3(n)

  // -------------------------------

  // Prove the following lemma. Do not rely on automatic induction
  // (that is, keep the `{:induction false}` attribute).
  lemma {:induction false} FibFibly(n: nat)
    ensures n % 2 == 0 ==> Fib(n) == -Fibly(n)
    ensures n % 2 != 0 ==> Fib(n) == Fibly(n)

  // -------------------------------

  // The `Fib` function exhibits terrible run-time behavior. A more
  // efficient way to compute `Fib(n)` is to call `IterativeAdding(n, 0, 1)`.
  // Prove that these two are the same by filling in the proof of
  // lemma `SameAsFib`.
  // Hint: You will need to prove a result that's more general than what
  // `SameAsFib` states. Define a second lemma for the more general
  // property, write a proof for it (with `{:induction false}`), and
  // call the second lemma from `SameAsFib` to give a proof for `SameAsFib`.
  // Still stuck? Step through `IterativeAdding(n, 0, 1)` for e.g. `n = 8`
  // and look for a pattern that generalizes to `a` & `b` other than 0 & 1.
  lemma {:induction false} SameAsFib(n: int)
    requires 0 <= n
    ensures Fib(n) == IterativeAdding(n, 0, 1)

  // -------------------------------

  // Prove the following distribution property of `Pow`.
  lemma {:induction false} Squaring(m: nat, n: nat)
    ensures Pow(m + n) == Pow(m) * Pow(n)

  // Prove that `Pow` and `FastPow` compute the same function.
  // Do not rely on automatic induction (that is, keep the `{:induction false}`
  // attribute).
  // Hint: This proof may make use of the `Squaring` lemma above.
  lemma {:induction false} FastPowCorrect(n: nat)
    ensures Pow(n) == FastPow(n)

  // -------------------------------

  // Prove that `IterApply'` satisfies the same recurrence pattern as in
  // the definition of `IterApply`.
  // Hint: Depending on how you write the proof, you may need to use
  // the property that a function distributes over if-then-else:
  //     F(if A then B else C) == if A then F(B) else F(C)
  lemma {:induction false} IterShuffle(n: nat, x: int)
    ensures IterApply'(n, x) == if n == 0 then x else F(IterApply'(n - 1, x))

  // Prove that `IterApply` and `IterApply'` come up with the same result.
  // Hint: Use `IterShuffle` in the proof.
  lemma {:induction false} SameIters(n: nat, x: int)
    ensures IterApply(n, x) == IterApply'(n, x)

  // -----------------------------------------------------------

  // State and prove a lemma to show that another way to compute
  // `SumTriples` is to first just sum the elements and then triple
  // that sum.
  lemma {:induction false} TripleSum(s: seq<int>)

  // ---------------------------------------------------

  // Prove the following lemma.
  lemma {:induction false} DoubleSum(s: seq<int>)
    ensures Sum(SumEachPair(Zip(s, s))) == 2 * Sum(s)
}