feat: use HSat in CNF

LeanSAT/AIG/CNF.lean

@@ -387,7 +387,7 @@ The key invariant about the `State` itself (without cache): The CNF we produce i
 at `cnfSatAssignment`.
 -/
 def State.Inv (cnf : CNF (CNFVar aig)) : Prop :=
-  ∀ (assign1 : Nat → Bool), cnf.sat (cnfSatAssignment aig assign1)
+  ∀ (assign1 : Nat → Bool), (cnfSatAssignment aig assign1) ⊨ cnf
 
 /--
 The `State` invariant always holds when we have an empty CNF.
@@ -403,7 +403,7 @@ theorem State.Inv_append (h1 : State.Inv cnf1) (h2 : State.Inv cnf2) :
   intro assign1
   specialize h1 assign1
   specialize h2 assign1
-  simp [CNF.sat] at h1 h2 ⊢
+  simp [(· ⊨ ·)] at h1 h2 ⊢
   constructor <;> assumption
 
 /--
@@ -412,15 +412,15 @@ theorem State.Inv_append (h1 : State.Inv cnf1) (h2 : State.Inv cnf2) :
 theorem State.Inv_constToCNF (heq : aig.decls[upper] = .const b)
     : State.Inv (aig := aig) (Decl.constToCNF (.inr ⟨upper, h⟩) b) := by
   intro assign1
-  simp [CNF.sat, denote_idx_const heq]
+  simp [(· ⊨ ·), denote_idx_const heq]
 
 /--
 `State.Inv` holds for the CNF that we produce for a `Decl.atom`
 -/
 theorem State.Inv_atomToCNF (heq : aig.decls[upper] = .atom a)
     : State.Inv (aig := aig) (Decl.atomToCNF (.inr ⟨upper, h⟩) (.inl a)) := by
   intro assign1
-  simp [CNF.sat, denote_idx_atom heq]
+  simp [(· ⊨ ·), denote_idx_atom heq]
 
 /--
 `State.Inv` holds for the CNF that we produce for a `Decl.gate`
@@ -436,7 +436,7 @@ theorem State.Inv_gateToCNF {aig : AIG Nat} {h} (heq : aig.decls[upper]'h = .gat
           rinv)
     := by
   intro assign1
-  simp [CNF.sat, denote_idx_gate heq]
+  simp [(· ⊨ ·), denote_idx_gate heq]
 
 /--
 The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.
@@ -545,23 +545,23 @@ def State.eval (state : State aig) (assign : CNFVar aig → Bool) : Bool :=
 /--
 The CNF within the state is sat.
 -/
-def State.sat (state : State aig) (assign : CNFVar aig → Bool) : Prop :=
-  state.cnf.sat assign
+def State.sat (assign : CNFVar aig → Bool) (state : State aig) : Prop :=
+  assign ⊨ state.cnf
 
-/--
-The CNF within the state is unsat.
--/
-def State.unsat (state : State aig) : Prop :=
-  state.cnf.unsat
+instance : HSat (CNFVar aig) (State aig) where
+  eval := State.sat
 
 @[simp]
 theorem State.eval_eq : State.eval state assign = state.cnf.eval assign := by simp [State.eval]
 
-@[simp]
-theorem State.sat_eq : State.sat state assign = state.cnf.sat assign := by simp [State.sat]
+theorem State.liff (state : State aig)
+    : Sat.liff (CNFVar aig) state state.cnf := by
+  simp [Sat.liff, (· ⊨ ·), sat]
 
-@[simp]
-theorem State.unsat_eq : State.unsat state = state.cnf.unsat := by simp [State.unsat]
+theorem State.equisat (state : State aig)
+    : Sat.equisat (CNFVar aig) state state.cnf := by
+  apply Sat.liff_unsat
+  apply State.liff
 
 end toCNF
 
@@ -647,9 +647,10 @@ theorem toCNF.go_marked :
 The CNF returned by `go` will always be SAT at `cnfSatAssignment`.
 -/
 theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool)
-    (state : toCNF.State aig) :
-    (go aig start h1 state).val.sat (cnfSatAssignment aig assign1) := by
+    (state : toCNF.State aig)
+    : (cnfSatAssignment aig assign1) ⊨ (go aig start h1 state).val := by
   have := (go aig start h1 state).val.inv assign1
