Relational algebra

AbbreviationTuple#✓fully proved

For a type \(A\) of attributes and a type \(D\) of values, a tuple is a partial assignment of values to attributes: a function that assigns to each attribute \(a \in A\) either a value in \(D\) or no value, in which case the tuple is undefined at \(a\).

abbrev Tuple (A D : Type*) := A → Option D

Used by 44

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Heath's theorem · Join of the projections of a relation · Unit relation of the natural join · Lossless decomposition into two schemes · Lossless binary decompositions from derivable dependencies · Membership in a join of projections · Satisfying a set of dependencies on a scheme · Synthesis is lossless · Compatible tuples · Compatibility with a merge, grouped from the left · Compatibility with a merge, grouped from the right · Databases conforming to a schema · Query equivalence · Truth value of a selection condition · Value of a query · Typing is sound · Selection conditions depend only on their attributes · Tuple over a schema · Relation over a schema · Natural join · Associativity of the natural join · Commutativity of the natural join · The natural join on a common schema is the intersection · Membership in a join · Merge of two tuples · Projection of a relation · Cascade of projections · Cascade of projections as a query rewrite · Cascade of projections onto a subset · Projection distributes over union · Renaming of attributes · Restriction of a tuple · Selection · Selections commute · Selection pushdown as a query rewrite · Selection pushdown into the left operand of a join · Selection pushdown into the right operand of a join · Selection commutes with projection · Selection distributes over difference · Cascade of selections · Cascade of selections as a query rewrite · Selection distributes over union

DefinitionTuple over a schema#✓fully proved

A tuple \(t\) is over the schema \(S\), a finite set of attributes, when \(t\) is defined exactly on the attributes of \(S\): for every attribute \(a\), the value \(t(a)\) is defined if and only if \(a \in S\).

def IsOver (S : Finset A) (t : Tuple A D) : Prop := ∀ a, (t a).isSome ↔ a ∈ S

Uses 1 · Used by 10

Statement usesTuple

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Heath's theorem · Membership in a join of projections · Synthesis is lossless · Typing is sound · Relation over a schema · The natural join on a common schema is the intersection · Membership in a join · Selection pushdown into the left operand of a join

DefinitionCompatible tuples#✓fully proved

Two tuples \(t\) and \(u\) are compatible (joinable) when they agree on every attribute where both are defined: for every attribute \(a\), either \(t\) is undefined at \(a\), or \(u\) is undefined at \(a\), or \(t(a) = u(a)\).

def Compatible (t u : Tuple A D) : Prop := ∀ a, t a = none ∨ u a = none ∨ t a = u a

Uses 1 · Used by 11

Statement usesTuple

Used byThe BCNF decomposition is lossless · Membership in a join of projections · Compatibility with a merge, grouped from the left · Compatibility with a merge, grouped from the right · Typing is sound · Natural join · Associativity of the natural join · Commutativity of the natural join · The natural join on a common schema is the intersection · Membership in a join · Selection pushdown into the left operand of a join

DefinitionMerge of two tuples#✓fully proved

The merge of tuples \(t\) and \(u\) is the tuple whose value at each attribute \(a\) is \(t(a)\) if \(t\) is defined at \(a\), and \(u(a)\) otherwise; it is undefined at \(a\) when neither \(t\) nor \(u\) is.

def merge (t u : Tuple A D) : Tuple A D := fun a => (t a).or (u a)

Uses 1 · Used by 11

Statement usesTuple

Used byThe BCNF decomposition is lossless · Membership in a join of projections · Compatibility with a merge, grouped from the left · Compatibility with a merge, grouped from the right · Typing is sound · Natural join · Associativity of the natural join · Commutativity of the natural join · The natural join on a common schema is the intersection · Membership in a join · Selection pushdown into the left operand of a join

TheoremCompatibility with a merge, grouped from the left#✓fully proved

For tuples \(t\), \(u\), \(v\): \(t\) and \(u\) are compatible and the merge of \(t\) and \(u\) is compatible with \(v\) if and only if \(t\), \(u\), \(v\) are pairwise compatible, that is, \(t\) and \(u\), \(t\) and \(v\), and \(u\) and \(v\) are compatible.

theorem compatible_merge_left {t u v : Tuple A D} :
    Compatible t u ∧ Compatible (merge t u) v ↔
      Compatible t u ∧ Compatible t v ∧ Compatible u v

Uses 3 · Used by 2

Statement usesTuple · Compatible tuples · Merge of two tuples

