From ef759d874f079b8454469ffb51c2df101d520c69 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 16 Feb 2025 14:30:04 -0800
Subject: [PATCH] fix: `grind` using `reducible` transparency setting (#7102)

This PR modifies `grind` to run with the `reducible` transparency
setting. We do not want `grind` to unfold arbitrary terms during
definitional equality tests. This PR also fixes several issues
introduced by this change. The most common problem was the lack of a
hint in proofs, particularly in those constructed using proof by
reflection. This PR also introduces new sanity checks when `set_option
grind.debug true` is used.
---
 src/Init/Grind/Util.lean                      | 16 ++++-
 src/Lean/Meta/AppBuilder.lean                 |  7 +-
 .../Meta/Tactic/Grind/Arith/Offset/Main.lean  |  4 +-
 src/Lean/Meta/Tactic/Grind/CasesMatch.lean    |  2 +-
 src/Lean/Meta/Tactic/Grind/EMatch.lean        |  9 ++-
 src/Lean/Meta/Tactic/Grind/EqResolution.lean  | 25 ++++++-
 src/Lean/Meta/Tactic/Grind/Intro.lean         |  8 ++-
 src/Lean/Meta/Tactic/Grind/Main.lean          |  2 +-
 src/Lean/Meta/Tactic/Grind/MatchCond.lean     | 30 ++------
 .../Meta/Tactic/Grind/MatchDiscrOnly.lean     | 22 ++++--
 src/Lean/Meta/Tactic/Grind/Proof.lean         |  4 +-
 src/Lean/Meta/Tactic/Grind/Simp.lean          |  7 +-
 src/Lean/Meta/Tactic/Grind/SimpUtil.lean      |  2 +-
 src/Lean/Meta/Tactic/Grind/Types.lean         | 11 ++-
 src/Lean/Meta/Tactic/Grind/Util.lean          | 70 ++++++++++++++++++-
 src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean |  6 +-
 src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean |  6 +-
 tests/lean/run/grind_ematch2.lean             | 22 +++---
 .../lean/run/grind_match_eq_propagation.lean  |  1 +
 19 files changed, 189 insertions(+), 65 deletions(-)

diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
index e79b07c235..adbb7b05db 100644
--- a/src/Init/Grind/Util.lean
+++ b/src/Init/Grind/Util.lean
@@ -14,6 +14,12 @@ def nestedProof (p : Prop) {h : p} : p := h
 /--
 Gadget for marking `match`-expressions that should not be reduced by the `grind` simplifier, but the discriminants should be normalized.
 We use it when adding instances of `match`-equations to prevent them from being simplified to true.
+
+Remark: it must not be marked as `[reducible]`. Otherwise, `simp` will reduce
+```
+simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
+```
+using `eq_self`.
 -/
 def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
 
@@ -28,7 +34,7 @@ Gadget for annotating the equalities in `match`-equations conclusions.
 `_origin` is the term used to instantiate the `match`-equation using E-matching.
 When `EqMatch a b origin` is `True`, we mark `origin` as a resolved case-split.
 -/
-def EqMatch (a b : α) {_origin : α} : Prop := a = b
+abbrev EqMatch (a b : α) {_origin : α} : Prop := a = b
 
 /--
 Gadget for annotating conditions of `match` equational lemmas.
@@ -36,7 +42,13 @@ We use this annotation for two different reasons:
 - We don't want to normalize them.
 - We have a propagator for them.
 -/
-def MatchCond (p : Prop) : Prop := p
+abbrev MatchCond (p : Prop) : Prop := p
+
+/--
+Similar to `MatchCond`, but not reducible. We use it to ensure `simp`
+will not eliminate it. After we apply `simp`, we replace it with `MatchCond`.
+-/
+def PreMatchCond (p : Prop) : Prop := p
 
 theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq) := by
   subst h; apply HEq.refl
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 26d333ee79..a80e489b80 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -165,12 +165,13 @@ def mkHEqTrans (h₁ h₂ : Expr) : MetaM Expr := do
     | _, none => throwAppBuilderException ``HEq.trans ("heterogeneous equality proof expected" ++ hasTypeMsg h₂ hType₂)
 
 /-- Given `h : HEq a b` where `a` and `b` have the same type, returns a proof of `Eq a b`. -/
