finding all uses of a theorem in mathlib

Stream: mathlib4

[Kevin Buzzard]

I'm guessing that this is easy if you know some metaprogramming. Working with a student, one of their lines of code was rcases Module.Finite.out (R := R) (M := M) with ⟨S, hS⟩, and when I looked at the definition of Module.Finite.out it struck me that perhaps R and M should just be explicit. My instinct now was to look at all occurrences of this theorem in mathlib to see if the facts backed me up, but all I can do as a non-meta user is to search for Module.Finite.out, which may well miss things (e.g. if Module.Finite is opened or if dot notation is being used).

So how do I search mathlib for all actual occurrences of Module.Finite.out?

[Alex Kontorovich]

I'm sure there are much, much smarter ways of doing this. But what I've sometimes resorted to is changing the name (e.g. to Module.Finite.outt) and committing. Then CI tells me where they all are...

[Damiano Testa]

Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.ilean:Module.Finite.out
Mathlib/RingTheory/FiniteType.ilean:Module.Finite.out
Mathlib/RingTheory/Finiteness.ilean:Module.Finite.out
Mathlib/RingTheory/IntegralClosure.ilean:Module.Finite.out
Mathlib/RingTheory/LocalProperties.ilean:Module.Finite.out
Mathlib/RingTheory/Artinian.ilean:Module.Finite.out
Mathlib/Algebra/Module/Torsion.ilean:Module.Finite.out

[Damiano Testa]

(As you can see, I scanned the ileans...)

[Damiano Testa]

I think that this only finds "explicit" usages: if you were searching for a simp-lemma, then, whenever simp pulls that lemma in, without you mentioning explicitly, I do not think that the ilean would contain that usage.

My mental model is "if you get a hover information, then it is in the ilean". I do not think that you get an ilean reference if there is no syntax for the lemma.

[Damiano Testa]

By the way, this is the command that I used:

grep -r -o ':Module.Finite.out"' .lake/build/lib/Mathlib/

-recurse into subdirs, -only print the matching text (for reference).

Note that the : before and the " after are to avoid matching names that contain the name that you are searching for.

[Damiano Testa]

You can add

findRefs () { grep -r -o ":${1}\"" .lake/build/lib/Mathlib/ ; }

to your bash_aliases file and then, from the mathlib4 dir you can simply do

$ findRefs Module.Finite.out

and you get the output above.

[Damiano Testa]

Also, I recently learned that if you right-click on the declaration and you look for Show call hierarchy, you get a list of all the places where the declaration is called. I suspect that this would give you the same hits as the grep above, but in VSCode and clickable. Depending on what you want to do, this can be quite convenient.

[Adam Topaz]

If you want all uses, including indirect ones, you can use docs#Lean.Expr.getUsedConstantsAsSet and check whether a given constant is used in its value.

[Adam Topaz]

It's quite easy to do.

[Adam Topaz]

give me about 5 mins and I can get you some code to do this.

[Adam Topaz]

It's not very fast, but here is something:

import Mathlib

open Lean
#eval show CoreM Unit from do
  let env ← getEnv
  for (n,c) in env.constants.toList do
    let some val := c.value? | continue
    if val.getUsedConstantsAsSet.contains `Module.Finite.out then
      println! n

[Adam Topaz]

this results in

Module.Finite.exists_fin
RingHom.Finite.to_isIntegral
Module.Finite.finiteType
isArtinian_of_fg_of_artinian'
Module.Finite.base_change
Module.Finite.of_surjective
Module.Finite.tensorProduct
Module.Finite.top
Submodule.annihilator_top_inter_nonZeroDivisors
finite_ofLocalizationSpan
LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
Module.Finite.prod
Module.finite_def
Module.Finite.pi

[Adam Topaz]

here's a slightly better version that also gives you the module names:

import Mathlib

open Lean
#eval show CoreM Unit from do
  let env ← getEnv
  for (n,c) in env.constants.toList do
    let some val := c.value? | continue
    if val.getUsedConstantsAsSet.contains `Module.Finite.out then
      let modName := env.getModuleFor? n |>.getD ""
      println! s!"{modName} : {n}"

output:

Mathlib.RingTheory.Finiteness : Module.Finite.exists_fin
Mathlib.RingTheory.IntegralClosure : RingHom.Finite.to_isIntegral
Mathlib.RingTheory.FiniteType : Module.Finite.finiteType
Mathlib.RingTheory.Artinian : isArtinian_of_fg_of_artinian'
Mathlib.RingTheory.Finiteness : Module.Finite.base_change
Mathlib.RingTheory.Finiteness : Module.Finite.of_surjective
Mathlib.RingTheory.Finiteness : Module.Finite.tensorProduct
Mathlib.RingTheory.Finiteness : Module.Finite.top
Mathlib.Algebra.Module.Torsion : Submodule.annihilator_top_inter_nonZeroDivisors
Mathlib.RingTheory.LocalProperties : finite_ofLocalizationSpan
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap : LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
Mathlib.RingTheory.Finiteness : Module.Finite.prod
Mathlib.RingTheory.Finiteness : Module.finite_def
Mathlib.RingTheory.Finiteness : Module.Finite.pi

[Kim Morrison]

Any advice about how we can make this more accessible? I think the API here is pretty complete. @Kevin Buzzard, how would the world have to be different so that you would have been able to work this out? :-)

[Kevin Buzzard]

I am too lazy/busy/uninterested in learning how to use Lean as a programming language, because I have very little coding experience and I am spoilt by the luxury of being able to ask such questions here. In other words, it's not you, it's me!

[Kevin Buzzard]

Anyway, the conclusion of this experiment (having run through most of the examples found above) is that it's probably fine that out takes implicit inputs, but anyone who wants to change it would run into lean4#3574 anyway (i.e. you can't change it, you would have to write out', which might to be honest be not a bad idea anyway).