refactor: final refactor of CNF.Literal

LeanSAT/CNF.lean

@@ -4,5 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import LeanSAT.CNF.Basic
+import LeanSAT.CNF.Literal
 import LeanSAT.CNF.Relabel
 import LeanSAT.CNF.RelabelFin

LeanSAT/CNF/Literal.lean

@@ -5,6 +5,9 @@ Authors: Josh Clune
 -/
 import LeanSAT.Sat
 
+/--
+CNF literals identified by some type `α`.
+-/
 abbrev Literal (α : Type u) := α × Bool
 
 namespace Literal
@@ -21,8 +24,14 @@ instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := by
   rw [HSat.eval, instHSat]
   exact Bool.decEq (p l.fst) l.snd
 
-def negateLiteral (l : Literal α) := (l.1, not l.2)
+/--
+Flip the polarity of `l`.
+-/
+def negate (l : Literal α) : Literal α := (l.1, not l.2)
 
+/--
+Output `l` as a DIMACS literal identifier.
+-/
 def dimacs [ToString α] (l : Literal α) : String :=
   if l.2 then
     s!"{l.1}"

LeanSAT/LRAT/CNF.lean

@@ -7,15 +7,15 @@ import LeanSAT.LRAT.Formula.Class
 
 namespace LRAT
 
-open Literal Clause Formula Misc Sat
+open Clause Formula Misc Sat
 
 namespace Literal
 
 theorem sat_iff (p : α → Bool) (a : α) (b : Bool) : p ⊨ (a, b) ↔ (p a) = b := by
   simp only [HSat.eval]
 
-theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ negateLiteral l ↔ p ⊭ l := by
-  simp only [negateLiteral, sat_iff]
+theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Literal.negate l ↔ p ⊭ l := by
+  simp only [Literal.negate, sat_iff]
   constructor
   . intro h pl
     rw [sat_iff, h, not] at pl
@@ -26,7 +26,7 @@ theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ negate
     split <;> simp_all
 
 theorem unsat_of_limplies_complement [HSat α t] (x : t) (l : Literal α) :
-    limplies α x l → limplies α x (negateLiteral l) → unsatisfiable α x := by
+    limplies α x l → limplies α x (Literal.negate l) → unsatisfiable α x := by
   intro h1 h2 p px
   specialize h1 p px
   specialize h2 p px
