Algebraic identities behind HAVING (count) provenance

This file gathers query-free algebraic identities, in an arbitrary commutative m-semiring, that underpin the correctness of the possible-world semantics for HAVING (count op C) predicates.

For a finite ambient set U : Finset ι and a family α : ι → K, we define

• A α W := ∏ x ∈ W, α x,
• T α U W := A α W ⊖ ⊕_{x ∈ U \ W} A α (W ∪ {x}),
• S α U C := ⊕_{W ⊆ U, |W| = C} A α W,
• F α U C := ⊕_{W ⊆ U, |W| ≥ C} T α U W.

The main results are the bounding lemma A_V ≤ ⊕_{V ⊆ W ⊆ U} T_U(W) in an idempotent m-semiring (upward_expansion), the collapse of the T-weighted sum over any upward-closed family of worlds to the A-weighted sum over its minimal elements in an absorptive m-semiring (upward_closed_collapse, with F_eq_S as the HAVING count ≥ C instance), include/exclude-style recurrences for S and F, and the per-world bound world_bound behind the = and ≤ cases.

def Having.A {ι K : Type} [CommSemiringWithMonus K] (α : ι → K) (W : Finset ι) : K

Monomial annotation of a subset: A_W = ∏_{x ∈ W} α x, with the convention A_∅ = 𝟙.

Equations

• Having.A α W = ∏ x ∈ W, α x

def Having.T {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U W : Finset ι) : K

T_U(W) = A_W ⊖ ⊕_{x ∈ U \ W} A_{W ∪ {x}}: the “exactly-W” contribution that removes from A_W all one-step extensions of W inside U.

Equations

• Having.T α U W = Having.A α W - ∑ x ∈ U \ W, Having.A α (insert x W)

def Having.S {ι K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) (C : ℕ) : K

S_C(U) = ⊕_{W ⊆ U, |W| = C} A_W: the JOIN-based provenance for a HAVING count = C aggregate (up to surface-level reindexing).

Equations

• Having.S α U C = ∑ W ∈ Finset.powersetCard C U, Having.A α W

def Having.F {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) (C : ℕ) : K

F_C(U) = ⊕_{W ⊆ U, |W| ≥ C} T_U(W): the possible-world provenance for a HAVING count ≥ C predicate.

Equations

• Having.F α U C = ∑ W ∈ U.powerset with C ≤ W.card, Having.T α U W

theorem Having.T_eq_mul_one_monus_sum {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_distrib : mul_sub_left_distributive K) (U W : Finset ι) : T α U W = A α W * (1 - ∑ x ∈ U \ W, α x)

Alternative form T_U(W) = A_W ⊗ (𝟙 ⊖ ⊕_{x ∈ U \ W} α x). This is the shape in which T_U(W) first arises from the possible-world semantics; the definition of T is the rewritten form obtained via distributivity of ⊗ over ⊖ and over ⊕. Holds in any commutative m-semiring with mul_sub_left_distributive.

theorem Having.SC_recurrence {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) {U : Finset ι} {u : ι} (hu : u ∈ U) (C : ℕ) : S α U (C + 1) = S α (U.erase u) (C + 1) + S α (U.erase u) C * α u

