First-occurrence order under injective CNF relabeling

Compaction assigns the position of a variable's first literal occurrence. The list of distinct variables keeps its order under this renaming, even though compact names may have gaps.

Main results

• Cslib.Logic.PL.CNF.distinctVars_relabel_of_injOn, Cslib.Logic.PL.CNF.numVars_relabel_of_injOn, Cslib.Logic.PL.CNF.numVars_relabel: injective variable relabelings preserve distinctVars order and numVars.
• Cslib.Logic.PL.CNF.count_vars_relabel_of_injOn, Cslib.Logic.PL.CNF.count_vars_relabel_le_of_injOn: they also preserve literal-occurrence counts and any uniform bound on them.
• Cslib.Logic.PL.CNF.distinctVars_compact: exact ordered list of compact variable names.
• Cslib.Logic.PL.CNF.idxOf_distinctVars_compact: graph vertex indices are preserved.

References

These are elementary list identities for the existing CNF compaction operation.

theorem Cslib.Logic.PL.CNF.distinctVars_relabel_of_injOn {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] (φ : CNF V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ φ.vars}) : (relabel f φ).distinctVars = List.map f φ.distinctVars

Relabeling injectively on the used variables preserves their first-occurrence order.

theorem Cslib.Logic.PL.CNF.numVars_relabel_of_injOn {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] (φ : CNF V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ φ.vars}) : (relabel f φ).numVars = φ.numVars

Relabeling injectively on the occurring variables preserves numVars.

@[simp]

theorem Cslib.Logic.PL.CNF.numVars_relabel {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {f : V → W} (hf : Function.Injective f) (φ : CNF V) : (relabel f φ).numVars = φ.numVars

Relabeling along an injective map preserves numVars.

theorem Cslib.Logic.PL.CNF.count_vars_relabel_of_injOn {V : Type u_1} {W : Type u_2} [DecidableEq W] [BEq V] [LawfulBEq V] (φ : CNF V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ φ.vars}) {v : V} (hv : v ∈ φ.vars) : List.count (f v) (relabel f φ).vars = List.count v φ.vars

Relabeling injectively on the occurring variables preserves the literal-occurrence count of every occurring variable.

theorem Cslib.Logic.PL.CNF.count_vars_relabel_le_of_injOn {V : Type u_1} {W : Type u_2} [DecidableEq W] [BEq V] [LawfulBEq V] (φ : CNF V) (f : V → W) (hf : Set.InjOn f {v : V | v ∈ φ.vars}) {B : ℕ} (h : ∀ (v : V), List.count v φ.vars ≤ B) (i : W) : List.count i (relabel f φ).vars ≤ B

Relabeling injectively on the occurring variables preserves any uniform bound on literal-occurrence counts.

theorem Cslib.Logic.PL.CNF.distinctVars_compact {V : Type u_1} [DecidableEq V] [BEq V] [LawfulBEq V] (φ : CNF V) : φ.compact.distinctVars = List.map (fun (a : V) => List.idxOf a φ.vars) φ.distinctVars

Compaction preserves the exact order of the distinct variables. Any lawful Boolean equality on the original variable type gives the same first-occurrence names.

theorem Cslib.Logic.PL.CNF.idxOf_distinctVars_compact {V : Type u_1} [DecidableEq V] [BEq V] [LawfulBEq V] (φ : CNF V) {v : V} (hv : v ∈ φ.vars) : List.idxOf (List.idxOf v φ.vars) φ.compact.distinctVars = List.idxOf v φ.distinctVars

The index of a used variable in the distinct-variable list is unchanged by compaction.

theorem Cslib.Logic.PL.CNF.getD_idxOf_distinctVars_compact {V : Type u_1} [DecidableEq V] [BEq V] [LawfulBEq V] {P : Type u_3} (φ : CNF V) (data : List P) (fallback : P) {v : V} (hv : v ∈ φ.vars) : data.getD (List.idxOf (List.idxOf v φ.vars) φ.compact.distinctVars) fallback = data.getD (List.idxOf v φ.distinctVars) fallback

Drawing data indexed by the distinct-variable list retain the same lookup after compaction.

theorem Cslib.Logic.PL.CNF.vars_compact {V : Type u_1} [DecidableEq V] [BEq V] [LawfulBEq V] (φ : CNF V) : φ.compact.vars = List.map (fun (a : V) => List.idxOf a φ.vars) φ.vars

Compaction relabels the full variable-occurrence list in its original order.

theorem Cslib.Logic.PL.CNF.count_vars_compact {V : Type u_1} [DecidableEq V] [BEq V] [LawfulBEq V] (φ : CNF V) {v : V} (hv : v ∈ φ.vars) : List.count (List.idxOf v φ.vars) φ.compact.vars = List.count v φ.vars

Every used variable keeps its exact literal-occurrence count after compaction.

theorem Cslib.Logic.PL.CNF.count_vars_compact_le {V : Type u_1} [DecidableEq V] [BEq V] [LawfulBEq V] (φ : CNF V) {k : ℕ} (h : ∀ (v : V), List.count v φ.vars ≤ k) (i : ℕ) : List.count i φ.compact.vars ≤ k

A bound on all original literal-occurrence counts also bounds every compact variable.

theorem Cslib.Logic.PL.occurrences_relabel {V : Type u_1} {W : Type u_2} (φ : CNF V) (f : V → W) : occurrences (CNF.relabel f φ) = List.map (fun (o : Occurrence V) => (o.1, o.2.1, f o.2.2.1, o.2.2.2)) (occurrences φ)

Relabeling preserves literal-occurrence order and both occurrence indices.