def Std.Sat.CNF.Clause.relabel {α : Type u_1} {β : Type u_2} (r : α → β) (c : Clause α) : Clause β

Change the literal type in a Clause from α to β by using r.

Equations

• Std.Sat.CNF.Clause.relabel r c = { atoms := Array.map r c.atoms, polarities := c.polarities, size_polarities := ⋯, isBool_polarities := ⋯ }

@[simp]

theorem Std.Sat.CNF.Clause.polarity_relabel {α : Type u_1} {β : Type u_2} {r : α → β} {c : Clause α} {i : Nat} : (relabel r c).polarity i = c.polarity i

@[simp]

theorem Std.Sat.CNF.Clause.literals_relabel {α : Type u_1} {β : Type u_2} {r : α → β} {c : Clause α} : (relabel r c).literals = List.map (fun (x : Literal α) => match x with | (i, n) => (r i, n)) c.literals

@[simp]

theorem Std.Sat.CNF.Clause.relabel_empty {α : Type u_1} {β : Type u_2} (r : α → β) : relabel r empty = empty

@[simp]

theorem Std.Sat.CNF.Clause.relabel_add {α : Type u_1} {β : Type u_2} {atom : α} {pol : Bool} (r : α → β) (c : Clause α) : relabel r (c.add atom pol) = (relabel r c).add (r atom) pol

@[simp]

theorem Std.Sat.CNF.Clause.eval_relabel {α : Type u_1} {β : Type u_2} {r : α → β} {a : β → Bool} {c : Clause α} : eval a (relabel r c) = eval (a ∘ r) c

@[simp]

theorem Std.Sat.CNF.Clause.relabel_id' {α : Type u_1} : relabel id = id

theorem Std.Sat.CNF.Clause.relabel_congr {α : Type u_1} {β : Type u_2} {c : Clause α} {r1 r2 : α → β} (hw : ∀ (v : α), VarMem v c → r1 v = r2 v) : relabel r1 c = relabel r2 c

@[simp]

theorem Std.Sat.CNF.Clause.relabel_relabel' {α✝ : Type u_1} {α✝¹ : Type u_2} {r1 : α✝ → α✝¹} {α✝² : Type u_3} {r2 : α✝² → α✝} : relabel r1 ∘ relabel r2 = relabel (r1 ∘ r2)

Relabelling

It is convenient to be able to construct a CNF using a more complicated literal type, but eventually we need to embed in Nat.

def Std.Sat.CNF.relabel {α : Type u_1} {β : Type u_2} (r : α → β) (f : CNF α) : CNF β

Change the literal type in a CNF formula from α to β by using r.

Equations

• Std.Sat.CNF.relabel r f = { clauses := Array.map (Std.Sat.CNF.Clause.relabel r) f.clauses }

@[simp]

theorem Std.Sat.CNF.relabel_empty {α : Type u_1} {β : Type u_2} {r : α → β} : relabel r empty = empty

@[simp]

theorem Std.Sat.CNF.relabel_add {α : Type u_1} {β : Type u_2} {f : CNF α} {c : Clause α} {r : α → β} : relabel r (f.add c) = (relabel r f).add (Clause.relabel r c)

@[simp]

theorem Std.Sat.CNF.eval_relabel {α : Type u_1} {β : Type u_2} (r : α → β) (a : β → Bool) (f : CNF α) : eval a (relabel r f) = eval (a ∘ r) f

@[simp]

theorem Std.Sat.CNF.relabel_append {α✝ : Type u_1} {α✝¹ : Type u_2} {r : α✝ → α✝¹} {f1 f2 : CNF α✝} : relabel r (f1 ++ f2) = relabel r f1 ++ relabel r f2

@[simp]

theorem Std.Sat.CNF.relabel_relabel {α✝ : Type u_1} {α✝¹ : Type u_2} {r1 : α✝ → α✝¹} {α✝² : Type u_3} {r2 : α✝² → α✝} {f : CNF α✝²} : relabel r1 (relabel r2 f) = relabel (r1 ∘ r2) f

@[simp]

theorem Std.Sat.CNF.relabel_id {α✝ : Type u_1} {x : CNF α✝} : relabel id x = x

theorem Std.Sat.CNF.relabel_congr {α : Type u_1} {β : Type u_2} {f : CNF α} {r1 r2 : α → β} (hw : ∀ (v : α), VarMem v f → r1 v = r2 v) : relabel r1 f = relabel r2 f

theorem Std.Sat.CNF.sat_relabel {α : Type u_1} {β✝ : Type u_2} {r1 : β✝ → Bool} {r2 : α → β✝} {f : CNF α} (h : Sat (r1 ∘ r2) f) : Sat r1 (relabel r2 f)

theorem Std.Sat.CNF.unsat_relabel {α : Type u_1} {β : Type u_2} {f : CNF α} (r : α → β) (h : f.Unsat) : (relabel r f).Unsat

theorem Std.Sat.CNF.unsat_relabel_iff {α : Type u_1} {β : Type u_2} {f : CNF α} {r : α → β} (hw : ∀ {v1 v2 : α}, VarMem v1 f → VarMem v2 f → r v1 = r v2 → v1 = v2) : (relabel r f).Unsat ↔ f.Unsat