module SortedListSet {
  export
    provides Set, Valid, Elements, Empty, Member, Add

  type Set = seq<int>

  ghost predicate Valid(s: Set) {
    forall i, j :: 0 <= i < j < |s| ==> s[i] < s[j]
  }

  ghost function Elements(s: Set): set<int> {
    set n | n in s
  }

  function Empty(): Set
    ensures var s := Empty();
      Valid(s) &&
      Elements(s) == {}
  {
    []
  }

  predicate Member(s: Set, n: int)
    requires Valid(s)
    ensures Member(s, n) <==> n in Elements(s)
  {
    if |s| == 0 then
      false
    else
      var mid := |s| / 2;
      // 1. Complete the implementation such that Dafny proves it correct.
      false
  }

  function Add(s: Set, n: int): Set
    requires Valid(s)
    ensures var s' := Add(s, n);
      Valid(s') &&
      Elements(s') == Elements(s) + {n}
  {
    if |s| == 0 then
      [n]
    else
      var mid := |s| / 2;
      if n == s[mid] then
        s
      else if n < s[mid] then
        // For this function, we must explain/convince Dafny that the
        // implementation is correct.
        ValidAddLeft(s[..mid], s[mid..], n, Add(s[..mid], n));
        Add(s[..mid], n) + s[mid..]
      else
        ValidAddRight(s[..mid+1], s[mid+1..], n, Add(s[mid+1..], n));
        s[..mid+1] + Add(s[mid+1..], n)
  }

  // 2. Write a specification whose postcondition is sufficient to prove `Add`,
  //    and whose precondition records what we know about s1, s2, n, & s1' in
  //    this case of `Add`
  lemma ValidAddLeft(s1: Set, s2: Set, n: int, s1': Set)

  lemma ValidAddRight(s1: Set, s2: Set, n: int, s2': Set)
    ensures false // (this lemma will be more or less symmetric)
}