Frozen restatement of the claims of a published paper

Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data, ICDE 2026 links to this library: eight of its definitions and results carry a hyperlink to a declaration page under https://provsql.org/lean-docs/, and the paper as a whole links to the landing page. Those links are in a PDF and cannot be fixed after the fact.

There is one published documentation tree, and it tracks main, so the paper's links deliberately reach material that has grown beyond the paper. What has to be guaranteed is therefore narrower, and sharper, than "the docs still match the paper":

1. the anchors still exist – checked by scripts/check-anchors.sh, which reads the Anchor: lines below;
2. the declarations they land on still subsume the paper's claims – checked by this file.

This module is what makes the second half mechanical. Each claim the paper makes is restated here in the paper's own form and proved by applying the library declaration the paper cites. If the library generalizes – a wider fragment, an extra hypothesis discharged, a fused operator – the proof still goes through, which is the right answer: the paper's claim is still there, subsumed. If a statement is ever weakened, this file stops compiling and lake build fails. No textual or anchor-level check distinguishes those two cases.

The statements below are therefore frozen: they were fixed when the paper was published and are never edited to follow the library. Only the proof terms may be re-plumbed. scripts/release.sh check compares this file against the hash in scripts/icde2026.sha256, so an edit is a deliberate act that shows up in a diff rather than a silent drift.

Scope

Two places where the library and the paper are not literally coextensive, both recorded here rather than papered over:

• The paper's relational algebra has an aggregation former γ_{i₁,…,i_m}[t₁:f₁,…,t_n:f_n], and its rewriting has a rule (R5) for it. Query, the declaration the paper's grammar links to, is the classical syntax: it carries the operators of RA⁺(∖) plus ProvSum, the ⊕-aggregation that rules (R1)–(R4) emit. General aggregation, and the rewriting rule for it, live on the kind-indexed syntax (AggQuery.Gamma, and the bare-grouping rewriting of Provenance.AggQueryGroupRewriting), which did not exist when the paper was written. This module deliberately does not import those: a frozen file should depend on as little as possible, and what it must pin is what the paper's anchors name.
• Accordingly, the rewriting correctness theorem restated below carries the hypothesis q.source, the fragment (R1)–(R4) covers.

Anchor: Provenance.html

Semirings with monus

The paper defines an m-semiring by three equations. In the library the monus is axiomatized instead by its Galois connection a ⊖ b ≤ c ↔ a ≤ b ⊕ c, which is strictly stronger: the three equations are theorems. That is exactly the shape of drift this file is meant to allow – a generalization of the cited declaration keeps these proofs one-liners.

theorem Icde2026.msemiring_axiom_i {K : Type} [SemiringWithMonus K] (a b : K) : a + (b - a) = b + (a - b)

The paper's m-semiring axiom (i): a ⊕ (b ⊖ a) = b ⊕ (a ⊖ b).

Anchor: Provenance/SemiringWithMonus.html#SemiringWithMonus

theorem Icde2026.msemiring_axiom_ii {K : Type} [SemiringWithMonus K] (a b c : K) : a - b - c = a - (b + c)

The paper's m-semiring axiom (ii): (a ⊖ b) ⊖ c = a ⊖ (b ⊕ c).

theorem Icde2026.msemiring_axiom_iii {K : Type} [SemiringWithMonus K] (a : K) : a - a = 0 ∧ 0 - a = 0

The paper's m-semiring axiom (iii): a ⊖ a = 𝟘 ⊖ a = 𝟘.

theorem Icde2026.delta_axiom_i {K : Type} [SemiringWithMonus K] : SemiringWithMonus.delta 0 = 0

The paper's δ-semiring axiom (i): δ(𝟘) = 𝟘.

theorem Icde2026.delta_axiom_ii {K : Type} [SemiringWithMonus K] {j : ℕ} (hj : 0 < j) : SemiringWithMonus.delta ↑j = 1

