From c2185020c5cba93caef84dc258b2bb4b179febb5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 27 Mar 2025 11:55:14 +0100 Subject: [PATCH] chore: revert "feat: make `isRfl` lazy" This reverts commit 39b64ddc928a22b4ca16bbd0b1f1c638e3eed150 due to unclear Mathlib fallout. --- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 12 +++--- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 47 ++++++++------------- src/Lean/Meta/Tactic/Split.lean | 2 +- src/Lean/Meta/Tactic/Unfold.lean | 2 +- 4 files changed, 26 insertions(+), 37 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 7946b024b8..bf8fde8dd6 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -110,8 +110,8 @@ where return false private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do - if (← getConfig).implicitDefEqProofs then - thm.getRfl + if thm.rfl then + return (← getConfig).implicitDefEqProofs else return false @@ -218,7 +218,7 @@ where else let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority for (thm, numExtraArgs) in candidates do - unless inErasedSet thm || (rflOnly && !(← thm.getRfl)) do + unless inErasedSet thm || (rflOnly && !thm.rfl) do if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}" return some result @@ -236,7 +236,7 @@ where else let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority for thm in candidates do - unless inErasedSet thm || (rflOnly && !(← thm.getRfl)) do + unless inErasedSet thm || (rflOnly && !thm.rfl) do let result? ← withNewMCtxDepth do let val ← thm.getValue let type ← inferType val @@ -352,7 +352,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) := def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do for matchEq in (← Match.getEquationsFor matcherName).eqnNames do -- Try lemma - match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rflTask := (← isRflTheorem matchEq) }) with + match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) }) with | none => pure () | some r => return .visit r return .continue @@ -433,7 +433,7 @@ def sevalGround : Simproc := fun e => do -- `declName` has equation theorems associated with it. for eqn in eqns do -- TODO: cache SimpTheorem to avoid calls to `isRflTheorem` - if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rflTask := (← isRflTheorem eqn) } then + if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } then trace[Meta.Tactic.simp.ground] "unfolded, {e} => {result.expr}" return .visit result return .continue diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index d0ef53b14d..8a4667764d 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -122,56 +122,45 @@ structure SimpTheorem where It is also viewed an `id` used to "erase" `simp` theorems from `SimpTheorems`. -/ origin : Origin - /-- True if `proof` is by `Eq.refl` or `rfl`. Lazy so `[simp]` doesn't block the main thread. -/ - rflTask : Task Bool + /-- `rfl` is true if `proof` is by `Eq.refl` or `rfl`. -/ + rfl : Bool deriving Inhabited -def SimpTheorem.getRfl (t : SimpTheorem) : CoreM Bool := - traceBlock "SimpTheorem.getRfl" t.rflTask - mutual - partial def isRflProofCore (env : Environment) (type : Expr) (proof : Expr) : Task Bool := + partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do match type with | .forallE _ _ type _ => if let .lam _ _ proof _ := proof then - isRflProofCore env type proof + isRflProofCore type proof else - .pure false + return false | _ => if type.isAppOfArity ``Eq 3 then if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then - .pure true + return true else if proof.isAppOfArity ``Eq.symm 4 then -- `Eq.symm` of rfl theorem is a rfl theorem - isRflProofCore env type proof.appArg! -- small hack: we don't need to set the exact type + isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type else if proof.getAppFn.isConst then -- The application of a `rfl` theorem is a `rfl` theorem -- A constant which is a `rfl` theorem is a `rfl` theorem - isRflTheoremCore env proof.getAppFn.constName! + isRflTheorem proof.getAppFn.constName! else - .pure false + return false else - .pure false + return false - partial def isRflTheoremCore (env : Environment) (declName : Name) : Task Bool := Id.run do - env.findTask declName |>.bind (sync := true) fun - | none => .pure false - | some aconst => aconst.constInfo.bind (sync := true) fun - | .thmInfo info => isRflProofCore env info.type info.value - | _ => .pure false + partial def isRflTheorem (declName : Name) : CoreM Bool := do + let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false + let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false + isRflProofCore info.type info.value end -def isRflProof (proof : Expr) : MetaM (Task Bool) := do - let env ← getEnv +def isRflProof (proof : Expr) : MetaM Bool := do if let .const declName .. := proof then - return isRflTheoremCore env declName + isRflTheorem declName else - let type ← inferType proof - return isRflProofCore env type proof - -def isRflTheorem (declName : Name) : MetaM (Task Bool) := do - let env ← getEnv - return isRflTheoremCore env declName + isRflProofCore (← inferType proof) proof instance : ToFormat SimpTheorem where format s := @@ -412,7 +401,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array match type.eq? with | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs) | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}" - return { origin, keys, perm, post, levelParams, proof, priority := prio, rflTask := (← isRflProof proof) } + return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) } private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool) (prio : Nat) : MetaM (Array SimpTheorem) := do let cinfo ← getConstVal declName diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index d994a1f900..a9525f1e4f 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -51,7 +51,7 @@ where let simpTheorem := { origin := .decl matchEqDeclName proof := mkConst matchEqDeclName - rflTask := (← isRflTheorem matchEqDeclName) + rfl := (← isRflTheorem matchEqDeclName) } match (← withReducible <| Simp.tryTheorem? e simpTheorem) with | none => return .continue diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean index df578584bc..524819f8b9 100644 --- a/src/Lean/Meta/Tactic/Unfold.lean +++ b/src/Lean/Meta/Tactic/Unfold.lean @@ -22,7 +22,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do return { expr := (← deltaExpand e (· == declName)) } where pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do - match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rflTask := (← isRflTheorem unfoldThm) }) with + match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) }) with | none => pure () | some r => match (← reduceMatcher? r.expr) with | .reduced e' => return .done { r with expr := e' }