Zulip Chat Archive

Stream: general

Topic: tac1;{tac2, tac3}


view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 24 2020 at 23:35):

tac1; { tac2, tac3 }?

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 23:35):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 23:36):

Yes.

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 23:38):

I'm getting an error on the semicolon.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 23:42):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 24 2020 at 23:42):

Oh wait, I misread the first example.

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 24 2020 at 23:43):

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

view this post on Zulip Reid Barton (Apr 24 2020 at 23:43):

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

view this post on Zulip Alex J. Best (Apr 24 2020 at 23:43):

split; try {rw h1, rw h2},

view this post on Zulip Reid Barton (Apr 24 2020 at 23:43):

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

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 23:44):

hence my question

view this post on Zulip Reid Barton (Apr 24 2020 at 23:45):

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

view this post on Zulip Reid Barton (Apr 24 2020 at 23:46):

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

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 23:53):

Thanks.

view this post on Zulip 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

view this post on Zulip 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