## Stream: general

### Topic: work_on_goals?

#### Alex J. Best (Apr 07 2020 at 15:25):

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 (Apr 07 2020 at 15:28):

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

#### Jannis Limperg (Apr 07 2020 at 15:48):

focus might be the what you're looking for.

#### Alex J. Best (Apr 07 2020 at 15:50):

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

#### Scott Morrison (Apr 07 2020 at 22:18):

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 (Apr 08 2020 at 00:44):

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 (Apr 08 2020 at 01:01):

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

#### Scott Morrison (Apr 08 2020 at 01:02):

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

#### Scott Morrison (Apr 08 2020 at 01:03):

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

#### Scott Morrison (Apr 08 2020 at 01:03):

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

Last updated: May 13 2021 at 17:42 UTC