From 2e779f79dea3ff7d1995eca8a146425597e6f181 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 28 Jan 2026 14:09:27 +1100 Subject: [PATCH] fix: bump numInstances for delayed grind theorem instances (#12176) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes a bug where delayed E-match theorem instances could cause uniqueId collisions in the instance tracking map. The `uniqueId` for theorem instances is generated using `numInstances`, but this counter was only bumped for immediately activated instances (`.ready` case), not for delayed instances (`.next` case). This caused ID collisions: 1. Theorem A matches, becomes delayed, gets `uniqueId = N` 2. Counter isn't bumped (stays at N) 3. Theorem B matches next, gets `uniqueId = N` (same!) 4. B's entry overwrites A's entry in `instanceMap` 5. A's tracking is lost This manifested as `grind?` and `finish?` producing `instantiate approx` (meaning "we couldn't determine which theorems to use") instead of proper `instantiate only [...]` with specific theorem lists. The fix bumps `numInstances` for delayed instances too, ensuring each theorem instance gets a truly unique ID. 🤖 Prepared with Claude Code Co-authored-by: Claude --- src/Lean/Meta/Tactic/Grind/Types.lean | 3 +++ tests/lean/run/grind_indexmap_trace.lean | 18 ++++++++---------- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index c05bbd78d2..0a8b1e9e4b 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -1679,6 +1679,9 @@ def addTheoremInstance (thm : EMatchTheorem) (proof : Expr) (prop : Expr) (gener modify fun s => { s with ematch.delayedThmInsts := s.ematch.delayedThmInsts.insert { expr := guard } thms ematch.numDelayedInstances := s.ematch.numDelayedInstances + 1 + -- Bump numInstances for delayed instances too, so that uniqueId generation + -- in EMatch.instantiateTheorem' doesn't produce collisions. + ematch.numInstances := s.ematch.numInstances + 1 } def DelayedTheoremInstance.check (delayed : DelayedTheoremInstance) : GoalM Unit := do diff --git a/tests/lean/run/grind_indexmap_trace.lean b/tests/lean/run/grind_indexmap_trace.lean index 1aff08f26c..943a9271a1 100644 --- a/tests/lean/run/grind_indexmap_trace.lean +++ b/tests/lean/run/grind_indexmap_trace.lean @@ -251,7 +251,7 @@ info: Try these: · instantiate only instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push] · instantiate only [= mem_indices_of_mem, = getElem_def] - instantiate only [usr getElem_indices_lt, usr Array.eq_empty_of_size_eq_zero] + instantiate only [usr getElem_indices_lt] instantiate only [size] cases #ffdf · instantiate only [usr getElem_indices_lt, =_ WF] @@ -260,8 +260,8 @@ info: Try these: · instantiate only instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push] [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set, - size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, - usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF', #f590, #ffdf] + size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF, + = Array.size_set, WF', #f590, #ffdf] -/ #guard_msgs in example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : @@ -294,11 +294,11 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : /-- info: Try these: [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set, - size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, - usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF', #f590, #ffdf] + size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF, + = Array.size_set, WF', #f590, #ffdf] [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set, - size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, - usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF'] + size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF, + = Array.size_set, WF'] [apply] grind => instantiate only [= mem_indices_of_mem, insert, = getElem_def] instantiate only [= getElem?_neg, = getElem?_pos] @@ -309,7 +309,7 @@ info: Try these: · instantiate only instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push] · instantiate only [= mem_indices_of_mem, = getElem_def] - instantiate only [usr getElem_indices_lt, usr Array.eq_empty_of_size_eq_zero] + instantiate only [usr getElem_indices_lt] instantiate only [size] cases #ffdf · instantiate only [usr getElem_indices_lt, =_ WF] @@ -357,7 +357,6 @@ info: Try these: [apply] ⏎ instantiate only [findIdx, insert, = mem_indices_of_mem] instantiate only [= getElem?_neg, = getElem?_pos] - instantiate approx cases #1bba · instantiate only [findIdx] · instantiate only @@ -380,7 +379,6 @@ info: Try these: [apply] grind => instantiate only [findIdx, insert, = mem_indices_of_mem] instantiate only [= getElem?_neg, = getElem?_pos] - instantiate approx cases #1bba · instantiate only [findIdx] · instantiate only