def
Std.Sat.CNF.Clause.relabel
{α : Type u_1}
{β : Type u_2}
(r : α → β)
(c : 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_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)
:
@[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.
Change the literal type in a CNF formula from α to β by using r.
Equations
@[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} {α_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
@[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
@[simp]
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 α},
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