proof->ast->proof

Stream: metaprogramming / tactics

[Jiaming Shan]

I want to get the ast(abstract syntax tree) of the lean code, modify the ast, and translate it back to lean code. What is the best tool I can use?

[Aaron Liu]

Do you want something like the syntax tree or something like the proof expression?

[Jiaming Shan]

I think I want syntax tree. For example, I want to do things like change all rw[a,b] to rw[a]; rw[b], so I want to use syntax tree to do this job (string pattern matching is too ugly and difficult to scale)

[Aaron Liu]

How do you have access to the code? You could take input as Syntax, for example

[Jiaming Shan]

I have lean proof source code.

[Jiaming Shan]

What do you mean by take input as Syntax?

[Aaron Liu]

def doStuff (stx : Syntax) : IO Unit := ...

[Jiaming Shan]

Actually I want the ast form to be something like json or python object so I can use my more familiar python to process it. Whether the community have such kind of tools, or I can only use metaprogramming in lean language itself to change the ast?

[Jiaming Shan]

Also, the proof is not necessarily correct, maybe use the wrong tactic or theorem or something else (that's why I want to change the proof).

[Jiaming Shan]

I found a project ast_export that can transform lean to json by toJson in lean, but it has not implemented the other direction, fromJson, while this has an implementation in lean https://github.com/leanprover/lean4/blob/master/src/Lean/Data/Json/FromToJson.lean
So I believe this can be done and I don't know if we already has a tool to do this.

[Siddhartha Gadgil]

The first thing to note about Lean is that it has two forms of internal representations, i.e., analogues of ASTs. There is Syntax and there is Expr. The latter is in the foundations of Lean.

[Siddhartha Gadgil]

It is quite straightforward to access both of them.

[Niels Voss]

Do note that Expr contains the actual code after the tactics have run. So if your plan is to modify tactics before they are run, then you can't use Expr and you have to use Syntax

[Niels Voss]

How do you imagine the Lean<->Python interface working? Are you planning on using Python to modify the Lean source code file, interact with the LSP, or just be a script that Lean will call and modify the tactics without actually changing the Lean source code?

[Jiaming Shan]

I want to fix a wrong lean proof, so what I imagine is that I want to first extract a syntax ast from lean code and export it in json format. (and if that tree have some runtime info that would be better (but maybe that should be another tree, like infotree)). Then I use python to work on that syntax tree and change and fix it (by syntax info and maybe some runtime info), then I translate the modified lean syntax tree back to lean code.

[Shreyas Srinivas]

I think you might be looking for unexpanders or delaborators in #mpil

[Shreyas Srinivas]

But if you insist on using json, I think lean-repl takes you from lean code to json. I am not sure how the other way could be accomplished systematically

[Jiaming Shan]

@Shreyas Srinivas Can you recommend me some material to learn the topic "unexpanders or delaborators in #mpil"?

[Shreyas Srinivas]

Mpil is short for “metaprogramming in lean 4”

[Jiaming Shan]

:rolling_on_the_floor_laughing: I see

[Shreyas Srinivas]

It’s a book that explains lean metaprogramming and it has chapters on delaborators and unexpanders

[Edward van de Meent]

well... it doesn't, really... it basically only mentions them in passing, imo.