chore: simplify proofs

.gitignore

@@ -1,2 +1,3 @@
 /.lake
 .DS_Store
+/build

LeanSAT/LRAT/Clause.lean

@@ -111,7 +111,7 @@ def empty {n : Nat} : DefaultClause n :=
   have nodup := by simp only [List.nodup_nil]
   ⟨clause, nodupkey, nodup⟩
 
-theorem empty_eq {n : Nat} : toList (empty : DefaultClause n) = [] := by rfl
+theorem empty_eq {n : Nat} : toList (empty : DefaultClause n) = [] := rfl
 
 def unit {n : Nat} (l : Literal (PosFin n)) : DefaultClause n :=
   let clause := [l]
@@ -127,7 +127,7 @@ def unit {n : Nat} (l : Literal (PosFin n)) : DefaultClause n :=
   have nodup : List.Nodup clause:= by simp
   ⟨clause, nodupkey, nodup⟩
 
-theorem unit_eq {n : Nat} (l : Literal (PosFin n)) : toList (unit l) = [l] := by rfl
+theorem unit_eq {n : Nat} (l : Literal (PosFin n)) : toList (unit l) = [l] := rfl
 
 def isUnit {n : Nat} (c : DefaultClause n) : Option (Literal (PosFin n)) :=
   match c.clause with
@@ -146,7 +146,7 @@ theorem isUnit_iff {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) :
 
 def negate {n : Nat} (c : DefaultClause n) : List (Literal (PosFin n)) := c.clause.map negateLiteral
 
