## Stream: general

### Topic: tac1;{tac2, tac3}

#### Kevin Buzzard (Apr 24 2020 at 23:34):

Is there a way of applying a tactic (which creates several goals) and then applying a list of tactics to all the resulting goals? I don't want to use tac1;tac2;tac3 because I think it looks ugly to use ; when tactics are not creating extra goals. I like this new by {tac1, tac2} style and I'd like to extend it to this case if possible.

#### Reid Barton (Apr 24 2020 at 23:35):

tac1; { tac2, tac3 }?

#### Kevin Buzzard (Apr 24 2020 at 23:35):

I couldn't get it to work. Am I just an idiot? I'll try again.

#### Reid Barton (Apr 24 2020 at 23:36):

Is that the kind of list you have in mind? You want to apply the same sequence of several tactics to each goal created by tac1?

Yes.

#### Kevin Buzzard (Apr 24 2020 at 23:38):

I'm getting an error on the semicolon.

#### Kevin Buzzard (Apr 24 2020 at 23:39):

example (a b c d e : ℕ) (h1 : c = d) (h2 : d = e) : a = c ∧ b = c :=
begin
split; {rw h1, rw h2},
end


Would you expect this to work?

#### Kevin Buzzard (Apr 24 2020 at 23:40):

example (a b c d e : ℕ) (h1 : c = d) (h2 : d = e) : a = c ∧ b = c :=
begin
split; rw h1; rw h2,
end


works fine but I don't like the semicolon after h1

#### Bryan Gin-ge Chen (Apr 24 2020 at 23:41):

I think the stuff in the braces has to succeed on every goal created by the tactic before the semicolon. I'm surprised the second example works.

#### Kevin Buzzard (Apr 24 2020 at 23:42):

It doesn't solve the goal, it just doesn't give an error.

#### Bryan Gin-ge Chen (Apr 24 2020 at 23:42):

Oh wait, I misread the first example.

#### Kevin Buzzard (Apr 24 2020 at 23:43):

example (a b c d e : ℕ) (h1 : c = d) (h2 : d = e) : a = c ∧ b = c :=
begin
split; rw h1; rw h2,
sorry, sorry
end


is OK but

example (a b c d e : ℕ) (h1 : c = d) (h2 : d = e) : a = c ∧ b = c :=
begin
split;{rw h1, rw h2},
sorry, sorry
end


gives

solve1 tactic failed, focused goal has not been solved
state:
a b c d e : ℕ,
h1 : c = d,
h2 : d = e
⊢ a = e


#### Reid Barton (Apr 24 2020 at 23:43):

Oh right, if you use { } then you have to finish the goal.

#### Reid Barton (Apr 24 2020 at 23:43):

You can also write split, all_goals {rw h1, rw h2}

#### Alex J. Best (Apr 24 2020 at 23:43):

 split; try {rw h1, rw h2},

#### Reid Barton (Apr 24 2020 at 23:43):

or split; rw [h1, h2] :upside_down:

#### Kevin Buzzard (Apr 24 2020 at 23:44):

hence my question

#### Reid Barton (Apr 24 2020 at 23:45):

I guess the try version is the one that does exactly what you asked

#### Reid Barton (Apr 24 2020 at 23:46):

the one with all_goals would also apply to any other goals you have floating around

Thanks.

#### Mario Carneiro (Apr 25 2020 at 01:04):

I use try for this. Unfortunately [...] doesn't work because it takes the line out of interactive mode, and do is already taken - I really want a notation for the identity function in interactive tactics

#### Mario Carneiro (Apr 25 2020 at 01:06):

I guess all_goals will also work - that is split; all_goals {rw h1, rw h2} - because when there is only one goal all_goals` is the identity

Last updated: May 13 2021 at 00:41 UTC