Horn syntax under variable relabeling

Relabeling changes no literal polarities or occurrences, even when different variables become identical. Consequently it preserves and reflects Horn and dual Horn syntax, without an injectivity hypothesis.

Main results

• Cslib.Logic.PL.Clause.isHorn_relabel: Horn clause syntax is invariant under relabeling.
• Cslib.Logic.PL.CNF.isHorn_relabel: Horn formula syntax is invariant under relabeling.
• Cslib.Logic.PL.CNF.isDualHorn_relabel: dual Horn syntax is invariant under relabeling.

theorem Cslib.Logic.PL.Clause.length_filter_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) (b : Bool) : (List.filter (fun (l : Literal W) => l.2 == b) (relabel f c)).length = (List.filter (fun (l : Literal V) => l.2 == b) c).length

Relabeling preserves the number of occurrences of either polarity, including repetitions.

@[simp]

theorem Cslib.Logic.PL.Clause.isHorn_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) : (relabel f c).IsHorn ↔ c.IsHorn

Horn clause syntax is invariant under arbitrary, possibly noninjective relabeling.

@[simp]

theorem Cslib.Logic.PL.CNF.isHorn_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (φ : CNF V) : (relabel f φ).IsHorn ↔ φ.IsHorn

Horn formula syntax is invariant under arbitrary relabeling.

@[simp]

theorem Cslib.Logic.PL.Clause.isDualHorn_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) : (relabel f c).IsDualHorn ↔ c.IsDualHorn

Dual Horn clause syntax is invariant under arbitrary relabeling.

@[simp]

theorem Cslib.Logic.PL.CNF.isDualHorn_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (φ : CNF V) : (relabel f φ).IsDualHorn ↔ φ.IsDualHorn

Dual Horn formula syntax is invariant under arbitrary relabeling.