From 2c87905d77b707c3283c1de759fd63269ac386a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 31 Dec 2024 03:46:09 +0100
Subject: [PATCH] feat: E-matching procedure for the `grind` tactic (#6481)

This PR implements E-matching for the (WIP) `grind` tactic. We still
need to finalize and internalize the new instances.
---
 src/Lean/Meta/Tactic/Grind.lean               |  23 +-
 src/Lean/Meta/Tactic/Grind/Core.lean          |   5 +-
 src/Lean/Meta/Tactic/Grind/EMatch.lean        | 241 ++++++++++++++++++
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean |  31 ++-
 src/Lean/Meta/Tactic/Grind/Internalize.lean   |   6 +-
 src/Lean/Meta/Tactic/Grind/Preprocessor.lean  |  13 +-
 src/Lean/Meta/Tactic/Grind/Proj.lean          |  20 +-
 src/Lean/Meta/Tactic/Grind/Proof.lean         |   8 +-
 src/Lean/Meta/Tactic/Grind/Types.lean         |   6 +
 tests/lean/run/grind_congr1.lean              |   9 +-
 tests/lean/run/grind_ematch1.lean             |  52 ++++
 tests/lean/run/grind_pattern1.lean            |  24 +-
 tests/lean/run/grind_pattern2.lean            |  24 +-
 tests/lean/run/grind_pre.lean                 |  12 +-
 tests/lean/run/grind_t1.lean                  |   8 +
 15 files changed, 404 insertions(+), 78 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Grind/EMatch.lean
 create mode 100644 tests/lean/run/grind_ematch1.lean

diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index 91c6bf6378..f20bb701ea 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -25,18 +25,23 @@ import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean
 
+/-! Trace options for `grind` users -/
 builtin_initialize registerTraceClass `grind
-builtin_initialize registerTraceClass `grind.eq
+builtin_initialize registerTraceClass `grind.assert
+builtin_initialize registerTraceClass `grind.eqc
+builtin_initialize registerTraceClass `grind.internalize
+builtin_initialize registerTraceClass `grind.ematch
+builtin_initialize registerTraceClass `grind.ematch.pattern
+builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.issues
-builtin_initialize registerTraceClass `grind.add
-builtin_initialize registerTraceClass `grind.pre
+builtin_initialize registerTraceClass `grind.simp
+
+/-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
 builtin_initialize registerTraceClass `grind.debug.proofs
-builtin_initialize registerTraceClass `grind.simp
-builtin_initialize registerTraceClass `grind.congr
-builtin_initialize registerTraceClass `grind.proof
-builtin_initialize registerTraceClass `grind.proof.detail
-builtin_initialize registerTraceClass `grind.pattern
-builtin_initialize registerTraceClass `grind.internalize
+builtin_initialize registerTraceClass `grind.debug.congr
+builtin_initialize registerTraceClass `grind.debug.pre
+builtin_initialize registerTraceClass `grind.debug.proof
+builtin_initialize registerTraceClass `grind.debug.proj
 
 end Lean
diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index 06c69ba3b5..58027e02db 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/src/Lean/Meta/Tactic/Grind/Core.lean
@@ -82,13 +82,13 @@ private partial def updateMT (root : Expr) : GoalM Unit := do
       updateMT parent
 
 private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
-  trace[grind.eq] "{lhs} {if isHEq then "≡" else "="} {rhs}"
   let lhsNode ← getENode lhs
   let rhsNode ← getENode rhs
   if isSameExpr lhsNode.root rhsNode.root then
     -- `lhs` and `rhs` are already in the same equivalence class.
     trace[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
     return ()
+  trace[grind.eqc] "{lhs} {if isHEq then "≡" else "="} {rhs}"
   let lhsRoot ← getENode lhsNode.root
   let rhsRoot ← getENode rhsNode.root
   let mut valueInconsistency := false
@@ -195,7 +195,7 @@ def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
 Adds a new `fact` justified by the given proof and using the given generation.
 -/
 def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
-  trace[grind.add] "{proof} : {fact}"
+  trace[grind.assert] "{fact}"
   if (← isInconsistent) then return ()
   resetNewEqs
   let_expr Not p := fact
@@ -203,7 +203,6 @@ def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
   go p true
 where
   go (p : Expr) (isNeg : Bool) : GoalM Unit := do
-    trace[grind.add] "isNeg: {isNeg}, {p}"
     match_expr p with
     | Eq _ lhs rhs => goEq p lhs rhs isNeg false
     | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
new file mode 100644
index 0000000000..a96f107d01
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -0,0 +1,241 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Internalize
+
+namespace Lean.Meta.Grind
+
+/-- Returns maximum term generation that is considered during ematching -/
+private def getMaxGeneration : GoalM Nat := do
+  return 10000 -- TODO
+
+/-- Returns `true` if the maximum number of instances has been reached. -/
+private def checkMaxInstancesExceeded : GoalM Bool := do
+  return false -- TODO
+
+namespace EMatch
+/-! This module implements a simple E-matching procedure as a backtracking search. -/
+
+/-- We represent an `E-matching` problem as a list of constraints. -/
+inductive Cnstr where
+  | /-- Matches pattern `pat` with term `e` -/
+    «match» (pat : Expr) (e : Expr)
+  | /-- This constraint is used to encode multi-patterns. -/
+    «continue» (pat : Expr)
+  deriving Inhabited
+
+/--
+Internal "marker" for representing unassigned elemens in the `assignment` field.
+This is a small hack to avoid one extra level of indirection by using `Option Expr` at `assignment`.
+-/
+private def unassigned : Expr := mkConst (Name.mkSimple "[grind_unassigned]")
+
+private def assignmentToMessageData (assignment : Array Expr) : Array MessageData :=
+  assignment.reverse.map fun e =>
+    if isSameExpr e unassigned then m!"_" else m!"{e}"
+
+/--
+Choice point for the backtracking search.
+The state of the procedure contains a stack of choices.
+-/
+structure Choice where
+  /-- Contraints to be processed. -/
+  cnstrs     : List Cnstr
+  /-- Maximum term generation found so far. -/
+  gen        : Nat
+  /-- Partial assignment so far. Recall that pattern variables are encoded as de-Bruijn variables. -/
+  assignment : Array Expr
+  deriving Inhabited
+
+/-- Theorem instances found so far. We only internalize them after we complete a full round of E-matching. -/
+structure TheoremInstance where
+  prop       : Expr
+  proof      : Expr
+  generation : Nat
+  deriving Inhabited
+
+/-- Context for the E-matching monad. -/
+structure Context where
+  /-- `useMT` is `true` if we are using the mod-time optimization. It is always set to false for new `EMatchTheorem`s. -/
+  useMT : Bool := true
+  /-- `EMatchTheorem` being processed. -/
+  thm   : EMatchTheorem := default
+  deriving Inhabited
+
+/-- State for the E-matching monad -/
+structure State where
+  /-- Choices that still have to be processed. -/
+  choiceStack  : List Choice := []
+  newInstances : PArray TheoremInstance := {}
+  deriving Inhabited
+
+abbrev M := ReaderT Context $ StateRefT State GoalM
+
+def M.run' (x : M α) : GoalM α :=
+  x {} |>.run' {}
+
+/--
+Assigns `bidx := e` in `c`. If `bidx` is already assigned in `c`, we check whether
+`e` and `c.assignment[bidx]` are in the same equivalence class.
+This function assumes `bidx < c.assignment.size`.
+Recall that we initialize the assignment array with the number of theorem parameters.
+-/
+private def assign? (c : Choice) (bidx : Nat) (e : Expr) : OptionT GoalM Choice := do
+  if h : bidx < c.assignment.size then
+    let v := c.assignment[bidx]
+    if isSameExpr v unassigned then
+      return { c with assignment := c.assignment.set bidx e }
+    else
+      guard (← isEqv v e)
+      return c
+  else
+    -- `Choice` was not properly initialized
+    unreachable!
+
+/--
+Returns `true` if the function `pFn` of a pattern is equivalent to the function `eFn`.
+Recall that we ignore universe levels in patterns.
+-/
+private def eqvFunctions (pFn eFn : Expr) : Bool :=
+  (pFn.isFVar && pFn == eFn)
+  || (pFn.isConst && eFn.isConstOf pFn.constName!)
+
+/--
+Matches arguments of pattern `p` with term `e`. Returns `some` if successful,
+and `none` otherwise. It may update `c`s assignment and list of contraints to be
+processed.
+-/
+private partial def matchArgs? (c : Choice) (p : Expr) (e : Expr) : OptionT GoalM Choice := do
+  if !p.isApp then return c -- Done
+  let pArg := p.appArg!
+  let eArg := e.appArg!
+  let goFn c := matchArgs? c p.appFn! e.appFn!
+  if isPatternDontCare pArg then
+    goFn c
+  else if pArg.isBVar then
+    goFn (← assign? c pArg.bvarIdx! eArg)
+  else if let some pArg := groundPattern? pArg then
+    guard (← isEqv pArg eArg)
+    goFn c
+  else
+    goFn { c with cnstrs := .match pArg eArg :: c.cnstrs }
+
+/--
+Matches pattern `p` with term `e` with respect to choice `c`.
+We traverse the equivalence class of `e` looking for applications compatible with `p`.
+For each candidate application, we match the arguments and may update `c`s assignments and contraints.
+We add the updated choices to the choice stack.
+-/
+private partial def processMatch (c : Choice) (p : Expr) (e : Expr) : M Unit := do
+  let maxGeneration ← getMaxGeneration
+  let pFn := p.getAppFn
+  let numArgs := p.getAppNumArgs
+  let mut curr := e
+  repeat
+    let n ← getENode curr
+    if n.generation <= maxGeneration
+       -- uses heterogeneous equality or is the root of its congruence class
+       && (n.heqProofs || isSameExpr curr n.cgRoot)
+       && eqvFunctions pFn curr.getAppFn
+       && curr.getAppNumArgs == numArgs then
+      if let some c ← matchArgs? c p curr |>.run then
+        let gen := n.generation
+        let c := { c with gen := Nat.max gen c.gen }
+        modify fun s => { s with choiceStack := c :: s.choiceStack }
+    curr ← getNext curr
+    if isSameExpr curr e then break
+
+/-- Processes `continue` contraint used to implement multi-patterns. -/
+private def processContinue (c : Choice) (p : Expr) : M Unit := do
+  let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
+    | return ()
+  let maxGeneration ← getMaxGeneration
+  for app in apps do
+    let n ← getENode app
+    if n.generation <= maxGeneration
+       && (n.heqProofs || isSameExpr n.cgRoot app) then
+      if let some c ← matchArgs? c p app |>.run then
+        let gen := n.generation
+        let c := { c with gen := Nat.max gen c.gen }
+        modify fun s => { s with choiceStack := c :: s.choiceStack }
+
+private partial def instantiateTheorem (c : Choice) : M Unit := do
+  trace[grind.ematch.instance] "{(← read).thm.origin.key} : {assignmentToMessageData c.assignment}"
+  -- TODO
+  return ()
+
+/-- Process choice stack until we don't have more choices to be processed. -/
+private partial def processChoices : M Unit := do
+  unless (← get).choiceStack.isEmpty do
+    let c ← modifyGet fun s : State => (s.choiceStack.head!, { s with choiceStack := s.choiceStack.tail! })
+    match c.cnstrs with
+    | [] => instantiateTheorem c
+    | .match p e :: cnstrs => processMatch { c with cnstrs } p e
+    | .continue p :: cnstrs => processContinue { c with cnstrs } p
+    processChoices
+
+private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
+  let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
+    | return ()
+  let numParams  := (← read).thm.numParams
+  let assignment := mkArray numParams unassigned
+  let useMT      := (← read).useMT
+  let gmt        := (← getThe Goal).gmt
+  for app in apps do
+    let n ← getENode app
+    if (n.heqProofs || isSameExpr n.cgRoot app) &&
+       (!useMT || n.mt == gmt) then
+      if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
+        modify fun s => { s with choiceStack := [c] }
+        processChoices
+
+def ematchTheorem (thm : EMatchTheorem) : M Unit := do
+  withReader (fun ctx => { ctx with thm }) do
+    let ps := thm.patterns
+    match ps, (← read).useMT with
+    | [p],   _     => main p []
+    | p::ps, false => main p (ps.map (.continue ·))
+    | _::_,  true  => tryAll ps []
+    | _,     _     => unreachable!
+where
+  /--
+  When using the mod-time optimization with multi-patterns,
+  we must start ematching at each different pattern. That is,
+  if we have `[p₁, p₂, p₃]`, we must execute
+  - `main p₁ [.continue p₂, .continue p₃]`
+  - `main p₂ [.continue p₁, .continue p₃]`
+  - `main p₃ [.continue p₁, .continue p₂]`
+  -/
+  tryAll (ps : List Expr) (cs : List Cnstr) : M Unit := do
+    match ps with
+    | []    => return ()
+    | p::ps =>
+      main p (cs.reverse ++ (ps.map (.continue ·)))
+      tryAll ps (.continue p :: cs)
+
+def ematchTheorems (thms : PArray EMatchTheorem) : M Unit := do
+  thms.forM ematchTheorem
+
+def internalizeNewInstances : M Unit := do
+  -- TODO
+  return ()
+
+end EMatch
+
+open EMatch
+
+/-- Performs one round of E-matching, and internalizes new instances. -/
+def ematch : GoalM Unit := do
+  let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
+    withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
+    withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
+    internalizeNewInstances
+  unless (← checkMaxInstancesExceeded) do
+    go (← get).thms (← get).newThms |>.run'
+    modify fun s => { s with thms := s.thms ++ s.newThms, newThms := {}, gmt := s.gmt + 1 }
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 907883cb86..82f59e81d9 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -125,15 +125,21 @@ private def getPatternFn? (pattern : Expr) : Option Expr :=
     | f@(.fvar _) => some f
     | _ => none
 
-private structure PatternFunInfo where
-  instImplicitMask : Array Bool
-  typeMask : Array Bool
+/--
+Returns a bit-mask `mask` s.t. `mask[i]` is true if the the corresponding argument is
+- a type or type former, or
+- a proof, or
+- an instance implicit argument
 
-private def getPatternFunInfo (f : Expr) (numArgs : Nat) : MetaM PatternFunInfo := do
+When `mask[i]`, we say the corresponding argument is a "support" argument.
+-/
+private def getPatternFunMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
   forallBoundedTelescope (← inferType f) numArgs fun xs _ => do
-    let typeMask ← xs.mapM fun x => isTypeFormer x
-    let instImplicitMask ← xs.mapM fun x => return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
-    return { typeMask, instImplicitMask }
+    xs.mapM fun x => do
+      if (← isTypeFormer x <||> isProof x) then
+        return true
+      else
+        return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
 
 private partial def go (pattern : Expr) (root := false) : M Expr := do
   if root && !pattern.hasLooseBVars then
@@ -143,11 +149,10 @@ private partial def go (pattern : Expr) (root := false) : M Expr := do
   assert! f.isConst || f.isFVar
   saveSymbol f.toHeadIndex
   let mut args := pattern.getAppArgs
-  let { instImplicitMask, typeMask }  ← getPatternFunInfo f args.size
+  let supportMask ← getPatternFunMask f args.size
   for i in [:args.size] do
     let arg := args[i]!
-    let isType := typeMask[i]?.getD false
-    let isInstImplicit := instImplicitMask[i]?.getD false
+    let isSupport := supportMask[i]?.getD false
     let arg ← if !arg.hasLooseBVars then
       if arg.hasMVar then
         pure dontCare
@@ -155,13 +160,13 @@ private partial def go (pattern : Expr) (root := false) : M Expr := do
         pure <| mkGroundPattern arg
     else match arg with
       | .bvar idx =>
-        if (isType || isInstImplicit) && (← foundBVar idx) then
+        if isSupport && (← foundBVar idx) then
           pure dontCare
         else
           saveBVar idx
           pure arg
       | _ =>
-        if isType || isInstImplicit then
+        if isSupport then
           pure dontCare
         else if let some _ := getPatternFn? arg then
           go arg
@@ -305,7 +310,7 @@ def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr)
   let proof := mkConst declName us
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
   assert! symbols.all fun s => s matches .const _
-  trace[grind.pattern] "{declName}: {patterns.map ppPattern}"
+  trace[grind.ematch.pattern] "{declName}: {patterns.map ppPattern}"
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"
      throwError "invalid pattern(s) for `{declName}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 99c35a8b92..341e2b7e50 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -22,7 +22,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do
       unless (← hasSameType f g) do
         trace[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
         return ()
-    trace[grind.congr] "{e} = {e'}"
+    trace[grind.debug.congr] "{e} = {e'}"
     pushEqHEq e e' congrPlaceholderProof
     let node ← getENode e
     setENode e { node with cgRoot := e' }
@@ -59,11 +59,11 @@ private partial def activateTheoremPatterns (fName : Name) (generation : Nat) :
       let thm := { thm with symbols }
       match symbols with
       | [] =>
-        trace[grind.pattern] "activated `{thm.origin.key}`"
         let thm := { thm with patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
+        trace[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
         modify fun s => { s with newThms := s.newThms.push thm }
       | _ =>
-        trace[grind.pattern] "reinsert `{thm.origin.key}`"
+        trace[grind.ematch] "reinsert `{thm.origin.key}`"
         modify fun s => { s with thmMap := s.thmMap.insert thm }
 
 partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
diff --git a/src/Lean/Meta/Tactic/Grind/Preprocessor.lean b/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
index 2e663fb59d..c8ebf593a1 100644
--- a/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
+++ b/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
@@ -18,6 +18,7 @@ import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Run
+import Lean.Meta.Tactic.Grind.EMatch
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -122,13 +123,14 @@ partial def loop (goal : Goal) : PreM Unit := do
     else
       loop goal
 
-def ppGoals : PreM Format := do
+def ppGoals (goals : PArray Goal) : PreM Format := do
   let mut r := f!""
-  for goal in (← get).goals do
+  for goal in goals do
     let (f, _) ← GoalM.run goal ppState
     r := r ++ Format.line ++ f
   return r
 
+-- TODO: refactor this code
 def preprocess (mvarId : MVarId) : PreM State := do
   mvarId.ensureProp
   -- TODO: abstract metavars
@@ -140,9 +142,12 @@ def preprocess (mvarId : MVarId) : PreM State := do
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   loop (← mkGoal mvarId)
+  let goals := (← get).goals
+  -- Testing `ematch` module here. We will rewrite this part later.
+  let goals ← goals.mapM fun goal => GoalM.run' goal ematch
   if (← isTracingEnabledFor `grind.pre) then
-    trace[grind.pre] (← ppGoals)
-  for goal in (← get).goals do
+    trace[grind.debug.pre] (← ppGoals goals)
+  for goal in goals do
     discard <| GoalM.run' goal <| checkInvariants (expensive := true)
   get
 
diff --git a/src/Lean/Meta/Tactic/Grind/Proj.lean b/src/Lean/Meta/Tactic/Grind/Proj.lean
index b742642b2f..d9bcb2de28 100644
--- a/src/Lean/Meta/Tactic/Grind/Proj.lean
+++ b/src/Lean/Meta/Tactic/Grind/Proj.lean
@@ -19,17 +19,21 @@ def propagateProjEq (parent : Expr) : GoalM Unit := do
   let .const declName _ := parent.getAppFn | return ()
   let some info ← getProjectionFnInfo? declName | return ()
   unless info.numParams + 1 == parent.getAppNumArgs do return ()
+  -- It is wasteful to add equation if `parent` is not the root of its congruence class
+  unless (← isCongrRoot parent) do return ()
   let arg := parent.appArg!
   let ctor ← getRoot arg
   unless ctor.isAppOf info.ctorName do return ()
-  if isSameExpr arg ctor then
-    let idx := info.numParams + info.i
-    unless idx < ctor.getAppNumArgs do return ()
-    let v := ctor.getArg! idx
-    pushEq parent v (← mkEqRefl v)
+  let parentNew ← if isSameExpr arg ctor then
+    pure parent
   else
-    let newProj := mkApp parent.appFn! ctor
-    let newProj ← shareCommon newProj
-    internalize newProj (← getGeneration parent)
+    let parentNew ← shareCommon (mkApp parent.appFn! ctor)
+    internalize parentNew (← getGeneration parent)
+    pure parentNew
+  trace[grind.debug.proj] "{parentNew}"
+  let idx := info.numParams + info.i
+  unless idx < ctor.getAppNumArgs do return ()
+  let v := ctor.getArg! idx
+  pushEq parentNew v (← mkEqRefl v)
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Proof.lean b/src/Lean/Meta/Tactic/Grind/Proof.lean
index 5887f83ffd..9b8cbcbd45 100644
--- a/src/Lean/Meta/Tactic/Grind/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Proof.lean
@@ -217,20 +217,20 @@ It assumes `a` and `b` are in the same equivalence class.
 @[export lean_grind_mk_eq_proof]
 def mkEqProofImpl (a b : Expr) : GoalM Expr := do
   let p ← go
-  trace[grind.proof.detail] "{p}"
+  trace[grind.debug.proof] "{p}"
   return p
 where
   go : GoalM Expr := do
     let n ← getRootENode a
     if !n.heqProofs then
-      trace[grind.proof] "{a} = {b}"
+      trace[grind.debug.proof] "{a} = {b}"
       mkEqProofCore a b (heq := false)
     else
       if (← hasSameType a b) then
-        trace[grind.proof] "{a} = {b}"
+        trace[grind.debug.proof] "{a} = {b}"
         mkEqOfHEq (← mkEqProofCore a b (heq := true))
       else
-        trace[grind.proof] "{a} ≡ {b}"
+        trace[grind.debug.proof] "{a} ≡ {b}"
         mkEqProofCore a b (heq := true)
 
 def mkHEqProof (a b : Expr) : GoalM Expr :=
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 0342646871..438f665bd4 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -283,6 +283,8 @@ structure Goal where
   Local theorem provided by users are added directly into `newThms`.
   -/
   thmMap       : EMatchTheorems
+  /-- Number of theorem instances generated so far -/
+  numInstances : Nat := 0
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -465,6 +467,10 @@ def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
   let interpreted ← isInterpreted e
   mkENodeCore e interpreted ctor generation
 
+/-- Returns `true` is `e` is the root of its congruence class. -/
+def isCongrRoot (e : Expr) : GoalM Bool := do
+  return isSameExpr e (← getENode e).cgRoot
+
 /-- Return `true` if the goal is inconsistent. -/
 def isInconsistent : GoalM Bool :=
   return (← get).inconsistent
diff --git a/tests/lean/run/grind_congr1.lean b/tests/lean/run/grind_congr1.lean
index 6d5c76d55b..d1faacb568 100644
--- a/tests/lean/run/grind_congr1.lean
+++ b/tests/lean/run/grind_congr1.lean
@@ -67,18 +67,15 @@ end Ex2
 example (f g : (α : Type) → α → α) (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → (h₃ : f = g) → HEq (f α a) (g β b) := by
   grind
 
-set_option trace.grind.proof true in
-set_option trace.grind.proof.detail true in
+set_option trace.grind.debug.proof true in
 example (f : {α : Type} → α → Nat → Bool → Nat) (a b : Nat) : f a 0 true = v₁ → f b 0 true = v₂ → a = b → v₁ = v₂ := by
   grind
 
-set_option trace.grind.proof true in
-set_option trace.grind.proof.detail true in
+set_option trace.grind.debug.proof true in
 example (f : {α : Type} → α → Nat → Bool → Nat) (a b : Nat) : f a b x = v₁ → f a b y = v₂ → x = y → v₁ = v₂ := by
   grind
 
-set_option trace.grind.proof true in
-set_option trace.grind.proof.detail true in
+set_option trace.grind.debug.proof true in
 theorem ex1 (f : {α : Type} → α → Nat → Bool → Nat) (a b c : Nat) : f a b x = v₁ → f c b y = v₂ → a = c → x = y → v₁ = v₂ := by
   grind
 
diff --git a/tests/lean/run/grind_ematch1.lean b/tests/lean/run/grind_ematch1.lean
new file mode 100644
index 0000000000..20c9a0c340
--- /dev/null
+++ b/tests/lean/run/grind_ematch1.lean
@@ -0,0 +1,52 @@
+set_option trace.grind.ematch.pattern true
+grind_pattern Array.get_set_eq  => a.set i v h
+grind_pattern Array.get_set_ne => (a.set i v hi)[j]
+
+-- Trace instances of the theorems above found using ematching
+
+set_option trace.grind.ematch.instance true
+
+/--
+info: [grind.ematch.instance] Array.get_set_eq : [α, bs, j, w, Lean.Grind.nestedProof (j < bs.toList.length) h₂]
+[grind.ematch.instance] Array.get_set_eq : [α, as, i, v, Lean.Grind.nestedProof (i < as.toList.length) h₁]
+[grind.ematch.instance] Array.get_set_ne : [α, bs, j, Lean.Grind.nestedProof (j < bs.toList.length) h₂, i, w, _, _]
+-/
+#guard_msgs (info) in
+example (as : Array α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        (_  : ds = bs)
+        (h₂ : j < bs.size)
+        (h₃ : cs = bs.set j w)
+        (h₄ : i ≠ j)
+        (h₅ : i < cs.size)
+        : p ↔ (cs[i] = as[i]) := by
+  fail_if_success grind
+  sorry
+
+opaque R : Nat → Nat → Prop
+theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry
+
+grind_pattern Rtrans => R a b, R b c
+
+/--
+info: [grind.ematch.instance] Rtrans : [b, c, d, _, _]
+[grind.ematch.instance] Rtrans : [a, b, c, _, _]
+-/
+#guard_msgs (info) in
+example : R a b → R b c → R c d → False := by
+  fail_if_success grind
+  sorry
+
+-- In the following test we are performing one round of ematching only
+/--
+info: [grind.ematch.instance] Rtrans : [c, d, e, _, _]
+[grind.ematch.instance] Rtrans : [c, d, n, _, _]
+[grind.ematch.instance] Rtrans : [b, c, d, _, _]
+[grind.ematch.instance] Rtrans : [a, b, c, _, _]
+-/
+#guard_msgs (info) in
+example : R a b → R b c → R c d → R d e → R d n → False := by
+  fail_if_success grind
+  sorry
diff --git a/tests/lean/run/grind_pattern1.lean b/tests/lean/run/grind_pattern1.lean
index 0eb1750bdc..5ca785dac1 100644
--- a/tests/lean/run/grind_pattern1.lean
+++ b/tests/lean/run/grind_pattern1.lean
@@ -1,20 +1,18 @@
-set_option trace.grind.pattern true
+set_option trace.grind.ematch.pattern true
 
 /--
-info: [grind.pattern] Array.getElem_push_lt: [@getElem ? `[Nat] #4 ? ? (@Array.push ? #3 #2) #1 ?]
+info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem ? `[Nat] #4 ? ? (@Array.push ? #3 #2) #1 ?]
 -/
 #guard_msgs in
 grind_pattern Array.getElem_push_lt => (a.push x)[i]
 
 
-/--
-info: [grind.pattern] List.getElem_attach: [@getElem ? `[Nat] ? ? ? (@List.attach #3 #2) #1 ?]
--/
+/-- info: [grind.ematch.pattern] List.getElem_attach: [@getElem ? `[Nat] ? ? ? (@List.attach #3 #2) #1 ?] -/
 #guard_msgs in
 grind_pattern List.getElem_attach => xs.attach[i]
 
 /--
-info: [grind.pattern] List.mem_concat_self: [@Membership.mem #2 ? ? (@HAppend.hAppend ? ? ? ? #1 (@List.cons ? #0 (@List.nil ?))) #0]
+info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 ? ? (@HAppend.hAppend ? ? ? ? #1 (@List.cons ? #0 (@List.nil ?))) #0]
 -/
 #guard_msgs in
 grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
@@ -34,7 +32,7 @@ the following theorem parameters cannot be instantiated:
   i : Nat
   h : i < a.size
 ---
-info: [grind.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2]
+info: [grind.ematch.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2]
 -/
 #guard_msgs in
 grind_pattern Array.getElem_push_lt => (a.push x)
@@ -56,13 +54,13 @@ instance [Boo α β] : Boo (List α) (Array β) where
 
 theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl
 
-/-- info: [grind.pattern] fEq: [@f ? ? ? ? #0] -/
+/-- info: [grind.ematch.pattern] fEq: [@f ? ? ? ? #0] -/
 #guard_msgs in
 grind_pattern fEq => f a
 
 theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl
 
-/-- info: [grind.pattern] fEq2: [@f ? ? ? ? #1] -/
+/-- info: [grind.ematch.pattern] fEq2: [@f ? ? ? ? #1] -/
 #guard_msgs in
 grind_pattern fEq2 => f a
 
@@ -78,7 +76,7 @@ the following theorem parameters cannot be instantiated:
   β : Type
   inst✝ : Boo α β
 ---
-info: [grind.pattern] gEq: [@g ? ? ? #0]
+info: [grind.ematch.pattern] gEq: [@g ? ? ? #0]
 -/
 #guard_msgs in
 grind_pattern gEq => g a
@@ -94,7 +92,7 @@ error: invalid pattern(s) for `hThm1`
 the following theorem parameters cannot be instantiated:
   c : Nat
 ---
-info: [grind.pattern] hThm1: [plus #2 #3]
+info: [grind.ematch.pattern] hThm1: [plus #2 #3]
 -/
 #guard_msgs in
 grind_pattern hThm1 => plus a b
@@ -106,11 +104,11 @@ the following theorem parameters cannot be instantiated:
   b : Nat
   h : b > 10
 ---
-info: [grind.pattern] hThm1: [plus #2 #1]
+info: [grind.ematch.pattern] hThm1: [plus #2 #1]
 -/
 #guard_msgs in
 grind_pattern hThm1 => plus a c
 
-/-- info: [grind.pattern] hThm1: [plus #2 #1, plus #2 #3] -/
+/-- info: [grind.ematch.pattern] hThm1: [plus #2 #1, plus #2 #3] -/
 #guard_msgs in
 grind_pattern hThm1 => plus a c, plus a b
diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean
index f8e696a136..647c917ece 100644
--- a/tests/lean/run/grind_pattern2.lean
+++ b/tests/lean/run/grind_pattern2.lean
@@ -13,12 +13,13 @@ grind_pattern contains_insert => contains (insertElem s a) a
 
 -- TheoremPattern activation test
 
-set_option trace.grind.pattern true
+set_option trace.grind.ematch true
+set_option trace.grind.ematch.pattern true
 
 /--
 warning: declaration uses 'sorry'
 ---
-info: [grind.pattern] activated `contains_insert`
+info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem ? #2 #1 #0) #0]
 -/
 #guard_msgs in
 example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
@@ -29,8 +30,8 @@ example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
 /--
 warning: declaration uses 'sorry'
 ---
-info: [grind.pattern] reinsert `contains_insert`
-[grind.pattern] activated `contains_insert`
+info: [grind.ematch] reinsert `contains_insert`
+[grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem ? #2 #1 #0) #0]
 -/
 #guard_msgs in
 example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
@@ -44,9 +45,7 @@ def foo (x : List Nat) (y : List Nat) := x ++ y ++ x
 
 theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl
 
-/--
-info: [grind.pattern] fooThm: [foo #0 `[[a, b]]]
--/
+/-- info: [grind.ematch.pattern] fooThm: [foo #0 `[[a, b]]] -/
 #guard_msgs in
 grind_pattern fooThm => foo x [a, b]
 
@@ -55,13 +54,13 @@ grind_pattern fooThm => foo x [a, b]
 warning: declaration uses 'sorry'
 ---
 info: [grind.internalize] foo x y
-[grind.pattern] activated `fooThm`
 [grind.internalize] [a, b]
 [grind.internalize] Nat
 [grind.internalize] a
 [grind.internalize] [b]
 [grind.internalize] b
 [grind.internalize] []
+[grind.ematch] activated `fooThm`, [foo #0 `[[a, b]]]
 [grind.internalize] x
 [grind.internalize] y
 [grind.internalize] z
@@ -71,3 +70,12 @@ set_option trace.grind.internalize true in
 example : foo x y = z → False := by
   fail_if_success grind
   sorry
+
+theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[i]+as[j] = as[i] + as[i] := by sorry
+
+
+/--
+info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 ? ? ? (@getElem ? `[Nat] ? ? ? #2 #5 ?) (@getElem ? `[Nat] ? ? ? #2 #4 ?)]
+-/
+#guard_msgs in
+grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁)
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index eec23c849b..e43acfa05c 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -74,13 +74,12 @@ theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x :=
 
 def h (a : α) := a
 
-set_option trace.grind.pre true in
+set_option trace.grind.debug.pre true in
 example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c ∧ c = a → a = b ∧ b = a → a = c := by
   grind
 
-set_option trace.grind.proof.detail true
-set_option trace.grind.proof true
-set_option trace.grind.pre true
+set_option trace.grind.debug.proof true
+set_option trace.grind.debug.pre true
 /--
 error: `grind` failed
 α : Type
@@ -112,9 +111,8 @@ info: [grind.issues] found congruence between
 -/
 #guard_msgs in
 set_option trace.grind.issues true in
-set_option trace.grind.proof.detail false in
-set_option trace.grind.proof false in
-set_option trace.grind.pre false in
+set_option trace.grind.debug.proof false in
+set_option trace.grind.debug.pre false in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
   fail_if_success grind
   sorry
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 59f8749a87..4bf739a213 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -75,3 +75,11 @@ example (a b c : Nat) (f : Nat → Nat) : p = { a := f b, c, b := 4 : Boo Nat }
 
 example (a b c : Nat) (f : Nat → Nat) : p.1 ≠ f a → p = { a := f b, c, b := 4 : Boo Nat } → f b = f c → a = c → False := by
   grind
+
+/--
+info: [grind.debug.proj] { a := b, b := v₁, c := v₂ }.a
+-/
+#guard_msgs (info) in
+set_option trace.grind.debug.proj true in
+example (a b d e : Nat) (x y z : Boo Nat) (f : Nat → Boo Nat) : (f d).1 ≠ a → f d = ⟨b, v₁, v₂⟩ → x.1 = e → y.1 = e → z.1 = e → f d = x → f d = y → f d = z → b = a → False := by
+  grind