fix: pattern selection for local lemmas (#6606)

This PR fixes a bug in the pattern selection in the `grind`.
leanprover · Jan 12, 2025 · acad587 · acad587
1 parent 8791a9c
commit acad587
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 6 deletions.
diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
@@ -43,8 +43,8 @@ attribute [grind_norm] not_false_eq_true
 
 -- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
--- @[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
---  by_cases p <;> by_cases q <;> simp [*]
+theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+  by_cases p <;> by_cases q <;> simp [*]
 
 -- And
 @[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -499,7 +499,7 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
-private inductive TheoremKind where
+inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
   deriving Inhabited, BEq
 

diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -51,6 +51,13 @@ private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
   let .fvar fvarId := p | return none
   return some fvarId
 
+/-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/
+private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+  try
+    mkEMatchTheoremWithKind? origin #[] proof kind
+  catch _ =>
+    return none
+
 private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   let proof ← mkEqTrueProof e
   let origin ← if let some fvarId := isEqTrueHyp? proof then
@@ -62,12 +69,12 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   let size := (← get).newThms.size
   let gen ← getGeneration e
   -- TODO: we should have a flag for collecting all unary patterns in a local theorem
-  if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .fwd then
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .fwd then
     activateTheorem thm gen
-  if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .bwd then
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .bwd then
     activateTheorem thm gen
   if (← get).newThms.size == size then
-    if let some thm ← mkEMatchTheoremWithKind? origin #[] proof .default then
+    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
       activateTheorem thm gen
   if (← get).newThms.size == size then
     trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"

diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
@@ -210,3 +210,6 @@ set_option trace.grind.ematch.instance true in
 set_option trace.grind.assert true in
 example (P Q R : α → Prop) (h₁ : ∀ x, Q x → P x) (h₂ : ∀ x, R x → False = (P x)) : Q a → R a → False := by
   grind
+
+example (w : Nat → Type) (h : ∀ n, Subsingleton (w n)) : True := by
+  grind