RFC: `termination_by structurally x`
nomeata opened this issue · 2 comments
Proposal
Right now if the user writes a recursive function without annotation, Lean tries
- structural recursion on each argument
- well-founded recursion with GuessLex
If the user wants to be explicit about structural recursion, they can use termination_by x. But they have no way of indicating that they want to use structural recursion on a specific argument.
Right now the above search procedure is not slow, to the need isn’t high, but once we have structural recursion on mutually recursive functions, the first step might consider many combinations, and it would be good if the user can just declare their intent.
Furthermore, if the user can be specific, they get a less noisy error message when the derecursifying fails.
Initial proposal for the syntax is
termination_by structurally x -- if x is bound before the colon
termination_by structurally x => x -- if x is bound after the colon
in analogy to the existing termination_by. This way, no new “definition trailing keyword” is introduced.
It can also be extended to more variants in the future, such as termination_by tail-recursion (which isn’t really “termination”, sigh.)
Once we have this, then termination_by? should not force well-founded recursion and should, if lean detects structural recursion, suggest the corresponding termination_by structurally … annotation.
Community Feedback
(none yet)
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.
I am happy to hear alternative syntax ideas; the termination_by structurally x suggested above is somewhat clunky.
I think it should be styled closer to options in tactic syntax, e.g. termination_by (method := structural). This also gives a bit more freedom to tweak the syntax without clashing with either the expr or ident parser.