Parse goal string

Stream: general

[Tung Tran]

Hi, I'm trying to parse a string as the current goal, e.g. false.

The problem was mentioned in this thread but it seems no solution was found.

[Mario Carneiro]

You can do it in the parser monad

[Jason Rute]

The situation has improved since I started that thread. Search for other threads (probably in reverse chronological order) where I talk about the parser monad. (And if you need to set a new goal, that is also possible.)

[Jason Rute]

It might however help if you explain your use case.

[Tung Tran]

@Jason Rute Thanks for the help! I was actually trying to modify the goal (e.g. add hypothesis, remove cases). I'm using the code found in one of the libraries in your PACT paper. Even though they are extremely helpful, it's hard to work with Lean's metaprogramming as I didn't have function programming experience.

Extending from the paper, I want to put GPT into a feedback loop with something like the hindsight experience replay. I relax a wrong answer by modifying the goal to fit the response, and pretending it was the goal we want to prove from the start. Would something like that work?

[Jason Rute]

HER (similar to say https://openreview.net/forum?id=QDDVxweQJy0) should work for tactic proofs but you will have to work out the logic exactly. You might have luck working in strings, but I suspect you will have a more robust system working directly with the lean objects. (Specifically taking the Lean goal output and manipulating that according to HER.) But yes, that involves a lot of meta programming since you don’t just have to access the goal statement but also the local context. Here is some code which serializes the tactic state to JSON and deserializes it. https://github.com/jesse-michael-han/lean-tpe-public/blob/master/src/tactic_state.lean Theoretically when you understand how it all works you should be able to manipulate the goal in the way you need for HER.

[Jason Rute]

But if you just want to get started playing with ideas, it might be easier to just take the pretty printed tactic state and do text manipulations on that and the use the parser to reload the manipulated goal string back into lean.

[Tung Tran]

Wow I've been trying to find something similar but to no avail. Thank you!

[Tung Tran]

And I just realized there's a meta-programming thread here. facepalm
I'm messing with the notebook you wrote actually, just to create a proof of concept.

[Jason Rute]

To give some history, that notebook was also my first attempt playing around. It worked ok, but wasn’t really that practical. It was also before we had the ability to parse a string into a Lean expression via https://leanprover-community.github.io/mathlib_docs/find/lean.parser.run_with_input.