Zulip Chat Archive

Stream: general

Topic: destructuring `suffices`


view this post on Zulip Reid Barton (Apr 15 2020 at 14:02):

obtain is basically a destructuring have, that is, a combination of have and rcases, right?
Would it be sensible to have a matching destructuring suffices?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:03):

It's the same thing but with the goals in another order, right? It would have n+1 goals with n "conclusions" following the case split and then 1 proof of the target type

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:04):

Do we have a rotate 1 tactic? Because it should have the same effect

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:04):

that is, move the first goal to the end and move everything else up by one

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:05):

I actually would like to rename obtain to let

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:06):

or possibly have; have is more correct but let lines up with term mode better

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:07):

If we did rename obtain to have, then destructuring suffices could be called just suffices

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:08):

obtain is called obtain instead of have because have was locked in core. obtain is what have should be, in the very same way that rintro is what intro should be, and rcases is what cases should be.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:08):

Unlike rcases, obtain backwards compatibly extends have syntax

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:09):

rintro is also backward compatible

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:09):

I also with rcases and rintros could clear all autogenerated names after doing their rfl magic. When I replace one name of rcases with _ it is either because a later rfl will discard it or because I don't plan to use it.

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:10):

Lean doesn't care about backward compatibility, right?

view this post on Zulip Reid Barton (Apr 15 2020 at 14:10):

Mario Carneiro said:

or possibly have; have is more correct but let lines up with term mode better

Yeah, this is annoying

view this post on Zulip Reid Barton (Apr 15 2020 at 14:10):

I think it's term mode's fault though

view this post on Zulip Reid Barton (Apr 15 2020 at 14:11):

and so have is better

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:12):

I often use rcases with a lot of underscores, but only half the time they are unnamed because of later rfl, the other half of the time they are just not going to be referred to, even if they appear in the goals or something

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:13):

and given stuff like assumption or simp * I think it would be a breaking change to delete auto named variables

view this post on Zulip Reid Barton (Apr 15 2020 at 14:15):

or tidy

view this post on Zulip Reid Barton (Apr 15 2020 at 14:15):

though tidy could adapt I suppose

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:15):

Patrick Massot said:

Lean doesn't care about backward compatibility, right?

Leo will do what he does, but I care about backward compatibility, at least to the extent that I feel the pain of updating a large codebase like mathlib following a big change. That is to say, changes are not verboten but they must be weighed against the cost of updating many proof scripts

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:16):

If you want to shoulder that responsibility, well okay then

view this post on Zulip Reid Barton (Apr 15 2020 at 14:17):

git grep '\bcases.*with' | wc -l is obviously a bit crude, but it's around 1000 lines which is indeed quite a lot

view this post on Zulip Reid Barton (Apr 15 2020 at 14:17):

and some uses without with would be affected as well

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:17):

I think this is bad style to have useful autogenerated names, but ok.

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:18):

Of course such a change would be much easier for the Lean 4 refactoring tools.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:18):

I think that in isabelle style you don't name anything and just use assumption or lookup by type

view this post on Zulip Reid Barton (Apr 15 2020 at 14:19):

More precisely what is bad style is to refer to an autogenerated name by name

view this post on Zulip Johan Commelin (Apr 15 2020 at 14:20):

Why is rcases incompatible with cases? Can't the parser check whether we have \< or not?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:20):

I recall some discussion about that

view this post on Zulip Johan Commelin (Apr 15 2020 at 14:21):

If the stuff following with starts with \< then use rcases, otherwise use ancient cases

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:21):

The only questionable spot is rcases _ with a

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:21):

because that fits in both grammars

view this post on Zulip Reid Barton (Apr 15 2020 at 14:22):

(oh, maybe that's what Patrick meant by "useful")

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:22):

Currently, I think both rcases and cases treat that as one case split, but compatibility with have and friends would require that to behave the same as have a := _

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:24):

I wouldn't care if cases _ with a is broken. I would never write that.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:24):

this is especially problematic for destructuring something like inhabited A using cases because cases h with a is the only reasonable way to write it

view this post on Zulip Johan Commelin (Apr 15 2020 at 14:25):

Why not cases h with \<a\>?

view this post on Zulip Reid Barton (Apr 15 2020 at 14:25):

