// In this file, you can find hints and suggestions for...
//  - writing ReverseLoop
//  - writing and verifying Split
//  - writing and verifying ComputeIsClosed


// ╭─────────────────────╮
// │ writing ReverseLoop │
// ╰─────────────────────╯

// A good way to go about ReverseLoop is to keep "popping" elements off of the
// front of the input list while "pushing" them onto the front of an accumulator
// list.


// ╭─────────────────────────────╮
// │ writing and verifying Split │
// ╰─────────────────────────────╯

// To verify Split, we found this lemma helpful.
lemma ReverseZip<X>(xs: List<X>, ys: List<X>)
  requires Length(xs) == Length(ys)
  ensures Reverse(Zip(xs, ys)) == Zip(Reverse(ys), Reverse(xs))

// Your implementation of Split should probably build up the two output lists xs
// and ys one element at a time, which is naturally done by repeatedly adding
// new elements to their beginnings, finishing by reversing them (using your
// ReverseLoop).  A key challenge is choosing a good loop invariant.  We suggest
// including an equation between argument ws and a way of reassembling its value
// using the variables the loop modifies.  (One of those variables will probably
// be initialized with ws but gradually reduced by "popping" elements off its
// front.)


// ╭─────────────────────────────────────────────────────────╮
// │ writing and verifying ComputeIsClosed (cycle detection) │
// ╰─────────────────────────────────────────────────────────╯

// We found two pretty different solutions to the problem, but let us sketch one
// of them here.

// We found the following helper method useful.
method ComputeToFirstDup<X>(f: X -> X, start: X, s: set<X>) returns (path: seq<X>)
  ensures |path| > 0
  ensures forall i :: 0 <= i < |path| ==> path[i] == Repeat(f, i, start)
  ensures forall x :: x in path[..|path|-1] ==> x in s
  ensures var last := path[|path|-1]; last !in s || last in path[..|path|-1]
// That is, this method finds the shortest sequence of the form
//   start, f(start), f(f(start)), ...
// that either encounters a duplicate or a value not in s.

// Further, to prove termination of the loop we put in the body of that method,
// we used this lemma, which is something of an application of the pigeonhole
// principle.
lemma DupFreeLengthBound<X>(path: seq<X>, s: set<X>)
  requires forall i, j :: 0 <= i < j < |path| ==> path[i] != path[j]
  requires forall x :: x in path ==> x in s
  ensures |path| <= |s|

// Our ComputeIsClosed calls ComputeToFirstDup, and, in the case where it does find a
// duplicate, we proceed to reason about how every element in the full sequence of
// repeated f application is represented in the path, hence all are in s.  The
// following two lemmas are helpful to express that argument, combined with some
// reasoning about quotients and remainders.  Specifically, if we say the
// previous matching path element appears at position i and the new duplicate at
// position j, then we get a repeating cycle of elements of length j - i.

lemma RepeatPlus<X>(f: X -> X, start: X, n: nat, m: nat)
  ensures Repeat(f, n + m, start) == Repeat(f, m, Repeat(f, n, start))

lemma RepeatLoop<X>(f: X -> X, start: X, n: nat, k: nat)
  requires Repeat(f, n, start) == start
  ensures Repeat(f, k*n, start) == start