def Std.Sat.CNF.IsNegationOf {α : Type u_1} (f : CNF α) (c : Clause α) : Prop

Equations

• f.IsNegationOf c = ∀ (a : α → Bool), Std.Sat.CNF.Sat a f ↔ ¬Std.Sat.CNF.Clause.Sat a c

theorem Std.Sat.CNF.isNegationOf_def {α✝ : Type u_1} {f : CNF α✝} {c : Clause α✝} : f.IsNegationOf c ↔ ∀ (a : α✝ → Bool), Sat a f ↔ ¬Clause.Sat a c

theorem Std.Sat.CNF.forall_mem_eq_not_of_isNegationOf_of_sat {α✝ : Type u_1} {f : CNF α✝} {c : Clause α✝} {a : α✝ → Bool} (h1 : f.IsNegationOf c) (h2 : Sat a f) (lit : Literal α✝) : lit ∈ c → a lit.fst = !lit.snd

def Std.Sat.CNF.Clause.negate {α : Type u_1} (c : Clause α) : CNF α

The negation of c as a CNF: one unit clause per literal of c, with the polarity flipped.

Equations

• c.negate = { clauses := c.atoms.mapFinIdx fun (i : Nat) (atom : α) (x : i < c.atoms.size) => Std.Sat.CNF.Clause.unit atom !c.polarity i }

@[simp]

theorem Std.Sat.CNF.Clause.negate_append {α✝ : Type u_1} {c1 c2 : Clause α✝} : (c1 ++ c2).negate = c1.negate ++ c2.negate

@[simp]

theorem Std.Sat.CNF.Clause.mem_negate_iff {α : Type u_1} {c c' : Clause α} : c' ∈ c.negate ↔ ∃ (lit : Literal α), lit ∈ c ∧ c' = unit lit.fst !lit.snd

theorem Std.Sat.CNF.isNegationOf_negate {α : Type u_1} (c : Clause α) : c.negate.IsNegationOf c

theorem Std.Sat.CNF.Clause.sat_negate_iff_sat_of_isNegationOf {α : Type u_1} {c : Clause α} (f : CNF α) (h : f.IsNegationOf c) (a : α → Bool) : CNF.Sat a c.negate ↔ CNF.Sat a f

theorem Std.Sat.CNF.exists_isNegationOf {α : Type u_1} (c : Clause α) : ∃ (f : CNF α), f.IsNegationOf c

theorem Std.Sat.CNF.isNegationOf_append_append_of_isNegationOf {α✝ : Type u_1} {f1 : CNF α✝} {c1 : Clause α✝} {f2 : CNF α✝} {c2 : Clause α✝} (h1 : f1.IsNegationOf c1) (h2 : f2.IsNegationOf c2) : (f1 ++ f2).IsNegationOf (c1 ++ c2)

theorem Std.Sat.CNF.isNegationOf_of_isNegationOf_of_biEntails {α✝ : Type u_1} {f1 : CNF α✝} {c : Clause α✝} {f2 : CNF α✝} (h1 : f1.IsNegationOf c) (h2 : f1.BiEntails f2) : f2.IsNegationOf c

theorem Std.Sat.CNF.isNegationOf_append_comm_left {α✝ : Type u_1} {f1 f2 : CNF α✝} {c : Clause α✝} : (f1 ++ f2).IsNegationOf c ↔ (f2 ++ f1).IsNegationOf c

theorem Std.Sat.CNF.isNegationOf_append_comm_right {α✝ : Type u_1} {f : CNF α✝} {c1 c2 : Clause α✝} : f.IsNegationOf (c1 ++ c2) ↔ f.IsNegationOf (c2 ++ c1)