The paper's δ-semiring axiom (ii): δ(𝟙 ⊕ ⋯ ⊕ 𝟙) = 𝟙, whatever the number of 𝟙s.

Why-provenance

The paper's proposition: for a set X, the structure (2^(2^X), ∅, {∅}, ∪, ⋓, ∖) is an m-semiring. Exhibiting the instance is only half of that – the operations have to be the stated ones – so each of the six is pinned separately.

theorem Icde2026.why_zero {α : Type} : Why.carrier 0 = ∅

Why-provenance: 𝟘 is ∅.

Anchor: Provenance/Semirings/Why.html#instSemiringWithMonusWhy

theorem Icde2026.why_one {α : Type} : Why.carrier 1 = {∅}

Why-provenance: 𝟙 is {∅}.

theorem Icde2026.why_add {α : Type} (a b : Why α) : (a + b).carrier = a.carrier ∪ b.carrier

Why-provenance: ⊕ is union of families.

theorem Icde2026.why_mul {α : Type} (a b : Why α) : (a * b).carrier = {z : Set α | ∃ (x : Set α) (y : Set α), x ∈ a.carrier ∧ y ∈ b.carrier ∧ z = x ∪ y}

Why-provenance: ⊗ is ⋓, the pairwise union of witnesses.

theorem Icde2026.why_monus {α : Type} (a b : Why α) : (a - b).carrier = a.carrier \ b.carrier

Why-provenance: ⊖ is set difference of families.

theorem Icde2026.why_isMSemiring {α : Type} : Nonempty (SemiringWithMonus (Why α))

Why-provenance is an m-semiring under exactly those operations.

Annotated databases

The paper: a K-relation of arity k is a finite multiset of k-tuples each carrying an annotation from K, and a K-instance over a schema D maps each relation name R to a K-relation of arity D(R).

theorem Icde2026.annotated_relation_eq {T : Type} [ValueType T] {K : Type} {n : ℕ} : AnnotatedRelation T K n = Multiset (Lex (Tuple T n × K))

A K-relation of arity n is a multiset of n-tuples paired with an annotation.

Anchor: Provenance/AnnotatedDatabase.html#AnnotatedDatabase

theorem Icde2026.annotated_database_lookup {T : Type} [ValueType T] {K : Type} {n : ℕ} (R : String) (d : AnnotatedDatabase T K) : AnnotatedDatabase.find n R d = AnnotatedDatabase.find n R d

A K-instance answers a relation name, at an arity, with a K-relation.

The relational algebra RA_k

Each clause of the paper's grammar, as the typing rule it is. Each is proved by exhibiting the corresponding constructor of Query.

Anchor: Provenance/Query.html#Query

def Icde2026.raRelation {T : Type} (n : ℕ) (R : String) : Query T n

relation: R ∈ RA_{D(R)}.

Equations

• Icde2026.raRelation n R = Query.Rel n R

def Icde2026.raProjection {T : Type} {n k : ℕ} (ts : Tuple (Term T k) n) (q : Query T k) : Query T n

projection: for q ∈ RA_k and terms t₁, …, t_n of max-index ≤ k, Π_{t₁,…,t_n}(q) ∈ RA_n.

Equations

• Icde2026.raProjection ts q = Π ts q

def Icde2026.raSelection {T : Type} {k : ℕ} (φ : Selection T k) (q : Query T k) : Query T k

selection: for q ∈ RA_k and φ a Boolean combination of comparisons between terms of max-index ≤ k, σ_φ(q) ∈ RA_k.

Equations

• Icde2026.raSelection φ q = σ φ q

def Icde2026.raProduct {T : Type} {k₁ k₂ : ℕ} (q₁ : Query T k₁) (q₂ : Query T k₂) : Query T (k₁ + k₂)

cross product: for q₁ ∈ RA_{k₁} and q₂ ∈ RA_{k₂}, q₁ × q₂ ∈ RA_{k₁+k₂}.

