RFC: Splitters as theorems, not definitions

TL;DR: Create match splitters as theorems if possible, to reduce compilation cost and module interface size.

Status Quo

Right now, when using split, or well-founded recursion, or functional induction, we generate a “splitter” for each match. This is similar to the match, but the alternatives have additional “none of the above” assumptions. Because users might want to use split in code, not just theorems, these declarations are definitions eliminating into Sort u.

In the majority of cases, I claim without having investigated, they are only used in proofs.

Proposal

The .splitter should eliminiate into Prop and become a theorem. The more general construction is still available as .psplitter (p as in polymorphic, cf. PSum, PUnit). Tactics like split look at the goal to determine which one they need.

Benefits

The benefits should be

• less time spent compiling declarations that we never run
• fewer linker symbols
• smaller exported module files (because we don’t need to expose the body of theorems)
• can use a non-private name for the .splitter realizable constant, because Lean allows name clashes of theorems with the same type (like equational theorems.)

While we are at it

While doing that refactoring, we should recognize when no splitters are needed at all (when the matcher has no overlap) and not even generate a definition for that. This needs some changes to the split tactic.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by tracing how match splitters are generated and how the split tactic selects them, including uses from well-founded recursion and functional induction. Investigate the .splitter and .psplitter distinction and cases where no splitter is needed. Done means proof-only splitters become theorems, polymorphic cases remain available, and unnecessary splitters are not generated.