From b1980ef8717aef252dabc6f296084a29a7bfc0dc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 10 Jun 2025 13:47:28 +1000 Subject: [PATCH] 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. --- .../Tactic/BVDecide/LRAT/Internal/Clause.lean | 4 +-- .../LRAT/Internal/Formula/RatAddResult.lean | 8 +----- .../LRAT/Internal/Formula/RatAddSound.lean | 13 +++------- .../LRAT/Internal/Formula/RupAddResult.lean | 2 +- .../LRAT/Internal/Formula/RupAddSound.lean | 2 -- tests/lean/grind/lrat_mvar.lean | 26 ------------------- 6 files changed, 6 insertions(+), 49 deletions(-) delete mode 100644 tests/lean/grind/lrat_mvar.lean diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean index bc26be37ef..041571336c 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean +++ b/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 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean index d63eb0dfc1..f641063b66 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean +++ b/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)) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index ba493245e9..8b39db4c60 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/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] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 619b0d8fb5..6d95ec4adf 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/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 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index 9b5c982f28..22d7f31a7e 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/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 diff --git a/tests/lean/grind/lrat_mvar.lean b/tests/lean/grind/lrat_mvar.lean deleted file mode 100644 index 6568ae8937..0000000000 --- a/tests/lean/grind/lrat_mvar.lean +++ /dev/null @@ -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⟩