Documentation

Std.Sat.CNF.Relabel

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

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

Equations
    Instances For
      @[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
      theorem Std.Sat.CNF.Clause.relabel_congr {α : Type u_1} {β : Type u_2} {c : Clause α} {r1 r2 : αβ} (hw : ∀ (v : α), Mem v cr1 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
        Instances For
          @[simp]
          theorem Std.Sat.CNF.relabel_nil {α : Type u_1} {β : Type u_2} {r : αβ} :
          @[simp]
          theorem Std.Sat.CNF.relabel_cons {α : Type u_1} {β : Type u_2} {c : Clause α} {f : List (Clause α)} {r : αβ} :
          @[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 α✝} :
          theorem Std.Sat.CNF.relabel_congr {α : Type u_1} {β : Type u_2} {f : CNF α} {r1 r2 : αβ} (hw : ∀ (v : α), Mem v fr1 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) :
          theorem Std.Sat.CNF.unsat_relabel_iff {α : Type u_1} {β : Type u_2} {f : CNF α} {r : αβ} (hw : ∀ {v1 v2 : α}, Mem v1 fMem v2 fr v1 = r v2v1 = v2) :