HepLean Documentation

Std.Sat.CNF.Relabel

source
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
Instances For
    source
    @[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
    source
    @[simp]
    theorem Std.Sat.CNF.Clause.relabel_id' {α : Type u_1} :
    Std.Sat.CNF.Clause.relabel id = id
    source
    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
    source
    @[simp]
    theorem Std.Sat.CNF.Clause.relabel_relabel' :
    ∀ {α : Type u_1} {α_1 : Type u_2} {r1 : α → α_1} {α_2 : Type u_3} {r2 : α_2 → α}, 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.

    source
    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
    Instances For
      source
      @[simp]
      theorem Std.Sat.CNF.relabel_nil {α : Type u_1} {β : Type u_2} {r : α → β} :
      Std.Sat.CNF.relabel r [] = []
      source
      @[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
      source
      @[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
      source
      @[simp]
      theorem Std.Sat.CNF.relabel_append :
      ∀ {α : Type u_1} {α_1 : Type u_2} {r : α → α_1} {f1 f2 : Std.Sat.CNF α}, Std.Sat.CNF.relabel r (f1 ++ f2) = Std.Sat.CNF.relabel r f1 ++ Std.Sat.CNF.relabel r f2
      source
      @[simp]
      theorem Std.Sat.CNF.relabel_relabel :
      ∀ {α : Type u_1} {α_1 : Type u_2} {r1 : α → α_1} {α_2 : Type u_3} {r2 : α_2 → α} {f : Std.Sat.CNF α_2}, Std.Sat.CNF.relabel r1 (Std.Sat.CNF.relabel r2 f) = Std.Sat.CNF.relabel (r1 ∘ r2) f
      source
      @[simp]
      theorem Std.Sat.CNF.relabel_id :
      ∀ {α : Type u_1} {x : Std.Sat.CNF α}, Std.Sat.CNF.relabel id x = x
      source
      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
      source
      theorem Std.Sat.CNF.sat_relabel {α : Type u_1} :
      ∀ {β : Type u_2} {r1 : β → Bool} {r2 : α → β} {f : Std.Sat.CNF α}, Std.Sat.CNF.Sat (r1 ∘ r2) f → Std.Sat.CNF.Sat r1 (Std.Sat.CNF.relabel r2 f)
      source
      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
      source
      theorem Std.Sat.CNF.nonempty_or_impossible {α : Type u_1} (f : Std.Sat.CNF α) :
      Nonempty α ∨ ∃ (n : Nat), f = List.replicate n []
      source
      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