Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: change all goals


view this post on Zulip Patrick Massot (Jan 19 2021 at 13:41):

I know how to use change_core to change the goal to some new defeq expr. What if I have a list of expr and I want to change the first goal to the first expr in my list, the second goal to the second expr etc.?

view this post on Zulip Jannis Limperg (Jan 19 2021 at 13:53):

tactic.focus should allow you to do this. Essentially you build a list of tactic that applies change_core e_i, then use focus to apply the ith tactic to the ith goal.

view this post on Zulip Patrick Massot (Jan 19 2021 at 14:01):

Thanks! I hacked something with swap but your solution is probably better.

view this post on Zulip Patrick Massot (Jan 19 2021 at 14:18):

And of course my hack didn't actually work when there are more than two goals, whereas tactic.focus' is exactly intended for the job.

view this post on Zulip Simon Hudon (Jan 19 2021 at 15:05):

If you're comfortable using get_goals / set_goals, that gs is your list of goals, try either of the following:

(es.zip gs).mmap' $ \lam (e, g), do { set_goals [g], change_core e, ..., done }

(if you intend to solve all goals in one go) or

do gs' <- (es.zip gs).mmap $ \lam (e, g),
   do { set_goals [g],
        change_core e,
        /- do some work here -/,
        get_goals },
   let gs' := gs'.join,
   /- now `gs'` is your new list of goals -/

view this post on Zulip Patrick Massot (Jan 19 2021 at 15:08):

Thanks. I'm not sure I understand this code, but Jannis' suggestion was enough for me.

view this post on Zulip Simon Hudon (Jan 19 2021 at 15:10):

Sorry, I don't do the change like you asked, just the focus part

view this post on Zulip Simon Hudon (Jan 19 2021 at 15:13):

Is the use of set_goals / get_goals the part that's unclear?

view this post on Zulip Patrick Massot (Jan 19 2021 at 15:15):

You changed the message since I wrote that (or while I was writing it). It's clearer now, although I still don't know what work you want to do there.

view this post on Zulip Simon Hudon (Jan 19 2021 at 15:21):

I assumed you would want to run a tactic on the goal after changing the statement.

view this post on Zulip Patrick Massot (Jan 19 2021 at 15:29):

No, I still need to keep some work to do for students.


Last updated: May 09 2021 at 21:10 UTC