chore: cleanup notes about grind in LRAT (#8623)

This PR cleans up some notes about `grind` failures in the LRAT checker,
now that some `grind` bugs have been fixed.

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -160,10 +160,8 @@ def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
   match mapOption with
   | none => none
   | some map =>
-    -- FIXME: Commenting this out gives an unknown metavariable error in `grind`!
-    -- reported as https://github.com/leanprover/lean4/pull/8607
     have mapnodup := map.distinct_keys
-    some ⟨map.toList, by grind, by grind⟩
+    some { clause := map.toList }
 
 @[simp]
 theorem ofArray.foldl_folder_none_eq_none : List.foldl ofArray.folder none ls = none := by

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean

@@ -134,13 +134,7 @@ theorem performRatCheck_fold_formula_eq {n : Nat} (f : DefaultFormula n)
   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
-    -- FIXME: this causes an internal `grind` error:
-    -- grind [formula_performRatCheck]
-    intro ih
-    rw [ih]
-    split
-    · exact formula_performRatCheck f hf p ratHints[idx]
-    · rfl
+    grind [formula_performRatCheck]
   exact Array.foldl_induction motive h_base h_inductive
 
 theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p : Literal (PosFin n))

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -372,10 +372,7 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
     have in_bounds_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
       (ih : in_bounds_motive idx.1 acc) : in_bounds_motive (idx.1 + 1) (confirmRupHint f.clauses acc rupHints[idx]) := by
       have h := size_assignments_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 rupHints[idx]
-      have : (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) = acc := rfl
-      simp [this] at *
-      omega -- FIXME `grind` fails here with an internal error
-      -- reported as https://github.com/leanprover/lean4/pull/8608
+      grind
     rw [Array.foldl_induction in_bounds_motive in_bounds_base in_bounds_inductive]
     exact i.2.2
   simp only [( · ⊨ ·)]
@@ -454,17 +451,13 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D
     motive (idx.1 + 1) (fold_fn acc ratHints[idx]) := by
     constructor
     · simp only [Fin.getElem_fin, fold_fn_def, ih.1]
-      -- grind [formula_performRatCheck] -- FIXME: internal grind error
-      split
-      · grind [formula_performRatCheck]
-      · rfl
+      grind [formula_performRatCheck]
     · intro h i
       rw [fold_fn_def] at h
       split at h
       · next acc_eq_true =>
         have i_lt_or_eq_idx : i.1 < idx.1 ∨ i.1 = idx.1 := by
-          -- grind -- FIXME: internal grind error
-          omega
+          omega -- FIXME: why can't `grind` to this?
         rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx
         · exact ih.2 acc_eq_true ⟨i.1, i_lt_idx⟩
         · simp only [getElem!_def, Fin.getElem?_fin, i_eq_idx, idx.2, Array.getElem?_eq_getElem]

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -596,7 +596,7 @@ theorem clear_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Rea
       specialize h ⟨i, i_lt_n⟩
       rcases h with ⟨h,_⟩
       · exact h
-      · omega -- FIXME: `grind` doesn't work here
+      · omega -- FIXME why can't `grind` do this?
 
 theorem clauses_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
     (performRupCheck f rupHints).1.clauses = f.clauses := by

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -554,7 +554,6 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
           simp only [List.get_eq_getElem] at hidx
-          -- grind -- FIXME: internal grind error
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -565,7 +564,6 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
           simp only [List.get_eq_getElem] at hidx
-          -- grind -- FIXME: internal grind error
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2

tests/lean/grind/lrat_mvar.lean

@@ -1,26 +0,0 @@
-import Std.Data.HashMap
-import Init.Grind
-
-set_option grind.warning false
-
-open Std
-
-structure Clause where
-  clause : List (Unit × Bool)
-  nodup : List.Nodup clause
-
-namespace Clause
-
-def folder (acc : Option (Std.HashMap Unit Bool)) (l : Unit) :
-      Option (Std.HashMap Unit Bool) := sorry
-
-example (ls : Array Unit) : Option Clause :=
-  ls.foldl folder (some ∅) |>.map fun map =>
-    have mapnodup := map.distinct_keys
-    ⟨map.toList, by grind⟩
-
-example (ls : Array Unit) : Option Clause :=
-  ls.foldl folder (some ∅) |>.map fun map =>
-    -- The following example is still failing, but
-    -- we don't get the unknown metavar bug anymore
-    ⟨map.toList, by grind⟩