From 17520fa0b8d8b56b89ad608946ce695e663159c4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Feb 2024 11:44:28 -0800 Subject: [PATCH] fix: cache issue at `split` tatic (#3258) closes #3229 --------- Co-authored-by: Scott Morrison Co-authored-by: Joachim Breitner --- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 3 ++- src/Lean/Meta/Tactic/Split.lean | 6 ++++-- src/Lean/Meta/Tactic/SplitIf.lean | 23 +++++++++++++++++------ tests/lean/run/3229.lean | 4 ++++ 4 files changed, 27 insertions(+), 9 deletions(-) create mode 100644 tests/lean/run/3229.lean diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 89d1f6e3d7..096cb5cc10 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index acb2dc1b1a..ec4b67be42 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean index 8a3c20dabc..eb5443be5d 100644 --- a/src/Lean/Meta/Tactic/SplitIf.lean +++ b/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! diff --git a/tests/lean/run/3229.lean b/tests/lean/run/3229.lean new file mode 100644 index 0000000000..2b7483d284 --- /dev/null +++ b/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