Zulip Chat Archive

Stream: general

Topic: work_on_goals?


view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Jannis Limperg (Apr 07 2020 at 15:48):

focus might be the what you're looking for.

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 { ... } }.

view this post on Zulip 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