Documentation

Std.Sat.CNF.Basic

@[reducible, inline]

abbrev Std.Sat.CNF.Clause (α : Type u) :

A clause in a CNF.

The literal (i, b) is satisfied if the assignment to i agrees with b.

Equations

Std.Sat.CNF.Clause α = List (Std.Sat.Literal α)

Instances For

@[reducible, inline]

abbrev Std.Sat.CNF (α : Type u) :

A CNF formula.

Literals are identified by members of α.

Equations

Std.Sat.CNF α = List (Std.Sat.CNF.Clause α)

Instances For

def Std.Sat.CNF.Clause.eval {α : Type u_1} (a : α → Bool) (c : Std.Sat.CNF.Clause α) :

Evaluating a Clause with respect to an assignment a.

Equations

Std.Sat.CNF.Clause.eval a c = List.any c fun (x : Std.Sat.Literal α) => match x with | (i, n) => a i == n

Instances For

@[simp]

theorem Std.Sat.CNF.Clause.eval_nil {α : Type u_1} (a : α → Bool) :

Std.Sat.CNF.Clause.eval a [] = false

@[simp]

theorem Std.Sat.CNF.Clause.eval_cons {α : Type u_1} {i : Std.Sat.Literal α} {c : List (Std.Sat.Literal α)} (a : α → Bool) :

Std.Sat.CNF.Clause.eval a (i :: c) = (a i.fst == i.snd || Std.Sat.CNF.Clause.eval a c)

def Std.Sat.CNF.eval {α : Type u_1} (a : α → Bool) (f : Std.Sat.CNF α) :

Evaluating a CNF formula with respect to an assignment a.

Equations

Std.Sat.CNF.eval a f = List.all f fun (c : Std.Sat.CNF.Clause α) => Std.Sat.CNF.Clause.eval a c

Instances For

@[simp]

theorem Std.Sat.CNF.eval_nil {α : Type u_1} (a : α → Bool) :

Std.Sat.CNF.eval a [] = true

@[simp]

theorem Std.Sat.CNF.eval_cons {α : Type u_1} {c : Std.Sat.CNF.Clause α} {f : List (Std.Sat.CNF.Clause α)} (a : α → Bool) :

Std.Sat.CNF.eval a (c :: f) = (Std.Sat.CNF.Clause.eval a c && Std.Sat.CNF.eval a f)

@[simp]

theorem Std.Sat.CNF.eval_append {α : Type u_1} (a : α → Bool) (f1 : Std.Sat.CNF α) (f2 : Std.Sat.CNF α) :

Std.Sat.CNF.eval a (f1 ++ f2) = (Std.Sat.CNF.eval a f1 && Std.Sat.CNF.eval a f2)

def Std.Sat.CNF.Sat {α : Type u_1} (a : α → Bool) (f : Std.Sat.CNF α) :

Equations

Std.Sat.CNF.Sat a f = (Std.Sat.CNF.eval a f = true)

Instances For

def Std.Sat.CNF.Unsat {α : Type u_1} (f : Std.Sat.CNF α) :

Equations

f.Unsat = ∀ (a : α → Bool), Std.Sat.CNF.eval a f = false

Instances For

theorem Std.Sat.CNF.sat_def {α : Type u_1} (a : α → Bool) (f : Std.Sat.CNF α) :

Std.Sat.CNF.Sat a f ↔ Std.Sat.CNF.eval a f = true

theorem Std.Sat.CNF.unsat_def {α : Type u_1} (f : Std.Sat.CNF α) :

f.Unsat ↔ ∀ (a : α → Bool), Std.Sat.CNF.eval a f = false

@[simp]

theorem Std.Sat.CNF.not_unsat_nil {α : Type u_1} :

¬Std.Sat.CNF.Unsat []

@[simp]

theorem Std.Sat.CNF.sat_nil {α : Type u_1} {assign : α → Bool} :

Std.Sat.CNF.Sat assign []

@[simp]

theorem Std.Sat.CNF.unsat_nil_cons {α : Type u_1} {g : Std.Sat.CNF α} :

Std.Sat.CNF.Unsat ([] :: g)

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

Variable v occurs in Clause c.

Equations

Std.Sat.CNF.Clause.Mem v c = ((v, false) ∈ c ∨ (v, true) ∈ c)

Instances For

instance Std.Sat.CNF.Clause.instDecidableMemOfDecidableEq {α : Type u_1} {v : α} {c : Std.Sat.CNF.Clause α} [DecidableEq α] :

Decidable (Std.Sat.CNF.Clause.Mem v c)

Equations