Equations

• Icde2026.raProduct q₁ q₂ = q₁ × q₂

def Icde2026.raMultisetSum {T : Type} {k : ℕ} (q₁ q₂ : Query T k) : Query T k

multiset sum: for q₁, q₂ ∈ RA_k, q₁ ⊎ q₂ ∈ RA_k.

Equations

• Icde2026.raMultisetSum q₁ q₂ = (q₁ ⊎ q₂)

def Icde2026.raDupElim {T : Type} {k : ℕ} (q : Query T k) : Query T k

duplicate elimination: for q ∈ RA_k, ε(q) ∈ RA_k.

Equations

• Icde2026.raDupElim q = ε q

def Icde2026.raDifference {T : Type} {k : ℕ} (q₁ q₂ : Query T k) : Query T k

multiset difference: for q₁, q₂ ∈ RA_k, q₁ - q₂ ∈ RA_k.

Equations

• Icde2026.raDifference q₁ q₂ = (q₁ - q₂)

def Icde2026.raJoin {T : Type} {k₁ k₂ : ℕ} (φ : Selection T (k₁ + k₂)) (q₁ : Query T k₁) (q₂ : Query T k₂) : Query T (k₁ + k₂)

join, the paper's syntactic sugar q₁ ⋈_φ q₂ ≝ σ_φ(q₁ × q₂).

Equations

• Icde2026.raJoin φ q₁ q₂ = σ φ (q₁ × q₂)

def Icde2026.raSetUnion {T : Type} {k : ℕ} (q₁ q₂ : Query T k) : Query T k

set union, the paper's syntactic sugar q₁ ∪ q₂ ≝ ε(q₁ ⊎ q₂).

Equations

• Icde2026.raSetUnion q₁ q₂ = ε (q₁ ⊎ q₂)

Plain multiset semantics

The paper's ⟦·⟧_I, clause by clause.

Anchor: Provenance/Query.html#Query.evaluate

theorem Icde2026.eval_rel {T : Type} [ValueType T] {n : ℕ} (R : String) (d : Database T) : (Query.Rel n R).evaluate d = (Database.find n R d).getD ∅

relation: ⟦R⟧_I ≝ I(R).

theorem Icde2026.eval_proj {T : Type} [ValueType T] {n k : ℕ} (ts : Tuple (Term T k) n) (q : Query T k) (d : Database T) : (Π ts q).evaluate d = Multiset.map (fun (u : Tuple T k) (l : Fin n) => (ts l).eval u) (q.evaluate d)

projection: ⟦Π_{t₁,…,t_n}(q)⟧_I ≝ {|(t₁(u),…,t_n(u)) | u ∈ ⟦q⟧_I|}.

theorem Icde2026.eval_sel {T : Type} [ValueType T] {n : ℕ} (φ : Selection T n) (q : Query T n) (d : Database T) : (σ φ q).evaluate d = Multiset.filter φ.eval (q.evaluate d)

selection: ⟦σ_φ(q)⟧_I ≝ {|u | u ∈ ⟦q⟧_I, φ(u)|}.

theorem Icde2026.eval_prod {T : Type} [ValueType T] {n k₁ k₂ : ℕ} {hn : k₁ + k₂ = n} (q₁ : Query T k₁) (q₂ : Query T k₂) (d : Database T) : (q₁ × q₂).evaluate d = Relation.cast hn (q₁.evaluate d * q₂.evaluate d)

cross product: ⟦q₁ × q₂⟧_I ≝ ⟦q₁⟧_I × ⟦q₂⟧_I.

theorem Icde2026.eval_sum {T : Type} [ValueType T] {n : ℕ} (q₁ q₂ : Query T n) (d : Database T) : (q₁ ⊎ q₂).evaluate d = q₁.evaluate d + q₂.evaluate d

multiset sum: ⟦q₁ ⊎ q₂⟧_I ≝ ⟦q₁⟧_I ⊎ ⟦q₂⟧_I.

