work_on_goals?

Stream: general

[Alex J. Best]

Is there a tactic or recommended way to work on a specific subset of the set of current goals, (I have 5 and I want to run one set of tactics on 3 of them and one set on the other two)? Currently all I can think of is naming my tactics scripts and calling the relevant one on each, but this would be unwieldy on more than 5.

[Alex J. Best]

Actually I guess this is a duplicate of the goal selectors topic we had recently, sorry!

[Jannis Limperg]

focus might be the what you're looking for.

[Alex J. Best]

Maybe not exactly what I'm looking for but definitely useful and not something I was aware of, thanks!

[Scott Morrison]

My students at one point had work_on_goals as a homework assignment. :-) It's only a few lines long --- someone should PR it!

[Lucas Allen]

I don't know how good this is.

namespace tactic.interactive

meta def work_on_goals (p : interactive.parse lean.parser.pexpr) (tac : itactic) : tactic unit :=
do gs ← get_goals,
   e ← to_expr p,
   l ← eval_expr (list ℕ) e,
   let gl := l.filter_map (λ x, gs.nth x),
   let glc := gs.remove_all gl,
   set_goals gl,
   all_goals tac,
   gs ← get_goals,
   set_goals (gs ++ glc)

end tactic.interactive

[Scott Morrison]

Oh, I wasn't certain what the intended semantics was here. I'd expected just tac, rather than all_goals tac.

[Scott Morrison]

i.e., the interactive tactic was for entering a scope in which you could only see a subset of the goals.

[Scott Morrison]

perhaps then some_goals [3,5,8] { ... } could be defined as work_on_goals [3,5,8] { all_goals { ... } }.

[Scott Morrison]

But besides deciding this, and giving an error message if eval_expr fails, and addings docs, yes, someone should PR this!