change all goals

Stream: metaprogramming / tactics

[Patrick Massot]

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.?

[Jannis Limperg]

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.

[Patrick Massot]

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

[Patrick Massot]

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.

[Simon Hudon]

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 -/

[Patrick Massot]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

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.

[Simon Hudon]

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

[Patrick Massot]

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