Correctness of Algorithm 2: COUNT enumeration

This file formalises Algorithm 2 of the HAVING / ProvSQL paper (Sen, Aryak & Senellart). The algorithm enumerates the non-empty subsets W of a finite set of occurrences U whose cardinality satisfies |W| op C for a fixed comparison operator op ∈ {=, ≠, <, ≤, >, ≥} and a constant C ∈ ℕ. The main result countEnum_correct shows that the list produced by countEnum coincides with that set, in the sense of membership.

The aggregate term t of the paper is irrelevant to COUNT and is dropped from the Lean signature; the paper notes this explicitly. The "distinct occurrences" hypothesis of the paper is encoded as List.Nodup and is needed in the spec only so that Finset cardinality matches list length: without it, the algorithm still returns subsets of occs.toFinset, but cardinality bookkeeping breaks.

def CountEnum.combinations {α : Type u_1} [DecidableEq α] : List α → ℕ → Finset α → List (Finset α)

Combinations(i, x, W) of Algorithm 2, expressed with the suffix list occs (representing the occurrences (uᵢ, αᵢ), …, (u_N, α_N)) instead of an explicit index i. Returns the list of subsets obtained by extending the accumulator W with exactly x further elements drawn from occs.

Equations

• CountEnum.combinations x✝¹ 0 x✝ = [x✝]
• CountEnum.combinations [] n.succ x✝ = []
• CountEnum.combinations (u :: rest) x_3.succ x✝ = CountEnum.combinations rest (x_3 + 1) x✝ ++ CountEnum.combinations rest x_3 (insert u x✝)

def CountEnum.addExact {α : Type u_1} [DecidableEq α] (occs : List α) (x : ℕ) : List (Finset α)

AddExact(x) of Algorithm 2: enumerate the non-empty subsets of occs of cardinality exactly x. The x = 0 case returns [] so that the empty world is excluded from the output.

Equations

• CountEnum.addExact occs x = if x = 0 then [] else CountEnum.combinations occs x ∅

def CountEnum.countEnum {α : Type u_1} [DecidableEq α] (occs : List α) (C : ℕ) (op : CompOp) : List (Finset α)

CountEnum(U, C, op) of Algorithm 2: the top-level routine. The six cases of the algorithm collapse into a single flatMap over the satisfying cardinalities x ∈ {0, …, N} because addExact occs 0 is already empty and addExact occs x is empty whenever x > N.

Equations

• CountEnum.countEnum occs C op = List.flatMap (CountEnum.addExact occs) (List.filter (fun (x : ℕ) => decide (op.eval x C)) (List.range (occs.length + 1)))

Correctness lemmas

theorem CountEnum.combinations_mem {α : Type u_1} [DecidableEq α] (occs : List α) : occs.Nodup → ∀ (x : ℕ) (W : Finset α), Disjoint W occs.toFinset → ∀ (S : Finset α), S ∈ combinations occs x W ↔ ∃ T ⊆ occs.toFinset, T.card = x ∧ S = W ∪ T

Membership characterisation of combinations. Under disjointness of the accumulator and the suffix list, the output enumerates exactly the sets of the form W ∪ T with T a subset of occs.toFinset of size x. Nodup occs is needed so that the disjointness is preserved on recursion (the head u must not appear later in the list).

theorem CountEnum.addExact_mem {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (x : ℕ) (S : Finset α) : S ∈ addExact occs x ↔ S ⊆ occs.toFinset ∧ S.card = x ∧ S ≠ ∅

Membership characterisation of addExact: the output enumerates the non-empty subsets of occs of cardinality exactly x.

theorem CountEnum.countEnum_correct {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (C : ℕ) (op : CompOp) (S : Finset α) : S ∈ countEnum occs C op ↔ S ⊆ occs.toFinset ∧ S ≠ ∅ ∧ op.eval S.card C

Correctness of Algorithm 2 (thm:count-enum-correct of the paper). For a list occs of distinct occurrences, a constant C : ℕ, and a comparison operator op, the list countEnum occs C op enumerates exactly the non-empty subsets S ⊆ occs.toFinset whose cardinality satisfies op.eval S.card C.

Home · Documentation · Publications · Contributors · Source · Cite