Hunting down axioms

Stream: Is there code for X?

[Tristan Figueroa-Reid]

Is there a way to see where axioms are used? I have a particular use of Classical which I don't believe should be invoked in a proof I'm at all - I'm trying to figure out where it's coming from.

[Edward van de Meent]

I believe someone wrote a tool for this once... searching zulip might be fruitful

[Henrik Böving]

#print axioms <declaration>

[Yaël Dillies]

Henrik, this only tells you whether an axiom is used, not where its use came from

[Henrik Böving]

Ah I see, I guess you could use a mutation of the print axioms code that also tracks where it found the axiom. Something like this:

import Lean

open Lean

structure State where
  visited : NameSet    := {}
  axioms  : Array (Name × Name) := #[]

abbrev M := ReaderT Environment $ StateM State

partial def collect (origin : Name) (c : Name) : M Unit := do
  let collectExpr (origin : Name) (e : Expr) : M Unit := e.getUsedConstants.forM (collect origin)
  let s ← get
  unless s.visited.contains c do
    modify fun s => { s with visited := s.visited.insert c }
    let env ← read
    match env.find? c with
    | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push (origin, c) }
    | some (ConstantInfo.defnInfo v)   => collectExpr c v.type *> collectExpr c v.value
    | some (ConstantInfo.thmInfo v)    => collectExpr c v.type *> collectExpr c v.value
    | some (ConstantInfo.opaqueInfo v) => collectExpr c v.type *> collectExpr c v.value
    | some (ConstantInfo.quotInfo _)   => pure ()
    | some (ConstantInfo.ctorInfo v)   => collectExpr c v.type
    | some (ConstantInfo.recInfo v)    => collectExpr c v.type
    | some (ConstantInfo.inductInfo v) => collectExpr c v.type *> v.ctors.forM (collect c)
    | none                             => pure ()

def foo [Monad m] [MonadEnv m] (constName : Name) : m (Array (Name × Name)) := do
  let env ← getEnv
  let (_, s) := ((collect constName constName).run env).run {}
  return s.axioms



def hack : Nat := sorry


def bar : Nat := hack


def foobar : Nat := bar + bar

#eval show MetaM _ from do foo ``foobar

though I only tested that on this trivial example, no guarantee that it works generally :D

[Eric Wieser]

https://github.com/leanprover-community/mathlib3/issues/10954 was our previous tracking issue for this

[Riccardo Brasca]

You can replace part of the proof by sorry and see when classical is not used anymore. But note that tactics very often use classical.

[Rémy Degenne]

There was discussion about that here: #Is there code for X? > ✔ Finding usages of `sorry` in external code @ 💬

[Rémy Degenne]

I have used that piece of code written by Kyle in my projects and it's quite useful to find the sorry that matter for your important results.

[Bryan Gin-ge Chen]

Sounds like something like this might be worth PRing to Batteries (?).