-def mkEqOfHEq (h : Expr) : MetaM Expr := do
+def mkEqOfHEq (h : Expr) (check := true) : MetaM Expr := do
   let hType ← infer h
   match hType.heq? with
   | some (α, a, β, b) =>
-    unless (← isDefEq α β) do
-      throwAppBuilderException ``eq_of_heq m!"heterogeneous equality types are not definitionally equal{indentExpr α}\nis not definitionally equal to{indentExpr β}"
+    if check then
+      unless (← isDefEq α β) do
+        throwAppBuilderException ``eq_of_heq m!"heterogeneous equality types are not definitionally equal{indentExpr α}\nis not definitionally equal to{indentExpr β}"
     let u ← getLevel α
     return mkApp4 (mkConst ``eq_of_heq [u]) α a b h
   | _ =>
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean
index 6867e3ded4..360afb8033 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean
@@ -233,6 +233,7 @@ def Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr := do
     return mkNatLE u (mkNatAdd v (Lean.toExpr c.k.toNat))
 
 def checkInvariants : GoalM Unit := do
+  unless (← isInconsistent) do
   let s ← get'
   for u in [:s.targets.size], es in s.targets.toArray do
     for (v, k) in es do
@@ -242,8 +243,7 @@ def checkInvariants : GoalM Unit := do
       trace[grind.debug.offset.proof] "{p} : {← inferType p}"
       check p
       unless (← withDefault <| isDefEq (← inferType p) (← Cnstr.toExpr c)) do
-        trace[grind.debug.offset.proof] "failed: {← inferType p} =?= {← Cnstr.toExpr c}"
-        unreachable!
+        throwError "`grind` internal error in the offset constraint module, constraint{indentExpr (← Cnstr.toExpr c)}\nis not definitionally equal to type of its proof{indentExpr (← inferType p)}"
 
 /--
 Adds an edge `u --(k) --> v` justified by the proof term `p`, and then
diff --git a/src/Lean/Meta/Tactic/Grind/CasesMatch.lean b/src/Lean/Meta/Tactic/Grind/CasesMatch.lean
index 31b9681d75..45c9644af2 100644
--- a/src/Lean/Meta/Tactic/Grind/CasesMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/CasesMatch.lean
@@ -23,7 +23,7 @@ conditions corresponding to overlapping patterns.
 private def addMatchCondsToAlt (alt : Expr) : Expr := Id.run do
   let .forallE _ d b _ := alt
     | return alt
-  let d := if isMatchCondCandidate d then markAsMatchCond d else d
+  let d := if isMatchCondCandidate d then markAsPreMatchCond d else d
   return alt.updateForallE! d (addMatchCondsToAlt b)
 
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 69cfedad27..9fe3ed8915 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -218,7 +218,7 @@ Annotate the conditions using `Grind.MatchCond`. See `MatchCond.lean`.
 private partial def annotateEqnTypeConds (prop : Expr) (k : Expr → M Expr := pure) : M Expr := do
   if let .forallE n d b bi := prop then
     let d := if (← isProp d) then
-      markAsMatchCond d
+      markAsPreMatchCond d
     else
       d
     withLocalDecl n bi d fun x => do
