Applying tactics to some but not all goals

Stream: new members

[Fancy Aluminum]

Hello,

I have a few goals that can be solved by an identical sequence of tactics:

  any_goals {unfold Rule.eval_head},
  any_goals {refine le_sup_iff.mpr _},
  any_goals{left},
  any_goals {simp},

(I'm not sure how to collapse that into a single usage of any_goals either )
However, some of these tactics also apply to later goals and destroy the proof I already developed for those goals.
So I'm wondering if there is a way to apply tactics only to select goals and not other ones.

Thanks,

[Arthur Paulino]

Have you tried tactic#work_on_goal?

[Arthur Paulino]

Hm the link doesn't work but work_on_goal i {⋯} applies the tactics ⋯ to the goal i (indexed from zero). You're not required to close the goals and Lean will remember any progress you make

[Fancy Aluminum]

I have not, is there a way to use work_on_goal so that it works on multiple goals at once? From the documentation it seems that it only works on one at a time

[Fancy Aluminum]

I suppose I could solve the goal that is being ruined by any_goals first and then try

[Damiano Testa]

I think that any_goals { tac1, tac2,... } should apply to all goals where the sequence tac1, tac2,... works. In particular, if one of the tactics does not work on the goals that you do not want to change, then you are in luck!

[Damiano Testa]

Notice that any_goals { tac1 }, any_goals { tac2 } is very different from any_goals { tac1, tac2 }: the former is much more likely of using tactic tac2 than the latter.

[Alex J. Best]

tactic#try might also be useful here?

[Fancy Aluminum]

Thanks :) I feel like I understand Lean a bit better now. I was able to solve it a few different ways with your suggestions

[Patrick Johnson]

Arthur Paulino said:

Hm the link doesn't work

docs#tactic.interactive.work_on_goal

[Junyan Xu]

(deleted)

[Junyan Xu]

For finer control and less wasted CPU cycles on with try or any_goals: if you want to apply the same thing to goals # 4, # 5, # 7, you can do

swap 4, swap 5, swap 7,
iterate 3 { /- same thing that applies to all three -/ },

because swap n doesn't actually exchange the first goal with the nth, but actually do a cyclic permutation of the first n goals.