Std.Sat.CNF.Relabel

source

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

Instances For

source

@[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

source

@[simp]

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

relabel id = id

source

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

source

@[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.

source

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

Instances For

source

@[simp]

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

relabel r [] = []

source

@[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

source

@[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

source

@[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

source

@[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

source

@[simp]

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

relabel id x = x

source

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

source

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)

source

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

(relabel r f).Unsat

source

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

Nonempty α ∨ ∃ (n : Nat ), f = List.replicate n []

source

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