feat: scope Sat notation

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

LeanSAT/BitBlast/BoolExpr/Basic.lean

@@ -7,7 +7,7 @@ import LeanSAT.Sat.Basic
 
 set_option linter.missingDocs false
 
-open Lean Meta
+open Lean Meta Sat
 
 inductive Gate
 | and

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 β]
 
 

LeanSAT/CNF/Basic.lean

@@ -6,6 +6,8 @@ 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⟩
 @[simp] theorem exists_or_eq_right (y : α) (p : α → Prop) : ∃ x : α, p x ∨ x = y := ⟨y, .inr rfl⟩

LeanSAT/CNF/Relabel.lean

@@ -5,6 +5,8 @@ Authors: Scott Morrison
 -/
 import LeanSAT.CNF.Basic
 
+open Sat
+
 set_option linter.missingDocs false
 
 namespace CNF

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`.

LeanSAT/Tactics/LRAT.lean

@@ -9,7 +9,7 @@ import LeanSAT.LRAT.LRATChecker
 import LeanSAT.LRAT.LRATCheckerSound
 import LeanSAT.External.Solver
 
-open Lean Elab Meta
+open Lean Elab Meta Sat
 
 namespace BVDecide