+  rw [State.liff]
   simp [this]
 
 /--
@@ -661,17 +662,18 @@ theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) :
     (⟦aig, ⟨start, h1⟩, assign1⟧ = sat?) := by
   intro h
   have := go_sat aig start h1 assign1 (.empty aig)
-  simp [CNF.sat] at this
+  simp [(· ⊨ ·), State.sat] at this
   simpa [this] using h
 
 /--
 Connect SAT results about the AIG to SAT results about the CNF.
 -/
-theorem toCNF.denote_as_go :
+theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool}:
     (⟦aig, ⟨start, h1⟩, projectLeftAssign assign⟧ = false)
       →
-    (CNF.eval assign ([(.inr ⟨start, h1⟩, true)] :: (go aig start h1 (.empty aig)).val.cnf) = false) := by
+    (assign ⊭ ([(.inr ⟨start, h1⟩, true)] :: (go aig start h1 (.empty aig)).val.cnf)) := by
   intro h
+  simp only [(· ⊨ ·)]
   match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with
   | true =>
     have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
@@ -684,14 +686,14 @@ theorem toCNF.denote_as_go :
 /--
 An AIG is unsat iff its CNF is unsat.
 -/
-theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).unsat ↔ entry.unsat := by
+theorem toCNF_equisat (entry : Entrypoint Nat) : unsatisfiable Nat (toCNF entry) ↔ entry.unsat := by
   dsimp [toCNF]
   rw [CNF.unsat_relabel_iff]
   . constructor
     . intro h assign1
       apply toCNF.go_as_denote
       specialize h (toCNF.cnfSatAssignment entry.aig assign1)
-      simpa using h
+      simpa [(· ⊨ ·)] using h
     . intro h assign
       apply toCNF.denote_as_go
       specialize h (toCNF.projectLeftAssign assign)

LeanSAT/CNF/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import LeanSAT.CNF.ForStd
+import LeanSAT.Sat
 
 -- Lemmas from Mathlib, to move to Lean:
 @[simp] theorem exists_or_eq_left (y : α) (p : α → Prop) : ∃ x : α, x = y ∨ p x := ⟨y, .inl rfl⟩
@@ -22,7 +23,7 @@ A clause in a CNF.
 
 The literal `(i, b)` is satisfied is the assignment to `i` agrees with `b`.
 -/
-abbrev CNF.Clause (α : Type) : Type := List (α × Bool)
+abbrev CNF.Clause (α : Type) : Type := List (Literal α)
 
 abbrev CNF (α : Type) : Type := List (CNF.Clause α)
 
@@ -42,17 +43,20 @@ def eval (f : α → Bool) (g : CNF α) : Bool := g.all fun c => c.eval f
 @[simp] theorem eval_append (f : α → Bool) (g h : CNF α) :
     eval f (g ++ h) = (eval f g && eval f h) := List.all_append
 
-def sat (g : CNF α) (f : α → Bool) : Prop := eval f g = true
-def unsat (g : CNF α) : Prop := ∀ f, eval f g = false
+instance : HSat α (Clause α) where
+  eval assign clause := Clause.eval assign clause
 
-@[simp] theorem unsat_nil_iff_false : unsat ([] : CNF α) ↔ False :=
-  ⟨fun h => by simp [unsat] at h, by simp⟩
+instance : HSat α (CNF α) where
+  eval assign cnf := eval assign cnf
 
-@[simp] theorem sat_nil : sat ([] : CNF α) assign ↔ True := by
-  simp [sat]
+@[simp] theorem unsat_nil_iff_false : unsatisfiable α ([] : CNF α) ↔ False :=
+  ⟨fun h => by simp [unsatisfiable, (· ⊨ ·)] at h, by simp⟩
 
-@[simp] theorem unsat_nil_cons : unsat ([] :: g) ↔ True := by
-  simp [unsat]
+@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by
+  simp [(· ⊨ ·)]
+
+@[simp] theorem unsat_nil_cons {g : CNF α} : unsatisfiable α ([] :: g) ↔ True := by
+  simp [unsatisfiable, (· ⊨ ·)]
 
 namespace Clause
 

LeanSAT/CNF/Relabel.lean

@@ -64,11 +64,11 @@ theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, mem a x → f a
   intro a m
   exact w _ (mem_of h m)
 
