Searching for lemmas to rename

Stream: mathlib4

[Patrick Massot]

It may be useful to post some code I used today. In a large refactor, I renamed Finsupp.total to Finsupp.linearCombination. The main pain point was to rename all lemmas whose named contained total. The meta-code I used to find them is:

import Mathlib


open Lean Elab Command Meta

-- Generalized monad for `Lean.Name.isBlackListed`
def Lean.Name.isBlackListed' {m : Type → Type} [Monad m] [MonadEnv m]
    (declName : Name) : m Bool := do
  if declName == ``sorryAx then return true
  if declName matches .str _ "inj" then return true
  if declName matches .str _ "noConfusionType" then return true
  let env ← getEnv
  pure $ declName.isInternalDetail
   || isAuxRecursor env declName
   || isNoConfusion env declName
  <||> isRec declName <||> isMatcher declName

namespace Mathlib.FindUnused

/-- Remove all blacklisted names from the given environment.
This might not be accurate since the blacklist function is a heuristic. -/
def filterNames {m : Type → Type} [Monad m] [MonadEnv m] {α : Type _}
    (env : HashMap Name α) : m (HashMap Name α) := do
  let mut env' := env
  for (n, _) in env do
    if ← n.isBlackListed' then
      env' := env'.erase n
  return env'

elab "#lemmas" : command => do
    let env ← filterNames (← getEnv).constants.map₁
    for (n, c) in env do
      if `Finsupp.linearCombination ∈ c.type.getUsedConstants && ((toString n).findSubstr? "total").isSome then do
        dbg_trace n

#lemmas

The two auxiliary functions were stolen from an old Zulip message by @Kyle Miller. Then the lemmas command look at all declarations and print the names of the declarations whose type involve Finsupp.linearCombination and whose name includes total. Of course in the future we will have much better ways of doing this using #13973, but I thought the above trick can already be useful to other people.

[Patrick Massot]

Note I’m defining a command because I always forget how to simply run code in CommandElabM without defining a command.

[Eric Wieser]

run_cmd?