Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The provenance-aware rewriting of queries, rules (R1) to (R4)

Lax392996.RewritingRules · concepts/Lax392996/RewritingRules.lean · lax-392996

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The rewriting q^\hat q of a source query qq of arity kk into a query of arity k+1k+1 over V⊎K\mathcal{V} \uplus \mathbb{K} whose last column carries the annotation, defined bottom up by the rules of the paper: (R1) a projection Πt1,…,tn(q)\Pi_{t_1, \dots, t_n}(q) becomes Πt1,…,tn,#(k+1)(q^)\Pi_{t_1, \dots, t_n, \#(k+1)}(\hat q); (R2) a cross product q1×q2q_1 \times q_2 becomes Π#1,…,#k1,#(k1+2),…,#(k1+k2+1),#(k1+1)⊗#(k1+k2+2)(q^1×q^2)\Pi_{\#1, \dots, \#k_1, \#(k_1+2), \dots, \#(k_1+k_2+1), \#(k_1+1) \otimes \#(k_1+k_2+2)}(\hat q_1 \times \hat q_2); (R3) a duplicate elimination ε(q)\varepsilon(q) becomes γ1,…,k[#(k+1):⊕](q^)\gamma_{1, \dots, k}[\#(k+1) : \oplus](\hat q), the grouping by the data columns with the ⊕\oplus-sum of the annotation column; (R4) a difference q1−q2q_1 - q_2 becomes the multiset sum of the tuples of q^1\hat q_1 whose data part survives the set difference of the data projections, annotation unchanged, and the tuples of q^1\hat q_1 joined with the ⊕\oplus-aggregated q^2\hat q_2 on the data columns, annotated by α⊖∑β\alpha \ominus \sum \beta. Relation names, selections and multiset sums are rewritten homomorphically. The four claims are the rules as the equations they are.

    Concept map
    3 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 rule_difference proven

    2 rule_dupelim proven

    3 rule_product proven

    4 rule_projection proven

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Fin.VecNotation
    2import Lax392996.Databases
    3import Lax392996.RelationalAlgebra
    4
    5/-!
    6---
    7title: The provenance-aware rewriting of queries, rules (R1) to (R4)
    8type: definition
    9---
    10The rewriting q^\hat q of a source query qq of arity kk into a query of
    11arity k+1k+1 over V⊎K\mathcal{V} \uplus \mathbb{K} whose last column carries
    12the annotation, defined bottom up by the rules of the paper: (R1) a
    13projection Πt1,…,tn(q)\Pi_{t_1, \dots, t_n}(q) becomes Πt1,…,tn,#(k+1)(q^)\Pi_{t_1, \dots, t_n, \#(k+1)}(\hat q)
    14; (R2) a cross product q1×q2q_1 \times q_2 becomes
    15Π#1,…,#k1,#(k1+2),…,#(k1+k2+1),#(k1+1)⊗#(k1+k2+2)(q^1×q^2)\Pi_{\#1, \dots, \#k_1, \#(k_1+2), \dots, \#(k_1+k_2+1), \#(k_1+1) \otimes \#(k_1+k_2+2)}(\hat q_1 \times \hat q_2)
    16; (R3) a duplicate elimination
    17ε(q)\varepsilon(q) becomes γ1,…,k[#(k+1):⊕](q^)\gamma_{1, \dots, k}[\#(k+1) : \oplus](\hat q), the
    18grouping by the data columns with the ⊕\oplus-sum of the annotation column;
    19(R4) a difference q1−q2q_1 - q_2 becomes the multiset sum of the tuples of
    20q^1\hat q_1 whose data part survives the set difference of the data
    21projections, annotation unchanged, and the tuples of q^1\hat q_1 joined with
    22the ⊕\oplus-aggregated q^2\hat q_2 on the data columns, annotated by α⊖∑β\alpha \ominus \sum \beta
    23. Relation names, selections and multiset sums are rewritten
    24homomorphically. The four claims are the rules as the equations they are.
    25-/
    26
    27namespace Lax392996.RewritingRules
    28
    29open Lax392996.Databases Lax392996.RelationalAlgebra
    30
    31variable {T : Type}
    32
    33/-- The rewriting of a source query, rules (R1) to (R4) applied bottom up. -/
    34def Query.rewriting {n : ℕ} {K : Type} [ValueType T] (q: Query T n) (hq: q.source) :
    35 Query (T⊕K) (n+1) := match q with
    36| Query.Rel n s => Query.Rel (n+1) s
    37| Query.Proj ts q =>
    38 let ts :=
    39 (λ (k: Fin (n+1)) => if h : ↑k<n then (ts ⟨k,h⟩).castToAnnotatedTuple
    40 else Term.index (Fin.last q.arity))
    41 Query.Proj ts (rewriting q (Query.source_proj hq rfl))
    42| Query.Sel φ q => Query.Sel φ.castToAnnotatedTuple (rewriting q (Query.source_sel hq rfl))
    43| @Query.Prod T n₁ n₂ n hn q₁ q₂ =>
    44 let tmp :=
    45 @Query.Prod (T⊕K) (n₁+1) (n₂+1) (n+2) (by omega) (rewriting q₁ (Query.source_prod hq rfl).left)
    46 let product := tmp (rewriting q₂ (Query.source_prod hq rfl).right)
    47 let ts : Tuple (Term (T⊕K) (n+2)) (n+1) :=
    48 (λ k: Fin (n+1) =>
    49 if ↑k<n₁ then Term.index (k.castLE (by simp))
    50 else if (↑k<n: Prop) then Term.index (Fin.ofNat _ (↑k+1))
    51 else Term.mul (Term.index (Fin.ofNat _ n₁)) (Term.index (Fin.ofNat _ (n+1))))
    52 Query.Proj ts product
    53| Query.Sum q₁ q₂ =>
    54 Query.Sum (rewriting q₁ (Query.source_sum hq rfl).left) (rewriting q₂ (Query.source_sum hq rfl).right)
    55| Query.Dedup q =>
    56 let q' := rewriting q (Query.source_dedup hq rfl)
    57 Query.ProvSum (λ (k: Fin n) ↦ k.castLE (by simp)) (Term.index (Fin.last n)) q'
    58| Query.Diff q₁ q₂ =>
    59 let q'₁ := rewriting q₁ (Query.source_diff hq rfl).left
    60 let q'₂ := rewriting q₂ (Query.source_diff hq rfl).right
    61 let joinCond₁ :=
    62 ((List.range n).map
    63 (λ k ↦ @Selection.BT (T⊕K) (2*n+1)
    64 (BoolTerm.EQ (Term.index (Fin.ofNat _ k)) (Term.index (Fin.ofNat _ (k+n+1)))))).foldr
    65 (λ t t' ↦ Selection.And t t') Selection.True
    66 let prod₁t := λ r ↦ Query.Sel joinCond₁ (@Query.Prod _ (n+1) n (2*n+1) (by omega) q'₁ r)
    67 let prod₁r := Query.Dedup (Query.Diff
    68 (Query.Proj (λ (k: Fin n) ↦ (Term.index (k.castLE (Nat.le_succ _)))) q'₁)
    69 (Query.Proj (λ (k: Fin n) ↦ (Term.index (k.castLE (Nat.le_succ _)))) q'₂))
    70 let prod₁ := prod₁t (prod₁r)
    71 let joinCond₂ :=
    72 ((List.range n).map
    73 (λ k ↦ @Selection.BT (T⊕K) (2*n+2)
    74 (BoolTerm.EQ (Term.index (Fin.ofNat _ k)) (Term.index (Fin.ofNat _ (k+n+1)))))).foldr
    75 (λ t t' ↦ Selection.And t t') Selection.True
    76 have h₂ : (2*n+2 - (n+1): ℕ) = n+1 := by omega
    77 let prod₂t := λ r ↦ Query.Sel joinCond₂ (@Query.Prod _ (n+1) (n+1) (2*n+2) (by omega) q'₁ r)
    78 let prod₂r := Query.ProvSum (λ (k: Fin n) ↦ (k.castLE (by simp))) (Term.index (Fin.last n)) q'₂
    79 let prod₂ := prod₂t (prod₂r)
    80 let ts₁ := (λ (k: Fin (n+1)) ↦ Term.index (k.castLE (by omega)))
    81 let ts₂ := (λ (k: Fin (n+1)) ↦ if ↑k<n then Term.index (k.castLE (by omega))
    82 else Term.sub (Term.index (Fin.ofNat _ n)) (Term.index (Fin.last (2*n+1))))
    83 Query.Sum (Query.Proj ts₁ prod₁) (Query.Proj ts₂ prod₂)
    84| Query.ProvSum _ _ _ => by simp[Query.source] at hq
    85| Query.Having _ _ _ _ _ _ _ => by simp[Query.source] at hq
    86
    87/-- **(R1) projection.** `Π_{t₁,…,t_n}(q)` is rewritten to
    88`Π_{t₁,…,t_n,#(k+1)}(q̂)`: the terms are carried over unchanged and the
    89annotation column of the rewritten argument is appended. -/
    90axiom rule_projection : ∀ [ValueType T] {K : Type} {n k : ℕ} (ts : Tuple (Term T k) n) (q : Query T k)
    91 (hq : (Query.Proj ts q).source),
    92 Query.rewriting (K := K) (Query.Proj ts q) hq
    93 = Query.Proj
    94 (fun l : Fin (n + 1) =>
    95 if h : (l : ℕ) < n then (ts ⟨l, h⟩).castToAnnotatedTuple
    96 else Term.index (Fin.last q.arity))
    97 (Query.rewriting q (Query.source_proj hq rfl))
    98
    99/-- **(R2) cross product.** `q₁ × q₂` is rewritten to
    100`Π_{#1,…,#k₁,#(k₁+2),…,#(k₁+k₂+1),#(k₁+1) ⊗ #(k₁+k₂+2)}(q̂₁ × q̂₂)`: the two
    101data blocks are kept, the two annotation columns are multiplied. -/
    102axiom rule_product : ∀ [ValueType T] {K : Type} {n n₁ n₂ : ℕ} {hn : n₁ + n₂ = n}
    103 (q₁ : Query T n₁) (q₂ : Query T n₂) (hq : (Query.Prod (hn := hn) q₁ q₂).source),
    104 Query.rewriting (K := K) (Query.Prod (hn := hn) q₁ q₂) hq
    105 = Query.Proj
    106 (fun l : Fin (n + 1) =>
    107 if (l : ℕ) < n₁ then Term.index (l.castLE (by simp))
    108 else if ((l : ℕ) < n : Prop) then Term.index (Fin.ofNat _ ((l : ℕ) + 1))
    109 else Term.mul (Term.index (Fin.ofNat _ n₁)) (Term.index (Fin.ofNat _ (n + 1))))
    110 (@Query.Prod (T ⊕ K) (n₁ + 1) (n₂ + 1) (n + 2) (by omega)
    111 (Query.rewriting q₁ (Query.source_prod hq rfl).left)
    112 (Query.rewriting q₂ (Query.source_prod hq rfl).right))
    113
    114/-- **(R3) duplicate elimination.** `ε(q)` is rewritten to
    115`γ_{1,…,k}[#(k+1) : ⊕](q̂)`: group by the data columns and `⊕`-sum the
    116annotation column. -/
    117axiom rule_dupelim : ∀ [ValueType T] {K : Type} {n : ℕ} (q : Query T n) (hq : (Query.Dedup q).source),
    118 Query.rewriting (K := K) (Query.Dedup q) hq
    119 = Query.ProvSum (fun l : Fin n => l.castLE (by simp)) (Term.index (Fin.last n))
    120 (Query.rewriting q (Query.source_dedup hq rfl))
    121
    122/-- **(R4) multiset difference.** `q₁ - q₂` is rewritten to the multiset sum of
    123two branches: the tuples of `q̂₁` whose data part survives the set difference of
    124the two data projections, carrying their annotation unchanged; and the tuples of
    125`q̂₁` matched against the `⊕`-aggregated `q̂₂`, carrying `α ⊖ Σβ`. Both branches
    126are joins on the `k` data columns. -/
    127axiom rule_difference : ∀ [ValueType T] {K : Type} {n : ℕ} (q₁ q₂ : Query T n)
    128 (hq : (Query.Diff q₁ q₂).source),
    129 Query.rewriting (K := K) (Query.Diff q₁ q₂) hq
    130 = (let q'₁ := Query.rewriting (K := K) q₁ (Query.source_diff hq rfl).left
    131 let q'₂ := Query.rewriting (K := K) q₂ (Query.source_diff hq rfl).right
    132 let joinCond₁ :=
    133 ((List.range n).map
    134 (fun j => @Selection.BT (T ⊕ K) (2 * n + 1)
    135 (BoolTerm.EQ (Term.index (Fin.ofNat _ j)) (Term.index (Fin.ofNat _ (j + n + 1)))))).foldr
    136 (fun t t' => Selection.And t t') Selection.True
    137 let prod₁t := fun r => Query.Sel joinCond₁ (@Query.Prod _ (n + 1) n (2 * n + 1) (by omega) q'₁ r)
    138 let prod₁r :=
    139 Query.Dedup (Query.Diff
    140 (Query.Proj (fun j : Fin n => Term.index (j.castLE (Nat.le_succ _))) q'₁)
    141 (Query.Proj (fun j : Fin n => Term.index (j.castLE (Nat.le_succ _))) q'₂))
    142 let prod₁ := prod₁t prod₁r
    143 let joinCond₂ :=
    144 ((List.range n).map
    145 (fun j => @Selection.BT (T ⊕ K) (2 * n + 2)
    146 (BoolTerm.EQ (Term.index (Fin.ofNat _ j)) (Term.index (Fin.ofNat _ (j + n + 1)))))).foldr
    147 (fun t t' => Selection.And t t') Selection.True
    148 let prod₂t := fun r => Query.Sel joinCond₂ (@Query.Prod _ (n + 1) (n + 1) (2 * n + 2) (by omega) q'₁ r)
    149 let prod₂r := Query.ProvSum (fun j : Fin n => j.castLE (by simp)) (Term.index (Fin.last n)) q'₂
    150 let prod₂ := prod₂t prod₂r
    151 let ts₁ := fun j : Fin (n + 1) => Term.index (j.castLE (by omega))
    152 let ts₂ := fun j : Fin (n + 1) =>
    153 if (j : ℕ) < n then Term.index (j.castLE (by omega))
    154 else Term.sub (Term.index (Fin.ofNat _ n)) (Term.index (Fin.last (2 * n + 1)))
    155 Query.Sum (Query.Proj ts₁ prod₁) (Query.Proj ts₂ prod₂))
    156
    157end Lax392996.RewritingRules
    158
    Show ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…