Counting assignments on a declared set of variables

CNF.modelCountOn counts assignments of a supplied finite set, extending them by false outside that set. When the set contains all occurring variables, each unused variable contributes a free Boolean choice. The original occurring-variable CNF.modelCount is unchanged and is recovered by declaring exactly the occurring variables.

Renaming by positions in distinctVars gives dense natural labels below numVars. This differs from the existing compact, whose first literal-occurrence positions can have gaps. The dense renaming preserves literal order, clause lengths and the occurring-variable count.

These are elementary semantic transport facts for the declared-variable convention of the native counting development in #1226. They do not implement a counting algorithm or assert a runtime bound.

Main definitions

• Cslib.Logic.PL.CNF.modelCountOn: count assignments on a declared finite set.
• Cslib.Logic.PL.CNF.validDeclaredInput: guard for clause widths ≤ k and variables < N.
• Cslib.Logic.PL.CNF.normalizeDeclaredLeaf: right-shift a declared count by unused variables.

Main results

• Cslib.Logic.PL.CNF.modelCountOn_vars: recover the original occurring-variable count.
• Cslib.Logic.PL.CNF.modelCountOn_eq_mul_modelCount: unused variables give independent choices.
• Cslib.Logic.PL.CNF.vars_dense_relabel: dense renaming has exactly the expected variable range.
• Cslib.Logic.PL.CNF.modelCountOn_dense_relabel: dense renaming preserves the declared count.
• Cslib.Logic.PL.CNF.validDeclaredInput_eq_true_iff: width and Finset.range N equivalence.
• Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_div, normalizeDeclaredLeaf_eq_modelCount, normalizeDeclaredLeaf_le_two_pow_numVars: division form, modelCount, and 2 ^ numVars bound.

def Cslib.Logic.PL.CNF.modelCountOn {V : Type u_1} [DecidableEq V] (φ : CNF V) (declared : Finset V) : ℕ

Count assignments of declared that satisfy the existing CNF evaluation, extending by false outside declared. To interpret this as a declared-variable formula, require that every occurring variable belongs to declared. No inhabitedness of the variable type is needed.

@[simp]

theorem Cslib.Logic.PL.CNF.modelCountOn_vars {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.modelCountOn φ.vars.toFinset = φ.modelCount

Declaring exactly the occurring variables recovers the existing model count.

@[simp]

theorem Cslib.Logic.PL.CNF.modelCountOn_nil {V : Type u_1} [DecidableEq V] (declared : Finset V) : modelCountOn [] declared = 2 ^ declared.card

Every declared variable is free in an empty formula, including when the declared set is empty.

theorem Cslib.Logic.PL.CNF.modelCountOn_eq_zero_of_nil_mem {V : Type u_1} [DecidableEq V] {φ : CNF V} (h : [] ∈ φ) (declared : Finset V) : φ.modelCountOn declared = 0

An empty clause rules out every assignment, regardless of the declared variables.

theorem Cslib.Logic.PL.CNF.modelCountOn_eq_mul_modelCount {V : Type u_1} [DecidableEq V] (φ : CNF V) (declared : Finset V) (hvars : φ.vars.toFinset ⊆ declared) : φ.modelCountOn declared = 2 ^ (declared.card - φ.numVars) * φ.modelCount

If the declared set contains all occurring variables, its unused variables independently contribute two choices each. The containment premise is essential because assignments outside the declared set are extended by false.

theorem Cslib.Logic.PL.CNF.vars_dense_relabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : (relabel (fun (a : V) => List.idxOf a φ.distinctVars) φ).vars.toFinset = Finset.range φ.numVars

Renaming by the duplicate-free variable list uses every index below numVars, without gaps. The original clause and literal order is retained.

theorem Cslib.Logic.PL.CNF.modelCount_dense_relabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : (relabel (fun (a : V) => List.idxOf a φ.distinctVars) φ).modelCount = φ.modelCount

Dense natural relabeling preserves the occurring-variable model count.

theorem Cslib.Logic.PL.CNF.modelCountOn_dense_relabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : (relabel (fun (a : V) => List.idxOf a φ.distinctVars) φ).modelCountOn (Finset.range φ.numVars) = φ.modelCount

Dense natural relabeling gives the original count on exactly numVars declared variables. This includes the empty formula without requiring a total map from V into Fin 0.

def Cslib.Logic.PL.CNF.validDeclaredInput (k N : ℕ) (φ : CNF ℕ) : Bool

Guard checking that every clause of φ has width ≤ k and every variable lies in < N.

theorem Cslib.Logic.PL.CNF.validDeclaredInput_eq_true_iff {k N : ℕ} {φ : CNF ℕ} : validDeclaredInput k N φ = true ↔ (∀ c ∈ φ, List.length c ≤ k) ∧ φ.vars.toFinset ⊆ Finset.range N

def Cslib.Logic.PL.CNF.normalizeDeclaredLeaf {P : Type u_2} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ

Right-shift normalization converting a declared-range count ψ.modelCountOn (Finset.range N) into ψ.modelCount (= h (p, ψ) >>> (NOf p - ψ.distinctVars.length)).

theorem Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_div {P : Type u_2} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : normalizeDeclaredLeaf NOf h x = h x / 2 ^ (NOf x.1 - x.2.numVars)

theorem Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_modelCount {P : Type u_2} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) (hh : h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))) : normalizeDeclaredLeaf NOf h (p, ψ) = ψ.modelCount

When ψ's variables lie in Finset.range (NOf p) and h (p, ψ) equals the declared-range count ψ.modelCountOn (Finset.range (NOf p)), normalizeDeclaredLeaf recovers ψ.modelCount.

theorem Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_le_two_pow_numVars {P : Type u_2} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) (hh : h (p, ψ) ≤ 2 ^ NOf p) : normalizeDeclaredLeaf NOf h (p, ψ) ≤ 2 ^ ψ.numVars

When ψ's variables lie in Finset.range (NOf p) and h (p, ψ) ≤ 2 ^ NOf p, normalizeDeclaredLeaf NOf h (p, ψ) is at most 2 ^ ψ.numVars.