fix: when indexing terms in simp, disable projection reduction

src/Lean/Elab/Tactic/Simp.lean

@@ -212,7 +212,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             match (← resolveSimpIdTheorem? term) with
             | .expr e  =>
               let name ← mkFreshId
-              thms ← addDeclToUnfoldOrTheorem ctx.metaConfig thms (.stx name arg) e post inv kind
+              thms ← addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
             | .simproc declName =>
               simprocs ← simprocs.add declName post
             | .ext (some ext₁) (some ext₂) _ =>
@@ -224,7 +224,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               simprocs  := simprocs.push (← ext₂.getSimprocs)
             | .none    =>
               let name ← mkFreshId
-              thms ← addSimpTheorem ctx.metaConfig thms (.stx name arg) term post inv
+              thms ← addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
           else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
             starArg := true
           else
@@ -329,7 +329,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     let hs ← getPropHyps
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
-        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr (config := ctx.metaConfig)
+        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr (config := ctx.indexConfig)
     let ctx := ctx.setSimpTheorems simpTheorems
     return { ctx, simprocs, dischargeWrapper }
 

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

@@ -242,7 +242,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
       let ctx ← getContext
       for x in xs do
         if (← isProof x) then
-          s ← s.addTheorem (.fvar x.fvarId!) x (config := ctx.metaConfig)
+          s ← s.addTheorem (.fvar x.fvarId!) x (config := ctx.indexConfig)
           updated := true
       if updated then
         withSimpTheorems s f
@@ -833,7 +833,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
-    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof (config := ctx.metaConfig)
+    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof (config := ctx.indexConfig)
     ctx := ctx.setSimpTheorems simpTheorems
   match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
   | (none, stats) => return (TacticResultCNM.closed, stats)

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -203,7 +203,7 @@ def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag :
 where
   /-- For `(← getConfig).index := true`, use discrimination tree structure when collecting `simp` theorem candidates. -/
   rewriteUsingIndex? : SimpM (Option Result) := do
-    let candidates ← withSimpConfig <| s.getMatchWithExtra e
+    let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
     if candidates.isEmpty then
       trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
       return none
@@ -221,7 +221,7 @@ where
   Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.
   -/
   rewriteNoIndex? : SimpM (Option Result) := do
-    let (candidates, numArgs) ← withSimpConfig <| s.getMatchLiberal e
+    let (candidates, numArgs) ← withSimpIndexConfig <| s.getMatchLiberal e
     if candidates.isEmpty then
       trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
       return none
@@ -245,7 +245,7 @@ where
 
   diagnoseWhenNoIndex (thm : SimpTheorem) : SimpM Unit := do
     if (← isDiagnosticsEnabled) then
-      let candidates ← withSimpConfig <| s.getMatchWithExtra e
+      let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
       for (candidate, _) in candidates do
         if unsafe ptrEq thm candidate then
           return ()

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -43,7 +43,7 @@ private def initEntries : M Unit := do
       let localDecl ← h.getDecl
       let proof  := localDecl.toExpr
       let ctx := (← get).ctx
-      simpThms ← simpThms.addTheorem (.fvar h) proof (config := ctx.metaConfig)
+      simpThms ← simpThms.addTheorem (.fvar h) proof (config := ctx.indexConfig)
       modify fun s => { s with ctx := s.ctx.setSimpTheorems simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
@@ -96,7 +96,7 @@ private partial def loop : M Bool := do
         trace[Meta.Tactic.simp.all] "entry.id: {← ppOrigin entry.id}, {entry.type} => {typeNew}"
         let mut simpThmsNew := (← getSimpTheorems).eraseTheorem (.fvar entry.fvarId)
         let idNew ← mkFreshId
-        simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew) (config := ctx.metaConfig)
+        simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew) (config := ctx.indexConfig)
         modify fun s => { s with
           modified         := true
           ctx              := ctx.setSimpTheorems simpThmsNew

src/Lean/Meta/Tactic/Simp/Simproc.lean

@@ -213,7 +213,7 @@ def SimprocEntry.tryD (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM
   | .inr proc => return (← proc e).addExtraArgs extraArgs
 
 def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM Step := do
-  let candidates ← withSimpConfig <| s.getMatchWithExtra e
+  let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
   if candidates.isEmpty then
     let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
@@ -250,7 +250,7 @@ def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Ex
       return .continue
 
 def dsimprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM DStep := do
-  let candidates ← withSimpConfig <| s.getMatchWithExtra e
+  let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
   if candidates.isEmpty then
     let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"

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

@@ -55,6 +55,7 @@ structure Context where
   private mk ::
   config            : Config := {}
   metaConfig        : ConfigWithKey := default
+  indexConfig       : ConfigWithKey := default
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
   simpTheorems      : SimpTheoremsArray := {}
@@ -119,8 +120,18 @@ private def updateArith (c : Config) : CoreM Config := do
     return c
 
 /--
-Converts `Simp.Config` into `Meta.ConfigWithKey`.
+Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
 -/
+private def mkIndexConfig (c : Config) : ConfigWithKey :=
+  { c with
+    proj         := .no
+    transparency := .reducible
+  : Meta.Config }.toConfigWithKey
+
+/--
+Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
+-/
+-- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib.
 private def mkMetaConfig (c : Config) : ConfigWithKey :=
   { c with
     proj         := if c.proj then .yesWithDelta else .no
@@ -129,7 +140,11 @@ private def mkMetaConfig (c : Config) : ConfigWithKey :=
 
 def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do
   let config ← updateArith config
-  return { config, simpTheorems, congrTheorems, metaConfig := mkMetaConfig config }
+  return {
+    config, simpTheorems, congrTheorems
+    metaConfig := mkMetaConfig config
+    indexConfig := mkIndexConfig config
+  }
 
 def Context.setConfig (context : Context) (config : Config) : Context :=
   { context with config }
@@ -214,12 +229,13 @@ abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
   withTheReader Context (fun ctx => { ctx with inDSimp := true })
 
 /--
-Executes `x` using a `MetaM` configuration inferred from `Simp.Config`.
+Executes `x` using a `MetaM` configuration for indexing terms.
+It is inferred from `Simp.Config`.
 For example, if the user has set `simp (config := { zeta := false })`,
 `isDefEq` and `whnf` in `MetaM` should not perform `zeta` reduction.
 -/
-@[inline] def withSimpConfig (x : SimpM α) : SimpM α := do
-  withConfigWithKey (← readThe Simp.Context).metaConfig x
+@[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do
+  withConfigWithKey (← readThe Simp.Context).indexConfig x
 
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result