style for proofs with `|`.

Stream: mathlib4

[Moritz Firsching]

I was wondering what the "correct" indentation should be for theorems that don't have a := but go directly to the cases using |. There are examples in the style guide, where there is no indentation, although not specifically, but only by accident in the section on "Calculation.

Searching in mathlib gives that there are at current master many more example with two spaces before the |:

When searching for ^(protected )?(def|lemma|theorem) (?!.*:=)(?<! where).*\n \|one finds 1216 results, and
^(protected )?(def|lemma|theorem) (?!.*:=)(?<! where).*\n\| yields only 13 results.

I don't care which convention should be used, but I think there would be benefits in making it consistent.

• If we decide to go with "two spaces before |, then

  • #7283 fixes the remaining 13 results
  • Perhaps we could fix this in the style guide? (Or is this a think that is done differently in mathlib from other parts of lean?)

• If we decide to go with "zero spaces before|, then

  • I will revert the 13 cases in #7382
  • I can prepare a pull request to change the 1216 results and adapt the proposed linter check in #7283

[Thomas Murrills]

My personal 2¢ is that non-indentation looks cleaner (the | itself serves as a distinguishing line-initial marker, you don’t also need indentation) and is consistent with match statements, which are doing the same thing. (I also feel this way about inductive.) I realize that this is against precedent, though. :)

[Kyle Miller]

My understanding of the mathlib style is that the body of a definition/theorem is indented by 2 spaces (that includes | cases) and if the type needs to continue on the next line it's indented by 4 spaces. The statistics you've collected appear to support that this is a common understanding.

I'm not surprised if the style guide accidentally makes a mistake here, since it's been adapted from the mathlib3 styleguide, and in mathlib3 we never indented the body of a definition/theorem.

[Kyle Miller]

I haven't really been clear on whether match statement alternatives should be indented or not, but not indenting seems to be the most common. One reason not to indent them is that you don't need to re-indent to go back and forth between having a match and not having a match. For example,

example (x : Nat) : Nat :=
  match x with
  | 0 => 0
  | n + 1 => n

vs

example : Nat -> Nat
  | 0 => 0
  | n + 1 => n

[Kyle Miller]

Similarly, switching between a match and a if let ... then doesn't require re-indenting the match bodies.

[Thomas Murrills]

Hmm, just to cast the alternative view in these terms, I’d consider a “body” to specifically be a term. | strikes me as postponing the body until after we destructure the arguments; I’d tentatively say a definition specified with | has multiple bodies (in this sense), one for each case.

I also think there’s value to having match cases and match-style definitions be consistently indented (relative to what they case on); they should be thought of the same way.

Also, not having the cases above be interchangeable has its benefits too! :) In particular, it tells you that you don’t have to read to the end of the line to see if := appears:

example : Expr × Nat → Expr := fun (x, n) => match x with
  | a => …
  | b => …

Ultimately these differences are rather small either way, of course…but how can we build a bikeshed without considering the psychological effects of what color we paint it? :P

[Kyle Miller]

I think discussing what color the bikeshed should be is a bit of a distraction since this bikeshed has been well and painted already. There's just some confusion about what color it is since there's a little variation. (That's not to say that there should never be discussion about it, but for sake of Moritz's effort to regularize things I think it'd be helpful focusing on the question of "what is the style" in this thread.)

[Ruben Van de Velde]

I imagine the current prevailing style is the one that mathport outputs :)

[Thomas Murrills]

Indeed, while the bias towards indentation is still present in std and core, it’s much less extreme—using the regexes above:

std:

• indented: 153 (31 files)
• non-indented: 16 (7 files)

core:

• indented: 817 (267 files)
• non-indented: 299 (156 files)

So, about 10-to-1 in std by command, but only 4 or 5 to 1 by file; under 3 to 1 in core by command, and less than 2 to 1 by file. (Files might better reflect preferences by author.)

I think “well and painted” really only applies when a deliberate choice has been made somewhere—which it might have been! But it’s not clear where yet (at least to me).

Currently it looks like an overall preference for one over the other, but with enough variation to suggest that no collectively-adopted choice has really been made, and that everyone is just painting their part of the shed the color that they’re familiar with. But maybe there has been a choice made somewhere, and most people just don’t know about it (even if adopting that choice’s conventions).

[Eric Wieser]

Isn't the mathport indentation based on what the core pretty printer says?

[Thomas Murrills]

That makes sense—I just checked, and if you pretty-print the syntax of one of these defs, it does come out indented. So if we are simply discussing what the standard is, that might be as good a standard as any…!

[Jireh Loreaux]

As for the style guide: I updated this from Lean 3 to Lean 4 and did not consider this issue at all. So whatever appears in the style guide currently is happenstance and should not be considered wisdom one way or the other.

[Mario Carneiro]

Thomas Murrills said:

Indeed, while the bias towards indentation is still present in std and core, it’s much less extreme—using the regexes above:

std:

• indented: 153 (31 files)
• non-indented: 16 (7 files)

Thanks for pointing out the exceptions. They have been fixed.

[Moritz Firsching]

Ok, thanks for the input everyone, sounds like "two spaces before |" is in fact the standard right now, I'll make a pr for the style guide correcting the example.

[Moritz Firsching]

Thomas Murrills said:

core:

• indented: 817 (267 files)
• non-indented: 299 (156 files)

I opened an issue asking if we want to change it there as well: lean4#2480

[Eric Wieser]

(lean4#2580, your link and its text was garbage I'm afraid)

[Mac Malone]

My 2 cents: In general, I consistently use the no-indent style and largely precisely for the reasons @Thomas Murrills mentioned. The only cases where places where this is not the case are due to external PRs. The pretty-printer indents because its formatting was done by Gabriel, who uses this style (and is responsible for one of the exceptions in Lake).