cnf_single_clause_satisfiable_iff

theoremverified

A CNF formula consisting of a single clause `c`, namely `[c]`, is satisfiable (`CnfSatisfiable [c]`) if and only if the clause `c` is non-empty (`c ≠ []`).

Statement

theorem cnf_single_clause_satisfiable_iff {V : Type*} (c : List (CnfLit V)) :
    CnfSatisfiable [c] ↔ c ≠ []

Source

folklore

Verified

07 Sep 2026

Axioms

propext

Built on 2

CnfSatisfiableA CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains…
CnfLitA CNF literal over a variable type V is either a positive variable or a negated variable.

Read back from the Lean

For any type V and any list c of literals over V, the single-clause CNF formula [c] is satisfiable if and only if c is non-empty (c ≠ []).

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- A single-clause CNF formula [c] is satisfiable if and only if the clause c is non-empty. -/
theorem cnf_single_clause_satisfiable_iff {V : Type*} (c : List (CnfLit V)) :
    CnfSatisfiable [c] ↔ c ≠ [] := by
  constructor
  · rintro ⟨τ, hτ⟩ rfl
    obtain ⟨l, hl, -⟩ := hτ [] (List.Mem.head _)
    cases hl
  · intro hc
    cases c with
    | nil => contradiction
    | cons l ls =>
      cases l with
      | pos v =>
        use (fun _ => true)
        intro c' hc'
        obtain rfl := List.mem_singleton.mp hc'
        exact ⟨CnfLit.pos v, List.Mem.head _, rfl⟩
      | neg v =>
        use (fun _ => false)
        intro c' hc'
        obtain rfl := List.mem_singleton.mp hc'
        exact ⟨CnfLit.neg v, List.Mem.head _, rfl⟩

Discuss this result Challenge it