fix: cache issue at split tatic (#3258)

closes #3229

---------

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -44,7 +44,8 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
 def simpMatchWF? (mvarId : MVarId) : MetaM (Option MVarId) :=
   mvarId.withContext do
     let target ← instantiateMVars (← mvarId.getType)
-    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
+    let discharge? ← mvarId.withContext do SplitIf.mkDischarge?
+    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? })
     let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
     if mvarId != mvarIdNew then return some mvarIdNew else return none
 where

src/Lean/Meta/Tactic/Split.lean

@@ -19,7 +19,8 @@ def getSimpMatchContext : MetaM Simp.Context :=
    }
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
-  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
+  let discharge? ← SplitIf.mkDischarge?
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     unless (← isMatcherApp e) do
@@ -36,7 +37,8 @@ def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   applySimpResultToTarget mvarId target r
 
 private def simpMatchCore (matchDeclName : Name) (matchEqDeclName : Name) (e : Expr) : MetaM Simp.Result := do
-  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? := SplitIf.discharge? })
+  let discharge? ← SplitIf.mkDischarge?
+  (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     if e.isAppOf matchDeclName then

src/Lean/Meta/Tactic/SplitIf.lean

@@ -31,9 +31,17 @@ def getSimpContext : MetaM Simp.Context :=
 
 /--
   Default `discharge?` function for `simpIf` methods.
-  It only uses hypotheses from the local context. It is effective
-  after a case-split. -/
-def discharge? (useDecide := false) : Simp.Discharge := fun prop => do
+  It only uses hypotheses from the local context that have `index < numIndices`.
+  It is effective after a case-split.
+
+  Remark: when `simp` goes inside binders it adds new local declarations to the
+  local context. We don't want to use these local declarations since the cached result
+  would depend on them (see issue #3229). `numIndices` is the size of the local
+  context `decls` field before we start the simplifying the expression.
+
+  Remark: this function is now private, and we should use `mkDischarge?`.
+-/
+private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge := fun prop => do
   let prop ← instantiateMVars prop
   trace[Meta.Tactic.splitIf] "discharge? {prop}, {prop.notNot?}"
   if useDecide then
@@ -44,7 +52,7 @@ def discharge? (useDecide := false) : Simp.Discharge := fun prop => do
       if r.isConstOf ``true then
         return some <| mkApp3 (mkConst ``of_decide_eq_true) prop d.appArg! (← mkEqRefl (mkConst ``true))
   (← getLCtx).findDeclRevM? fun localDecl => do
-     if localDecl.isAuxDecl then
+     if localDecl.index ≥ numIndices || localDecl.isAuxDecl then
        return none
      else if (← isDefEq prop localDecl.type) then
        return some localDecl.toExpr
@@ -56,6 +64,9 @@ def discharge? (useDecide := false) : Simp.Discharge := fun prop => do
          else
            return none
 
+def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
+  return discharge? (← getLCtx).numIndices useDecide
+
 /-- Return the condition of an `if` expression to case split. -/
 partial def findIfToSplit? (e : Expr) : Option Expr :=
   if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then
@@ -82,14 +93,14 @@ open SplitIf
 
 def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some mvarId', _) ← simpTarget mvarId ctx {} (discharge? useDecide) (mayCloseGoal := false) then
+  if let (some mvarId', _) ← simpTarget mvarId ctx {} (← mvarId.withContext <| mkDischarge? useDecide) (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!
 
 def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} discharge? (mayCloseGoal := false) then
+  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} (← mvarId.withContext <| mkDischarge?) (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!

tests/lean/run/3229.lean

@@ -0,0 +1,4 @@
+-- This example exposed a caching issue with the `discharge?` method used by the `split` tactic.
+example (b : Bool) :
+    (if b then 1 else if b then 1 else 0) = (if b then 1 else 0) := by
+  split <;> rfl