chore: remove Entails

src/Std/Sat.lean

@@ -4,5 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Std.Sat.Basic
 import Std.Sat.CNF

src/Std/Sat/CNF/Basic.lean

@@ -46,20 +46,21 @@ def eval (a : α → Bool) (f : CNF α) : Bool := f.all fun c => c.eval a
 @[simp] theorem eval_append (a : α → Bool) (f1 f2 : CNF α) :
     eval a (f1 ++ f2) = (eval a f1 && eval a f2) := List.all_append
 
-instance : Entails α (Clause α) where
-  eval assign clause := Clause.eval assign clause
+def sat (a : α → Bool) (f : CNF α) : Prop := eval a f = true
+def unsat (f : CNF α) : Prop := ∀ a, eval a f = false
 
-instance : Entails α (CNF α) where
-  eval assign cnf := eval assign cnf
+theorem sat_def (a : α → Bool) (f : CNF α) : sat a f ↔ (eval a f = true) := by rfl
+theorem unsat_def (f : CNF α) : unsat f ↔ (∀ a, eval a f = false) := by rfl
 
-@[simp] theorem not_unsatisfiable_nil : ¬Unsatisfiable α ([] : CNF α) :=
-  fun h => by simp [Unsatisfiable, (· ⊨ ·)] at h
 
-@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) := by
-  simp [(· ⊨ ·)]
+@[simp] theorem not_unsatisfiable_nil : ¬unsat ([] : CNF α) :=
+  fun h => by simp [unsat_def] at h
 
-@[simp] theorem unsat_nil_cons {g : CNF α} : Unsatisfiable α ([] :: g) := by
-  simp [Unsatisfiable, (· ⊨ ·)]
+@[simp] theorem sat_nil {assign : α → Bool} : sat assign ([] : CNF α) := by
+  simp [sat_def]
+
+@[simp] theorem unsat_nil_cons {g : CNF α} : unsat ([] :: g) := by
+  simp [unsat_def]
 
 namespace Clause
 

src/Std/Sat/CNF/Literal.lean

@@ -6,7 +6,6 @@ Authors: Josh Clune
 prelude
 import Init.Data.Hashable
 import Init.Data.ToString
-import Std.Sat.Basic
 
 namespace Std
 namespace Sat
@@ -20,12 +19,6 @@ abbrev Literal (α : Type u) := α × Bool
 namespace Literal
 variable (α : Type) [Hashable α]
 
-instance : Entails α (Literal α) where
-  eval := fun p l => p l.1 = l.2
-
-instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) :=
-  inferInstanceAs (Decidable (p l.1 = l.2))
-
 /--
 Flip the polarity of `l`.
 -/

src/Std/Sat/CNF/Relabel.lean

@@ -76,12 +76,12 @@ theorem relabel_congr {f : CNF α} {r1 r2 : α → β} (hw : ∀ v, Mem v f →
   intro v m
   exact hw _ (mem_of h m)
 
-theorem sat_relabel {f : CNF α} (h : (r1 ∘ r2) ⊨ f) : r1 ⊨ (relabel r2 f) := by
-  simp_all [(· ⊨ ·)]
+theorem sat_relabel {f : CNF α} (h : sat (r1 ∘ r2) f) : sat r1 (relabel r2 f) := by
+  simp_all [sat_def]
 
-theorem unsat_relabel {f : CNF α} (r : α → β) (h : Unsatisfiable α f) :
-    Unsatisfiable β (relabel r f) := by
-  simp_all [Unsatisfiable, (· ⊨ ·)]
+theorem unsat_relabel {f : CNF α} (r : α → β) (h : unsat f) :
+    unsat (relabel r f) := by
+  simp_all [unsat_def]
 
 theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.replicate n [] := by
   induction f with
@@ -97,7 +97,7 @@ theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.re
 
 theorem unsat_relabel_iff {f : CNF α} {r : α → β}
     (hw : ∀ {v1 v2}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2) :
-    Unsatisfiable β (relabel r f) ↔ Unsatisfiable α f := by
+    unsat (relabel r f) ↔ unsat f := by
   rcases nonempty_or_impossible f with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)
   · refine ⟨fun h => ?_, unsat_relabel r⟩
     have em := Classical.propDecidable
@@ -115,7 +115,7 @@ theorem unsat_relabel_iff {f : CNF α} {r : α → β}
       · exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).1
     rw [relabel_relabel, relabel_congr, relabel_id]
     exact this
-  · cases n <;> simp [Unsatisfiable, (· ⊨ ·), List.replicate_succ]
+  · cases n <;> simp [unsat_def, List.replicate_succ]
 
 end CNF
 

src/Std/Sat/CNF/RelabelFin.lean

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