feat: use HSat

LeanSAT/AIG/CNF.lean

@@ -7,6 +7,8 @@ import LeanSAT.AIG.Basic
 import LeanSAT.AIG.Lemmas
 import LeanSAT.CNF
 
+open Sat
+
 /-!
 This module contains an implementation of a verified Tseitin transformation on AIGs. The key results
 are the `toCNF` function and the `toCNF_equisat` correctness statement. The implementation is
@@ -387,7 +389,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 +405,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 +414,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 +438,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 +547,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 +649,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 +664,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 +688,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/BitBlast/BoolExpr/Basic.lean

@@ -3,9 +3,11 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import LeanSAT.Sat.Basic
+
 set_option linter.missingDocs false
 
-open Lean Meta
+open Lean Meta Sat
 
 inductive Gate
 | and
@@ -68,14 +70,16 @@ def eval (f : α → Bool) : BoolExpr α → Bool
 @[simp] theorem eval_not : eval f (.not x) = !eval f x := rfl
 @[simp] theorem eval_gate : eval f (.gate g x y) = g.eval (eval f x) (eval f y) := rfl
 
-def sat (x : BoolExpr α) (f : α → Bool) : Prop := eval f x = true
+def sat (f : α → Bool) (x : BoolExpr α) : Prop := eval f x = true
 
-theorem sat_and {x y : BoolExpr α} {f} (hx : sat x f) (hy : sat y f) : sat (.gate .and x y) f := by
-  simp only [sat] at *
-  simp [hx, hy, Gate.eval]
+instance : HSat α (BoolExpr α) where
+  eval := sat
 
-theorem sat_true : sat (.const true) f := rfl
+theorem sat_and {x y : BoolExpr α} {f : α → Bool} (hx : f ⊨ x) (hy : f ⊨ y)
+    : f ⊨ (BoolExpr.gate .and x y) := by
+  simp only [(· ⊨ ·), sat] at *
+  simp [hx, hy, Gate.eval]
 
-def unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false
+theorem sat_true {f : α → Bool} : f ⊨ (BoolExpr.const true : BoolExpr α) := rfl
 
 end BoolExpr

LeanSAT/BitBlast/BoolExpr/BitBlast.lean

@@ -14,6 +14,8 @@ through the use of a cache that re-uses sub-circuits if possible.
 
 namespace AIG
 
+open Sat
+
 variable {β : Type} [Hashable β] [DecidableEq β]
 
 
@@ -148,7 +150,9 @@ theorem ofBoolExprCachedDirect_eval_eq_eval (expr : BoolExpr α) (assign) :
     ⟦ofBoolExprCachedDirect expr, assign⟧ = expr.eval assign := by
   apply ofBoolExprCached.go_eval_eq_eval
 
-theorem ofBoolExprCachedDirect_unsat_iff {expr : BoolExpr α} : (ofBoolExprCachedDirect expr).unsat ↔ expr.unsat := by
+theorem ofBoolExprCachedDirect_unsat_iff {expr : BoolExpr α}
+    : (ofBoolExprCachedDirect expr).unsat ↔ unsatisfiable α expr := by
+  simp [unsatisfiable, (· ⊨ ·), BoolExpr.sat]
   constructor
   all_goals
     intro h assign

LeanSAT/CNF/Basic.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import LeanSAT.CNF.ForStd
+import LeanSAT.Sat
+
+open 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 +25,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 +45,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
+
+instance : HSat α (CNF α) where
+  eval assign cnf := eval assign cnf
 
-@[simp] theorem unsat_nil_iff_false : unsat ([] : CNF α) ↔ False :=
-  ⟨fun h => by simp [unsat] at h, by simp⟩
+@[simp] theorem unsat_nil_iff_false : unsatisfiable α ([] : CNF α) ↔ False :=
+  ⟨fun h => by simp [unsatisfiable, (· ⊨ ·)] at h, by simp⟩
 
-@[simp] theorem sat_nil : sat ([] : CNF α) assign ↔ True := by
-  simp [sat]
+@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by
+  simp [(· ⊨ ·)]
 
-@[simp] theorem unsat_nil_cons : unsat ([] :: g) ↔ True := by
-  simp [unsat]
+@[simp] theorem unsat_nil_cons {g : CNF α} : unsatisfiable α ([] :: g) ↔ True := by
+  simp [unsatisfiable, (· ⊨ ·)]
 
 namespace Clause
 

LeanSAT/CNF/Relabel.lean

@@ -5,6 +5,8 @@ Authors: Scott Morrison
 -/
 import LeanSAT.CNF.Basic
 
+open Sat
+
 set_option linter.missingDocs false
 
 namespace CNF
@@ -64,11 +66,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 +86,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 +104,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/LRAT/Clause.lean

@@ -9,6 +9,8 @@ import LeanSAT.Util.PosFin
 import LeanSAT.Util.Misc
 import LeanSAT.LRAT.Assignment
 
+open Sat
+
 namespace LRAT
 
 /-- ReduceResult is an inductive datatype used specifically for the output of the `reduce` function. The intended

LeanSAT/LRAT/Formula/Class.lean

@@ -8,6 +8,8 @@ import LeanSAT.LRAT.Clause
 
 namespace LRAT
 
+open Sat
+
 /-- Typeclass for formulas. An instance [Formula α β σ] indicates that σ is
     the type of a formula with variables of type α, clauses of type β, and clause ids of type Nat -/
 class Formula (α : outParam (Type u)) (β : outParam (Type v)) [Clause α β] (σ : Type w) [HSat α σ] where

LeanSAT/LRAT/Formula/Implementation.lean

@@ -8,7 +8,7 @@ import LeanSAT.LRAT.Assignment
 
 namespace LRAT
 
-open Assignment DefaultClause Literal Std ReduceResult
+open Assignment DefaultClause Literal Std ReduceResult Sat
 
 /-- The structure `DefaultFormula n` takes in a parameter `n` which is intended to be one greater than the total number of variables that
     can appear in the formula (hence why the parameter `n` is called `numVarsSucc` below). The structure has 4 fields:

LeanSAT/Sat/Basic.lean

@@ -10,12 +10,12 @@ Authors: Josh Clune
 class HSat (α : Type u) (β : Type v) :=
   (eval : (α → Bool) → β → Prop)
 
-infix:25 " ⊨ " => HSat.eval
-notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f)
+namespace Sat
 
-def unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := ∀ (p : α → Bool), p ⊭ f
+scoped infix:25 " ⊨ " => HSat.eval
+scoped notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f)
 
-namespace Sat
+def _root_.unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := ∀ (p : α → Bool), p ⊭ f
 
 /-- f1 and f2 are logically equivalent -/
 def liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop :=

LeanSAT/Sat/Literal.lean

@@ -9,6 +9,8 @@ abbrev Literal (α : Type u) := α × Bool
 
 namespace Literal
 
+open Sat
+
 instance [Hashable α] : Hashable (Literal α) where
   hash := fun x => if x.2 then hash x.1 else hash x.1 + 1
 

LeanSAT/Tactics/Glue.lean

@@ -7,7 +7,7 @@ import LeanSAT.CNF.RelabelFin
 
 import LeanSAT.LRAT.LRATChecker
 
-open Lean Elab Meta
+open Lean Elab Meta Sat
 
 /--
 Turn a `CNF Nat`, that might contain `0` as a variable, to a `CNF PosFin`.
@@ -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