include "pset04_definitions.dfy"

module Pset4 {
  import opened Defs
  
  // PART 1: Stable Sorting

  // This is an extension of the MergeSort discussed in class.
  // Here, the list being sorted is of an arbitrary type. The sort key is
  // an integer extracted from each element using a function to integers.
  // Check out the definitions and commentary in pset04_definitions.dfy.


  // Prove that the keys of the MergeSort output are ordered.
  lemma MergeSortOrdered<X>(len: nat, xs: List<X>, key: X -> int)
    requires len == Length(xs)
    ensures Ordered(MergeSortAux(len, xs, key), key)

  // The following lemma says that MergeSort is stable.
  lemma MergeSortStable<X>(len: nat, xs: List<X>, key: X -> int, k: int)
    requires len == Length(xs)
    ensures ProjectKeys(xs, key, k) == ProjectKeys(MergeSortAux(len, xs, key), key, k)


  // PART 2: Query Optimization

  // Again, take a look at pset04_definitions.dfy before tackling these lemmas.

  lemma CombineProjectsOptimizationCorrect(query: Query)
    ensures QEval(query) == QEval(CombineProjectsOptimization(query))

  lemma ProjectUnionOptimizationCorrect(query: Query)
    ensures QEval(query) == QEval(ProjectUnionOptimization(query))
}