Exact three-literal clauses with distinct variables

Clause.IsExactThreeDistinct and CNF.IsExactThreeDistinct require exactly three pairwise distinct variables per clause. Literal polarities are unrestricted.

Main results

• Clause.isExactThreeDistinct_iff: the explicit three-literal characterization.

def Cslib.Logic.PL.Clause.IsExactThreeDistinct {V : Type u_1} (c : Clause V) : Prop

A clause has three distinct variables when it has length 3 and its variables have no duplicates.

def Cslib.Logic.PL.CNF.IsExactThreeDistinct {V : Type u_1} (φ : CNF V) : Prop

A formula is an exact 3-CNF with distinct variables per clause when every clause has three distinct variables.

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableIsExactThreeDistinctOfDecidableEq {V : Type u_1} [DecidableEq V] {c : Clause V} : Decidable c.IsExactThreeDistinct

Whether a clause has three distinct variables is decidable.

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableIsExactThreeDistinctOfDecidableEq_1 {V : Type u_1} [DecidableEq V] {φ : CNF V} : Decidable φ.IsExactThreeDistinct

Whether every clause of a CNF formula has three distinct variables is decidable.

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.length_eq {V : Type u_1} {c : Clause V} (hc : c.IsExactThreeDistinct) : List.length c = 3

An exact 3-clause with distinct variables has length 3.

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.nodup_map_fst {V : Type u_1} {c : Clause V} (hc : c.IsExactThreeDistinct) : (List.map Prod.fst c).Nodup

The variables of an exact 3-clause with distinct variables have no duplicates.

theorem Cslib.Logic.PL.Clause.isExactThreeDistinct_iff {V : Type u_1} {c : Clause V} : c.IsExactThreeDistinct ↔ ∃ (l₁ : Literal V), ∃ (l₂ : Literal V), ∃ (l₃ : Literal V), c = [l₁, l₂, l₃] ∧ l₁.fst ≠ l₂.fst ∧ l₁.fst ≠ l₃.fst ∧ l₂.fst ≠ l₃.fst

Every exact 3-clause with distinct variables is a list of three literals on pairwise distinct variables.