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