From 0afa1d1e5dda3cfedd4a847421271fef64e9743c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 8 Jan 2025 13:37:29 -0800
Subject: [PATCH] feat: apply E-matching for local lemmas in `grind` (#6582)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds support for creating local E-matching theorems for
universal propositions known to be true. It allows `grind` to
automatically solve examples such as:

```lean
example (b : List α) (p : α → Prop) (h₁ : ∀ a ∈ b, p a) (h₂ : ∃ a ∈ b, ¬p a) : False := by
  grind
```
---
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean |  9 +++--
 src/Lean/Meta/Tactic/Grind/ForallProp.lean    | 29 +++++++++++++++
 src/Lean/Meta/Tactic/Grind/Internalize.lean   |  2 +-
 src/Lean/Meta/Tactic/Grind/Types.lean         |  2 +
 tests/lean/run/grind_t1.lean                  | 37 +++++++++++++++++++
 5 files changed, 74 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 96e6b069018..1170a8dffa8 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -57,7 +57,8 @@ inductive Origin where
   is the provided grind argument. The `id` is a unique identifier for the call.
   -/
   | stx (id : Name) (ref : Syntax)
-  | other (id : Name)
+  /-- It is local, but we don't have a local hypothesis for it. -/
+  | local (id : Name)
   deriving Inhabited, Repr, BEq
 
 /-- A unique identifier corresponding to the origin. -/
@@ -65,14 +66,14 @@ def Origin.key : Origin → Name
   | .decl declName => declName
   | .fvar fvarId   => fvarId.name
   | .stx id _      => id
-  | .other id      => id
+  | .local id      => id
 
 def Origin.pp [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData := do
   match o with
   | .decl declName => return MessageData.ofConst (← mkConstWithLevelParams declName)
   | .fvar fvarId   => return mkFVar fvarId
   | .stx _ ref     => return ref
-  | .other id      => return id
+  | .local id      => return id
 
 instance : BEq Origin where
   beq a b := a.key == b.key
@@ -598,7 +599,7 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
     | return none
   return some (ps, s.symbols.toList)
 
-private def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
     return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := true))
   else if kind == .eqRhs then
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index 04d49e88a62..b8be9355c7f 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -46,6 +46,32 @@ where
       -- b = True → (a → b) = True
       pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
 
+private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
+  let_expr eq_true _ p := proof | return none
+  let .fvar fvarId := p | return none
+  return some fvarId
+
+private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
+  let proof ← mkEqTrueProof e
+  let origin ← if let some fvarId := isEqTrueHyp? proof then
+    pure <| .fvar fvarId
+  else
+    let idx ← modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
+    pure <| .local ((`local).appendIndexAfter idx)
+  let proof := mkApp2 (mkConst ``of_eq_true) e proof
+  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
+    activateTheorem thm gen
+  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
+      activateTheorem thm gen
+  if (← get).newThms.size == size then
+    trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"
+
 def propagateForallPropDown (e : Expr) : GoalM Unit := do
   let .forallE n a b bi := e | return ()
   if (← isEqFalse e) then
@@ -62,5 +88,8 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       let h ← mkEqFalseProof e
       pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
       pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
+  else if (← isEqTrue e) then
+    if b.hasLooseBVars then
+      addLocalEMatchTheorems e
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 980aca39772..eaaf18f107e 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -101,7 +101,7 @@ private partial def internalizePattern (pattern : Expr) (generation : Nat) : Goa
   else pattern.withApp fun f args => do
     return mkAppN f (← args.mapM (internalizePattern · generation))
 
-private partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
   -- Recall that we use the proof as part of the key for a set of instances found so far.
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 3665bece75a..50e072162a6 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -393,6 +393,8 @@ structure Goal where
   numSplits : Nat := 0
   /-- Case-splits that do not have to be performed anymore. -/
   resolvedSplits : PHashSet ENodeKey := {}
+  /-- Next local E-match theorem idx. -/
+  nextThmIdx : Nat := 0
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 9c75284afdf..3bf2a21185e 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -173,3 +173,40 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
         (h₄ : b₁ = b₂)
         : HEq a₂ b₂ := by
   grind
+
+/--
+info: [grind.assert] ∀ (a : α), a ∈ b → p a
+[grind.ematch.pattern] h₁: [@Membership.mem `[α] `[List α] `[List.instMembership] `[b] #1]
+[grind.ematch.pattern] h₁: [p #1]
+[grind.assert] w ∈ b
+[grind.assert] ¬p w
+[grind.ematch.instance] h₁: w ∈ b → p w
+[grind.assert] w ∈ b → p w
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.pattern true in
+set_option trace.grind.ematch.instance true in
+set_option trace.grind.assert true in
+example (b : List α) (p : α → Prop) (h₁ : ∀ a ∈ b, p a) (h₂ : ∃ a ∈ b, ¬p a) : False := by
+  grind
+
+/--
+info: [grind.assert] ∀ (x : α), Q x → P x
+[grind.ematch.pattern] h₁: [Q #1]
+[grind.ematch.pattern] h₁: [P #1]
+[grind.assert] ∀ (x : α), R x → False = P x
+[grind.ematch.pattern] h₂: [R #1]
+[grind.ematch.pattern] h₂: [P #1]
+[grind.assert] Q a
+[grind.assert] R a
+[grind.ematch.instance] h₁: Q a → P a
+[grind.ematch.instance] h₂: R a → False = P a
+[grind.assert] Q a → P a
+[grind.assert] R a → False = P a
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.pattern true in
+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