include "pset07_definitions.dfy"

// Please read the definitions file first, for the data-structure definition we use.
// Also, see pset07_hints.dfy for hints (spoiler alert!) based on our solution.

module Pset7 {
  import opened Defs
  export
    provides Defs, Valid, EmptyCorrect, MemberCorrect, InsertCorrect, ValidBalanced
  // That last line is important: to the outside world, this module will only
  // reveal the type signature of a predicate you will define, plus the
  // statements of four lemmas you will prove!  As a result, client code can be
  // written and verified independently of data-structure details.

  // Define a predicate formalizing the data-structure invariant of red-black
  // trees.  Note that the need to prove the following lemmas will "keep you
  // honest," so that this definition can be neither too flexible nor too
  // restrictive.
  ghost predicate Valid(s: Tree)

  // Prove the next three lemmas to explain what it means for the red-black-tree
  // implementation to be a correct implementation of finite sets.

  lemma EmptyCorrect()
    ensures Valid(Empty())
    ensures Elements(Empty()) == {}

  lemma MemberCorrect(x: int, s: Tree)
    requires Valid(s)
    ensures Member(x, s) == (x in Elements(s))

  lemma InsertCorrect(x: int, s: Tree)
    requires Valid(s)
    ensures Valid(Insert(x, s))
    ensures Elements(Insert(x, s)) == Elements(s) + {x}

  // Finally, prove your invariant also implies balance.
  lemma ValidBalanced(s: Tree)
    requires Valid(s)
    ensures Balanced(s)

  // Note that we wouldn't actually have been able to prove the first three
  // lemmas if we just used Balanced instead of Valid: it's too flexible of a
  // property to give strong-enough induction hypotheses.
}