tree structure from a proof

Stream: metaprogramming / tactics

[Anthony Bordg]

Among Lean's metaprogramming features, can one find some operation that takes as input the identifier of a theorem and output some kind of generalized tree/graph representation of its proof script? E.g. a tree whose leaves would be the premises of the said theorem, the root its end goal (conclusion) and with the other nodes corresponding to some intermediate goals occurring within the proof script; the parents of a node being the statements that used this node to be discharged (in this sense a child can have more than one parent).

[Aaron Liu]

Well we have #explode

[Aaron Liu]

You could also interpret the Expr of the proof as a sort of tree

[Aaron Liu]

The nodes are the subexpressions

[Damiano Testa]

It depends on how explicitly you want this, but the InfoTree contains a lot of this information.

[Eric Wieser]

Is paperproof along the lines of what you're asking for?

[Anthony Bordg]

Aaron Liu said:

Well we have #explode

Does it require to import some libraries?

[Aaron Liu]

It's in Mathlib/Tactic/Explode.lean and produces a fitch-style proof string

[Anthony Bordg]

Thank you. Good to know, though I'm not sure how usable this would be, because it can produce huge 4-column diagrams.

[Anthony Bordg]

Damiano Testa said:

It depends on how explicitly you want this, but the InfoTree contains a lot of this information.

Actually, something a little less explicit than #explode may be better. Now I have to understand how to use InfoTree :)

[Damiano Testa]

I don't have a thorough understanding of InfoTrees, but my mental model is that all the information that you can get by placing your cursor anywhere in a command and looking at the infoview is contained in the InfoTree (and more!).

[Damiano Testa]

So, you'll probably have to do quite a bit of pruning to get what you want, but it'll be there!

[Anthony Bordg]

Eric Wieser said:

Is paperproof along the lines of what you're asking for?

Thank you for the pointer, it's certainly relevant - and a nice tool for displaying proof histories! - even though it's more oriented as a displaying tool for human visualisation and less as a data-extraction tool for ML.

[Adam Topaz]

@Anthony Bordg a little while ago I made www.github.com/adamtopaz/expr_graph . I don’t know if it works with current mathlib. If you think this is useful for you, please let me know and I’ll update it to the latest version of lean/mathlib.

[Adam Topaz]

It’s not quite the tree-like structure you’re looking for, but it’s related, and it does work for arbitrary expressions