Evaluating a clause

Two basic facts about Cslib.Logic.PL.Clause.eval, complementing Cslib.Logic.PL.Clause.eval_eq_true_iff: a clause is false exactly when every literal is read against its polarity, and its value depends only on the values of its variables. They live in this leaf module rather than in CslibFrontier.Logics.Propositional.CNF, which is widely imported.

Main results

• Cslib.Logic.PL.Clause.eval_eq_false_iff: a clause is false iff each of its literals is false.
• Cslib.Logic.PL.Clause.eval_congr: a clause depends only on the values of its variables.

theorem Cslib.Logic.PL.Clause.eval_eq_false_iff {V : Type u_1} (σ : V → Bool) (c : Clause V) : eval σ c = false ↔ ∀ (l : Literal V), l ∈ c → σ l.fst = !l.snd

A clause is false exactly when each of its literals is read against its polarity.

theorem Cslib.Logic.PL.Clause.eval_congr {V : Type u_1} {σ τ : V → Bool} {c : Clause V} (h : ∀ (l : Literal V), l ∈ c → σ l.fst = τ l.fst) : eval σ c = eval τ c

A clause only depends on the values of its variables.

theorem Cslib.Logic.PL.CNF.countP_eval_congr {V : Type u_1} {σ τ : V → Bool} {φ : CNF V} (h : ∀ (v : V), v ∈ φ.vars → σ v = τ v) : List.countP (Clause.eval σ) φ = List.countP (Clause.eval τ) φ

The number of satisfied clauses in a CNF depends only on the values of its variables.