chore: simproc PR changes (#496)

See leanprover/lean4#3124

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Std/Lean/Meta/Simp.lean

@@ -53,15 +53,18 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
     simpOnlyBuiltins.foldlM (·.addConst ·) {}
   else
     pure simpTheorems
+  let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← Meta.getSimpCongrTheorems
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
     config       := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
-  }
+  } simprocs
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
-    let mut simpTheorems := r.ctx.simpTheorems
+    let ctx := r.ctx
+    let mut simpTheorems := ctx.simpTheorems
+    let simprocs := r.simprocs
     /-
     When using `zeta := false`, we do not expand let-declarations when using `[*]`.
     Users must explicitly include it in the list.
@@ -70,7 +73,9 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    return { ctx := { r.ctx with simpTheorems }, dischargeWrapper }
+    let ctx := { ctx with simpTheorems }
+    return { ctx, simprocs, dischargeWrapper }
+
 
 end Simp
 

Std/Tactic/NormCast.lean

@@ -24,13 +24,13 @@ initialize registerTraceClass `Tactic.norm_cast
 /-- Prove `a = b` using the given simp set. -/
 def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) := do
   let go : SimpM (Option Simp.Result) := do
-    let methods := Simp.DefaultMethods.methods
-    let a' ← Simp.simp a methods
-    let b' ← Simp.simp b methods
+    let a' ← Simp.simp a
+    let b' ← Simp.simp b
     unless ← isDefEq a'.expr b'.expr do return none
     mkEqTrans a' (← mkEqSymm b b')
   withReducible do
-    (go { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
+    (go (← Simp.mkDefaultMethods).toMethodsRef
+      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
 
 /-- Prove `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
@@ -325,8 +325,8 @@ syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 @[inherit_doc pushCast, tactic pushCast] def evalPushCast : Tactic := fun stx => do
-  let { ctx, dischargeWrapper, .. } ← withMainContext do
+  let { ctx, simprocs, dischargeWrapper } ← withMainContext do
     mkSimpContext' (← pushCastExt.getTheorems) stx (eraseLocal := false)
   let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? =>
-    discard <| simpLocation ctx discharge? (expandOptLocation stx[5])
+    discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])

Std/Tactic/SimpTrace.lean

@@ -36,44 +36,10 @@ syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
 macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
 
 open TSyntax.Compat in
--- adapted from traceSimpCall
 /-- Constructs the syntax for a simp call, for use with `simp?`. -/
 def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tactic) := do
