In structured proof, how to focus on a specific goal in interaction mode

[subfish-zhou]

Hi,
In Lean, if the intermediate step of a proof has multiple goals, we can use some structured instruction "·" or "|" to focus on a certain goal. For example:

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  . apply Or.inr
    assumption
  . apply Or.inl
    assumption

But if I use this "·" in dojo.run_tac(), it usually returns LeanError.

I checked some TracedTheorem, and it seems that we can only use structured proofs if a structured tactic proves a goal completely. Although Lean can still apply the tactic to the current state without using structured instruction, this may cause the tactic to be applied to another goal (if it can't be applied to the first goal successfully).
If we are using a generative model that provides tactic suggestions for specific goals, it is difficult to control the direction of the proof search.

Similarly, the "match" expression and "induction" expression has the same problem, for example:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    match h with
    | ⟨_, Or.inl _⟩ => apply Or.inl; constructor <;> assumption
    | ⟨_, Or.inr _⟩ => apply Or.inr; constructor <;> assumption
  . intro h
    match h with
    | Or.inl ⟨hp, hq⟩ => constructor; exact hp; apply Or.inl; exact hq
    | Or.inr ⟨hp, hr⟩ => constructor; exact hp; apply Or.inr; exact hr

I can't use dojo.run_tac(state, "| ⟨_, Or.inl _⟩ => apply Or.inl; constructor <;> assumption"), here only "apply Or.inl; constructor <;> assumption" is considered tactic.

"calc" mode seems to have a similar problem.

I'm wondering if there is a good way to deal with this situation?

[darabos]

Your first example can be rewritten as:

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  apply Or.inr
  assumption
  apply Or.inl
  assumption

Almost all · blocks work just as well without introducing a block. Perhaps the other multi-tactic constructions can also be phrased as equivalent flat tactic sequences in some way.

[subfish-zhou]

The motivation for this problem is that I want to develop a tactic generation model that focuses on a single goal, and in a certain state I want to expand a specific goal to evaluate it. Structured instructions are also natural to humans, and it would be a shame if we could not use them.

btw, the same issue happens on official REPL. It looks like the issue comes from Lean itself.

[darabos]

You can just take the first goal from the state, generate tactics for that, and run those tactics without a ·. Almost all tactics operate on just the first goal. (Exceptions are all_goals, swap, and maybe some more.)

[subfish-zhou]

What if I want to prove the second goal first? Additionally, if I generate a proof for the first goal, but it doesn't succeed on the first goal but succeeds on the second goal, there doesn't seem to be a good way to check this.

[darabos]

Sorry, I don't mean to be dismissive of your questions. I've been looking at the same questions. I'll just share the ideas we had, in case you find them useful.

What if I want to prove the second goal first?

It's simplest to just solve them in order. You have to solve them all anyway. But you can skip a goal by running · sorry, or reorder goals with pick_goal. For example:

example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h
  pick_goal 2
  apply Or.inl
  assumption
  apply Or.inr
  assumption

(swap is a shorthand for pick_goal 2.)

[subfish-zhou]

Thank you! pick_goal is really helpful.