Stream: general

Topic: swap one goal

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?

Simon Hudon (Oct 21 2020 at 01:44):

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

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.

Simon Hudon (Oct 21 2020 at 01:52):

So it can be kind of noisy

Simon Hudon (Oct 21 2020 at 01:52):

I also feel like it should be an error

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 }

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.

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

Simon Hudon (Oct 21 2020 at 01:59):

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

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 _

Reid Barton (Oct 21 2020 at 02:03):

then I had a swap that did nothing

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

Reid Barton (Oct 21 2020 at 02:04):

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

Simon Hudon (Oct 21 2020 at 02:06):

I see what you mean

Simon Hudon (Oct 21 2020 at 02:06):

It would make things better to get swap to fail

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}.

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

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