@@ -247,10 +247,17 @@ private def addNewInstance (thm : EMatchTheorem) (proof : Expr) (generation : Na
   if grind.debug.proofs.get (← getOptions) then
     check proof
   let mut prop ← inferType proof
+  let mut proof := proof
   if Match.isMatchEqnTheorem (← getEnv) thm.origin.key then
     prop ← annotateMatchEqnType prop (← read).initApp
+    -- We must add a hint here because `annotateMatchEqnType` introduces `simpMatchDiscrsOnly` and
+    -- `Grind.PreMatchCond` which are not reducible.
+    proof ← mkExpectedTypeHint proof prop
   else if (← isEqnThm thm.origin.key) then
     prop ← annotateEqnTypeConds prop
+    -- We must add a hint because `annotateEqnTypeConds` introduces `Grind.PreMatchCond`
+    -- which is not reducible.
+    proof ← mkExpectedTypeHint proof prop
   trace_goal[grind.ematch.instance] "{← thm.origin.pp}: {prop}"
   addTheoremInstance thm proof prop (generation+1)
 
diff --git a/src/Lean/Meta/Tactic/Grind/EqResolution.lean b/src/Lean/Meta/Tactic/Grind/EqResolution.lean
index 7bd3409f61..b7a4c07064 100644
--- a/src/Lean/Meta/Tactic/Grind/EqResolution.lean
+++ b/src/Lean/Meta/Tactic/Grind/EqResolution.lean
@@ -5,12 +5,35 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.AppBuilder
+import Lean.Meta.MatchUtil
 
 namespace Lean.Meta.Grind
 /-! A basic "equality resolution" procedure. -/
 
-private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := withNewMCtxDepth do
+/--
+Similar to `forallMetaTelescopeReducing`, but if `prop` resulting type is of the form `¬ p`, it will "convert" it so `p → False`, and
+will return a hypothesis for it and return `False` as the resulting type.
+-/
+private def forallMetaTelescopeReducingAndUnfoldingNot (prop : Expr) : MetaM (Array Expr × Expr) := do
   let (ms, _, type) ← forallMetaTelescopeReducing prop
+  if let some p ← matchNot? type then
+    let m ← mkFreshExprMVar p
+    return (ms.push m, mkConst ``False)
+  return (ms, type)
+
+private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := withNewMCtxDepth do
+  /-
+  We use `forallMetaTelescopeReducingAndUnfoldingNot` because we want to treat
+  ```
+  ∀ x, ¬ f x = f a
+  ```
+  as
+  ```
+  ∀ x, f x = f a → False
+  ```
+  recall that `¬` is not reducible.
+  -/
+  let (ms, type) ← forallMetaTelescopeReducingAndUnfoldingNot prop
   if ms.isEmpty then return none
   let mut progress := false
   for m in ms do
diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean
index 5fcffff25a..a0b1e5271a 100644
--- a/src/Lean/Meta/Tactic/Grind/Intro.lean
+++ b/src/Lean/Meta/Tactic/Grind/Intro.lean
@@ -31,7 +31,7 @@ We added this feature because it may be coming from external sources
 -/
 private def preprocessHypothesis (e : Expr) : GoalM Simp.Result := do
   if isMatchCondCandidate e then
-    preprocess (markAsMatchCond e)
+    preprocess (markAsPreMatchCond e)
   else
     preprocess e
 
@@ -141,7 +141,11 @@ private def isEagerCasesCandidate (goal : Goal) (type : Expr) : Bool := Id.run d
   return goal.split.casesTypes.isEagerSplit declName
 
 private def applyCases? (goal : Goal) (fvarId : FVarId) : GrindM (Option (List Goal)) := goal.mvarId.withContext do
-  let type ← whnfD (← fvarId.getType)
+  /-
+  Remark: we used to use `whnfD`. This was a mistake, we don't want to unfold user-defined abstractions.
+  Example: `a ∣ b` is defined as `∃ x, b = a * x`
+  -/
+  let type ← whnf (← fvarId.getType)
   if isEagerCasesCandidate goal type then
     if let .const declName _ := type.getAppFn then
       saveCases declName true
diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean
index ef21c42708..81439377cb 100644
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@@ -153,7 +153,7 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
   return MessageData.joinSep msgs m!"\n"
 
 def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
-  let go : GrindM Result := do
+  let go : GrindM Result := withReducible do
     let goals ← initCore mvarId params
     let (failures, skipped) ← solve goals fallback
     trace[grind.debug.final] "{← ppGoals goals}"
diff --git a/src/Lean/Meta/Tactic/Grind/MatchCond.lean b/src/Lean/Meta/Tactic/Grind/MatchCond.lean
index 51587be182..e818d5d8d8 100644
--- a/src/Lean/Meta/Tactic/Grind/MatchCond.lean
+++ b/src/Lean/Meta/Tactic/Grind/MatchCond.lean
@@ -7,7 +7,6 @@ prelude
 import Init.Grind
 import Init.Simproc
 import Lean.Meta.Tactic.Contradiction
-import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 
@@ -65,8 +64,11 @@ In the two equational theorems above, we have the following conditions.
 - `(∀ (b_1 c : S), b = S.mk2 1 (b_1.mk4 c) → False)`
 - `(∀ (a_1 : Bool) (b_1 c : S), a = S.mk3 a_1 → b = b_1.mk4 c → False)`
 ```
-When instantiating the equations (and `match`-splitter), we wrap the conditions with the gadget `Grind.MatchCond`.
-This gadget is used for implementing truth-value propagation. See the propagator `propagateMatchCond` below.
+When instantiating the equations (and `match`-splitter), we wrap the conditions with the gadget `Grind.PreMatchCond`.
+`Grind.PreMatchCond` uses the default reducibility setting and cannot be accidentally reduced by `simp`.
+After `simp` is applied, it is replaced with `Grind.MatchCond` which is reducible.
+This `Grind.MatchCond` is used for implementing truth-value propagation.
+See the propagator `propagateMatchCond` below.
 For example, given a condition `C` of the form `Grind.MatchCond (∀ (a : Nat),  t = S.mk1 a → False)`,
 if `t` is merged with an equivalence class containing `S.mk2 n s`, then `C` is asseted to `true` by `propagateMatchCond`.
 
@@ -80,26 +82,6 @@ would require major refactoring and affect many modules, this issue is important
 A different representation could simplify `grind`, but it could add extra complexity to other modules.
 -/
 
-/--
-Returns `Grind.MatchCond e`.
-Recall that `Grind.MatchCond` is an identity function,
-but the following simproc is used to prevent the term `e` from being simplified,
-and we have special support for propagating is truth value.
--/
-def markAsMatchCond (e : Expr) : Expr :=
-  mkApp (mkConst ``Grind.MatchCond) e
-
-def isMatchCond (e : Expr) : Bool :=
-  e.isAppOfArity ``Grind.MatchCond 1
-
-builtin_dsimproc_decl reduceMatchCond (Grind.MatchCond _) := fun e => do
-  let_expr Grind.MatchCond _ ← e | return .continue
-  return .done e
-
-/-- Adds `reduceMatchCond` to `s` -/
-def addMatchCond (s : Simprocs) : CoreM Simprocs := do
-  s.add ``reduceMatchCond (post := false)
-
 /--
 Returns `some (α?, lhs, rhs)` if `e` is of the form
 - `Eq _ lhs rhs` (`?α := none`), or
@@ -305,7 +287,7 @@ where
         return none
     let isHEq := α?.isSome
     let h ← if isHEq then
-      mkEqOfHEq (← mkHEqTrans (← mkHEqProof root.self lhs) h)
+      mkEqOfHEq (← mkHEqTrans (← mkHEqProof root.self lhs) h) (check := false)
     else
       mkEqTrans (← mkEqProof root.self lhs) h
     if root.ctor then
diff --git a/src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean b/src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean
index f2750a0dd8..8acaa6e0f9 100644
--- a/src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean
+++ b/src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean
@@ -18,6 +18,9 @@ the discriminants of a `match`-expression. See `reduceSimpMatchDiscrsOnly`.
 def markAsSimpMatchDiscrsOnly (e : Expr) : MetaM Expr :=
   mkAppM ``Grind.simpMatchDiscrsOnly #[e]
 
+def isSimpMatchDiscrsOnly (e : Expr) :=
+  e.isAppOfArity ``Grind.simpMatchDiscrsOnly 2
+
 builtin_simproc_decl reduceSimpMatchDiscrsOnly (Grind.simpMatchDiscrsOnly _) := fun e => do
   let_expr Grind.simpMatchDiscrsOnly _ m ← e | return .continue
   let .const declName _ := m.getAppFn
@@ -33,10 +36,19 @@ def addSimpMatchDiscrsOnly (s : Simprocs) : CoreM Simprocs := do
   s.add ``reduceSimpMatchDiscrsOnly (post := false)
 
 /-- Erases `Grind.simpMatchDiscrsOnly` annotations. -/
-def eraseSimpMatchDiscrsOnly (e : Expr) : CoreM Expr := do
-  let pre (e : Expr) := do
-    let_expr Grind.simpMatchDiscrsOnly _ a := e | return .continue e
-    return .continue a
-  Core.transform e (pre := pre)
+def eraseSimpMatchDiscrsOnly (e : Expr) : MetaM Simp.Result := do
+  if e.find? isSimpMatchDiscrsOnly |>.isNone then
+    return { expr := e }
+  else
+    let pre (e : Expr) := do
+      let_expr Grind.simpMatchDiscrsOnly _ a := e | return .continue e
+      return .continue a
+    let e' ← Core.transform e (pre := pre)
+    /-
+    `grind` uses the `.reducible` transparency setting, and `Grind.simpMatchDiscrsOnly` is not
+    reducible. Thus, `e` and `e'` are not definitionally equal in this setting, and we must
+    add a hint.
+    -/
+    return { expr := e', proof? := (← mkExpectedTypeHint (← mkEqRefl e') (← mkEq e e')) }
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Proof.lean b/src/Lean/Meta/Tactic/Grind/Proof.lean
index f395c3fe89..58ec60e11f 100644
--- a/src/Lean/Meta/Tactic/Grind/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Proof.lean
@@ -39,7 +39,7 @@ Given `h : HEq a b`, returns a proof `a = b` if `heq == false`.
 Otherwise, it returns `h`.
 -/
 private def mkEqOfHEqIfNeeded (h : Expr) (heq : Bool) : MetaM Expr := do
-  if heq then return h else mkEqOfHEq h
+  if heq then return h else mkEqOfHEq h (check := false)
 
 /--
 Given `lhs` and `rhs` that are in the same equivalence class,
@@ -240,7 +240,7 @@ mutual
     else if heq then
       mkHEqOfEq lhsEqRhs
     else
-      mkEqOfHEq lhsEqRhs
+      mkEqOfHEq lhsEqRhs (check := false)
 
 end
 
diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean
index 7c5269d0ad..ea535d146f 100644
--- a/src/Lean/Meta/Tactic/Grind/Simp.lean
+++ b/src/Lean/Meta/Tactic/Grind/Simp.lean
@@ -35,7 +35,12 @@ def preprocess (e : Expr) : GoalM Simp.Result := do
   let e' ← eraseIrrelevantMData e'
   let e' ← foldProjs e'
   let e' ← normalizeLevels e'
-  let e' ← eraseSimpMatchDiscrsOnly e'
+  let r' ← eraseSimpMatchDiscrsOnly e'
+  let r ← r.mkEqTrans r'
+  let e' := r'.expr
+  let r' ← replacePreMatchCond e'
+  let r ← r.mkEqTrans r'
+  let e' := r'.expr
   let e' ← canon e'
   let e' ← shareCommon e'
   trace_goal[grind.simp] "{e}\n===>\n{e'}"
diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
index 6fefba6bc3..d4ea2c98ed 100644
--- a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
@@ -41,7 +41,7 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   -/
   let s := s.erase ``List.reduceReplicate
   let s ← addSimpMatchDiscrsOnly s
-  let s ← addMatchCond s
+  let s ← addPreMatchCondSimproc s
   return #[s]
 
 /-- Returns the simplification context used by `grind`. -/
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index a9ec6b3363..89ea1b1180 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -568,6 +568,9 @@ def markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool :=
 
 /-- Adds a new fact `prop` with proof `proof` to the queue for processing. -/
 def addNewFact (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
+  if grind.debug.get (← getOptions) then
+    unless (← withReducible <| isDefEq (← inferType proof) prop) do
+      throwError "`grind` internal error, trying to assert{indentExpr prop}\nwith proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\nwhich is not definitionally equal with `reducible` transparency setting}"
   modify fun s => { s with newFacts := s.newFacts.enqueue { proof, prop, generation } }
 
 /-- Adds a new theorem instance produced using E-matching. -/
@@ -704,7 +707,13 @@ def Goal.getTarget? (goal : Goal) (e : Expr) : Option Expr := Id.run do
 If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
 Otherwise, it pushes `HEq lhs rhs`.
 -/
-def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit :=
+def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
+  if grind.debug.get (← getOptions) then
+    unless proof == congrPlaceholderProof do
+      let expectedType ← if isHEq then mkHEq lhs rhs else mkEq lhs rhs
+      unless (← withReducible <| isDefEq (← inferType proof) expectedType) do
+        throwError "`grind` internal error, trying to assert equality{indentExpr expectedType}\nwith proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\nwhich is not definitionally equal with `reducible` transparency setting}"
+      trace[grind.debug] "pushEqCore: {expectedType}"
   modify fun s => { s with newEqs := s.newEqs.push { lhs, rhs, proof, isHEq } }
 
 /-- Return `true` if `a` and `b` have the same type. -/
diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean
index 4fdb42055d..553d2b5074 100644
--- a/src/Lean/Meta/Tactic/Grind/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Util.lean
@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Simproc
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Transform
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Clear
+import Lean.Meta.Tactic.Simp.Simproc
 
 namespace Lean.Meta.Grind
 /--
@@ -35,6 +37,13 @@ def _root_.Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Exp
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
+/--
+Returns `true` if `declName` is the name of a grind helper declaration that
+should not be unfolded by `unfoldReducible`.
+-/
+def isGrindGadget (declName : Name) : Bool :=
+  declName == ``Grind.EqMatch
+
 /--
 Unfolds all `reducible` declarations occurring in `e`.
 -/
@@ -42,6 +51,7 @@ def unfoldReducible (e : Expr) : MetaM Expr :=
   let pre (e : Expr) : MetaM TransformStep := do
     let .const declName _ := e.getAppFn | return .continue
     unless (← isReducible declName) do return .continue
+    if isGrindGadget declName then return .continue
     let some v ← unfoldDefinition? e | return .continue
     return .visit v
   Core.transform e (pre := pre)
@@ -123,7 +133,18 @@ def foldProjs (e : Expr) : MetaM Expr := do
       return .done e
     if h : idx < info.fieldNames.size then
       let fieldName := info.fieldNames[idx]
-      return .done (← mkProjection s fieldName)
+      /-
+      In the test `grind_cat.lean`, the following operation fails if we are not using default
+      transparency. We get the following error.
+      ```
+      error: AppBuilder for 'mkProjection', structure expected
+        T
+      has type
+        F ⟶ G
+      ```
+      We should make `mkProjection` more robust.
+      -/
+      return .done (← withDefault <| mkProjection s fieldName)
     else
       trace[grind.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
       return .done e
@@ -147,4 +168,51 @@ This function is used for normalzing E-matching patterns. Note that it does not
 @[extern "lean_grind_normalize"] -- forward definition
 opaque normalize (e : Expr) : MetaM Expr
 
+/--
+Returns `Grind.MatchCond e`.
+We have special support for propagating is truth value.
+See comment at `MatchCond.lean`.
+-/
+def markAsMatchCond (e : Expr) : Expr :=
+  mkApp (mkConst ``Grind.MatchCond) e
+
+def isMatchCond (e : Expr) : Bool :=
+  e.isAppOfArity ``Grind.MatchCond 1
+
+/--
+Returns `Grind.PreMatchCond e`.
+Recall that `Grind.PreMatchCond` is an identity function,
+but the simproc `reducePreMatchCond` is used to prevent the term `e` from being simplified.
+`Grind.PreMatchCond` is later converted into `Grind.MatchCond`.
+See comment at `MatchCond.lean`.
+-/
+def markAsPreMatchCond(e : Expr) : Expr :=
+  mkApp (mkConst ``Grind.PreMatchCond) e
+
+def isPreMatchCond (e : Expr) : Bool :=
+  e.isAppOfArity ``Grind.PreMatchCond 1
+
+builtin_dsimproc_decl reducePreMatchCond (Grind.PreMatchCond _) := fun e => do
+  let_expr Grind.PreMatchCond _ ← e | return .continue
+  return .done e
+
+/-- Adds `reducePreMatchCond` to `s` -/
+def addPreMatchCondSimproc (s : Simprocs) : CoreM Simprocs := do
+  s.add ``reducePreMatchCond (post := false)
+
+/--
+Converts `Grind.PreMatchCond` into `Grind.MatchCond`.
+Recall that `Grind.PreMatchCond` uses default reducibility setting, but
+`Grind.MatchCond` does not.
+-/
+def replacePreMatchCond (e : Expr) : MetaM Simp.Result := do
+  if e.find? isPreMatchCond |>.isNone then
+    return { expr := e }
+  else
+    let pre (e : Expr) := do
+      let_expr Grind.PreMatchCond p := e | return .continue e
+      return .continue (markAsMatchCond p)
+    let e' ← Core.transform e (pre := pre)
+    return { expr := e', proof? := (← mkExpectedTypeHint (← mkEqRefl e') (← mkEq e e')) }
+
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
index caa6428fa9..373b5a5ba4 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
@@ -144,15 +144,15 @@ def simpDvdCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
       let h := mkApp3 (mkConst ``Int.Linear.RawDvdCnstr.eq_false_of_isUnsat) (toContextExpr atoms) (toExpr c) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq lhs r))
 
-def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
-  let (e, atoms) ← toLinearExpr e
+def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
+  let (e, atoms) ← toLinearExpr input
   let p  := e.toPoly
   let e' := p.toExpr
   if e != e' then
     -- We only return some if monomials were fused
     let p := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_toPoly_eq) (toContextExpr atoms) (toExpr e) (toExpr e') reflBoolTrue
     let r ← e'.denoteExpr atoms
-    return some (r, p)
+    return some (r, ← mkExpectedTypeHint p (← mkEq input r))
   else
     return none
 
diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
index 0279a2a6dc..e1599f7993 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
@@ -67,8 +67,8 @@ def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   else
     simpCnstrPos? e
 
-def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
-  let (e, ctx) ← toLinearExpr e
+def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
+  let (e, ctx) ← toLinearExpr input
   let p  := e.toPoly
   let p' := p.norm
   if p'.length < p.length then
@@ -76,7 +76,7 @@ def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let e' : LinearExpr := p'.toExpr
     let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
     let r ← e'.toArith ctx
-    return some (r, p)
+    return some (r, ← mkExpectedTypeHint p (← mkEq input r))
   else
     return none
 
diff --git a/tests/lean/run/grind_ematch2.lean b/tests/lean/run/grind_ematch2.lean
index 2d3d6f3847..2337074bb8 100644
--- a/tests/lean/run/grind_ematch2.lean
+++ b/tests/lean/run/grind_ematch2.lean
@@ -47,23 +47,23 @@ info: [grind] Counters
     [thm] Array.size_set ↦ 3
 ---
 info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 11842, num: 3):
-    [reduction] LT.lt ↦ 11842
+  [reduction] unfolded declarations (max: 11519, num: 3):
+    [reduction] LT.lt ↦ 11519
     [reduction] getElem ↦ 76
-    [reduction] Nat.lt ↦ 35
+    [reduction] Nat.lt ↦ 34
   [reduction] unfolded instances (max: 38, num: 1):
     [reduction] Array.instGetElemNatLtSize ↦ 38
-  [reduction] unfolded reducible declarations (max: 7091, num: 7):
-    [reduction] Array.size ↦ 7091
-    [reduction] Array.toList ↦ 1897
-    [reduction] autoParam ↦ 1724
-    [reduction] outParam ↦ 172
+  [reduction] unfolded reducible declarations (max: 6907, num: 7):
+    [reduction] Array.size ↦ 6907
+    [reduction] Array.toList ↦ 1851
+    [reduction] autoParam ↦ 1675
+    [reduction] outParam ↦ 168
     [reduction] Ne ↦ 60
     [reduction] GT.gt ↦ 46
     [reduction] List.casesOn ↦ 24
-  [def_eq] heuristic for solving `f a =?= f b` (max: 5067, num: 2):
-    [def_eq] Nat.lt ↦ 5067
-    [def_eq] List.length ↦ 1691
+  [def_eq] heuristic for solving `f a =?= f b` (max: 4929, num: 2):
+    [def_eq] Nat.lt ↦ 4929
+    [def_eq] List.length ↦ 1645
   [kernel] unfolded declarations (max: 106, num: 5):
     [kernel] LT.lt ↦ 106
     [kernel] outParam ↦ 46
diff --git a/tests/lean/run/grind_match_eq_propagation.lean b/tests/lean/run/grind_match_eq_propagation.lean
index e1579bf118..276bf21ef3 100644
--- a/tests/lean/run/grind_match_eq_propagation.lean
+++ b/tests/lean/run/grind_match_eq_propagation.lean
@@ -1,3 +1,4 @@
+set_option grind.debug true
 inductive S where
   | mk1 (n : Nat)
   | mk2 (n : Nat) (s : S)