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 = List.map (fun (x : Std.Sat.Literal α) => match x with | (i, n) => (r i, n)) c

@[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 : α), Mem 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 = List.map (Std.Sat.CNF.Clause.relabel r) f

@[simp]

theorem Std.Sat.CNF.relabel_nil {α : Type u_1} {β : Type u_2} {r : α → β} : relabel r [] = []

@[simp]

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

@[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 : α), Mem 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.nonempty_or_impossible {α : Type u_1} (f : CNF α) : Nonempty α ∨ ∃ (n : Nat), f = List.replicate n []

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