rsuffices

Stream: general

[Yaël Dillies]

I feel like rsuffices is misnamed. It's not a recursive suffices. What would alternative names be, before #16159 lands and makes renaming painful?

[Jason KY.]

I like the name rsuffices since its intuitive if you know what the other r-version of tactics do

[Eric Wieser]

The game here is "obtain is to have as ____ is to suffices", right?

[Eric Wieser]

Which makes rsuffices look like a bad name because we're not using similar syntax to rcases

[Eric Rodriguez]

for the record, #15735 was quite a fan of the name. I originally named it as suffices'.

[Eric Rodriguez]

one thing to note about rsuffices and that may be worth fixing is that:

rsuffices (ha|hb) : p ∨ q,
{ { stuff_for_p },
  { stuff_for_q } },
{ rest }

is invalid syntax, and instead you have to skip the outer grouping bracket. I don't know how much of an issue this is.

[Yaël Dillies]

I actually expect that behavior. It's quite nice.

[Eric Wieser]

Maybe it's actually obtain that is badly named and it should be called rhave.

[Eric Rodriguez]

in some ways I feel like obtain should be called have

[Yaël Dillies]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/rsuffices.3F/near/281623150 :upside_down:

[Yaël Dillies]

I mean, yeah. In an ideal world we wouldn't have have/haveI/obtain (and no obtainI?!), cases/casesI/rcases, intro/intros/rintro/rintros/introsI, but just one of each family.

[Eric Rodriguez]

you forgot introsI L) I was going to add obtainI/rcasesI as it's useful for docs#eq_zero_or_ne_zero, but I agree it's a bit of a farce we need all this

[Eric Wieser]

The I versions are a necessary evil to avoid performance issues I believe

[Yaël Dillies]

That's still 2x blowup on the number of tactics :frown:

[Eric Rodriguez]

it'll be gone in lean4!

[Eric Wieser]

Although I guess they could just unfreeze the cache if trying to intro without unfreezing fails

[Kyle Miller]

They could use a flag, like !, for resetting the instance cache. (So have! or intros!)

[Eric Rodriguez]

there is some kind of precedent for this: i believe LTE uses a zero-width space for by exactI

[Eric Rodriguez]

yep: https://github.com/leanprover-community/lean-liquid/blob/master/src/hacks_and_tricks/by_exactI_hack.lean

[Kyle Miller]

Sometimes I've wondered what it would be like if we had a more systematic approach to flags, perhaps intros/I for the /I flag, rather than needing to come up with some symbol for each one. The thought experiment is "if the syntax were solved, would we use more flags?"

[Kyle Miller]

You'd write tactic/a/b/c to apply multiple flags. One precedent is MS-DOS switches, and another is an odd language called Rebol that has "refinements" for a similar purpose to give function variants.

[Eric Wieser]

intros x y z { unfreeze := tt } feels like our standard syntax for flags

[Eric Wieser]

Of course, that's longer than unfreezingI { intros x y z }

[Mario Carneiro]

You can almost always replace tacticI with resetI, tactic or tactic, resetI or unfreezingI { tactic } which is why I didn't make copies of all tactics to begin with, only the common ones