Zulip Chat Archive

Stream: general

Topic: Parse goal string

Tung Tran (Feb 02 2022 at 22:35):

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 (Feb 02 2022 at 23:04):

You can do it in the parser monad

Jason Rute (Feb 06 2022 at 04:03):

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 (Feb 06 2022 at 04:04):

It might however help if you explain your use case.

Tung Tran (Feb 08 2022 at 02:14):

@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 (Feb 08 2022 at 02:50):

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 (Feb 08 2022 at 02:52):

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 (Feb 08 2022 at 02:58):

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

Tung Tran (Feb 08 2022 at 03:02):

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 (Feb 08 2022 at 03:08):

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.

Last updated: Dec 20 2023 at 11:08 UTC