Style: induction proofs

Stream: mathlib4

[Rudy Peterson]

Hello,

Is the preferred style for induction proofs of the form:

induction _  with
| c1 => ...
| c2 => ...
...

as opposed to

induction _
case c1 => ...
case c2 => ...
...

Is one style also preferred for case analysis with cases?

Is there documentation on Lean community for this? My apologies for missing anything.

Thank you!

[Kim Morrison]

I don't think anyone specifies a style. My experience is that you will see the former more in mathematics, and the later more in programming, but it's far from uniform.

[Ruben Van de Velde]

I, doing only mathematics, would specify the format because it makes the structure more obvious

[Kim Morrison]

I think it would be reasonable (I'd be in favour) to require the first form in Mathlib. (There's only 50-ish of the second form to clean up.)

[Yaël Dillies]

Could we please stop codifying everything? The suggestion here would amount to extra review burden for very little gain. There are better things to think about!

[Michael Rothgang]

Consistent style/not having to think about certain aspects also has benefits. If it's just a one-time PR of 50 lines, that seems fine with me --- this is my personal opinion.

[Yaël Dillies]

(eg I can already hear the follow-up discussion "Since we don't allow induction c; case c1=> ...; case c2 => ..., should we forbid induction c; case c2=> ...; all_goals ...?")

[Pim Otte]

Imho, the long term strategy here is to only codify things that are either checked by a linter, or important. The burden on contributors to fix linted issues is minor, and then reviewers don't have to manually think about these and can instead focus on the more architecturally impactful aspects.

[Kim Morrison]

Yes, I really really don't like things like this being raised in review. Complete waste of time there. But it's a different matter when we're talking about linters or code formatters.

[Rudy Peterson]

Ah sorry, I didn't mean to suggest one way or the other, I was requested to change the style in my PR and I wanted to make sure :sweat_smile:

[Wrenna Robson]

Kim Morrison said:

Yes, I really really don't like things like this being raised in review. Complete waste of time there. But it's a different matter when we're talking about linters or code formatters.

Yeah I would agree with this - think it is very reasonable to lint stuff (which can then often be easily fixed) but it wastes time in manual review.