Include/exclude recurrence for the JOIN-based provenance S: S_{C+1}(U) = S_{C+1}(U \ {u}) ⊕ S_C(U \ {u}) ⊗ α u. The proof partitions (insert u U').powersetCard (C+1) into subsets that do not contain u and images of C-sized subsets of U' under insert u.

theorem Having.sum_le_of_forall_le {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_idem : idempotent K) {s : Finset ι} {f : ι → K} {a : K} (hle : ∀ x ∈ s, f x ≤ a) : ∑ x ∈ s, f x ≤ a

In an idempotent CommSemiringWithMonus, if every summand of a Finset.sum is bounded above by a, then so is the sum. The empty sum is 0 ≤ a by canonical ordering; the inductive step uses a + a = a.

theorem Having.upward_expansion {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_idem : idempotent K) (U V : Finset ι) : V ⊆ U → A α V ≤ ∑ W ∈ U.powerset with V ⊆ W, T α U W

Upward expansion bound: in an idempotent m-semiring, the monomial of any subset V ⊆ U is bounded above by the sum of T_U(W) over all supersets W ⊇ V inside U. The proof is by strong induction on (U \ V).card, using le_plus_monus for the inductive step and the auxiliary sum_le_of_forall_le to collapse multiplicities by idempotence.

theorem Having.FC_recurrence {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_idem : idempotent K) (h_distrib : mul_sub_left_distributive K) {U : Finset ι} {u : ι} (hu : u ∈ U) (C : ℕ) : F α U (C + 1) = F α (U.erase u) (C + 1) + F α (U.erase u) C * α u

Include/exclude recurrence for the possible-world provenance F: F_{C+1}(U) = F_{C+1}(U \ {u}) ⊕ F_C(U \ {u}) ⊗ α u, in any idempotent commutative m-semiring with left-distributivity of ⊗ over ⊖. The proof splits the powerset of U by whether u ∈ W, simplifies the u ∈ W part to F_C(U') ⊗ α u, and combines two opposite inequalities using the upward expansion bound upward_expansion.

Upward-closed family collapse in absorptive m-semirings

The provenance of a finite family F of subsets, weighted by A, agrees with the provenance of any subfamily M ⊆ F such that every element of F contains some element of M. When F is upward-closed under inclusion, the canonical such M is the set of minimal elements of F.

theorem Having.mul_le_mul_left_canonical {K : Type} [CommSemiringWithMonus K] (a : K) {b c : K} (h : b ≤ c) : a * b ≤ a * c

Multiplication on the left is monotone in any SemiringWithMonus (the CanonicallyOrderedAdd structure makes the additive witness of ≤ multiply through).

theorem Having.prod_le_one_absorptive {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (α : ι → K) (S : Finset ι) : ∏ x ∈ S, α x ≤ 1

In an absorptive CommSemiringWithMonus, any finite product of annotations is bounded above by 𝟙.

theorem Having.A_le_of_subset_absorptive {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (α : ι → K) {W W' : Finset ι} (hW'W : W' ⊆ W) : A α W ≤ A α W'

In an absorptive CommSemiringWithMonus, the monomial A is monotone decreasing under inclusion: enlarging a subset can only decrease its annotation, since each additional factor is bounded by 𝟙.

theorem Having.absorbing_subfamily {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_abs : absorptive K) {F M : Finset (Finset ι)} (hM_sub : M ⊆ F) (hcover : ∀ W ∈ F, ∃ W' ∈ M, W' ⊆ W) : ∑ W ∈ F, A α W = ∑ W ∈ M, A α W

Upward-closed family collapse: in an absorptive commutative m-semiring, the A-weighted sum over a finite family F equals the A-weighted sum over any subfamily M ⊆ F such that every element of F is a superset of some element of M. Taking M = the minimal elements of F (when F is upward-closed) is the canonical application: the provenance of an upward-closed family of worlds collapses to the provenance of its minimal worlds.

theorem Having.upward_closed_collapse {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_abs : absorptive K) {U : Finset ι} {F M : Finset (Finset ι)} (hFU : ∀ W ∈ F, W ⊆ U) (hF_up : ∀ W ∈ F, ∀ (W' : Finset ι), W ⊆ W' → W' ⊆ U → W' ∈ F) (hM_sub : M ⊆ F) (hcover : ∀ W ∈ F, ∃ V ∈ M, V ⊆ W) : ∑ W ∈ F, T α U W = ∑ V ∈ M, A α V

Upward-closed collapse of the possible-world provenance. In an absorptive commutative m-semiring, the ⊕-sum of the world annotations T_U(W) over an upward-closed family F of subsets of U equals the ⊕-sum of the monomials A_V over any subfamily M ⊆ F such that every element of F contains some element of M (canonically, the minimal elements of F).

Unlike absorbing_subfamily, which relates two A-weighted sums, this is the statement needed to collapse a possible-world provenance (a T-weighted sum): the ≤ half bounds each T_U(W) ≤ A_W ≤ A_V (by monus_le and A_le_of_subset_absorptive), and the ≥ half recovers each A_V from upward_expansion, whose index set is contained in F by upward closure. Note that mul_sub_left_distributive is not needed.

F equals S: algebraic skeleton of HAVING count ≥ C

The possible-world provenance F_C(U) agrees with the join-based provenance S_C(U) for all C ≥ 1, in any absorptive commutative m-semiring: the family of worlds of cardinality ≥ C is upward-closed with the worlds of cardinality exactly C as minimal elements, so upward_closed_collapse applies. An alternative, recurrence-driven proof goes through FC_recurrence and SC_recurrence (with F_zero_eq_one closing the C = 1 base), at the price of the additional mul_sub_left_distributive hypothesis used by FC_recurrence; the recurrences are kept as results of independent interest.

theorem Having.F_zero_eq_one {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_idem : idempotent K) (h_abs : absorptive K) (α : ι → K) (U : Finset ι) : F α U 0 = 1

In an absorptive idempotent m-semiring, F α U 0 = 𝟙: the unconstrained possible-world provenance collapses to 𝟙. Lower bound from upward_expansion with V = ∅; upper bound from T α U W ≤ A α W and A α W ≤ 𝟙 (the latter via prod_le_one_absorptive).

theorem Having.F_eq_S {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (α : ι → K) (U : Finset ι) (C : ℕ) : F α U (C + 1) = S α U (C + 1)

Algebraic skeleton for HAVING count ≥ C: in an absorptive commutative m-semiring, the possible-world provenance F_C(U) equals the join-based provenance S_C(U) for all C ≥ 1. This is the instance of upward_closed_collapse for the upward-closed family of worlds of cardinality ≥ C, whose minimal elements are the worlds of cardinality exactly C; in particular mul_sub_left_distributive is not needed (it re-enters only when relating T to the factored form of the world annotation, see T_eq_mul_one_monus_sum). Absorptive is a strictly stronger hypothesis than the bare “idempotent + distributive” combination one might wish for, and it is essential: TropicalR.F_ne_S exhibits a non-absorptive (but idempotent and distributive) instance – Tropical (WithTop ℝ) – for which the conclusion fails. The idempotent m-semirings in the library that are absorptive (Bool, BoolFunc, IntervalUnion, Tropical (WithTop ℕ), Viterbi, Łukasiewicz, MinMax) all satisfy the conclusion.

The = and ≤ cases

F_eq_S settles HAVING count ≥ C. The = and ≤ cases do not follow from it formally; both rest on the per-world upper bound world_bound below.

theorem Having.world_bound {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) {U W : Finset ι} (hWU : W ⊆ U) {j C : ℕ} (hjW : j ≤ W.card) (hWC : W.card ≤ C) : T α U W ≤ S α U j - S α U (C + 1)

Per-world upper bound. For j ≤ |W| ≤ C, the annotation of a single world W is already below S_j(U) ⊖ S_{C+1}(U).

The order of the steps matters: bounding A_W by S_j(U) inside the subtrahend of T_U(W) = A_W ⊖ (A_W ⊗ E_W) would move the monus the wrong way. The bound is applied instead to the factored form T_U(W) = A_W ⊗ (𝟙 ⊖ E_W), whose second factor does not mention A_W.

Unlike for F_eq_S, the mul_sub_left_distributive hypothesis here is essential and not an artifact of the proof: ChainFive.not_world_bound exhibits an absorptive commutative m-semiring without it in which the conclusion fails (and with it the conclusions of G_eq_S_monus_S and atMost_eq_S_monus_S, which rest on this bound).

def Having.G {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) (C : ℕ) : K

G_C(U) = ⊕_{W ⊆ U, |W| = C} T_U(W): the possible-world provenance of a HAVING count = C predicate.

Equations

• Having.G α U C = ∑ W ∈ Finset.powersetCard C U, Having.T α U W

theorem Having.sum_monus {K : Type} [CommSemiringWithMonus K] {ι' : Type} [DecidableEq ι'] (h_idem : idempotent K) (s : Finset ι') (f : ι' → K) (c : K) : ∑ x ∈ s, f x - c = ∑ x ∈ s, (f x - c)

Monus distributes over a finite sum with a fixed subtrahend: the Finset form of add_monus_of_idempotent.

theorem Having.G_eq_S_monus_S {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (C : ℕ) : G α U C = S α U C - S α U (C + 1)

The = case. The possible-world provenance of HAVING count = C is the join-side difference S_C(U) ⊖ S_{C+1}(U). This does not follow from F_eq_S; the ≤ half is world_bound and the ≥ half replaces the subtrahend of each T_U(W) by the larger S_{C+1}(U).

theorem Having.atMost_eq_S_monus_S {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (C : ℕ) : ∑ W ∈ U.powerset with 1 ≤ W.card ∧ W.card ≤ C, T α U W = S α U 1 - S α U (C + 1)

The ≤ case. The possible-world provenance of HAVING count ≤ C on non-empty worlds is S_1(U) ⊖ S_{C+1}(U).

Collapse to minimal worlds, and the size of the index sets

upward_closed_collapse specializes to any family of worlds cut out by a superset-monotone predicate: the provenance collapses to the ⊕-sum of the monomials of the minimal valid worlds. For SUM(t) op c predicates over ℕ-weights with op ∈ {≥, >}, a bounded-ratio hypothesis on the weights (c ≤ k ⊗ t i for every occurrence) bounds the size of the minimal worlds by k (resp. k + 1), so the collapsed sum ranges over an index set of at most ∑_{i ≤ k} C(|U|, i) terms. The cardinality facts are stated as Finset.card statements about the index sets of the sums; they say nothing about running time.

@[instance_reducible]

instance Having.decidableMinimal {ι : Type} [DecidableEq ι] {P : Finset ι → Prop} [DecidablePred P] (V : Finset ι) : Decidable (∀ V' ⊂ V, ¬P V')

Minimality of a world with respect to a predicate is decidable: only the subsets of the world need inspecting.

Equations

• Having.decidableMinimal V = decidable_of_iff (∀ V' ∈ V.powerset, V' ≠ V → ¬P V') ⋯

theorem Having.exists_minimal_subset {ι : Type} {P : Finset ι → Prop} {W : Finset ι} : P W → ∃ V ⊆ W, P V ∧ ∀ V' ⊂ V, ¬P V'

Every world satisfying P contains a world satisfying P that is minimal among all worlds (not merely among its own subsets). Strong induction on the cardinality.

theorem Having.collapse_to_minimal {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_abs : absorptive K) (U : Finset ι) {P : Finset ι → Prop} [DecidablePred P] (hmono : ∀ ⦃W W' : Finset ι⦄, W ⊆ W' → P W → P W') : ∑ W ∈ U.powerset with P W, T α U W = ∑ V ∈ Finset.filter P U.powerset with ∀ V' ⊂ V, ¬P V', A α V

Collapse to minimal worlds. In an absorptive commutative m-semiring, for any predicate P on worlds that is monotone under supersets, the T-weighted possible-world provenance of the valid worlds inside U collapses to the ⊕-sum of the monomials of the minimal valid worlds. This is the workhorse behind the tractable COUNT ≥ and bounded- ratio SUM ≥ / > cases.

theorem Having.sum_ge_collapse {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_abs : absorptive K) (U : Finset ι) (t : ι → ℕ) (c : ℕ) : ∑ W ∈ U.powerset with c ≤ ∑ i ∈ W, t i, T α U W = ∑ V ∈ {W ∈ U.powerset | c ≤ ∑ i ∈ W, t i} with ∀ V' ⊂ V, ¬c ≤ ∑ i ∈ V', t i, A α V

HAVING SUM(t) ≥ c collapse. Instance of collapse_to_minimal for the superset-monotone predicate c ≤ ∑_{i ∈ W} t i over ℕ-weights.

theorem Having.sum_gt_collapse {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (h_abs : absorptive K) (U : Finset ι) (t : ι → ℕ) (c : ℕ) : ∑ W ∈ U.powerset with c < ∑ i ∈ W, t i, T α U W = ∑ V ∈ {W ∈ U.powerset | c < ∑ i ∈ W, t i} with ∀ V' ⊂ V, ¬c < ∑ i ∈ V', t i, A α V

HAVING SUM(t) > c collapse. As sum_ge_collapse, for the strict comparison.

theorem Having.minimal_card_le_of_sum_ge {ι : Type} {t : ι → ℕ} {c k : ℕ} {U W : Finset ι} (hratio : ∀ i ∈ U, t i ≠ 0 → c ≤ k * t i) (hWU : W ⊆ U) (_hW : c ≤ ∑ i ∈ W, t i) (hmin : ∀ W' ⊂ W, ¬c ≤ ∑ i ∈ W', t i) : W.card ≤ k

Bounded ratio bounds the minimal worlds of SUM(t) ≥ c. If every occurrence of the group with a nonzero value satisfies c ≤ k ⊗ t i (read: c / t i ≤ k), then any minimal world with ∑ t ≥ c has at most k occurrences: a zero-valued occurrence never belongs to a minimal world (removing it leaves the sum unchanged), and any k-subset of nonzero values already reaches the threshold.

theorem Having.minimal_card_le_of_sum_gt {ι : Type} {t : ι → ℕ} {c k : ℕ} {U W : Finset ι} (hratio : ∀ i ∈ U, t i ≠ 0 → c ≤ k * t i) (hWU : W ⊆ U) (_hW : c < ∑ i ∈ W, t i) (hmin : ∀ W' ⊂ W, ¬c < ∑ i ∈ W', t i) : W.card ≤ k + 1

Bounded ratio bounds the minimal worlds of SUM(t) > c. If every occurrence of the group with a nonzero value satisfies c ≤ k ⊗ t i, then any minimal world with ∑ t > c has at most k + 1 occurrences: a zero-valued occurrence never belongs to a minimal world, k nonzero values reach c, and one further nonzero value makes the comparison strict (which also covers the boundary case c = 0).

theorem Having.card_powerset_filter_card_le {ι : Type} [DecidableEq ι] (U : Finset ι) (k : ℕ) : {W ∈ U.powerset | W.card ≤ k}.card = ∑ i ∈ Finset.range (k + 1), U.card.choose i

Size of the COUNT ≤ k index set: the worlds of cardinality at most k inside U number ∑_{i ≤ k} C(|U|, i). This is a statement about the number of terms of the possible-world ⊕-sum, not about running time.

theorem Having.card_minimal_sum_ge_le {ι : Type} [DecidableEq ι] (U : Finset ι) (t : ι → ℕ) {c k : ℕ} (hratio : ∀ i ∈ U, t i ≠ 0 → c ≤ k * t i) : {V ∈ {W ∈ U.powerset | c ≤ ∑ i ∈ W, t i} | ∀ V' ⊂ V, ¬c ≤ ∑ i ∈ V', t i}.card ≤ ∑ i ∈ Finset.range (k + 1), U.card.choose i

Size of the collapsed SUM(t) ≥ c index set under the bounded- ratio hypothesis: the minimal valid worlds number at most ∑_{i ≤ k} C(|U|, i).

Home · Documentation · Publications · Contributors · Source · Cite