Zulip Chat Archive

Stream: general

Topic: swap one goal


view this post on Zulip Reid Barton (Oct 21 2020 at 01:34):

Just something that occurred to me, but should swap when there's just one goal be an error? Or are there cases (probably involving things like ;?) where the current behavior (do nothing) is useful?

view this post on Zulip Simon Hudon (Oct 21 2020 at 01:44):

Are you asking because not having an error is giving you trouble?

view this post on Zulip Reid Barton (Oct 21 2020 at 01:48):

No actual trouble, I just had a swap that did nothing left over in my proof after a refactor.

view this post on Zulip Simon Hudon (Oct 21 2020 at 01:52):

So it can be kind of noisy

view this post on Zulip Simon Hudon (Oct 21 2020 at 01:52):

I also feel like it should be an error

view this post on Zulip Simon Hudon (Oct 21 2020 at 01:54):

If you're swapping the first two goals, you should know what the two goals correspond to, i.e. that they exist and they say something specific. Otherwise, you could do try { swap }

view this post on Zulip Reid Barton (Oct 21 2020 at 01:54):

I haven't really thought about it, but most tactics fail instead of doing nothing, on the premise that the user probably intended for something to happen.

view this post on Zulip Reid Barton (Oct 21 2020 at 01:56):

I'm using the slightly awkward specialize h _, swap, { ... }, repeatedly to provide a series of complicated arguments to a hypothesis

view this post on Zulip Simon Hudon (Oct 21 2020 at 01:59):

I don't see the connection between this last part and the rest

view this post on Zulip Reid Barton (Oct 21 2020 at 02:03):

I think what happened was that one of the { ... }s actually turned out to be trivial, so I moved it inline in place of the _

view this post on Zulip Reid Barton (Oct 21 2020 at 02:03):

then I had a swap that did nothing

view this post on Zulip Simon Hudon (Oct 21 2020 at 02:04):

I don't think I would say that we shouldn't let tactic do nothing. Sometimes, it's a natural generalization, like providing zero arguments to a function can sometimes make sense. Especially when you're trying to apply the same tactics multiple times

view this post on Zulip Reid Barton (Oct 21 2020 at 02:04):

but the whole construction feels kind of awkward in the first place

view this post on Zulip Simon Hudon (Oct 21 2020 at 02:06):

I see what you mean

view this post on Zulip Simon Hudon (Oct 21 2020 at 02:06):

It would make things better to get swap to fail

view this post on Zulip Floris van Doorn (Oct 21 2020 at 06:48):

I also think swap should fail on one goal. Someone who wants it can still run try {swap}.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 06:52):

If swap did a rotation, then it would be reasonable for it to succeed on 1 goal

view this post on Zulip Mario Carneiro (Oct 21 2020 at 06:52):

but I think the present behavior is to move goal n to the front, in which case it should probably require that goal n exists


Last updated: May 14 2021 at 04:22 UTC