theorem Icde2026.eval_dedup {T : Type} [ValueType T] {n : ℕ} (q : Query T n) (d : Database T) : (ε q).evaluate d = Multiset.dedup (q.evaluate d)

duplicate elimination: ⟦ε(q)⟧_I maps t to 1 when ⟦q⟧_I(t) > 0 and to 0 otherwise.

theorem Icde2026.eval_diff {T : Type} [ValueType T] {n : ℕ} (q₁ q₂ : Query T n) (d : Database T) (r₂ : Multiset (Tuple T n)) (hr : r₂ = q₂.evaluate d) : (q₁ - q₂).evaluate d = Multiset.filter (fun (u : Tuple T n) => u ∉ r₂) (q₁.evaluate d)

multiset difference: every copy of a tuple occurring at all in ⟦q₂⟧_I is removed from ⟦q₁⟧_I.

Semantics over annotated databases

The paper's ⟪·⟫_Î: the same operators, with ⊕ on multiset sum and duplicate elimination, ⊗ on cross product, and ⊖ on difference.

Anchor: Provenance/QueryAnnotatedDatabase.html#Query.evaluateAnnotated

theorem Icde2026.aeval_rel {T : Type} [ValueType T] {K : Type} {n : ℕ} [SemiringWithMonus K] [DecidableEq K] (R : String) (hq : (Query.Rel n R).source) (d : AnnotatedDatabase T K) : (Query.Rel n R).evaluateAnnotated hq d = (AnnotatedDatabase.find n R d).getD ∅

relation: ⟪R⟫_Î ≝ Î(R).

theorem Icde2026.aeval_proj {T : Type} [ValueType T] {K : Type} {n k : ℕ} [SemiringWithMonus K] [DecidableEq K] (ts : Tuple (Term T k) n) (q : Query T k) (hq : (Π ts q).source) (d : AnnotatedDatabase T K) : (Π ts q).evaluateAnnotated hq d = Multiset.map (fun (p : AnnotatedTuple T K k) => (fun (l : Fin n) => (ts l).eval p.1, p.2)) (q.evaluateAnnotated ⋯ d)

projection: the annotation rides along unchanged.

theorem Icde2026.aeval_sel {T : Type} [ValueType T] {K : Type} {n : ℕ} [SemiringWithMonus K] [DecidableEq K] (φ : Selection T n) (q : Query T n) (hq : (σ φ q).source) (d : AnnotatedDatabase T K) : (σ φ q).evaluateAnnotated hq d = Multiset.filter (fun (p : AnnotatedTuple T K n) => φ.eval p.1) (q.evaluateAnnotated ⋯ d)

selection: the predicate reads the data part only.

theorem Icde2026.aeval_prod {T : Type} [ValueType T] {K : Type} {n k₁ k₂ : ℕ} [SemiringWithMonus K] [DecidableEq K] {hn : k₁ + k₂ = n} (q₁ : Query T k₁) (q₂ : Query T k₂) (hq : (q₁ × q₂).source) (d : AnnotatedDatabase T K) : (q₁ × q₂).evaluateAnnotated hq d = Multiset.map (fun (xy : AnnotatedTuple T K k₁ × AnnotatedTuple T K k₂) => (⋯.mp (Fin.append xy.1.1 xy.2.1), xy.1.2 * xy.2.2)) (Multiset.product (q₁.evaluateAnnotated ⋯ d) (q₂.evaluateAnnotated ⋯ d))

cross product: annotations multiply, α ⊗ β.

theorem Icde2026.aeval_sum {T : Type} [ValueType T] {K : Type} {n : ℕ} [SemiringWithMonus K] [DecidableEq K] (q₁ q₂ : Query T n) (hq : (q₁ ⊎ q₂).source) (d : AnnotatedDatabase T K) : (q₁ ⊎ q₂).evaluateAnnotated hq d = q₁.evaluateAnnotated ⋯ d + q₂.evaluateAnnotated ⋯ d