-  let mut stx := stx.unsetTrailing
-  if stx[3].isNone then
-    stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
-  let mut args := #[]
-  let mut localsOrStar := some #[]
-  let lctx ← getLCtx
-  let env ← getEnv
-  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
-    match thm with
-    | .decl declName inv => -- global definitions in the environment
-      if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← if inv then
-          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
-        else
-          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
-    | .fvar fvarId => -- local hypotheses in the context
-      if let some ldecl := lctx.find? fvarId then
-        localsOrStar := localsOrStar.bind fun locals =>
-          if !ldecl.userName.isInaccessibleUserName &&
-              (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then
-            some (locals.push ldecl.userName)
-          else
-            none
-      -- Note: the `if let` can fail for `simp (config := {contextual := true})` when
-      -- rewriting with a variable that was introduced in a scope. In that case we just ignore.
-    | .stx _ thmStx => -- simp theorems provided in the local invocation
-      args := args.push thmStx
-    | .other _ => -- Ignore "special" simp lemmas such as constructed by `simp_all`.
-      pure ()     -- We can't display them anyway.
-  if let some locals := localsOrStar then
-    args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
-  else
-    args := args.push (← `(Parser.Tactic.simpStar| *))
-  let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  pure <| stx.setArg 4 (mkNullNode argsStx)
+  let stx := stx.unsetTrailing
+  mkSimpOnly stx usedSimps
 
 elab_rules : tactic
   | `(tactic|
@@ -82,9 +48,11 @@ elab_rules : tactic
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+    let { ctx, simprocs, dischargeWrapper } ←
+      withMainContext <| mkSimpContext stx (eraseLocal := false)
     let usedSimps ← dischargeWrapper.with fun discharge? =>
-      simpLocation ctx discharge? <| (loc.map expandLocation).getD (.targets #[] true)
+      simpLocation ctx (simprocs := simprocs) discharge? <|
+        (loc.map expandLocation).getD (.targets #[] true)
     let stx ← mkSimpCallStx stx usedSimps
     TryThis.addSuggestion tk stx (origSpan? := ← getRef)
 

Std/Tactic/Simpa.lean

@@ -53,59 +53,6 @@ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic
 
 open private useImplicitLambda from Lean.Elab.Term
 
--- FIXME: remove when lean4#1862 lands
-open TSyntax.Compat in
-/--
-If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
-`usedSimps` is the set of simp lemmas used by this invocation, then `mkSimpOnly`
-creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
-invocation.
--/
-private def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax.Tactic := do
-  let isSimpAll := stx[0].getAtomVal == "simp_all"
-  let mut stx := stx
-  if stx[3].isNone then
-    stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
-  let mut args := #[]
-  let mut localsOrStar := some #[]
-  let lctx ← getLCtx
-  let env ← getEnv
-  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
-    match thm with
-    | .decl declName inv => -- global definitions in the environment
-      if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← if inv then
-          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
-        else
-          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
-    | .fvar fvarId => -- local hypotheses in the context
-      if isSimpAll then
-        continue
-        -- `simp_all` uses all hypotheses anyway, so we do not need to include
-        -- them in the arguments. In fact, it would be harmful to do so:
-        -- `simp_all only [h]`, where `h` is a hypothesis, simplifies `h` to
-        -- `True` and subsequenly removes it from the context, whereas
-        -- `simp_all` does not. So to get behavior equivalent to `simp_all`, we
-        -- must omit `h`.
-      if let some ldecl := lctx.find? fvarId then
-        localsOrStar := localsOrStar.bind fun locals =>
-          if !ldecl.userName.isInaccessibleUserName &&
-              (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then
-            some (locals.push ldecl.userName)
-          else
-            none
-      -- Note: the `if let` can fail for `simp (config := {contextual := true})` when
-      -- rewriting with a variable that was introduced in a scope. In that case we just ignore.
-    | .stx _ thmStx => -- simp theorems provided in the local invocation
-      args := args.push thmStx
-    | .other _ => -- Ignore "special" simp lemmas such as constructed by `simp_all`.
-      pure ()     -- We can't display them anyway.
-  if let some locals := localsOrStar then
-    args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
-  else
-    args := args.push (← `(Parser.Tactic.simpStar| *))
-  let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  return stx.setArg 4 (mkNullNode argsStx)
 
 /-- Gets the value of the `linter.unnecessarySimpa` option. -/
 def getLinterUnnecessarySimpa (o : Options) : Bool :=
@@ -117,13 +64,14 @@ elab_rules : tactic
 | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
       $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
   let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
-  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper } ←
+    withMainContext <| mkSimpContext stx (eraseLocal := false)
   let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
   -- TODO: have `simpa` fail if it doesn't use `simp`.
   let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? => do
-    let (some (_, g), usedSimps) ←
-        simpGoal (← getMainGoal) ctx (simplifyTarget := true) (discharge? := discharge?)
+    let (some (_, g), usedSimps) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
+        (simplifyTarget := true) (discharge? := discharge?)
       | if getLinterUnnecessarySimpa (← getOptions) then
           logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
     g.withContext do
@@ -135,7 +83,7 @@ elab_rules : tactic
         pure (h, g)
       else
         (← g.assert `h (← inferType e) e).intro1
-      let (result?, usedSimps) ← simpGoal g ctx (fvarIdsToSimp := #[h])
+      let (result?, usedSimps) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
         (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
       match result? with
       | some (xs, g) =>
@@ -151,8 +99,9 @@ elab_rules : tactic
               m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
       pure usedSimps
     else if let some ldecl := (← getLCtx).findFromUserName? `this then
-      if let (some (_, g), usedSimps) ← simpGoal g ctx (fvarIdsToSimp := #[ldecl.fvarId])
-          (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?) then
+      if let (some (_, g), usedSimps) ← simpGoal g ctx (simprocs := simprocs)
+          (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
+          (discharge? := discharge?) then
         g.assumption; pure usedSimps
       else
         pure usedSimps

Std/Tactic/SqueezeScope.lean

@@ -95,13 +95,14 @@ elab_rules : tactic
     let stx := tac.raw
     let usedSimps ← match stx.getKind with
     | ``Parser.Tactic.simp => do
-      let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+      let { ctx, simprocs, dischargeWrapper } ←
+        withMainContext <| mkSimpContext stx (eraseLocal := false)
       dischargeWrapper.with fun discharge? =>
-        simpLocation ctx discharge? (expandOptLocation stx[5])
+        simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
     | ``Parser.Tactic.simpAll => do
-      let { ctx, .. } ← mkSimpContext stx
+      let { ctx, simprocs, .. } ← mkSimpContext stx
         (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-      let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+      let (result?, usedSimps) ← simpAll (← getMainGoal) ctx simprocs
       match result? with
       | none => replaceMainGoal []
       | some mvarId => replaceMainGoal [mvarId]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-09
+leanprover/lean4:nightly-2024-01-10