modularising/tracing theorems

Stream: general

[metakuntyyy]

So my use case is I want to understand the "boundaries" of theorems, what I can stub/sorry so that I can construct a graph of a more complex proof/construction in mathlib. In metamath everything is very explicit. All hypotheses are explicit, and every proof step is explicit. I want to do something similar with regards to the proof of https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.html#AlgebraicClosure.instIsAlgClosureOfIsAlgebraic theorem.

What would be the best way to trace the theorem down to its dependent theorems? Is there any utility that I can run over the database, that spits out a theorem list X used in the proof of theorem Y. Because then I could build a graph of all theorems I need to port over to get a good understanding of what I necessarily need to understand.

In particular I'm worried about the following two points:

• How do I distinguish when I need data and when I don't? (I plan to start a backwards trace from the theorem I want to port, in particular, when can I stub proofs with sorry to achieve modularity)
• How can I make sure that tactics aren't doing something that is "too much magic". In particular how do I deconstruct tactics and figure out how to simpify them (going lower in the abstraction hierarchy)

I think I'd rather state my "wish" first. I'd like to input a theorem R in the mathlib4 database that outputs a graph G with R as the root and I want two vertices A and B to be connected A->B if B is part of the proof of A.

Here is an example for https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/CharP/Frobenius.html#iterateFrobenius_add
Edges would go to: RingHom.ext, iterate_frobenius_add_apply.

Then I could use those two newly added theorems and continue: for example with iterate_frobenius_add_apply I would get iterateFrobenius_def, add_comm, pow_add, pow_mul.

Are there any utilities that I can use, if there aren't, are there any API's such that I can query the database and build it myself? When I talked to @Kim Morrison she helped me remove "import Mathlib" to the minimal set of imports with a trace option that gave the correct output.

[Aaron Liu]

metakuntyyy said:

• How can I make sure that tactics aren't doing something that is "too much magic". In particular how do I deconstruct tactics and figure out how to simpify them (going lower in the abstraction hierarchy)

You can see what a tactic outputs using show_term

[Aaron Liu]

Here's some code I wrote just now that can get you all the constants used in a theorem:

import Mathlib

run_meta do
  let name := ``iterateFrobenius_add
  let const ← Lean.getConstInfo name
  let type := const.type
  let val? := const.value?
  let typeConsts := type.getUsedConstants
  let valConsts? := val?.map Lean.Expr.getUsedConstants
  let allConsts := typeConsts.mergeUnsortedDedup (valConsts?.getD #[])
  Lean.logInfo (allConsts.map Lean.MessageData.ofConstName).toList

[Aaron Liu]

This prints

[CommSemiring,
 Nat,
 ExpChar,
 AddCommMonoidWithOne.toAddMonoidWithOne,
 NonAssocSemiring.toAddCommMonoidWithOne,
 Semiring.toNonAssocSemiring,
 CommSemiring.toSemiring,
 Eq,
 RingHom,
 iterateFrobenius,
 HAdd.hAdd,
 instHAdd,
 instAddNat,
 RingHom.comp,
 RingHom.ext,
 iterateFrobenius_add_apply]

[Aaron Liu]

You can also filter for just the theorems:

import Mathlib

run_meta do
  let name := ``iterateFrobenius_add
  let const ← Lean.getConstInfo name
  let type := const.type
  let val? := const.value?
  let typeConsts := type.getUsedConstants
  let valConsts? := val?.map Lean.Expr.getUsedConstants
  let allConsts := typeConsts.mergeUnsortedDedup (valConsts?.getD #[])
  let thms ← allConsts.filterM fun e => Lean.ConstantInfo.isTheorem <$> (Lean.getConstInfo e)
  Lean.logInfo (thms.map Lean.MessageData.ofConstName).toList

[Aaron Liu]

This prints

[RingHom.ext, iterateFrobenius_add_apply]

[metakuntyyy]

Oh wow, that is really great. Do you know by any chance how this interacts with tactics in particular those that do "lots of magic"?
WIll it print everything that those tactics also use?

I will definitely experiment with that one a bit.

[Aaron Liu]

It doesn't print everything the tactic uses, only the stuff that ends up in the proof.

[Aaron Liu]

linarith for example internally uses the simplex algorithm to find contradictions (see file#Tactic/Linarith/Oracle/SimplexAlgorithm and its imports if you're interested), but you see none of this in the generated proof term, because the proof doesn't need all the details of how a contradiction is found, it only needs the contradiction.

[metakuntyyy]

Ok that's a good point regarding linarith. It has "two" steps, the algorithm and the certificate. The algorithm (here a made up algorithm is used) "finds" a solution, lets say x<2 and y>3 and z=5 leads to a contradiction. Do the values end up in a proof, even though the algorithm had to calculate say thousand different failed cases that were necessary for the algorithm to find a solution?

In other words, let's assume I want to prove that graph A is colourable with three colours while graph B is not. And let's assume I have a specific tactic sat3, that proves those colourabilites while searching for all graphs. It is clear that the proof that graph A is colourable only needs to output the colouring and not all previously failed calculations. But to prove that graph B is not it would need to output to the kernel that it checked all cases.

Do those proof terms end up being part of this output, or are they opaque in a sense that the meta tactics have no access to them?

[Aaron Liu]

The proof term is what gets sent to the kernel. Tactics and such can see them, but there's generally no point, since all proofs are equal anyways.

[metakuntyyy]

Ah so I can print out the full proof term for every theorem?

[Aaron Liu]

Yes, just set_option pp.proofs true and then #print theorem_name

[Patrick Massot]

Depending on what you call the “full proof term”, you probably also want to set other pretty-printing options (maybe even pp.all).

[metakuntyyy]

Ok I've tried both your options, they work. I think "set_option pp.all true" might be a little too much overkill. I am now trying to figure out what kind of options there are

import Mathlib

elab "#printalloptions" : command => do
  let opts ← Lean.getOptions
  let kvs ← opts.entries

Unfortunately I get a very weird error that I can't decipher.
Error Message:

type mismatch
  opts.entries
has type
  List (Lean.Name × Lean.DataValue) : Type
but is expected to have type
  Lean.Elab.Command.CommandElabM (?m.191518 __discr✝¹ __discr✝ x✝ opts) : Type

[metakuntyyy]

Apparently this fixed it

import Mathlib
import Lean
open Lean

set_option pp.all true

elab "#printalloptions" : command => do
  let opts ← getOptions
  let entries := opts.entries
  IO.print entries

#printalloptions

I still have to research what the difference between the left arrow and := is

[Aaron Liu]

The ← assignment runs a monadic value, while the := binds a value without running anything. So if you have e : m Bool then let c ← e will leave c : Bool and let c := e will leave c : m Bool.

[metakuntyyy]

Is this related to the "state" that the do command introduced. Is that to make "getOptions" pure it has to introduce an environment to inject and running the monadic value gives you the state?

I assume getOptions is not "pure" by itself, to make it pure we need to inject the state as a parameter.

If I translated this in Rust would this syntax fit:

fn getOptions(state: State) ->(State,Options);

Basically something that returns me the state and options back. If I modify the state I have to pass the state into future calls?

Did I understand that correctly?

[Aaron Liu]

Something like that. When you do the := this is guaranteed supposed to have no side effects, and when you do ←, there are side effects.

[metakuntyyy]

Thank you very much for the patience and help. I'll experiment and play around a bit with all this information and see if how far I can make it before getting stuck.

[Patrick Massot]

Another tip: type set_option pp. and then trigger auto-complete to see what pretty-printing options exist.