Indentation in structured proofs

Stream: mathlib4

[Bhavik Mehta]

Do we have a convention for how indentation should look for structured proofs? Specifically, in examples like the below, do we prefer the first or the second?

import Mathlib.Data.Nat.Factorial.Basic

theorem test (n : ℕ) : 0 < Nat.factorial n := by
  induction n with
  | zero =>
    simp
  | succ n _ =>
    rw [Nat.factorial_succ]
    simpa

theorem test2 (n : ℕ) : 0 < Nat.factorial n := by
  induction n with
  | zero =>
      simp
  | succ n _ =>
      rw [Nat.factorial_succ]
      simpa

My preference is for the second option, since it makes the structure of the structured proof visually cleaner, but my stronger preference is for a consistent approach.

[Eric Wieser]

I think the pretty-printer encodes the rule here:

run_cmd do
  -- deliberately mixed style
  let stx ← `(command|
  theorem test (n : ℕ) : 0 < Nat.factorial n := by
    induction n with
    | zero =>
      simp
    | succ n _ =>
        rw [Nat.factorial_succ]
        simpa)
  -- prints the first option
  Lean.logInfo stx

[Eric Wieser]

If you want the second option, I think probably it would have to come with a change to the pretty-printer for induction in core

[Bhavik Mehta]

Hmm, although the pretty printer doesn't encode our rule for := by being together:

run_cmd do
  let stx ← `(command|
  theorem test (nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn : ℕ) :
      0 < Nat.factorial nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn := by
    induction n
    · simp
    · simpa [Nat.factorial_succ])
  Lean.logInfo stx

[Eric Wieser]

I think fixing that is on the path to having an autoformatter :)

[Bhavik Mehta]

Sure, but it makes me doubt whether "the pretty-printer says so" is the correct guideline to use!

[Eric Wieser]

I suspect by falls in the category of "it was hard to train the pretty-printer to do the right thing", whereas I would expect induction to explicitly indicate the number of indentation levels, making it a conscious choice

[Bhavik Mehta]

Note also that https://leanprover-community.github.io/contribute/style.html#calculations gives an example of using the second option with the equation compiler (and I can't find any other examples of either style in the written guidelines)

[Markus Himmel]

Not that it matters for mathlib, but the standard library style guide asks for the first option.