Used byCompatibility with a merge, grouped from the right · Associativity of the natural join

TheoremCompatibility with a merge, grouped from the right#✓fully proved

For tuples \(t\), \(u\), \(v\): \(u\) and \(v\) are compatible and \(t\) is compatible with the merge of \(u\) and \(v\) if and only if \(t\), \(u\), \(v\) are pairwise compatible, that is, \(t\) and \(u\), \(t\) and \(v\), and \(u\) and \(v\) are compatible.

theorem compatible_merge_right {t u v : Tuple A D} :
    Compatible u v ∧ Compatible t (merge u v) ↔
      Compatible t u ∧ Compatible t v ∧ Compatible u v

Uses 4 · Used by 1

Statement usesTuple · Compatible tuples · Merge of two tuples

Proof usesCompatibility with a merge, grouped from the left

Used byAssociativity of the natural join

DefinitionRestriction of a tuple#✓fully proved

For a finite set \(T\) of attributes and a tuple \(t\), the restriction \(t|_T\) is the tuple that agrees with \(t\) on every attribute in \(T\) and is undefined on every attribute outside \(T\).

def restrict (T : Finset A) (t : Tuple A D) : Tuple A D := fun a => if a ∈ T then t a else none

Uses 1 · Used by 13

Statement usesTuple

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Heath's theorem · Membership in a join of projections · Synthesis is lossless · Typing is sound · Selection conditions depend only on their attributes · Membership in a join · Projection of a relation · Cascade of projections · Projection distributes over union · Selection pushdown into the left operand of a join · Selection commutes with projection

39 fully proved

Selection conditions

InductiveSelection conditions#✓fully proved

The selection conditions over attributes \(A\) and values \(D\) are generated by: the condition that always holds; the equality \(a = c\) of an attribute \(a\) with a constant \(c \in D\); the equality \(a = b\) of two attributes \(a\) and \(b\); the negation of a condition; and the conjunction of two conditions.