@@ -69,7 +69,7 @@ theorem limplies_iff_mem [DecidableEq α] [Clause α β] (l : Literal α) (c : 
         exfalso
         rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
         . exact v_not_in_c h1
-        . simp only [negateLiteral, Bool.not_true] at negv_not_in_c
+        . simp only [Literal.negate, Bool.not_true] at negv_not_in_c
           exact negv_not_in_c h2
   . intro h p pl
     apply Exists.intro l.1

LeanSAT/LRAT/Clause.lean

@@ -20,13 +20,13 @@ inductive ReduceResult (α : Type u)
   | reducedToUnit (l : Literal α)
   | reducedToNonunit
 
-open Misc Literal Assignment ReduceResult
+open Misc Assignment ReduceResult
 
 /-- Typeclass for clauses. An instance [Clause α β] indicates that β is
     the type of a clause with variables of type α. -/
 class Clause (α : outParam (Type u)) (β : Type v) where
   toList : β → CNF.Clause α
-  not_tautology : ∀ c : β, ∀ l : Literal α, l ∉ toList c ∨ negateLiteral l ∉ toList c
+  not_tautology : ∀ c : β, ∀ l : Literal α, l ∉ toList c ∨ Literal.negate l ∉ toList c
   ofArray : Array (Literal α) → Option β -- Returns none if the given array contains complementary literals
   ofArray_eq :
     ∀ arr : Array (Literal α), (∀ i : Fin arr.size, ∀ j : Fin arr.size, i.1 ≠ j.1 → arr[i] ≠ arr[j]) →
@@ -38,7 +38,7 @@ class Clause (α : outParam (Type u)) (β : Type v) where
   isUnit : β → Option (Literal α)
   isUnit_iff : ∀ c : β, ∀ l : Literal α, isUnit c = some l ↔ toList c = [l]
   negate : β → CNF.Clause α
-  negate_iff : ∀ c : β, negate c = (toList c).map negateLiteral
+  negate_iff : ∀ c : β, negate c = (toList c).map Literal.negate
   insert : β → Literal α → Option β -- Returns none if the result is a tautology
   delete : β → Literal α → β
   delete_iff : ∀ c : β, ∀ l : Literal α, ∀ l' : Literal α,
@@ -88,8 +88,8 @@ namespace DefaultClause
 
 def toList {n : Nat} (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause
 
-theorem not_tautology {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) : ¬ l ∈ toList c ∨ ¬negateLiteral l ∈ toList c := by
-  simp only [toList, negateLiteral]
+theorem not_tautology {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) : ¬ l ∈ toList c ∨ ¬Literal.negate l ∈ toList c := by
+  simp only [toList, Literal.negate]
   have h := c.nodupkey l.1
   by_cases hl : l.2
   . simp only [hl, Bool.not_true]
@@ -137,9 +137,9 @@ theorem isUnit_iff {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) :
     simp only [false_iff]
     apply hne
 
-def negate {n : Nat} (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map negateLiteral
+def negate {n : Nat} (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate
 
-theorem negate_iff {n : Nat} (c : DefaultClause n) : negate c = (toList c).map negateLiteral := rfl
+theorem negate_iff {n : Nat} (c : DefaultClause n) : negate c = (toList c).map Literal.negate := rfl
 
 /-- Attempts to add the literal (idx, b) to clause c. Returns none if doing so would make c a tautology -/
 def insert {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClause n) :=

LeanSAT/LRAT/Formula/Basic.lean

@@ -6,8 +6,6 @@ Authors: Josh Clune
 import LeanSAT.LRAT.Formula.Implementation
 import LeanSAT.LRAT.CNF
 
-open Literal
-
 namespace LRAT
 namespace DefaultFormula
 

LeanSAT/LRAT/Formula/Implementation.lean

@@ -9,7 +9,7 @@ import LeanSAT.CNF.Basic
 
 namespace LRAT
 
-open Assignment DefaultClause Literal Std ReduceResult Sat
+open Assignment DefaultClause 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:
@@ -191,14 +191,14 @@ def performRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHin
 
 /-- Returns an array of indices corresponding to clauses that contain the negation of l -/
 def getRatClauseIndices {n : Nat} (clauses : Array (Option (DefaultClause n))) (l : Literal (PosFin n)) : Array Nat :=
-  let negL := negateLiteral l
+  let negL := Literal.negate l
   let filter_fn := fun i =>
     match clauses[i]! with
     | none => false
     | some c => c.contains negL
   (Array.range clauses.size).filter filter_fn
 
-/-- Checks that for each clause c ∈ f such that (negateLiteral pivot) ∈ c, c's index is in ratHints.map (fun x => x.1). This
+/-- Checks that for each clause c ∈ f such that (Literal.negate pivot) ∈ c, c's index is in ratHints.map (fun x => x.1). This
     function assumes that ratHints are ordered by the value of their first argument, which is consistent with LRAT's specification -/
 def ratHintsExhaustive {n : Nat} (f : DefaultFormula n) (pivot : Literal (PosFin n)) (ratHints : Array (Nat × Array Nat)) : Bool :=
   let ratClauseIndices := getRatClauseIndices f.clauses pivot
@@ -250,7 +250,7 @@ def performRatAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (pivot
       else if derivedEmpty then (f, false) -- This should be a rupAdd rather than a ratAdd
       else -- derivedEmpty is false and encounteredError is false
         let fold_fn := fun (f, allChecksPassed) ratHint =>
-          if allChecksPassed then performRatCheck f (negateLiteral pivot) ratHint
+          if allChecksPassed then performRatCheck f (Literal.negate pivot) ratHint
           else (f, false)
         let (f, allChecksPassed) := ratHints.foldl fold_fn (f, true)
         if not allChecksPassed then (f, false)

LeanSAT/LRAT/Formula/RatAddResult.lean

@@ -5,8 +5,6 @@ Authors: Josh Clune
 -/
 import LeanSAT.LRAT.Formula.RupAddSound
 
-open Literal
-
 namespace LRAT
 namespace DefaultFormula
 
@@ -208,7 +206,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
             have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
               ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
                (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
-            simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
+            simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
               performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
               restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
               clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]