tac1;{tac2, tac3}

Stream: general

[Kevin Buzzard]

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]

tac1; { tac2, tac3 }?

[Kevin Buzzard]

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

[Reid Barton]

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?

[Kevin Buzzard]

Yes.

[Kevin Buzzard]

I'm getting an error on the semicolon.

[Kevin Buzzard]

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]

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]

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]

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

[Bryan Gin-ge Chen]

Oh wait, I misread the first example.

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Alex J. Best]

split; try {rw h1, rw h2},

[Reid Barton]

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

[Kevin Buzzard]

hence my question

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

Thanks.

[Mario Carneiro]

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]

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