inductive Cond (A D : Type*)
  /-- The condition that always holds. -/
  | tt
  /-- `a = c` for an attribute `a` and a constant `c`. -/
  | eqConst (a : A) (c : D)
  /-- `a = b` for attributes `a` and `b`. -/
  | eqAttr (a b : A)
  /-- Negation. -/
  | not (c : Cond A D)
  /-- Conjunction. -/
  | and (c c' : Cond A D)

Used by 17

Used byAttributes of a selection condition · Truth value of a selection condition · Value of a query · Typing is sound · Selection conditions depend only on their attributes · Relational algebra queries · Schema of a query · Selection · Selections commute · Selection pushdown as a query rewrite · Selection pushdown into the left operand of a join · Selection pushdown into the right operand of a join · Selection commutes with projection · Selection distributes over difference · Cascade of selections · Cascade of selections as a query rewrite · Selection distributes over union

DefinitionTruth value of a selection condition#✓fully proved

The truth value of a selection condition on a tuple \(t\) is defined by recursion: the always-true condition holds; \(a = c\) holds when \(t\) is defined at \(a\) with value \(c\); \(a = b\) holds when \(t(a) = t(b)\) as possibly undefined values, so it also holds when \(t\) is undefined at both \(a\) and \(b\); a negation holds when the negated condition fails; and a conjunction holds when both conditions hold.

def eval [DecidableEq D] : Cond A D → Tuple A D → Bool
  | tt, _ => true
  | eqConst a c, t => t a == some c
  | eqAttr a b, t => t a == t b
  | not c, t => !c.eval t
  | and c c', t => c.eval t && c'.eval t

Uses 2 · Used by 9

Statement usesSelection conditions · Tuple

Used byTyping is sound · Selection conditions depend only on their attributes · Selection · Selections commute · Selection pushdown into the left operand of a join · Selection commutes with projection · Selection distributes over difference · Cascade of selections · Selection distributes over union

DefinitionAttributes of a selection condition#✓fully proved

The set of attributes mentioned by a selection condition, defined by recursion: it is empty for the always-true condition; for the comparison \(a = d\) of an attribute \(a\) with a constant \(d\) it is \(\{a\}\); for the comparison \(a = b\) of attributes \(a\) and \(b\) it is \(\{a, b\}\); for the negation \(\neg \varphi\) of a condition \(\varphi\) it is the set of attributes of \(\varphi\); and for the conjunction \(\varphi \land \psi\) of conditions \(\varphi\) and \(\psi\) it is the union of the attributes of \(\varphi\) and of \(\psi\).

def attrs [DecidableEq A] : Cond A D → Finset A
  | tt => ∅
  | eqConst a _ => {a}
  | eqAttr a b => {a, b}
  | not c => c.attrs
  | and c c' => c.attrs ∪ c'.attrs

Uses 1 · Used by 8

Statement usesSelection conditions

Used byTyping is sound · Selection conditions depend only on their attributes · Schema of a query · Selection pushdown as a query rewrite · Selection pushdown into the left operand of a join · Selection pushdown into the right operand of a join · Selection commutes with projection · Cascade of selections as a query rewrite

TheoremSelection conditions depend only on their attributes#✓fully proved

Let \(c\) be a selection condition, \(t\) a tuple and \(T\) a finite set of attributes containing every attribute of \(c\). Then \(c\) has the same truth value on the restriction of \(t\) to \(T\) as on \(t\).

theorem eval_restrict [DecidableEq A] [DecidableEq D] {T : Finset A} (t : Tuple A D) :
    ∀ c : Cond A D, c.attrs ⊆ T → c.eval (t.restrict T) = c.eval t

Uses 5 · Used by 2

Statement usesSelection conditions · Attributes of a selection condition · Truth value of a selection condition · Tuple · Restriction of a tuple

Used bySelection pushdown into the left operand of a join · Selection commutes with projection

The operators

DefinitionRelation over a schema#✓fully proved

A finite set \(r\) of tuples is a relation over the schema \(S\), a finite set of attributes, when every tuple \(t \in r\) is over \(S\), that is, \(t\) is defined exactly on the attributes of \(S\).

def IsOver (S : Finset A) (r : Finset (Tuple A D)) : Prop := ∀ t ∈ r, t.IsOver S

Uses 2 · Used by 13

Statement usesTuple · Tuple over a schema

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Heath's theorem · Lossless decomposition into two schemes · Lossless binary decompositions from derivable dependencies · Membership in a join of projections · Synthesis is lossless · Databases conforming to a schema · Typing is sound · The natural join on a common schema is the intersection · Membership in a join · Selection pushdown into the left operand of a join · Selection pushdown into the right operand of a join

DefinitionSelection#✓fully proved

For a selection condition \(c\) and a finite set \(r\) of tuples, the selection \(\sigma_c(r)\) is the set of tuples \(t \in r\) on which \(c\) evaluates to true.

def select (c : Cond A D) (r : Finset (Tuple A D)) : Finset (Tuple A D) :=
  r.filter fun t => c.eval t = true

Uses 3 · Used by 9

Statement usesSelection conditions · Truth value of a selection condition · Tuple

Used byValue of a query · Typing is sound · Selections commute · Selection pushdown into the left operand of a join · Selection pushdown into the right operand of a join · Selection commutes with projection · Selection distributes over difference · Cascade of selections · Selection distributes over union

TheoremCascade of selections#✓fully proved

Write \(\sigma_c\) for selection by a selection condition \(c\). For selection conditions \(c\) and \(c'\) and a finite set \(r\) of tuples, \(\sigma_c(\sigma_{c'}(r)) = \sigma_{c' \land c}(r)\): selecting by \(c'\) and then by \(c\) is the same as selecting once by the conjunction \(c' \land c\).

theorem select_select (c c' : Cond A D) (r : Finset (Tuple A D)) :
    select c (select c' r) = select (.and c' c) r

Uses 4 · Used by 1

Statement usesSelection conditions · Tuple · Selection

Proof usesTruth value of a selection condition

Used byCascade of selections as a query rewrite

TheoremSelections commute#✓fully proved

For all selection conditions \(c\) and \(c'\) and every finite set \(r\) of tuples, selecting by \(c'\) and then by \(c\) gives the same result as selecting by \(c\) and then by \(c'\): \(\sigma_c(\sigma_{c'}(r)) = \sigma_{c'}(\sigma_c(r))\).

theorem select_comm (c c' : Cond A D) (r : Finset (Tuple A D)) :
    select c (select c' r) = select c' (select c r)

Uses 4

Statement usesSelection conditions · Tuple · Selection

Proof usesTruth value of a selection condition

DefinitionNatural join#✓fully proved

The natural join \(r \bowtie s\) of finite sets of tuples \(r\) and \(s\) is the set of merges of \(t\) and \(u\) over all pairs of tuples \(t \in r\) and \(u \in s\) that are compatible, that is, agree on every attribute where both are defined. The merge of \(t\) and \(u\) takes the value of \(t\) where \(t\) is defined and the value of \(u\) otherwise.

def join (r s : Finset (Tuple A D)) : Finset (Tuple A D) :=
  ((r ×ˢ s).filter fun p => Compatible p.1 p.2).image fun p => merge p.1 p.2

Uses 3 · Used by 15

Statement usesTuple · Compatible tuples · Merge of two tuples

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Heath's theorem · Join of the projections of a relation · Lossless decomposition into two schemes · Lossless binary decompositions from derivable dependencies · Membership in a join of projections · Value of a query · Typing is sound · Associativity of the natural join · Commutativity of the natural join · The natural join on a common schema is the intersection · Membership in a join · Selection pushdown into the left operand of a join · Selection pushdown into the right operand of a join

DefinitionRenaming of attributes#✓fully proved

For a permutation \(f\) of the attributes and a finite set \(r\) of tuples, the renaming \(\rho_f(r)\) is the finite set of the tuples \(t \circ f^{-1}\) for \(t \in r\): each tuple keeps its values, and its value at an attribute \(a\) moves to the attribute \(f(a)\).

def rename (f : A ≃ A) (r : Finset (Tuple A D)) : Finset (Tuple A D) :=
  r.image fun t => t ∘ f.symm

Uses 1 · Used by 2

Statement usesTuple

Used byValue of a query · Typing is sound

TheoremCommutativity of the natural join#✓fully proved

For all finite sets \(r\) and \(s\) of tuples, \(r \bowtie s = s \bowtie r\), where \(\bowtie\) is the natural join.

theorem join_comm (r s : Finset (Tuple A D)) : join r s = join s r

Uses 4 · Used by 3

Statement usesTuple · Natural join

Proof usesCompatible tuples · Merge of two tuples

Used byThe BCNF decomposition is lossless · Lossless binary decompositions from derivable dependencies · Selection pushdown into the right operand of a join

TheoremAssociativity of the natural join#✓fully proved

For all finite sets \(r\), \(s\) and \(w\) of tuples, \((r \bowtie s) \bowtie w = r \bowtie (s \bowtie w)\), where \(\bowtie\) is the natural join.

theorem join_assoc (r s w : Finset (Tuple A D)) :
    join (join r s) w = join r (join s w)

Uses 6 · Used by 1

Statement usesTuple · Natural join

Proof usesCompatible tuples · Compatibility with a merge, grouped from the left · Compatibility with a merge, grouped from the right · Merge of two tuples

Used byThe BCNF decomposition is lossless

TheoremThe natural join on a common schema is the intersection#✓fully proved

If \(r\) and \(s\) are relations over the same schema \(S\), that is, finite sets of tuples each over \(S\), then their natural join is their intersection: \(r \bowtie s = r \cap s\).

theorem join_eq_inter {S : Finset A} {r s : Finset (Tuple A D)} (hr : IsOver S r)
    (hs : IsOver S s) : join r s = r ∩ s

Uses 6

Statement usesRelation over a schema · Tuple · Natural join

Proof usesCompatible tuples · Tuple over a schema · Merge of two tuples

TheoremSelection distributes over union#✓fully proved

Assume the set of attributes is finite. Let \(c\) be a selection condition and write \(\sigma_c\) for selection by \(c\). For finite sets \(r\) and \(s\) of tuples, \(\sigma_c(r \cup s) = \sigma_c(r) \cup \sigma_c(s)\).

theorem select_union (c : Cond A D) (r s : Finset (Tuple A D)) :
    select c (r ∪ s) = select c r ∪ select c s

Uses 4

Statement usesSelection conditions · Tuple · Selection

Proof usesTruth value of a selection condition

TheoremSelection distributes over difference#✓fully proved

Assume the set of attributes is finite. Let \(c\) be a selection condition and write \(\sigma_c\) for selection by \(c\). For finite sets \(r\) and \(s\) of tuples, \(\sigma_c(r \setminus s) = \sigma_c(r) \setminus \sigma_c(s)\).

theorem select_sdiff (c : Cond A D) (r s : Finset (Tuple A D)) :
    select c (r \ s) = select c r \ select c s

Uses 4

Statement usesSelection conditions · Tuple · Selection

Proof usesTruth value of a selection condition

DefinitionProjection of a relation#✓fully proved

For a finite set \(T\) of attributes and a finite set \(r\) of tuples, the projection \(\pi_T(r)\) is the finite set of the restrictions to \(T\) of the tuples of \(r\): \(\pi_T(r) = \{ t|_T : t \in r \}\).

def project (T : Finset A) (r : Finset (Tuple A D)) : Finset (Tuple A D) :=
  r.image (Tuple.restrict T)

Uses 2 · Used by 14

Statement usesTuple · Restriction of a tuple

Used byThe BCNF decomposition is lossless · Converse of the lossless-join test for two schemes · Heath's theorem · Join of the projections of a relation · Lossless decomposition into two schemes · Lossless binary decompositions from derivable dependencies · Membership in a join of projections · Synthesis is lossless · Value of a query · Typing is sound · Cascade of projections · Cascade of projections onto a subset · Projection distributes over union · Selection commutes with projection

TheoremMembership in a join#✓fully proved

Let \(r\) be a relation over the schema \(S\) and \(s\) a relation over the schema \(S'\), that is, finite sets of tuples each over \(S\), respectively each over \(S'\). A tuple \(t\) belongs to the natural join \(r \bowtie s\) if and only if \(t\) is over \(S \cup S'\), the restriction of \(t\) to \(S\) belongs to \(r\), and the restriction of \(t\) to \(S'\) belongs to \(s\).

theorem mem_join_iff {S S' : Finset A} {r s : Finset (Tuple A D)} (hr : IsOver S r)
    (hs : IsOver S' s) {t : Tuple A D} :
    t ∈ join r s ↔ t.IsOver (S ∪ S') ∧ t.restrict S ∈ r ∧ t.restrict S' ∈ s

Uses 7 · Used by 3

Statement usesRelation over a schema · Tuple · Tuple over a schema · Restriction of a tuple · Natural join

Proof usesCompatible tuples · Merge of two tuples

Used byConverse of the lossless-join test for two schemes · Heath's theorem · Membership in a join of projections

TheoremSelection pushdown into the left operand of a join#✓fully proved

Let \(r\) be a relation over a schema \(S\), that is, a finite set of tuples each defined exactly on the attributes of \(S\), and let \(s\) be any finite set of tuples. If every attribute of the selection condition \(c\) lies in \(S\), then \(\sigma_c(r \bowtie s) = \sigma_c(r) \bowtie s\), where \(\sigma_c\) is selection by \(c\) and \(\bowtie\) is the natural join.

theorem select_join_left {S : Finset A} {r : Finset (Tuple A D)} (s : Finset (Tuple A D))
    (c : Cond A D) (hr : IsOver S r) (hc : c.attrs ⊆ S) :
    select c (join r s) = join (select c r) s

Uses 12 · Used by 2

Statement usesSelection conditions · Attributes of a selection condition · Relation over a schema · Tuple · Natural join · Selection

Proof usesTruth value of a selection condition · Selection conditions depend only on their attributes · Compatible tuples · Tuple over a schema · Merge of two tuples · Restriction of a tuple

Used bySelection pushdown as a query rewrite · Selection pushdown into the right operand of a join

TheoremSelection pushdown into the right operand of a join#✓fully proved

Let \(s\) be a relation over a schema \(S'\), that is, a finite set of tuples each defined exactly on the attributes of \(S'\), and let \(r\) be any finite set of tuples. If every attribute of the selection condition \(c\) lies in \(S'\), then \(\sigma_c(r \bowtie s) = r \bowtie \sigma_c(s)\), where \(\sigma_c\) is selection by \(c\) and \(\bowtie\) is the natural join.

theorem select_join_right {S' : Finset A} (r : Finset (Tuple A D)) {s : Finset (Tuple A D)}
    (c : Cond A D) (hs : IsOver S' s) (hc : c.attrs ⊆ S') :
    select c (join r s) = join r (select c s)

Uses 8

Statement usesSelection conditions · Attributes of a selection condition · Relation over a schema · Tuple · Natural join · Selection

Proof usesCommutativity of the natural join · Selection pushdown into the left operand of a join

TheoremCascade of projections#✓fully proved

Assume the set of attributes is finite. For all finite sets of attributes \(T\) and \(T'\) and every finite set \(r\) of tuples, \(\pi_T(\pi_{T'}(r)) = \pi_{T \cap T'}(r)\), where \(\pi_T\) is projection onto \(T\).

theorem project_project (T T' : Finset A) (r : Finset (Tuple A D)) :
    project T (project T' r) = project (T ∩ T') r

Uses 3 · Used by 1

Statement usesTuple · Projection of a relation

Proof usesRestriction of a tuple

Used byCascade of projections onto a subset

TheoremCascade of projections onto a subset#✓fully proved

Assume the set of attributes is finite. For finite sets of attributes \(T \subseteq T'\) and every finite set \(r\) of tuples, \(\pi_T(\pi_{T'}(r)) = \pi_T(r)\), where \(\pi_T\) is projection onto \(T\).

theorem project_project_of_subset {T T' : Finset A} (h : T ⊆ T') (r : Finset (Tuple A D)) :
    project T (project T' r) = project T r

Uses 3 · Used by 2

Statement usesTuple · Projection of a relation

Proof usesCascade of projections

Used byThe BCNF decomposition is lossless · Cascade of projections as a query rewrite

TheoremSelection commutes with projection#✓fully proved

Assume the set of attributes is finite. Let \(c\) be a selection condition, \(T\) a finite set of attributes containing every attribute of \(c\), and \(r\) a finite set of tuples. Then \(\sigma_c(\pi_T(r)) = \pi_T(\sigma_c(r))\), where \(\sigma_c\) is selection by \(c\) and \(\pi_T\) is projection onto \(T\).

theorem select_project {T : Finset A} (c : Cond A D) (r : Finset (Tuple A D))
    (hc : c.attrs ⊆ T) : select c (project T r) = project T (select c r)

Uses 8

Statement usesSelection conditions · Attributes of a selection condition · Tuple · Projection of a relation · Selection

Proof usesTruth value of a selection condition · Selection conditions depend only on their attributes · Restriction of a tuple

TheoremProjection distributes over union#✓fully proved

For every finite set \(T\) of attributes and all finite sets \(r\) and \(s\) of tuples, the projection onto \(T\) of \(r \cup s\) is the union of the projections onto \(T\) of \(r\) and of \(s\): \(\pi_T(r \cup s) = \pi_T(r) \cup \pi_T(s)\).

theorem project_union (T : Finset A) (r s : Finset (Tuple A D)) :
    project T (r ∪ s) = project T r ∪ project T s

Uses 3

Statement usesTuple · Projection of a relation

Proof usesRestriction of a tuple

Queries

InductiveRelational algebra queries#✓fully proved

The relational algebra queries over base relations named by \(N\), with attributes \(A\) and values \(D\), are generated by: the base relation named \(n\) for each \(n \in N\); the selection \(\sigma_c(e)\) of a query \(e\) by a selection condition \(c\); the projection \(\pi_T(e)\) of a query \(e\) on a finite set of attributes \(T\); the natural join of two queries; the union of two queries; the difference of two queries; and the renaming \(\rho_f(e)\) of a query \(e\) along a permutation \(f\) of \(A\).

Cslib.Databases.Expr · 15 lines

inductive Expr (N A D : Type*)
  /-- The base relation named `n`. -/
  | rel (n : N)
  /-- Selection. -/
  | select (c : Cond A D) (e : Expr N A D)
  /-- Projection. -/
  | project (T : Finset A) (e : Expr N A D)
  /-- Natural join. -/
  | join (e e' : Expr N A D)
  /-- Union. -/
  | union (e e' : Expr N A D)
  /-- Difference. -/
  | diff (e e' : Expr N A D)
  /-- Renaming along a permutation of the attributes. -/
  | rename (f : A ≃ A) (e : Expr N A D)

Uses 1 · Used by 7

Statement usesSelection conditions

Used byQuery equivalence · Value of a query · Typing is sound · Cascade of projections as a query rewrite · Schema of a query · Selection pushdown as a query rewrite · Cascade of selections as a query rewrite

DefinitionValue of a query#✓fully proved

Given a database \(\mathrm{db}\), which assigns a finite set of tuples \(\mathrm{db}(n)\) to each relation name \(n\), the value of a relational algebra query on \(\mathrm{db}\) is the finite set of tuples defined by recursion on the query: the base relation \(n\) has value \(\mathrm{db}(n)\); for a query \(e\) with value \(v\), the selection \(\sigma_c(e)\) by a selection condition \(c\), the projection \(\pi_T(e)\) onto a finite set \(T\) of attributes and the renaming \(\rho_f(e)\) along a permutation \(f\) of the attributes have values \(\sigma_c(v)\), \(\pi_T(v)\) and \(\rho_f(v)\); and the natural join, the union and the difference of queries \(e\) and \(e'\) with values \(v\) and \(v'\) have values \(v \bowtie v'\), \(v \cup v'\) and \(v \setminus v'\).

def eval (db : N → Finset (Tuple A D)) : Expr N A D → Finset (Tuple A D)
  | rel n => db n
  | select c e => Databases.select c (e.eval db)
  | project T e => Databases.project T (e.eval db)
  | join e e' => Databases.join (e.eval db) (e'.eval db)
  | union e e' => e.eval db ∪ e'.eval db
  | diff e e' => e.eval db \ e'.eval db
  | rename f e => Databases.rename f (e.eval db)

Uses 7 · Used by 5

Statement usesSelection conditions · Relational algebra queries · Tuple · Natural join · Projection of a relation · Renaming of attributes · Selection

Used byQuery equivalence · Typing is sound · Cascade of projections as a query rewrite · Selection pushdown as a query rewrite · Cascade of selections as a query rewrite

DefinitionSchema of a query#✓fully proved

Given a database schema assigning a finite set \(\mathrm{sch}(n)\) of attributes to each base relation name \(n\), the schema of a relational algebra query is either a finite set of attributes or undefined (the query is ill-formed), defined by recursion on the query: the base relation \(n\) has schema \(\mathrm{sch}(n)\); if \(e\) has schema \(S\), then the selection \(\sigma_c(e)\) has schema \(S\) when every attribute of the condition \(c\) lies in \(S\), the projection \(\pi_T(e)\) has schema \(T\) when \(T \subseteq S\), and the renaming \(\rho_f(e)\) along a permutation \(f\) of the attributes has schema \(f(S)\); if \(e\) and \(e'\) have schemas \(S\) and \(S'\), then the natural join of \(e\) and \(e'\) has schema \(S \cup S'\), and their union and their difference have schema \(S\) when \(S = S'\). In every other case, including when an operand is ill-formed, the schema is undefined.

def schema (sch : N → Finset A) : Expr N A D → Option (Finset A)
  | rel n => some (sch n)
  | select c e => (e.schema sch).bind fun S => if c.attrs ⊆ S then some S else none
  | project T e => (e.schema sch).bind fun S => if T ⊆ S then some T else none
  | join e e' => (e.schema sch).bind fun S => (e'.schema sch).map fun S' => S ∪ S'
  | union e e' => (e.schema sch).bind fun S => (e'.schema sch).bind fun S' =>
      if S = S' then some S else none
  | diff e e' => (e.schema sch).bind fun S => (e'.schema sch).bind fun S' =>
      if S = S' then some S else none
  | rename f e => (e.schema sch).map fun S => S.map f.toEmbedding

Uses 3 · Used by 5

Statement usesSelection conditions · Attributes of a selection condition · Relational algebra queries

Used byQuery equivalence · Typing is sound · Cascade of projections as a query rewrite · Selection pushdown as a query rewrite · Cascade of selections as a query rewrite

DefinitionDatabases conforming to a schema#✓fully proved

Let \(N\) be a set of relation names. A database schema assigns to each name \(n \in N\) a finite set of attributes \(\mathrm{sch}(n)\), and a database assigns to each name \(n\) a finite set of tuples \(\mathrm{db}(n)\). The database \(\mathrm{db}\) conforms to the database schema \(\mathrm{sch}\) when, for every name \(n\), the set \(\mathrm{db}(n)\) is a relation over \(\mathrm{sch}(n)\).

def Conforms (sch : N → Finset A) (db : N → Finset (Tuple A D)) : Prop :=
  ∀ n, IsOver (sch n) (db n)

Uses 2 · Used by 5

Statement usesRelation over a schema · Tuple

Used byQuery equivalence · Typing is sound · Cascade of projections as a query rewrite · Selection pushdown as a query rewrite · Cascade of selections as a query rewrite

TheoremTyping is sound#✓fully proved

A well-formed query evaluates, on every conforming database, to a relation over its inferred schema.

theorem eval_isOver {sch : N → Finset A} {db : N → Finset (Tuple A D)} (hdb : Conforms sch db) :
    ∀ (e : Expr N A D) {S : Finset A}, e.schema sch = some S → IsOver S (e.eval db)

Uses 17 · Used by 1

Statement usesRelational algebra queries · Databases conforming to a schema · Value of a query · Schema of a query · Relation over a schema · Tuple

Proof usesSelection conditions · Attributes of a selection condition · Truth value of a selection condition · Compatible tuples · Tuple over a schema · Merge of two tuples · Restriction of a tuple · Natural join · Projection of a relation · Renaming of attributes · Selection

Used bySelection pushdown as a query rewrite

DefinitionQuery equivalence#✓fully proved

Let \(\mathrm{sch}\) be a database schema, assigning a finite set of attributes to each relation name. Two queries \(e\) and \(e'\) are equivalent with respect to \(\mathrm{sch}\) when there is a finite set of attributes \(S\) such that the inferred schemas of \(e\) and of \(e'\) with respect to \(\mathrm{sch}\) are both \(S\) (in particular both queries are well-formed), and \(e\) and \(e'\) evaluate to the same relation on every database that conforms to \(\mathrm{sch}\).

def Equiv (sch : N → Finset A) (e e' : Expr N A D) : Prop :=
  ∃ S, e.schema sch = some S ∧ e'.schema sch = some S ∧
    ∀ db, Conforms sch db → e.eval db = e'.eval db

Uses 5 · Used by 3

Statement usesRelational algebra queries · Databases conforming to a schema · Value of a query · Schema of a query · Tuple

Used byCascade of projections as a query rewrite · Selection pushdown as a query rewrite · Cascade of selections as a query rewrite

TheoremSelection pushdown as a query rewrite#✓fully proved

Fix a database schema \(\mathrm{sch}\) assigning a finite set of attributes to each base relation name. Let \(e\) and \(e'\) be well-formed queries with schemas \(S\) and \(S'\), and let \(c\) be a selection condition all of whose attributes lie in \(S\). Then the query \(\sigma_c(e \bowtie e')\), the selection by \(c\) of the natural join of \(e\) and \(e'\), is equivalent to the query \(\sigma_c(e) \bowtie e'\): both are well-formed with the same schema, and they have equal values on every database conforming to \(\mathrm{sch}\).

theorem select_join {sch : N → Finset A} {e e' : Expr N A D} {S S' : Finset A}
    (he : e.schema sch = some S) (he' : e'.schema sch = some S') (c : Cond A D)
    (hc : c.attrs ⊆ S) :
    Equiv sch (select c (join e e')) (join (select c e) e')

Uses 10

Statement usesSelection conditions · Attributes of a selection condition · Relational algebra queries · Query equivalence · Schema of a query

Proof usesDatabases conforming to a schema · Value of a query · Typing is sound · Tuple · Selection pushdown into the left operand of a join

TheoremCascade of selections as a query rewrite#✓fully proved

Fix a database schema \(\mathrm{sch}\) assigning a finite set of attributes to each base relation name. Let \(e\) be a well-formed query with schema \(S\), and let \(c\) and \(c'\) be selection conditions all of whose attributes lie in \(S\). Then the query \(\sigma_c(\sigma_{c'}(e))\), the selection by \(c\) of the selection of \(e\) by \(c'\), is equivalent to the query \(\sigma_{c' \land c}(e)\), the selection of \(e\) by the conjunction \(c' \land c\): both are well-formed with the same schema, and they have equal values on every database conforming to \(\mathrm{sch}\).

theorem select_select {sch : N → Finset A} {e : Expr N A D} {S : Finset A}
    (he : e.schema sch = some S) {c c' : Cond A D} (hc : c.attrs ⊆ S) (hc' : c'.attrs ⊆ S) :
    Equiv sch (select c (select c' e)) (select (.and c' c) e)

Uses 9

Statement usesSelection conditions · Attributes of a selection condition · Relational algebra queries · Query equivalence · Schema of a query

Proof usesDatabases conforming to a schema · Value of a query · Tuple · Cascade of selections

TheoremCascade of projections as a query rewrite#✓fully proved

Fix a database schema \(\mathrm{sch}\) assigning a finite set of attributes to each base relation name. Let \(e\) be a well-formed query with schema \(S\), and let \(T \subseteq T' \subseteq S\) be finite sets of attributes. Then the query \(\pi_T(\pi_{T'}(e))\), the projection onto \(T\) of the projection of \(e\) onto \(T'\), is equivalent to the query \(\pi_T(e)\), the projection of \(e\) onto \(T\): both are well-formed with the same schema, and they have equal values on every database conforming to \(\mathrm{sch}\).

theorem project_project {sch : N → Finset A} {e : Expr N A D} {S T T' : Finset A}
    (he : e.schema sch = some S) (hT' : T' ⊆ S) (hT : T ⊆ T') :
    Equiv sch (project T (project T' e)) (project T e)

Uses 7

Statement usesRelational algebra queries · Query equivalence · Schema of a query

Proof usesDatabases conforming to a schema · Value of a query · Tuple · Cascade of projections onto a subset

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.