From d6478e15c71cd277da94eef8271ad86bebb54abb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 4 Jun 2025 20:57:25 +1000 Subject: [PATCH] chore: remove slow and unnecessary `@[grind]` annotations (#8630) --- src/Init/Data/Array/Lemmas.lean | 1 - src/Init/GetElem.lean | 4 +--- tests/lean/run/grind_indexmap.lean | 4 ---- tests/lean/run/grind_ite.lean | 12 ++++++------ 4 files changed, 7 insertions(+), 14 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index faf90d79e7..b14cce9171 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -133,7 +133,6 @@ grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]? theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b := _root_.getElem?_eq_some_iff -@[grind →] theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a := getElem?_eq_some_iff.mp diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 27c7c30ed5..207fa866c0 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -193,7 +193,7 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v simp only [getElem?_def] at h ⊢ split <;> simp_all -@[simp, grind =] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] +@[simp] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i := by simp only [getElem?_def] split <;> simp_all @@ -238,8 +238,6 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e := getElem?_eq_some_iff.mp h -grind_pattern getElem_of_getElem? => c[i]?, some e - @[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i): (some c[i] = c[i]?) ↔ True := by diff --git a/tests/lean/run/grind_indexmap.lean b/tests/lean/run/grind_indexmap.lean index f760de2ec3..66fb944e24 100644 --- a/tests/lean/run/grind_indexmap.lean +++ b/tests/lean/run/grind_indexmap.lean @@ -6,10 +6,6 @@ import Std.Data.HashMap set_option grind.warning false --- These are not good `grind` lemmas at present; they really slow things down. --- TODO: remove globally, or work out how to make them usable. -attribute [-grind] getElem?_pos getElem?_neg getElem!_pos getElem!_neg - macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| grind) open Std diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean index a47a6ec573..96eff8044e 100644 --- a/tests/lean/run/grind_ite.lean +++ b/tests/lean/run/grind_ite.lean @@ -156,7 +156,7 @@ theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) : (normalize assign e).normalized ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → ¬ v ∈ assign := by - fun_induction normalize with grind (gen := 7) + fun_induction normalize with grind (gen := 7) (splits := 9) -- We can also prove other variations, where we spell "`v` is not in `assign`" -- different ways, and `grind` doesn't mind. @@ -165,13 +165,13 @@ example (assign : Std.HashMap Nat Bool) (e : IfExpr) : (normalize assign e).normalized ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign.contains v = false := by - fun_induction normalize with grind (gen := 7) + fun_induction normalize with grind (gen := 7) (splits := 9) example (assign : Std.HashMap Nat Bool) (e : IfExpr) : (normalize assign e).normalized ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by - fun_induction normalize with grind (gen := 8) + fun_induction normalize with grind (gen := 8) (splits := 9) /-- We recall the statement of the if-normalization problem. @@ -207,18 +207,18 @@ theorem normalize'_spec (assign : Std.TreeMap Nat Bool) (e : IfExpr) : (normalize' assign e).normalized ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → ¬ v ∈ assign := by - fun_induction normalize' with grind (gen := 7) + fun_induction normalize' with grind (gen := 7) (splits := 9) example (assign : Std.TreeMap Nat Bool) (e : IfExpr) : (normalize' assign e).normalized ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign.contains v = false := by - fun_induction normalize' with grind (gen := 7) + fun_induction normalize' with grind (gen := 7) (splits := 9) example (assign : Std.TreeMap Nat Bool) (e : IfExpr) : (normalize' assign e).normalized ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign[v]? = none := by - fun_induction normalize' with grind (gen := 8) + fun_induction normalize' with grind (gen := 8) (splits := 9) end IfExpr