-theorem negate_iff {n : Nat} (c : DefaultClause n) : negate c = (toList c).map negateLiteral := by rfl
+theorem negate_iff {n : Nat} (c : DefaultClause n) : negate c = (toList c).map negateLiteral := 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) :=
@@ -230,7 +230,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n))) (arrNodup : ∀ i : Fin ar
     split at heq
     . simp only at heq
     . next acc =>
-      specialize ih acc (by rfl)
+      specialize ih acc rfl
       rcases ih with ⟨hsize, ih⟩
       simp only at ih
       simp only [insert] at heq

LeanSAT/LRAT/Formula/Basic.lean

@@ -36,8 +36,7 @@ def assignments_invariant {n : Nat} (f : DefaultFormula n) : Prop :=
 
 theorem assignments_invariant_of_strong_assignments_invariant {n : Nat} (f : DefaultFormula n) :
   strong_assignments_invariant f → assignments_invariant f := by
-  intro h
-  rcases h with ⟨hsize, h⟩
+  intro ⟨hsize, h⟩
   apply Exists.intro hsize
   intro i b hb p pf
   specialize h i b hb
@@ -131,7 +130,7 @@ theorem ofArray_readyForRupAdd {n : Nat} (arr : Array (Option (DefaultClause n))
               simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
               have i_eq_l : i = l := Subtype.ext i_eq_l
               simp only [unit, b_eq_true, i_eq_l]
-              have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := by rfl
+              have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
               simp only [heq] at c_def
               rw [c_def] at cOpt_in_arr
               exact cOpt_in_arr
@@ -165,7 +164,7 @@ theorem ofArray_readyForRupAdd {n : Nat} (arr : Array (Option (DefaultClause n))
               simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
               have i_eq_l : i = l := Subtype.ext i_eq_l
               simp only [unit, b_eq_false, i_eq_l]
-              have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := by rfl
+              have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
               simp only [heq] at c_def
               rw [c_def] at cOpt_in_arr
               exact cOpt_in_arr
@@ -245,7 +244,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
   intro f_readyForRupAdd
   simp only [insert]
   split
-  . apply And.intro f_readyForRupAdd.1 ∘ Exists.intro f_readyForRupAdd.2.1
+  . refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b hb
     simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
@@ -258,7 +257,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
   . next l hc =>
     have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by
       rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
-    apply And.intro f_readyForRupAdd.1 ∘ Exists.intro hsize
+    refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b
     have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
@@ -299,7 +298,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
   . next l hc =>
     have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by
       rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
-    apply And.intro f_readyForRupAdd.1 ∘ Exists.intro hsize
+    refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b
     have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
@@ -319,8 +318,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
         . next l_eq_i =>
           have b_eq_false : b = true := by
             by_cases b = true
-            . next b_eq_true =>
-              exact b_eq_true
+            . assumption
             . next b_eq_false =>
               simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
           simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb
@@ -341,9 +339,7 @@ theorem insert_readyForRatAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
   readyForRatAdd f → readyForRatAdd (insert f c) := by
   intro h
   constructor
-  . simp only [insert, h.1]
-    split
-    repeat { rfl }
+  . simp only [insert, h.1] <;> split <;> rfl
   . exact insert_readyForRupAdd f c h.2
 
 theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : List (Literal (PosFin n)))
@@ -388,9 +384,8 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : List (Li
   simp only [toList, insertRatUnits, Prod.mk.eta, Array.toList_eq, List.append_assoc, List.mem_append,
     List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
   intro h
-  have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by
-    intro l hl
-    exact Or.inl hl
+  have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) :=
+    fun _ => Or.inl
   have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
     (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.ratUnits.data ∨ l ∈ units)
     (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
@@ -482,7 +477,7 @@ theorem deleteOne_preserves_strong_assignments_invariant {n : Nat} (f : DefaultF
             . next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx.1 < f.clauses.size := by
-                have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl
+                have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
                 conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact idx.2
               simp only [getElem!, id_eq_idx, idx_in_bounds2, dite_true, Array.getElem_eq_data_get] at heq
@@ -519,7 +514,7 @@ theorem deleteOne_preserves_strong_assignments_invariant {n : Nat} (f : DefaultF
             . next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx.1 < f.clauses.size := by
-                have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl
+                have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
                 conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact idx.2
               simp only [getElem!, id_eq_idx, idx_in_bounds2, dite_true, Array.getElem_eq_data_get] at heq
@@ -580,7 +575,7 @@ theorem deleteOne_preserves_strong_assignments_invariant {n : Nat} (f : DefaultF
             . next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx.1 < f.clauses.size := by
-                have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl
+                have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
                 conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact idx.2
               simp only [getElem!, id_eq_idx, idx_in_bounds2, dite_true, Array.getElem_eq_data_get] at heq
@@ -631,27 +626,9 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
   c ∈ toList (deleteOne f id) → c ∈ toList f := by
   simp only [deleteOne]
   intro h1
-  split at h1
-  . exact h1
-  . rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
-    rw [toList, List.mem_append, List.mem_append, or_assoc]
-    rcases h1 with h1 | h1 | h1
-    . apply Or.inl
-      simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
-      simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
-      rw [Array.set!, Array.setD] at h1
-      split at h1
-      . simp only [Array.data_set] at h1
-        rcases List.get_of_mem h1 with ⟨i, h4⟩
-        rw [List.get_set] at h4
-        split at h4
-        . exact False.elim h4
-        . rw [← h4]
-          apply List.get_mem
-      . exact h1
-    . exact (Or.inr ∘ Or.inl) h1
-    . exact (Or.inr ∘ Or.inr) h1
-  . rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
+  split at h1 <;> first
+  | exact h1
+  | rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
     rw [toList, List.mem_append, List.mem_append, or_assoc]
     rcases h1 with h1 | h1 | h1
     . apply Or.inl

LeanSAT/LRAT/Formula/Implementation.lean

@@ -61,7 +61,7 @@ instance {n : Nat} : Inhabited (DefaultFormula n) where
 def toList {n : Nat} (f : DefaultFormula n) : List (DefaultClause n) :=
   (f.clauses.toList.filterMap id) ++ (f.rupUnits.toList.map unit) ++ (f.ratUnits.toList.map unit)
 
-def ofArray_fold_fn : Array Assignment → Option (DefaultClause n) → Array Assignment := fun assignments cOpt =>
+def ofArray_fold_fn (assignments : Array Assignment) (cOpt : Option (DefaultClause n)) : Array Assignment :=
   match cOpt with
   | none => assignments
   | some c =>
@@ -77,17 +77,14 @@ def ofArray {n : Nat} (clauses : Array (Option (DefaultClause n))) : DefaultForm
   ⟨clauses, #[], #[], assignments⟩
 
 def insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : DefaultFormula n :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    match isUnit c with
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  match isUnit c with
     | none => ⟨clauses.push c, rupUnits, ratUnits, assignments⟩
     | some (l, true) => ⟨clauses.push c, rupUnits, ratUnits, assignments.modify l addPosAssignment⟩
     | some (l, false) => ⟨clauses.push c, rupUnits, ratUnits, assignments.modify l addNegAssignment⟩
-
 def deleteOne {n : Nat} (f : DefaultFormula n) (id : Nat) : DefaultFormula n :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    match clauses[id]! with
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  match clauses[id]! with
     | none => ⟨clauses, rupUnits, ratUnits, assignments⟩
     | some ⟨[l], _, _⟩ => ⟨clauses.set! id none, rupUnits, ratUnits, assignments.modify l.1 (removeAssignment l.2)⟩
     | some _ => ⟨clauses.set! id none, rupUnits, ratUnits, assignments⟩
@@ -112,32 +109,28 @@ def insertUnit : Array (Literal (PosFin n)) × Array Assignment × Bool →
 
 /-- Returns an updated formula f and a bool which indicates whether a contradiction was found in the process of updating f -/
 def insertRupUnits {n : Nat} (f : DefaultFormula n) (ls : List (Literal (PosFin n))) : DefaultFormula n × Bool :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    let (rupUnits, assignments, foundContradiction) := ls.foldl insertUnit (rupUnits, assignments, false)
-    (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  let (rupUnits, assignments, foundContradiction) := ls.foldl insertUnit (rupUnits, assignments, false)
+  (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
 
 /-- Returns an updated formula f and a bool which indicates whether a contradiction was found in the process of updating f -/
 def insertRatUnits {n : Nat} (f : DefaultFormula n) (ls : List (Literal (PosFin n))) : DefaultFormula n × Bool :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    let (ratUnits, assignments, foundContradiction) := ls.foldl insertUnit (ratUnits, assignments, false)
-    (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  let (ratUnits, assignments, foundContradiction) := ls.foldl insertUnit (ratUnits, assignments, false)
+  (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
 
 def clearUnit : Array Assignment → Literal (PosFin n) → Array Assignment
   | assignments, (l, b) => assignments.modify l (removeAssignment b)
 
 def clearRupUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    let assignments := rupUnits.foldl clearUnit assignments
-    ⟨clauses, #[], ratUnits, assignments⟩
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  let assignments := rupUnits.foldl clearUnit assignments
+  ⟨clauses, #[], ratUnits, assignments⟩
 
 def clearRatUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    let assignments := ratUnits.foldl clearUnit assignments
-    ⟨clauses, rupUnits, #[], assignments⟩
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  let assignments := ratUnits.foldl clearUnit assignments
+  ⟨clauses, rupUnits, #[], assignments⟩
 
 /-- Reverts assignments to the array it was prior to adding derivedLits -/
 def restoreAssignments {n : Nat} (assignments : Array Assignment) (derivedLits : List (PosFin n × Bool)) :
@@ -174,10 +167,9 @@ def confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n))) : Arra
     Note: This function assumes that any rupUnits and ratUnits corresponding to this rup check have already been added to f. -/
 def performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
   DefaultFormula n × List (Literal (PosFin n)) × Bool × Bool :=
-  match f with
-  | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-    let (assignments, derivedLits, derivedEmpty, encounteredError) := rupHints.foldl (confirmRupHint clauses) (assignments, [], false, false)
-    (⟨clauses, rupUnits, ratUnits, assignments⟩, derivedLits, derivedEmpty, encounteredError)
+  let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+  let (assignments, derivedLits, derivedEmpty, encounteredError) := rupHints.foldl (confirmRupHint clauses) (assignments, [], false, false)
+  (⟨clauses, rupUnits, ratUnits, assignments⟩, derivedLits, derivedEmpty, encounteredError)
 
 /-- Attempts to verify that c can be added to f via unit propagation. If it can, it returns ((f.insert c), true). If it can't,
     it returns false as the second part of the tuple (and no guarantees are made about what formula is returned) -/
@@ -192,13 +184,12 @@ def performRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHin
     if encounteredError then (f, false)
     else if not derivedEmpty then (f, false)
     else -- derivedEmpty is true and encounteredError is false
-      match f with
-      | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
-        let assignments := restoreAssignments assignments derivedLits
-        -- assignments should now be the same as it was before the performRupCheck call
-        let f := clearRupUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
-        -- f should now be the same as it was before insertRupUnits
-        (f.insert c, true)
+      let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
+      let assignments := restoreAssignments assignments derivedLits
+      -- assignments should now be the same as it was before the performRupCheck call
+      let f := clearRupUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
+      -- f should now be the same as it was before insertRupUnits
+      (f.insert c, true)
 
 /-- 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 :=

LeanSAT/LRAT/Formula/RatAddResult.lean

@@ -149,7 +149,7 @@ theorem performRatCheck_preserves_formula {n : Nat} (f : DefaultFormula n) (hf :
         ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
          (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
          (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
-         (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := by rfl
+         (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
       simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits]
       rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
         clear_insertRat f hf (negate (DefaultClause.delete c p))]
@@ -165,7 +165,7 @@ theorem performRatCheck_fold_preserves_formula {n : Nat} (f : DefaultFormula n)
             else (x.1, false)) (f, true) 0 ratHints.size
       performRatCheck_fold_res.1 = f := by
   let motive (_idx : Nat) (acc : DefaultFormula n × Bool) := acc.1 = f
-  have h_base : motive 0 (f, true) := by rfl
+  have h_base : motive 0 (f, true) := rfl
   have h_inductive (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool) :
     motive idx.1 acc → motive (idx.1 + 1) (if acc.2 then performRatCheck acc.1 p ratHints[idx] else (acc.1, false)) := by
     intro ih
@@ -207,7 +207,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
               exact And.intro f_readyForRatAdd.1 hsize
             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⟩ := by rfl
+               (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,
               performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
               restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,