Style: stream-of-conciousness obtain

Stream: mathlib4

[Michael Rothgang]

As a follow-up in spirit in #10640: there still are a few uses of "stream of conciousness" obtain. Considering that similar syntax for have/suffices/replace was removed, shall we do the same with obtain?

[Michael Rothgang]

How would one find all such places? Go to definition on such an obtain points to Std.Tactic.RCases. Editing the meta code is above my current lean level.

[Michael Rothgang]

(I fixed ~50 such uses locally; I can imagine around 100 uses all of mathlib, eventually. Basic grepping has 250-300 hits, but most of them are fine, just across multiple lines.)

[Emilie (Shad Amethyst)]

Michael Rothgang said:

How would one find all such places? Go to definition on such an obtain points to Std.Tactic.RCases. Editing the meta code is above my current lean level.

Clever grep searches? :)
I get 299 results, although it contains some false positives: https://gist.github.com/adri326/fed4ee870da7efe3a9df6e3a9db851d4

[Emilie (Shad Amethyst)]

I used rg --pre just-the-code --pcre2 '^\s*(obtain)(?:(?!:=|by|from).)*$' -A 3 (where just-the-code is a little tool I wrote yesterday evening, that strips out comments and strings)

[Michael Stoll]

What is wrong with

have h : <statement>
· <proof>

?

[Emilie (Shad Amethyst)]

I think it's just a style decision: we already have have h : <statement> := by <proof>, which has a few more capabilities (the by can be dropped, which then usually hints that the proof can be further optimized), so there's no need to have multiple ways of writing the same thing

[Michael Stoll]

Is this (i.e., the style decision) documented somewhere?

[Emilie (Shad Amethyst)]

It does not look to be mentionned in the style guidelines yet, though it will be enforced through #10534 by forbidding the import of the corresponding tactic file

[Michael Stoll]

Hm, sufffices : <statement> by <proof> or ... from <term> (as is used in #10640) gives me an error.

[Michael Rothgang]

Emilie (Shad Amethyst) said:

I used rg --pre just-the-code --pcre2 '^\s*(obtain)(?:(?!:=|by|from).)*$' -A 3 (where just-the-code is a little tool I wrote yesterday evening, that strips out comments and strings)

My incantation was rg "obtain ⟨" | rg -v ":=", yielding 272 hits (on top of my fixes). rg is ripgrep, a Rust clone of grep. This count doesn't capture multi-line obtain's ending in :=.

Anyway: I was rather looking for an equivalent of "remove Mathlib.Tactic.Have", that would catch all occurrences :-)

[Emilie (Shad Amethyst)]

We should have a linter for that, really, since we can't disable the obtains tactic from std4

[Michael Rothgang]

In any case: I pushed what I have to branch#MR-obtain. I won't have time this week to pursue that further. Feel free to adopt if you like. (Perhaps after getting sufficient maintainer buy-in.)

[Michael Stoll]

Michael Stoll said:

Hm, sufffices : <statement> by <proof> or ... from <term> (as is used in #10640) gives me an error.

Turns out that suffices <name> : <statement> from/by ... is OK. Why does the syntax not work without providing a name?

[Ruben Van de Velde]

Michael Stoll said:

Michael Stoll said:

Hm, sufffices : <statement> by <proof> or ... from <term> (as is used in #10640) gives me an error.

Turns out that suffices <name> : <statement> from/by ... is OK. Why does the syntax not work without providing a name?

It works if you drop the : entirely

[Ruben Van de Velde]

As to why - accident of parsing

[Michael Stoll]

The error message could be more helpful...

[Ruben Van de Velde]

Yeah, accidents of parsing don't tend to get great error messages :)

[Michael Stoll]

But I have to admit that the docstring of suffices gives this information. (It just didn't occur to me to look at it.)

[Eric Wieser]

There's no need to try to match this with regexes, we can make the syntax itself throw a warning

[Emilie (Shad Amethyst)]

But I like my regexes :(

[Emilie (Shad Amethyst)]

They make for nice custom, local linters if you run them on your git diff

[Michael Rothgang]

I just filed #11045 with what I have (plus a few more fixes).
I have a list of 90 remaining hits to be investigated. @Emilie (Shad Amethyst) If you like, I can share.

[Michael Rothgang]

I wrote a syntax linter against this in #13220 - the remaining syntax replacements (about 30) are in #13219. The description for #13220 also contains my best effort at summarising why this removal is discussed.

[Michael Rothgang]

In the same vein: I realised mathlib has about 40 uses of stream-of-conciousness rsuffices (which is a wrapper around obtain). Are these undesirable also? If so, I could use help removing them.
I've also made the linter flag them, so looking at the warnings in #13220 will tell you where to go.

[Ruben Van de Velde]

I think the rsuffices syntax only works that way

[Michael Rothgang]

Ah, so linting it makes no sense... I see, I'll take it out again.

[Yury G. Kudryashov]

It makes sense if you fix rsuffices syntax.

[Michael Rothgang]

Sure: I'll put this on my eternal list - but let's rather land an obtain linter first.