Split tactic_state into multiple

Stream: general

[fzyzcjy]

Hi friends! I wonder how a tactic_state can be splited into multiple sub-goals. For example, suppose a tactic_state contains goal A and goal B, I want to obtain two tactic_state objects, one for goal A and another for goal B. Thanks for any suggestions!

Context: I am trying to reproduce the SOTA paper, thus needs to modify lean-gym, such that it can create multiple subgoals. The lean-gym currently only creates one subgoal. I have tried to read tactic writing and metaprogramming related tutorials but still cannot find out a way yet.

[Mario Carneiro]

this doesn't make sense to do. Each tactic_state represents a partial proof of the original goal, so unless goal B has already been closed you can't have a tactic state containing only goal A without erroneously dropping goal B

[fzyzcjy]

@Mario Carneiro Hi thanks for the reply! Totally agree that partially proving goal A without B proved is nonsense. However, that paper is doing a tree search, so roughly speaking, the AI (which interacts with Lean) will solve goal A and B separately using two searches. I am willing to accept unsoundness at this phase, because later the AI can generate a full proof and I can just plug in that proof text into a .lean file and let Lean check again.

[Mario Carneiro]

A goal in lean is represented as a mvar, which you can manipulate using get_goals and set_goals. So you can just do [A, B] <- get_goals, set_goals [A] if you want to drop B

[fzyzcjy]

Thank you so much! Let me try it