From 5a849dee9b415eb2ddc96abae69c66c675ae8aaa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Apr 2025 14:09:26 -0700 Subject: [PATCH] fix: `grind` ematch theorem activation issue (#7861) This PR fixes an issue that prevented theorems from being activated in `grind`. --- src/Lean/Meta/Tactic/Grind.lean | 2 ++ src/Lean/Meta/Tactic/Grind/Internalize.lean | 10 +++++++--- tests/lean/run/grind_ematch_theorem_activation.lean | 13 +++++++++++++ tests/lean/run/grind_erase_attr.lean | 2 -- tests/lean/run/grind_pattern2.lean | 5 +---- tests/lean/run/grind_usr.lean | 4 ++-- 6 files changed, 25 insertions(+), 11 deletions(-) create mode 100644 tests/lean/run/grind_ematch_theorem_activation.lean diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index a6d1d7d34c..30a4ee48a3 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -74,5 +74,7 @@ builtin_initialize registerTraceClass `grind.debug.mbtc builtin_initialize registerTraceClass `grind.debug.ematch builtin_initialize registerTraceClass `grind.debug.proveEq builtin_initialize registerTraceClass `grind.debug.pushNewFact +builtin_initialize registerTraceClass `grind.debug.ematch.activate +builtin_initialize registerTraceClass `grind.debug.appMap end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 8968b7a38d..4afab2cc90 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -42,6 +42,7 @@ adds entry `f ↦ e` to `appMap`. Recall that `appMap` is a multi-map. -/ private def updateAppMap (e : Expr) : GoalM Unit := do let key := e.toHeadIndex + trace_goal[grind.debug.appMap] "{e} => {repr key}" modify fun s => { s with appMap := if let some es := s.appMap.find? key then s.appMap.insert key (e :: es) @@ -168,13 +169,16 @@ private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Un modify fun s => { s with ematch.thmMap := thmMap } let appMap := (← get).appMap for thm in thms do + trace[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`" unless (← get).ematch.thmMap.isErased thm.origin do let symbols := thm.symbols.filter fun sym => !appMap.contains sym let thm := { thm with symbols } match symbols with - | [] => activateTheorem thm generation + | [] => + trace_goal[grind.debug.ematch.activate] "`{thm.origin.key}`" + activateTheorem thm generation | _ => - trace_goal[grind.ematch] "reinsert `{thm.origin.key}`" + trace_goal[grind.debug.ematch.activate] "reinsert `{thm.origin.key}`" modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm } /-- @@ -256,6 +260,7 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt internalizeMatchCond e generation else e.withApp fun f args => do mkENode e generation + updateAppMap e checkAndAddSplitCandidate e pushCastHEqs e addMatchEqns f generation @@ -280,7 +285,6 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt internalize arg generation e registerParent e arg addCongrTable e - updateAppMap e Arith.internalize e parent? propagateUp e propagateBetaForNewApp e diff --git a/tests/lean/run/grind_ematch_theorem_activation.lean b/tests/lean/run/grind_ematch_theorem_activation.lean new file mode 100644 index 0000000000..fd0065e060 --- /dev/null +++ b/tests/lean/run/grind_ematch_theorem_activation.lean @@ -0,0 +1,13 @@ +reset_grind_attrs% +set_option grind.warning false + +attribute [grind] List.length_set +attribute [grind →] List.eq_nil_of_length_eq_zero +attribute [grind] List.getElem_set + +open List in +example {as : List α} {i : Nat} (h : i < as.length) : + as.set i as[i] = as := by + apply ext_getElem + · sorry + · grind diff --git a/tests/lean/run/grind_erase_attr.lean b/tests/lean/run/grind_erase_attr.lean index f2c851cb11..94e2b914ac 100644 --- a/tests/lean/run/grind_erase_attr.lean +++ b/tests/lean/run/grind_erase_attr.lean @@ -14,8 +14,6 @@ set_option trace.grind.assert true /-- info: [grind.assert] ¬f (f (f a)) = f a -[grind.assert] f (f (f (f a))) = f (f (f a)) -[grind.assert] f (f (f a)) = f (f a) [grind.assert] f (f a) = f a -/ #guard_msgs (info) in diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean index b6c4d3d0c4..6f126ba4b4 100644 --- a/tests/lean/run/grind_pattern2.lean +++ b/tests/lean/run/grind_pattern2.lean @@ -22,10 +22,7 @@ example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by grind -/-- -info: [grind.ematch] reinsert `contains_insert` -[grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] --/ +/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/ #guard_msgs (info) in example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by diff --git a/tests/lean/run/grind_usr.lean b/tests/lean/run/grind_usr.lean index 7e21e0ed38..e1fcf65c87 100644 --- a/tests/lean/run/grind_usr.lean +++ b/tests/lean/run/grind_usr.lean @@ -14,9 +14,9 @@ example : f (f (f x)) = f x := by grind only [fthm] /-- -info: [grind.ematch.instance] fthm: f (f (f (f x))) = f (f (f x)) +info: [grind.ematch.instance] fthm: f (f x) = f x [grind.ematch.instance] fthm: f (f (f x)) = f (f x) -[grind.ematch.instance] fthm: f (f x) = f x +[grind.ematch.instance] fthm: f (f (f (f x))) = f (f (f x)) -/ #guard_msgs (info) in set_option trace.grind.ematch.instance true in