Zulip Chat Archive

Stream: general

Topic: rsuffices


Yaël Dillies (Aug 19 2022 at 19:59):

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. (Aug 19 2022 at 20:02):

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

Eric Wieser (Aug 19 2022 at 22:14):

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

Eric Wieser (Aug 19 2022 at 22:19):

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

Eric Rodriguez (Aug 19 2022 at 22:20):

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

Eric Rodriguez (Aug 19 2022 at 22:22):

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 (Aug 19 2022 at 22:22):

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

Eric Wieser (Aug 19 2022 at 22:23):

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

Eric Rodriguez (Aug 19 2022 at 22:24):

in some ways I feel like obtain should be called have

Yaël Dillies (Aug 19 2022 at 22:24):

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

Yaël Dillies (Aug 19 2022 at 22:25):

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 (Aug 19 2022 at 22:26):

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 (Aug 19 2022 at 22:27):

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

Yaël Dillies (Aug 19 2022 at 22:27):

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

Eric Rodriguez (Aug 19 2022 at 22:28):

it'll be gone in lean4!

Eric Wieser (Aug 19 2022 at 22:28):

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

Kyle Miller (Aug 19 2022 at 22:36):

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

Eric Rodriguez (Aug 19 2022 at 22:37):

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

Eric Rodriguez (Aug 19 2022 at 22:38):

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

Kyle Miller (Aug 19 2022 at 22:39):

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 (Aug 19 2022 at 22:39):

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 (Aug 20 2022 at 06:45):

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

Eric Wieser (Aug 20 2022 at 06:46):

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

Mario Carneiro (Aug 20 2022 at 07:23):

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


Last updated: Dec 20 2023 at 11:08 UTC