Zulip Chat Archive

Stream: general

Topic: destructuring `suffices`


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?

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

Mario Carneiro (Apr 15 2020 at 14:04):

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

Mario Carneiro (Apr 15 2020 at 14:04):

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

Mario Carneiro (Apr 15 2020 at 14:05):

I actually would like to rename obtain to let

Mario Carneiro (Apr 15 2020 at 14:06):

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

Mario Carneiro (Apr 15 2020 at 14:07):

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

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.

Mario Carneiro (Apr 15 2020 at 14:08):

Unlike rcases, obtain backwards compatibly extends have syntax

Mario Carneiro (Apr 15 2020 at 14:09):

rintro is also backward compatible

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.

Patrick Massot (Apr 15 2020 at 14:10):

Lean doesn't care about backward compatibility, right?

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

Reid Barton (Apr 15 2020 at 14:10):

I think it's term mode's fault though

Reid Barton (Apr 15 2020 at 14:11):

and so have is better

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

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

Reid Barton (Apr 15 2020 at 14:15):

or tidy

Reid Barton (Apr 15 2020 at 14:15):

though tidy could adapt I suppose

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

Mario Carneiro (Apr 15 2020 at 14:16):

If you want to shoulder that responsibility, well okay then

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

Reid Barton (Apr 15 2020 at 14:17):

and some uses without with would be affected as well

Patrick Massot (Apr 15 2020 at 14:17):

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

Patrick Massot (Apr 15 2020 at 14:18):

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

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

Reid Barton (Apr 15 2020 at 14:19):

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

Johan Commelin (Apr 15 2020 at 14:20):

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

Mario Carneiro (Apr 15 2020 at 14:20):

I recall some discussion about that

Johan Commelin (Apr 15 2020 at 14:21):

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

Mario Carneiro (Apr 15 2020 at 14:21):

The only questionable spot is rcases _ with a

Mario Carneiro (Apr 15 2020 at 14:21):

because that fits in both grammars

Reid Barton (Apr 15 2020 at 14:22):

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

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 := _

Patrick Massot (Apr 15 2020 at 14:24):

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

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

Johan Commelin (Apr 15 2020 at 14:25):

Why not cases h with \<a\>?

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)

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.

Reid Barton (Apr 15 2020 at 14:26):

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

Mario Carneiro (Apr 15 2020 at 14:27):

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

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

Johan Commelin (Apr 15 2020 at 14:28):

Hmmm, good point

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

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

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?)

Mario Carneiro (Apr 15 2020 at 14:31):

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

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

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?

Mario Carneiro (Apr 15 2020 at 14:32):

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

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)

Reid Barton (Apr 15 2020 at 14:33):

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

Mario Carneiro (Apr 15 2020 at 14:33):

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

Reid Barton (Apr 15 2020 at 14:33):

rather than renaming all have to have_ or whatever

Reid Barton (Apr 15 2020 at 14:34):

ahh, hmm

Mario Carneiro (Apr 15 2020 at 14:34):

because it involves replacing have

Mario Carneiro (Apr 15 2020 at 14:35):

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

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.

Mario Carneiro (Apr 15 2020 at 14:36):

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

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

Mario Carneiro (Apr 15 2020 at 14:38):

Currently, obtain h, fails

Johan Commelin (Apr 15 2020 at 15:02):

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

Johan Commelin (Apr 15 2020 at 15:03):

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

Reid Barton (Apr 15 2020 at 15:04):

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

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:

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

Keeley Hoek (Apr 15 2020 at 15:11):

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

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: Aug 03 2023 at 10:10 UTC