Disjunctive normal form

Formulas in disjunctive normal form over a type of variables V, dual to the conjunctive normal form of Cslib.Logic.PL.CNF. A term is a list of literals read conjunctively, and a formula is a list of terms read disjunctively. Negating every literal turns a term into a clause and a formula in disjunctive normal form into the negation of a formula in conjunctive normal form (DNF.eval_negate).

Main definitions

• Cslib.Logic.PL.Term, Cslib.Logic.PL.DNF, Cslib.Logic.PL.DNF.eval.
• Cslib.Logic.PL.DNF.negate, Cslib.Logic.PL.CNF.negate: the negation, in the dual normal form.

Main results

• Cslib.Logic.PL.DNF.eval_eq_true_iff, Cslib.Logic.PL.Term.eval_eq_true_iff: the semantics as quantifiers over terms and literals.
• Cslib.Logic.PL.DNF.eval_negate: de Morgan duality.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

@[reducible, inline]

abbrev Cslib.Logic.PL.Term (V : Type u_2) : Type u_2

A term is a conjunction of literals.

@[reducible, inline]

abbrev Cslib.Logic.PL.DNF (V : Type u_2) : Type u_2

A formula in disjunctive normal form is a disjunction of terms.

def Cslib.Logic.PL.Term.eval {V : Type u_1} (σ : V → Bool) (t : Term V) : Bool

A term holds when all of its literals do.

def Cslib.Logic.PL.DNF.eval {V : Type u_1} (σ : V → Bool) (φ : DNF V) : Bool

A formula holds when one of its terms does.

theorem Cslib.Logic.PL.Term.eval_eq_true_iff {V : Type u_1} (σ : V → Bool) (t : Term V) : eval σ t = true ↔ ∀ (l : Literal V), l ∈ t → σ l.fst = l.snd

A term holds when every literal does.

theorem Cslib.Logic.PL.Term.eval_update_of_forall_ne {V : Type u_1} [DecidableEq V] {t : Term V} {i : V} (hi : ∀ (l : Literal V), l ∈ t → l.fst ≠ i) (x : V → Bool) (b : Bool) : eval (Function.update x i b) t = eval x t

Flipping a variable that a term does not mention does not change its value.

@[simp]

theorem Cslib.Logic.PL.Term.eval_nil {V : Type u_1} (σ : V → Bool) : eval σ [] = true

@[simp]

theorem Cslib.Logic.PL.Term.eval_cons {V : Type u_1} (σ : V → Bool) (l : Literal V) (t : Term V) : eval σ (l :: t) = (Literal.eval σ l && eval σ t)

theorem Cslib.Logic.PL.DNF.eval_eq_true_iff {V : Type u_1} (σ : V → Bool) (φ : DNF V) : eval σ φ = true ↔ ∃ (t : Term V), t ∈ φ ∧ Term.eval σ t = true

A formula holds when some term does.

@[simp]

theorem Cslib.Logic.PL.DNF.eval_nil {V : Type u_1} (σ : V → Bool) : eval σ [] = false

@[simp]

theorem Cslib.Logic.PL.DNF.eval_append {V : Type u_1} (σ : V → Bool) (φ ψ : DNF V) : eval σ (φ ++ ψ) = (eval σ φ || eval σ ψ)

@[simp]

theorem Cslib.Logic.PL.DNF.eval_cons {V : Type u_1} (σ : V → Bool) (t : Term V) (φ : DNF V) : eval σ (t :: φ) = (Term.eval σ t || eval σ φ)

def Cslib.Logic.PL.Term.negate {V : Type u_1} (t : Term V) : Clause V

The clause of the negated literals of a term.

@[simp]

theorem Cslib.Logic.PL.Term.eval_negate {V : Type u_1} (σ : V → Bool) (t : Term V) : Clause.eval σ t.negate = !eval σ t

def Cslib.Logic.PL.DNF.negate {V : Type u_1} (φ : DNF V) : CNF V

The formula in conjunctive normal form of the negation of a formula in disjunctive normal form.

@[simp]

theorem Cslib.Logic.PL.DNF.eval_negate {V : Type u_1} (σ : V → Bool) (φ : DNF V) : CNF.eval σ φ.negate = !eval σ φ

De Morgan duality.

def Cslib.Logic.PL.Clause.negate {V : Type u_1} (c : Clause V) : Term V

The term of the negated literals of a clause.

@[simp]

theorem Cslib.Logic.PL.Clause.eval_negate {V : Type u_1} (σ : V → Bool) (c : Clause V) : Term.eval σ c.negate = !eval σ c

@[simp]

theorem Cslib.Logic.PL.Clause.length_negate {V : Type u_1} (c : Clause V) : List.length c.negate = List.length c

theorem Cslib.Logic.PL.Clause.map_fst_negate {V : Type u_1} (c : Clause V) : List.map Prod.fst c.negate = List.map Prod.fst c

def Cslib.Logic.PL.CNF.negate {V : Type u_1} (φ : CNF V) : DNF V

The formula in disjunctive normal form of the negation of a formula in conjunctive normal form.

@[simp]

theorem Cslib.Logic.PL.CNF.eval_negate {V : Type u_1} (σ : V → Bool) (φ : CNF V) : DNF.eval σ φ.negate = !eval σ φ

De Morgan duality, from conjunctive to disjunctive normal form.