multiset sum: the two annotated relations are added.

theorem Icde2026.aeval_dedup {T : Type} [ValueType T] {K : Type} {n : ℕ} [SemiringWithMonus K] [DecidableEq K] (q : Query T n) (hq : (ε q).source) (d : AnnotatedDatabase T K) : (ε q).evaluateAnnotated hq d = ↑↑(groupByKey (q.evaluateAnnotated ⋯ d))

duplicate elimination: the copies of a tuple are collapsed into one, annotated by the ⊕-sum of their annotations.

theorem Icde2026.aeval_diff {T : Type} [ValueType T] {K : Type} {n : ℕ} [SemiringWithMonus K] [DecidableEq K] (q₁ q₂ : Query T n) (hq : (q₁ - q₂).source) (d : AnnotatedDatabase T K) : (q₁ - q₂).evaluateAnnotated hq d = Multiset.map (fun (x : AnnotatedTuple T K n) => match x with | (u, a) => (u, a - (Option.map Prod.snd (List.find? (fun (x : Tuple T n × K) => decide (x.1 = u)) ↑(groupByKey (q₂.evaluateAnnotated ⋯ d)))).getD 0)) (q₁.evaluateAnnotated ⋯ d)

multiset difference: a tuple of the left argument keeps its slot, with annotation α ⊖ Σβ where Σβ is the ⊕-sum of the annotations of its copies in the right argument.

The rewriting rules (R1)–(R4)

The paper gives five rules; (R5), aggregation, is not part of this classical rewriting (see Scope above). Each rule below is stated as the equation it is: applying the rewriting to an operator produces exactly the paper's right-hand side. The annotation lives in the last column, so a query of arity n rewrites to one of arity n+1.

Anchor: Provenance/QueryRewriting.html#query.Rewriting

