feat: add Grind.Config.reducible (#11480)

This PR adds the `grind` option `reducible` (default: `true`). When
enabled, definitional equality tests expand only declarations marked as
`@[reducible]`.
Use `grind -reducible` to allow expansion of non-reducible declarations
during definitional equality tests.
This option affects only definitional equality; the canonicalizer and
theorem pattern internalization always unfold reducible declarations
regardless of this setting.

Author: leodemoura

src/Init/Grind/Config.lean

@@ -202,6 +202,15 @@ structure Config where
   ```
   -/
   funCC := true
+  /--
+  When `true`, use reducible transparency when trying to close goals.
+  In this setting, only declarations marked with `@[reducible]` are unfolded during
+  definitional equality tests.
+
+  This option does not affect the canonicalizer or how theorem patterns are internalized;
+  reducible declarations are always unfolded in those contexts.
+  -/
+  reducible := true
   deriving Inhabited, BEq
 
 /--

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -283,12 +283,12 @@ def tryTactic (tac : GrindTacticM α) : GrindTacticM Bool := do
 open Grind
 
 /-
-**Note**: Recall that `grind` uses `Reducible` setting to avoid expensive definitionally equality tests.
+**Note**: Recall that `grind` uses the reducibility specified at `Config.reducible`
 -/
-def liftGrindM (k : GrindM α) : GrindTacticM α := withReducible do
+def liftGrindM (k : GrindM α) : GrindTacticM α := do
   let ctx ← read
   let s ← get
-  let (a, state) ← liftMetaM <| k ctx.methods.toMethodsRef ctx.ctx |>.run s.state
+  let (a, state) ← liftMetaM <| (Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.state
   modify fun s => { s with state }
   return a
 

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -500,9 +500,9 @@ where
       -- which is not reducible.
       proof := mkExpectedPropHint proof prop
     /-
-    **Note**: Must restore `reducible` setting because with use `withDefault` at `instantiateTheorem`.
+    **Note**: Restores grind transparency setting because with use `withDefault` at `instantiateTheorem`.
     -/
-    withReducible do
+    withGTransparency do
       addTheoremInstance thm proof prop (generation+1) guards
 
 private def synthesizeInsts (mvars : Array Expr) (bis : Array BinderInfo) : OptionT M Unit := do

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -262,7 +262,7 @@ def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
   return { failure?, issues, config := params.config, counters, simp, splitDiags }
 
 def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) (evalTactic? : Option EvalTactic := none) : MetaM α := do
-  let go : GrindM α := withReducible do
+  let go : GrindM α := withGTransparency do
     let goal ← initCore mvarId params
     k goal
   go.run params (evalTactic? := evalTactic?)

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -298,6 +298,14 @@ def withSplitSource [MonadControlT GrindM m] [Monad m] (splitSource : SplitSourc
 def getConfig : GrindM Grind.Config :=
   return (← readThe Context).config
 
+/--
+Runs `k` with the transparency setting specified by `Config.reducible`.
+Uses reducible transparency if `reducible` is `true`, otherwise default transparency.
+-/
+abbrev withGTransparency [MonadControlT MetaM n] [MonadLiftT GrindM n] [Monad n] (k : n α) : n α := do
+  let m := if (← getConfig).reducible then .reducible else .default
+  withTransparency m k
+
 /-- Returns the internalized `True` constant.  -/
 def getTrueExpr : GrindM Expr := do
   return (← readThe Context).trueExpr
@@ -1025,7 +1033,7 @@ def markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool :=
 /-- Adds a new fact `prop` with proof `proof` to the queue for preprocessing and the assertion. -/
 def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) (splitSource : SplitSource) : GoalM Unit := do
   if grind.debug.get (← getOptions) then
-    unless (← withReducible <| isDefEq (← inferType proof) prop) do
+    unless (← withGTransparency <| isDefEq (← inferType proof) prop) do
       throwError "`grind` internal error, trying to assert{indentExpr prop}\n\
         with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
         which is not definitionally equal with `reducible` transparency setting}"
@@ -1182,7 +1190,7 @@ def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
       throwError "`grind` internal error, rhs of new equality has not been internalized{indentExpr rhs}"
     if proof != congrPlaceholderProof && proof != eqCongrSymmPlaceholderProof then
       let expectedType ← if isHEq then mkHEq lhs rhs else mkEq lhs rhs
-      unless (← withReducible <| isDefEq (← inferType proof) expectedType) do
+      unless (← withGTransparency <| isDefEq (← inferType proof) expectedType) do
         throwError "`grind` internal error, trying to assert equality{indentExpr expectedType}\n\
             with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
             which is not definitionally equal with `reducible` transparency setting}"

tests/lean/run/grind_reducible.lean

@@ -0,0 +1,50 @@
+variable {α β γ : Type}
+
+structure Equiv (α β : Type) where
+  toFun : α → β
+  invFun : β → α
+
+infixl:25 " ≃ " => Equiv
+
+namespace Equiv
+
+instance : CoeFun (α ≃ β) (fun _ => α → β) := ⟨toFun⟩
+
+@[ext, grind ext] theorem ext {f g : Equiv α β} (H : ∀ x, f x = g x) : f = g := sorry
+
+theorem congr_fun {f g : Equiv α β} (h : f = g) (x : α) : f x = g x := by rw [h]
+
+def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
+
+def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
+
+def sigmaCongrRight {α : Type} {β₁ β₂ : α → Type} (F : ∀ a, β₁ a ≃ β₂ a) : (Σ a, β₁ a) ≃ Σ a, β₂ a where
+  toFun a := ⟨a.1, F a.1 a.2⟩
+  invFun a := ⟨a.1, (F a.1).symm a.2⟩
+
+def sigmaEquivProd (α β : Type) : (Σ _ : α, β) ≃ α × β where
+  toFun a := ⟨a.1, a.2⟩
+  invFun a := ⟨a.1, a.2⟩
+
+end Equiv
+
+variable {α₁ β₁ β₂ : Type} (e : α₁ → β₁ ≃ β₂)
+
+def prodCongrRight : α₁ × β₁ ≃ α₁ × β₂ where
+  toFun ab := ⟨ab.1, e ab.1 ab.2⟩
+  invFun ab := ⟨ab.1, (e ab.1).symm ab.2⟩
+
+example :
+    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
+    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
+  grind -reducible only [Equiv.congr_fun]
+
+example :
+    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
+    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
+  grind -reducible only => finish only [Equiv.congr_fun]
+
+example :
+    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
+    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
+  grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]