indentation

Stream: mathlib4

[Kevin Buzzard]

@[elab_as_elim]
theorem trans_induction_on {P : ∀ {a b : α}, TransGen r a b → Prop} {a b : α} (h : TransGen r a b)
    (base : ∀ {a b} (h : r a b), P (single h))
    (ih : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) :
    P h := by
  induction h
  case single a h => exact base h
  case tail b c hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)

Have I understood the conventions yet? 4 spaces for the continuation of the statement of the theorem, colon at the end, still 4 spaces for the type, two spaces for the proof, don't need any more indentation even though there are two goals after induction.

[Mario Carneiro]

only thing I would mention is that it is preferable to use

  induction h with
  | single a h => exact base h
  | tail b c hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)

instead of induction; case when it's just listing all the cases

[Kevin Buzzard]

I blame the guy who wrote the porting program for that one.

[Mario Carneiro]

ooh, that would be pretty fancy if we could try to apply that transformation. It's possible to do the syntactic transformation, but we basically have no idea whether the tactic will work

[Mario Carneiro]

the more common pattern in mathlib uses induction h with _ _ _ a b _ c and this kind of thing is pretty hopeless to transform into a well structured induction without type info

[Mario Carneiro]

I'm hoping that we will eventually get auto-applicable linters that will just recommend to replace working induction' proofs with correctly structured induction proofs