Unused theorems

Stream: lean4

[Sky Wilshaw]

I'm looking to prune my theorem tree. There's only a few "target" theorems that my project is aiming for - is there a way to see which theorems are never used in proving my targets?

[Sky Wilshaw]

I seem to remember something about trimming imports to make MWEs - perhaps the same kind infrastructure could be used for this?

[Damiano Testa]

Depending on what you want to prune exactly, the command #tips defined below will scan the declarations above it and report that ones that are not used by declarations in the current file.

import Lean.Elab.Print
import Mathlib.Lean.Expr.Basic

open Lean

/-- extracts the names of the declarations in `env` on which `decl` depends. -/
-- source:
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Counting.20prerequisites.20of.20a.20theorem/near/425370265
def getVisited (env : Environment) (decl : Name) :=
  let (_, { visited, .. }) := Elab.Command.CollectAxioms.collect decl |>.run env |>.run {}
  visited

/-- `#tips` prints a list of the declarations of the current file that are
defined but not used in the current file. -/
elab "#tips " : command => do
  let env ← getEnv
  let md ← mkModuleData env
  let decls ← md.constNames.filterM fun d => return !(← d.isBlackListed)
  let mut unseen := decls
  for t in decls do
    let mut seen? := false
    let tvisited := getVisited env t
    for u in decls do
      unless u == t do
        seen? := tvisited.contains u
        if seen? then unseen := unseen.erase u
  logInfo m!"unseen: {unseen}"

[Damiano Testa]

I limited the scope to a single file, since it is expensive to run this command.

[Sky Wilshaw]

Thank you! I want to use it in a multi-file setting, but I can just modify this code to my precise use case.