theorem Icde2026.rule_projection {T : Type} [ValueType T] {K : Type} {n k : ℕ} (ts : Tuple (Term T k) n) (q : Query T k) (hq : (Π ts q).source) : (Π ts q).rewriting hq = (Π fun (l : Fin (n + 1)) => if h : ↑l < n then (ts ⟨↑l, h⟩).castToAnnotatedTuple else #(Fin.last q.arity)) (q.rewriting ⋯)

(R1) projection. Π_{t₁,…,t_n}(q) is rewritten to Π_{t₁,…,t_n,#(k+1)}(q̂): the terms are carried over unchanged and the annotation column of the rewritten argument is appended.

theorem Icde2026.rule_product {T : Type} [ValueType T] {K : Type} {n n₁ n₂ : ℕ} {hn : n₁ + n₂ = n} (q₁ : Query T n₁) (q₂ : Query T n₂) (hq : (q₁ × q₂).source) : (q₁ × q₂).rewriting hq = (Π fun (l : Fin (n + 1)) => if ↑l < n₁ then #(Fin.castLE ⋯ l) else if ↑l < n then #(Fin.ofNat (n + 2) (↑l + 1)) else (#(Fin.ofNat (n + 2) n₁)).mul #(Fin.ofNat (n + 2) (n + 1))) (q₁.rewriting ⋯ × q₂.rewriting ⋯)

(R2) cross product. q₁ × q₂ is rewritten to Π_{#1,…,#k₁,#(k₁+2),…,#(k₁+k₂+1),#(k₁+1) ⊗ #(k₁+k₂+2)}(q̂₁ × q̂₂): the two data blocks are kept, the two annotation columns are multiplied.

theorem Icde2026.rule_dupelim {T : Type} [ValueType T] {K : Type} {n : ℕ} (q : Query T n) (hq : (ε q).source) : (ε q).rewriting hq = Query.ProvSum (fun (l : Fin n) => Fin.castLE ⋯ l) (#(Fin.last n)) (q.rewriting ⋯)

(R3) duplicate elimination. ε(q) is rewritten to γ_{1,…,k}[#(k+1) : ⊕](q̂): group by the data columns and ⊕-sum the annotation column. This is the rule that makes duplicate elimination the ⊕-gate creator, and ProvSum is its target operator.

theorem Icde2026.rule_difference {T : Type} [ValueType T] {K : Type} {n : ℕ} (q₁ q₂ : Query T n) (hq : (q₁ - q₂).source) : (q₁ - q₂).rewriting hq = have q'₁ := q₁.rewriting ⋯; have q'₂ := q₂.rewriting ⋯; have joinCond₁ := List.foldr (fun (t t' : Selection (T ⊕ K) (2 * n + 1)) => t.And t') Selection.True (List.map (fun (j : ℕ) => Selection.BT ((fun (x y : Term (T ⊕ K) (2 * n + 1)) => BoolTerm.EQ x y) #(Fin.ofNat (2 * n + 1) j) #(Fin.ofNat (2 * n + 1) (j + n + 1)))) (List.range n)); have prod₁t := fun (r : Query (T ⊕ K) n) => σ joinCond₁ (q'₁ × r); have prod₁r := ε ((Π fun (j : Fin n) => #(Fin.castLE ⋯ j)) q'₁ - (Π fun (j : Fin n) => #(Fin.castLE ⋯ j)) q'₂); have prod₁ := prod₁t prod₁r; have joinCond₂ := List.foldr (fun (t t' : Selection (T ⊕ K) (2 * n + 2)) => t.And t') Selection.True (List.map (fun (j : ℕ) => Selection.BT ((fun (x y : Term (T ⊕ K) (2 * n + 2)) => BoolTerm.EQ x y) #(Fin.ofNat (2 * n + 2) j) #(Fin.ofNat (2 * n + 2) (j + n + 1)))) (List.range n)); have prod₂t := fun (r : Query (T ⊕ K) (n + 1)) => σ joinCond₂ (q'₁ × r); have prod₂r := Query.ProvSum (fun (j : Fin n) => Fin.castLE ⋯ j) (#(Fin.last n)) q'₂; have prod₂ := prod₂t prod₂r; have ts₁ := fun (j : Fin (n + 1)) => #(Fin.castLE ⋯ j); have ts₂ := fun (j : Fin (n + 1)) => if ↑j < n then #(Fin.castLE ⋯ j) else (#(Fin.ofNat (2 * n + 1 + 1) n)).sub #(Fin.last (2 * n + 1)); Π ts₁ prod₁ ⊎ Π ts₂ prod₂

(R4) multiset difference. q₁ - q₂ is rewritten to the multiset sum of two branches: the tuples of q̂₁ whose data part survives the set difference of the two data projections, carrying their annotation unchanged; and the tuples of q̂₁ matched against the ⊕-aggregated q̂₂, carrying α ⊖ Σβ. Both branches are joins on the k data columns.

Correctness of the rewriting

The paper's theorem: let D be a schema, q a query over D, K an appropriate algebraic structure, Î a K-instance over D, and q̂ the query obtained by applying the rewriting rules recursively bottom up. Then ⟪q⟫_Î = ⟦q̂⟧_Î.

The equality is between an annotated relation and a plain one, so it is stated through the encoding that puts the annotation in the last column (toComposite), which is what "the same relation" means once the rewriting has moved the annotation into the data.

Anchor: Provenance/QueryRewriting.html#Query.rewriting_valid

theorem Icde2026.rewriting_valid {T : Type} [ValueType T] {K : Type} {n : ℕ} [SemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (q : Query T n) (hq : q.source) (d : AnnotatedDatabase T K) : (q.evaluateAnnotated hq d).toComposite = (q.rewriting hq).evaluate d.toComposite

⟪q⟫_Î = ⟦q̂⟧_Î, for q in the fragment the rules (R1)–(R4) cover.

Home · Documentation · Publications · Contributors · Source · Cite