-theorem sat_relabel (h : sat x (g ∘ f)) : sat (relabel f x) g := by
-  simp_all [sat]
+theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by
+  simp_all [(· ⊨ ·)]
 
-theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsat x) : unsat (relabel f x) := by
-  simp_all [unsat]
+theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsatisfiable α x) : unsatisfiable β (relabel f x) := by
+  simp_all [unsatisfiable, (· ⊨ ·)]
 
 theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by
   induction x with
@@ -84,7 +84,7 @@ theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.re
 
 theorem unsat_relabel_iff {x : CNF α} {f : α → β}
     (w : ∀ {a b}, mem a x → mem b x → f a = f b → a = b) :
-    unsat (relabel f x) ↔ unsat x := by
+    unsatisfiable β (relabel f x) ↔ unsatisfiable α x := by
   rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)
   · refine ⟨fun h => ?_, unsat_relabel f⟩
     have em := Classical.propDecidable
@@ -102,6 +102,6 @@ theorem unsat_relabel_iff {x : CNF α} {f : α → β}
       · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1
     rw [relabel_relabel, relabel_congr, relabel_id]
     exact this
-  · cases n <;> simp [unsat, relabel, Clause.relabel, List.replicate_succ]
+  · cases n <;> simp [unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ]
 
 end CNF

LeanSAT/CNF/RelabelFin.lean

@@ -106,7 +106,8 @@ def relabelFin (g : CNF Nat) : CNF (Fin g.numLiterals) :=
   else
     List.replicate g.length []
 
-theorem unsat_relabelFin : unsat g.relabelFin ↔ unsat g := by
+theorem unsat_relabelFin {g : CNF Nat} :
+    unsatisfiable (Fin g.numLiterals) g.relabelFin ↔ unsatisfiable Nat g := by
   dsimp [relabelFin]
   split <;> rename_i h
   · apply unsat_relabel_iff

LeanSAT/Tactics/Glue.lean

@@ -18,7 +18,8 @@ def CNF.lift (cnf : CNF Nat) : CNF (PosFin (cnf.numLiterals + 1)) :=
   let cnf := cnf.relabelFin
   cnf.relabel (fun lit => ⟨lit.val + 1, by omega⟩)
 
-theorem CNF.unsat_of_lift_unsat (cnf : CNF Nat) : CNF.unsat cnf.lift → CNF.unsat cnf := by
+theorem CNF.unsat_of_lift_unsat (cnf : CNF Nat)
+    : unsatisfiable (PosFin (cnf.numLiterals + 1)) cnf.lift → unsatisfiable Nat cnf := by
   intro h2
   have h3 :=
     CNF.unsat_relabel_iff

LeanSAT/Tactics/LRAT.lean

@@ -152,9 +152,10 @@ def verifyCert (formula : LratFormula) (cert : LratCert) : Bool :=
     checkerResult = .success
   | none => false
 
-theorem verifyCert_correct : ∀ cnf cert, verifyCert (LratFormula.ofCnf cnf) cert = true → cnf.unsat := by
+theorem verifyCert_correct
+    : ∀ cnf cert, verifyCert (LratFormula.ofCnf cnf) cert = true → unsatisfiable Nat cnf := by
   intro c b h1
-  dsimp[verifyCert] at h1
+  dsimp [verifyCert] at h1
   split at h1
   . simp only [decide_eq_true_eq] at h1
     have h2 :=
@@ -173,8 +174,7 @@ theorem verifyCert_correct : ∀ cnf cert, verifyCert (LratFormula.ofCnf cnf) ce
     apply CNF.unsat_of_lift_unsat c
     intro assignment
     unfold CNF.convertLRAT at h2
-    have h2 := (LRAT.unsat_of_cons_none_unsat _ h2) assignment
-    apply eq_false_of_ne_true
+    replace h2 := (LRAT.unsat_of_cons_none_unsat _ h2) assignment
     intro h3
     apply h2
     simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
@@ -183,7 +183,7 @@ theorem verifyCert_correct : ∀ cnf cert, verifyCert (LratFormula.ofCnf cnf) ce
       CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
       List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
     rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
-    simp only [CNF.eval, List.all_eq_true] at h3
+    simp only [(· ⊨ ·), CNF.eval, List.all_eq_true] at h3
     split at hrclause2
     . next heq =>
       rw [← heq] at hrclause2