Correctness of COUNT enumeration

This file formalises a count-based enumeration algorithm. 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.

An aggregate term t would be irrelevant to COUNT and is dropped from the Lean signature. The "distinct occurrences" hypothesis 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): 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): 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): 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.combinations_nodup {α : Type u_1} [DecidableEq α] (occs : List α) : occs.Nodup → ∀ (x : ℕ) (W : Finset α), Disjoint W occs.toFinset → (combinations occs x W).Nodup

The enumeration combinations contains no duplicate subset. As in combinations_mem, the disjointness of the accumulator and the suffix list is preserved through the recursion; the two recursive calls produce sets that differ on membership of the head u.

theorem CountEnum.addExact_nodup {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (x : ℕ) : (addExact occs x).Nodup

The enumeration addExact contains no duplicate subset.

theorem CountEnum.countEnum_nodup {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (C : ℕ) (op : CompOp) : (countEnum occs C op).Nodup

The top-level enumeration countEnum contains no duplicate subset: within one bucket x by addExact_nodup, and across buckets because a subset in bucket x has cardinality exactly x. This is not cosmetic: the provenance attached to the enumeration is the ⊕-sum of the world annotations over the returned list, and in a non-idempotent m-semiring a duplicated world would change the value.

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 countEnum. 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