Std.Sat.CNF.Clause.instDecidableMemOfDecidableEq = inferInstanceAs (Decidable ((v, false) ∈ c ∨ (v, true) ∈ c))

@[simp]

theorem Std.Sat.CNF.Clause.not_mem_nil {α : Type u_1} {v : α} :

¬Std.Sat.CNF.Clause.Mem v []

@[simp]

theorem Std.Sat.CNF.Clause.mem_cons {α : Type u_1} {l : Std.Sat.Literal α} {c : List (Std.Sat.Literal α)} {v : α} :

Std.Sat.CNF.Clause.Mem v (l :: c) ↔ v = l.fst ∨ Std.Sat.CNF.Clause.Mem v c

theorem Std.Sat.CNF.Clause.mem_of :

∀ {α : Type u_1} {c : Std.Sat.CNF.Clause α} {v : α} {p : Bool}, (v, p) ∈ c → Std.Sat.CNF.Clause.Mem v c

theorem Std.Sat.CNF.Clause.eval_congr {α : Type u_1} (a1 : α → Bool) (a2 : α → Bool) (c : Std.Sat.CNF.Clause α) (hw : ∀ (i : α), Std.Sat.CNF.Clause.Mem i c → a1 i = a2 i) :

Std.Sat.CNF.Clause.eval a1 c = Std.Sat.CNF.Clause.eval a2 c

def Std.Sat.CNF.Mem {α : Type u_1} (v : α) (f : Std.Sat.CNF α) :

Variable v occurs in CNF formula f.

Equations

Std.Sat.CNF.Mem v f = ∃ (c : Std.Sat.CNF.Clause α), c ∈ f ∧ Std.Sat.CNF.Clause.Mem v c

Instances For

instance Std.Sat.CNF.instDecidableMemOfDecidableEq {α : Type u_1} {v : α} {f : Std.Sat.CNF α} [DecidableEq α] :

Decidable (Std.Sat.CNF.Mem v f)

Equations

Std.Sat.CNF.instDecidableMemOfDecidableEq = inferInstanceAs (Decidable (∃ (x : Std.Sat.CNF.Clause α), x ∈ f ∧ Std.Sat.CNF.Clause.Mem v x))

theorem Std.Sat.CNF.any_not_isEmpty_iff_exists_mem {α : Type u_1} {f : Std.Sat.CNF α} :

(List.any f fun (c : Std.Sat.CNF.Clause α) => !List.isEmpty c) = true ↔ ∃ (v : α), Std.Sat.CNF.Mem v f

theorem Std.Sat.CNF.not_exists_mem :

∀ {α : Type u_1} {f : Std.Sat.CNF α}, (¬∃ (v : α), Std.Sat.CNF.Mem v f) ↔ ∃ (n : Nat), f = List.replicate n []

instance Std.Sat.CNF.instDecidableExistsMemOfDecidableEq {α : Type u_1} {f : Std.Sat.CNF α} [DecidableEq α] :

Decidable (∃ (v : α), Std.Sat.CNF.Mem v f)

Equations

Std.Sat.CNF.instDecidableExistsMemOfDecidableEq = decidable_of_iff ((List.any f fun (c : Std.Sat.CNF.Clause α) => !List.isEmpty c) = true) ⋯

theorem Std.Sat.CNF.not_mem_nil {α : Type u_1} {v : α} :

¬Std.Sat.CNF.Mem v []

theorem Std.Sat.CNF.mem_cons {α : Type u_1} {v : α} {c : Std.Sat.CNF.Clause α} {f : Std.Sat.CNF α} :

Std.Sat.CNF.Mem v (c :: f) ↔ Std.Sat.CNF.Clause.Mem v c ∨ Std.Sat.CNF.Mem v f

theorem Std.Sat.CNF.mem_of :

∀ {α : Type u_1} {f : Std.Sat.CNF α} {c : Std.Sat.CNF.Clause α} {v : α}, c ∈ f → Std.Sat.CNF.Clause.Mem v c → Std.Sat.CNF.Mem v f

@[simp]

theorem Std.Sat.CNF.mem_append {α : Type u_1} {v : α} {f1 : Std.Sat.CNF α} {f2 : Std.Sat.CNF α} :

Std.Sat.CNF.Mem v (f1 ++ f2) ↔ Std.Sat.CNF.Mem v f1 ∨ Std.Sat.CNF.Mem v f2

theorem Std.Sat.CNF.eval_congr {α : Type u_1} (a1 : α → Bool) (a2 : α → Bool) (f : Std.Sat.CNF α) (hw : ∀ (v : α), Std.Sat.CNF.Mem v f → a1 v = a2 v) :

Std.Sat.CNF.eval a1 f = Std.Sat.CNF.eval a2 f