destructuring `suffices`

Stream: general

[Reid Barton]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

I actually would like to rename obtain to let

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

Unlike rcases, obtain backwards compatibly extends have syntax

[Mario Carneiro]

rintro is also backward compatible

[Patrick Massot]

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]

Lean doesn't care about backward compatibility, right?

[Reid Barton]

Mario Carneiro said:

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

Yeah, this is annoying

[Reid Barton]

I think it's term mode's fault though

[Reid Barton]

and so have is better

[Mario Carneiro]

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]

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

[Reid Barton]

or tidy

[Reid Barton]

though tidy could adapt I suppose

[Mario Carneiro]

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]

If you want to shoulder that responsibility, well okay then

[Reid Barton]

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]

and some uses without with would be affected as well

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Johan Commelin]

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

[Mario Carneiro]

I recall some discussion about that

[Johan Commelin]

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

[Mario Carneiro]

The only questionable spot is rcases _ with a

[Mario Carneiro]

because that fits in both grammars

[Reid Barton]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

Why not cases h with \<a\>?

[Reid Barton]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

Hmmm, good point

[Mario Carneiro]

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]

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]

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]

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

[Andrew Ashworth]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

rather than renaming all have to have_ or whatever

[Reid Barton]

ahh, hmm

[Mario Carneiro]

because it involves replacing have

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Reid Barton]

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]

Currently, obtain h, fails

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Patrick Massot]

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]

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

[Keeley Hoek]

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

[Keeley Hoek]

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