Collect commands dependencies

Stream: metaprogramming / tactics

[Han Han]

How can I extract the minimal set of commands that a constant depends on?

For example, suppose I have

import Mathlib

variable {K : Type*} {R : Type*}

local notation "q" => Fintype.card K

local notation "useless" => Fintype.card R

section none

end none

namespace FiniteField

variable [GroupWithZero K] [Fintype K]

theorem pow_card_sub_one_eq_one' (a : K) (ha : a ≠ 0) : a ^ (q - 1) = 1 := by
  calc
    a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
      rw [Units.val_pow_eq_pow_val, Units.val_mk0]
    _ = 1 := by
      classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl

end FiniteField

I’d like to automatically collect just the necessary context for pow_card_sub_one_eq_one' , e.g.

import Mathlib

variable {K : Type*}

local notation "q" => Fintype.card K

namespace FiniteField

variable [GroupWithZero K] [Fintype K]

end FiniteField

Thanks for any help!

[Kyle Miller]

Maybe you could figure this out by using the infotrees?

The infotrees from elaborating the theorem should include a number of source positions that are within some of those previous commands (e.g. for variables inside variable), as well as some identifiers referring to elaborators defined for the local notation. These elaborators will have declaration range information recorded, so you can figure out that these are for the local notation.

The namespace command won't be seen as a dependency. You can at least synthesize this information from the CommandElab state. See how #where is implemented for example.

[Han Han]

Thanks! I’ll check out infotrees and see how #where works. That’s really helpful!