// This time your exercise is right here at the top:

// 1. Fix the specification of this lemma, which is trying to state
//    that performing a Union followed by a Select is the same as
//    performing Selects (with the same condition) and then Union.

// 2. And then prove it. Hint: state & prove a lemma about the two List
//    operations that are used to define what Select and Union mean.

lemma SelectUnion(p: Pred, q0: Query, q1: Query)
  ensures Select(p, Union(q0, q1)) == Union(Select(p, q0), Select(p, q1))
{
}

// ... and now here are all the defintions that led up to it:

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

function Length<T>(xs: List<T>): nat {
  match xs
  case Nil => 0
  case Cons(_, tail) => 1 + Length(tail)
}

function Append<X>(xs: List<X>, ys: List<X>): List<X>
  ensures Length(Append(xs, ys)) == Length(xs) + Length(ys)
{
  match xs
  case Nil => ys
  case Cons(x, tail) => Cons(x, Append(tail, ys))
}

function Map<X, Y>(xs: List<X>, f: X -> Y): List<Y> {
  match xs
  case Nil => Nil
  case Cons(x, tail) => Cons(f(x), Map(tail, f))
}

function Filter<X>(xs: List<X>, p: X -> bool): List<X> {
  match xs
  case Nil => Nil
  case Cons(x, tail) =>
    if p(x) then Cons(x, Filter(tail, p)) else Filter(tail, p)
}

type Name = string

// A row in a database table is a labeled tuple. We can represent it as a map
// from attribute names to values. For simplicity, we'll only consider integer
// values.
type Row = map<Name, int>

// A table is a list of rows.
type Table = List<Row>

// Now, here are some operations for computing tables based on other tables.
datatype Query =
  | Source(rows: Table)                 // A literal table of data
  | Union(q0: Query, q1: Query)         // Combining the rows of two tables
  | Project(names: set<Name>, q: Query) // Postprocessing a query by
                                        // *dropping* attributes not in the
                                        // given set
  | Select(cond: Pred, q: Query)        // Filtering query results according
                                        // to a predicate on rows.

// For filtering queries, the condition is an expression we evaluate.
// Let's keep them very simple for now:
datatype Pred =
  | AttrEq(name: Name, value: int)
  | And(p0: Pred, p1: Pred)

type State = map<Name, int>

// How do we evaluate predicates?
function PEval(pred: Pred, st: State): bool {
  match pred
  case AttrEq(name, value) => name in st && st[name] == value
  case And(p0, p1) => PEval(p0, st) && PEval(p1, st)
}

// And how do we evaluate database queries?
function QEval(q: Query): Table {
  match q
  case Source(rows) => rows
  case Union(q0, q1) => Append(QEval(q0), QEval(q1))
  case Project(names, q) => Map(QEval(q), ProjectNames(names))
  case Select(cond, q) => Filter(QEval(q), EvalCondition(cond))
}

function ProjectNames(names: set<Name>): (Row -> Row) {
  (row: Row) => row - (row.Keys - names)
}

function EvalCondition(cond: Pred): (Row -> bool) {
  (row: Row) => PEval(cond, row)
}