def Std.Sat.CNF.Clause.relabel {α : Type u_1} {β : Type u_2} (r : α → β) (c : Std.Sat.CNF.Clause α) : Std.Sat.CNF.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 : Std.Sat.CNF.Clause α} : Std.Sat.CNF.Clause.eval a (Std.Sat.CNF.Clause.relabel r c) = Std.Sat.CNF.Clause.eval (a ∘ r) c

@[simp]

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

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

@[simp]

theorem Std.Sat.CNF.Clause.relabel_relabel' {α✝ : Type u_1} {α✝¹ : Type u_2} {r1 : α✝ → α✝¹} {α✝² : Type u_3} {r2 : α✝² → α✝} : Std.Sat.CNF.Clause.relabel r1 ∘ Std.Sat.CNF.Clause.relabel r2 = Std.Sat.CNF.Clause.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 : Std.Sat.CNF α) : Std.Sat.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 : α → β} : Std.Sat.CNF.relabel r [] = []

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem Std.Sat.CNF.nonempty_or_impossible {α : Type u_1} (f : Std.Sat.CNF α) : Nonempty α ∨ ∃ (n : Nat), f = List.replicate n []

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