Something like `#print dependencies my_theorem`?

Stream: new members

[Isak Colboubrani]

You can inspect the axioms on which a theorem depends by writing #print axioms my_theorem:

import Mathlib
#print axioms Nat.mul_assoc
'Nat.mul_assoc' depends on axioms: [propext]

Is there any similar command that lists the named theorems a given theorem uses?

At present, I use the following manual procedure which works but is rather time‑consuming.

For instance, with Nat.mul_assoc:

#print Nat.mul_assoc shows that it uses the theorem Nat.left_distrib.

#print Nat.left_distrib shows that it uses the theorems Nat.add_left_comm, Nat.zero_mul and Nat.succ_mul.

You can repeat this until you reach the most fundamental lemmas.

Ideally, I'd like to be able to write:

import Mathlib
#print dependencies Nat.mul_assoc
-- or `#print_dependencies Nat.mul_assoc`
'Nat.mul_assoc' depends on theorems: [Nat.left_distrib, Nat.add_left_comm, Nat.zero_mul, Nat.succ_mul, …]

And—with a verbose flag—get a full dependency tree:

import Mathlib
#print verbose_dependencies Nat.mul_assoc
'Nat.mul_assoc' depends on theorems: [Nat.left_distrib, Nat.add_left_comm, Nat.zero_mul, Nat.succ_mul, …]

Dependency tree:
Nat.mul_assoc
  Nat.left_distrib
   Nat.add_left_comm
      Nat.add_assoc
      … etc …
  … etc…
  Nat.zero_mul
    Nat.mul_succ

One might even render it using fancy Unicode box‑drawing characters (bonus points!):

Nat.mul_assoc
├─ Nat.left_distrib
├─ Nat.add_left_comm
│   └─ Nat.add_assoc
└─ Nat.zero_mul
    └─ Nat.mul_succ

[Kyle Miller]

If not, sounds like a nice metaprogramming exercise :-)

[Isak Colboubrani]

The list of transitive dependencies can become quite large (as expected maybe). For example, if my approach is correct, Nat.fold_succ depends (directly or indirectly) on 431 named theorems.

Direct theorem dependencies of Nat.fold_succ:
* Nat.fold.proof_3
* Nat.fold.proof_4
* eq_self
* of_eq_true

Transitive theorem dependencies of Nat.fold_succ:
* And.comm
* And.symm
* Bool.and_eq_true
* Bool.decide_and
* Bool.false_and
…
* of_eq_true
* or_true
* trivial
* true_and
* true_or

For Nat.mul_assoc:

Direct theorem dependencies of Nat.mul_assoc:
* Eq.trans
* Nat.left_distrib
* congr
* congrArg
* eq_self
* of_eq_true

Transitive theorem dependencies of Nat.mul_assoc:
* Eq.symm
* Eq.trans
* Nat.add_assoc
* Nat.add_comm
* Nat.add_left_comm
* Nat.add_right_comm
* Nat.add_succ
* Nat.left_distrib
* Nat.mul_succ
* Nat.succ_add
* Nat.succ_mul
* Nat.zero_add
* Nat.zero_mul
* congr
* congrArg
* eq_self
* eq_true
* of_eq_true
* trivial

Does the output look correct?

[Isak Colboubrani]

Nat.mul_assoc has six direct theorem dependencies:

Direct theorem dependencies of Nat.mul_assoc:
* Eq.trans
* Nat.left_distrib
* congr
* congrArg
* eq_self
* of_eq_true

It would be helpful to highlight which of the theorems that are "basic building blocks" in the sense that they do not refer to any other named theorem. In this case, Eq.trans, congr and congrArg would qualify.

What would be an appropriate term for these? Primitive theorems?

For example:

Direct theorem dependencies of Nat.mul_assoc:
* Eq.trans (primitive)
* Nat.left_distrib
* congr (primitive)
* congrArg (primitive)
* eq_self
* of_eq_true

[Isak Colboubrani]

Perhaps in practice, one can distinguish two flavours of "primitive theorems":

• Core Lean primitives – e.g. Eq.trans, congr, congrArg, etc., typically defined in Prelude.lean.
• Domain-specific primitives – results like Nat.zero_add or Nat.succ_add whose proofs invoke no named theorems beyond those core Lean primitives.

What would be appropriate terms for these two classes of "primitive theorems"?