cases definitely treats it as one case split, rcases is rarely used with this syntax (I found a couple uses by Sebastien)

view this post on Zulip Johan Commelin (Apr 15 2020 at 14:25):

Anyway, we can make a choice in that corner case, and fix the breakage. It will be a lot less then the 1000 results from Reid's grep.

view this post on Zulip Reid Barton (Apr 15 2020 at 14:26):

There's ~125 uses of cases _ with a for single-letter variables a

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:27):

What if we remove rcases and just use obtain/have?

view this post on Zulip Reid Barton (Apr 15 2020 at 14:28):

there's also rcases with a | b to consider so determining which case you're in is not quite as simple as described above

view this post on Zulip Johan Commelin (Apr 15 2020 at 14:28):

Hmmm, good point

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:28):

cases still needs to exist for the non-with version, and it can also be used as the lower level single split version

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:30):

I wonder if there are cases where the rcases order is more readable. I know I have written some mile long rcases patterns

view this post on Zulip Reid Barton (Apr 15 2020 at 14:30):

I like this but actually removing rcases would have the largest maintenance burden so far. I suppose we could just deprecate it (in which case what has changed really?)

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:31):

It has a weird name so deprecating it shouldn't be a problem

view this post on Zulip Andrew Ashworth (Apr 15 2020 at 14:31):

I imagine when Lean 4 comes around and all of mathlib is rewritten, it being deprecated means you'll get the transition for free

view this post on Zulip Reid Barton (Apr 15 2020 at 14:32):

Is it possible to do something like open tactic.interactive.core to cause foo in interactive mode to be understood as tactic.interactive.core.foo?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:32):

no, the only thing that affects this lookup is begin [foo] end

view this post on Zulip Reid Barton (Apr 15 2020 at 14:33):

hmm. Presumably we'd need have for a while before rcases is available (for example, in the core library)

view this post on Zulip Reid Barton (Apr 15 2020 at 14:33):

I was hoping we could play with the namespaces in the core library

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:33):

I was planning to move rcases into the core library for this

view this post on Zulip Reid Barton (Apr 15 2020 at 14:33):

rather than renaming all have to have_ or whatever

view this post on Zulip Reid Barton (Apr 15 2020 at 14:34):

ahh, hmm

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:34):

because it involves replacing have

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:35):

I wonder if kenny will start a "have is slow" thread after this change though

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:36):

I was also worried about that. Those are very core tactics, and maybe slowing them down is a bad idea.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:36):

we definitely need to make sure that have x := foo and such are fast-pathed

view this post on Zulip Reid Barton (Apr 15 2020 at 14:36):

so is the summary:

  • Leave cases alone
  • Move rcases into core
  • Deprecate rcases but incorporate its functionality into have (effectively replacing obtain) and suffices

view this post on Zulip Mario Carneiro (Apr 15 2020 at 14:38):

Currently, obtain h, fails

view this post on Zulip Johan Commelin (Apr 15 2020 at 15:02):

Are these remarks by Keeley relevant: https://github.com/leanprover-community/mathlib/pull/2300#discussion_r408577486 ?

view this post on Zulip Johan Commelin (Apr 15 2020 at 15:03):

It sounds like we can transparently repurpose all begin ... end block to be begin [foo] ... end

view this post on Zulip Reid Barton (Apr 15 2020 at 15:04):

Well, it's no longer relevant if the plan is to move have into core

view this post on Zulip Patrick Massot (Apr 15 2020 at 15:06):

Johan Commelin said:

Are these remarks by Keeley relevant: https://github.com/leanprover-community/mathlib/pull/2300#discussion_r408577486 ?

Oh, @Keeley Hoek is back! :tada:

view this post on Zulip Keeley Hoek (Apr 15 2020 at 15:09):

But yes, to be clear, you could already do the [foo] thing by local instance-ing a particular interactive.executor

view this post on Zulip Keeley Hoek (Apr 15 2020 at 15:11):

(Maybe with a command or something to add sugar to make it look nicer)

view this post on Zulip Keeley Hoek (Apr 15 2020 at 15:11):

(And as a result the namespace under which the interactive tactics are resolved is changed---I think, at any rate it should do this)


Last updated: May 13 2021 at 19:20 UTC