induction in mathlib4

Stream: mathlib4

[Patrick Massot]

Do we have a policy about using new style induction in mathlib4? I just wrote https://github.com/leanprover-community/mathlib4/commit/609f55046d748c758ddbac56f2a376947ff78e37 on my not yet ready but merged anyway PR. Should we spend time on such edits?

[Eric Wieser]

I think it probably falls under the general policy I've assumed which is "don't cleanup proofs unless they're already non-trivially broken"

[Eric Wieser]

I certainly think we want to use new-style induction as much as possible, but I don't think the port is the necessarily the time to make the switch

[Patrick Massot]

Eric Wieser said:

I certainly think we want to use new-style induction as much as possible, but I don't think the port is the necessarily the time to make the switch

I don't understand that bit. Switching doesn't make anything more difficult downstream, right? I would understand that we don't enforce switching during the port.

[Eric Wieser]

Switching makes porting PRs have bigger diffs, which makes them harder to review. It also makes it hard to forward-port changes, since the diff won't match up as well.

[Ruben Van de Velde]

I think forward ports might be the strongest argument at this point, yeah

[Patrick Massot]

I think this yet another argument in favor of avoiding anything that creates a forward-port obligation.

[Eric Wieser]

I think "keep porting PRs easy to review" is a good reason too

[Eric Wieser]

The shorter porting PRs are (compared to the mathport output) the quicker the review and the sooner we finish mathlib4

[Mario Carneiro]

Also keep in mind that, like the function arrow switch, upgrading induction proofs to the new style is something that can be done fully automatically post-port, so doing it early is likely a waste of effort

[Mario Carneiro]

(Tools for making large-scale syntactic transformations to lean code will come eventually, but they are not a high priority right now and it will be easier to think about this stuff after the port)

[Patrick Massot]

Why isn't it done by mathport if it can be made fully automatically? This is a honest naive question, I'm not complaining about anything.

[Mario Carneiro]

It can only be done knowing the elaborated context

[Mario Carneiro]

which means it can be done by e.g. a linter but not by mathport which sees syntax only

[Mario Carneiro]

basically it relies on the human input to fix all the red squiggles before it can be applied

[Patrick Massot]

Ok, makes sense. Then I'll definitely refrain from doing this in future porting PRs.

[Patrick Massot]

Speaking of priorities, it would be nice to prioritize restoring the structure skeleton code action and get a induction code action, because writing the layout of those new style induction proofs by hand is really tedious and feels like we are working for the computer instead of having the computer work for us.