RFC: custom recursors

Proposal

In a language that compiles pattern matching down to recursor theroems, it seems natural to be able to define custom recursors and have pattern matching and induction work just as before. Here are some use-cases (and I invite interested parties to expand):

• Arrays as stacks.

  I switched some code that was maintaining a stack from using Lists to arrays for performance reasons, and going from pattern matching to if … then … else and isEmpty and pop and back made it more ugly. It would be great if I could somehow use patterns .empty and .snoc xs s (possibly with nicer syntax) in match statements.o

• Fin n.

  This is defined as a subtype of Nat, which is a nice definitions. But some programs and proofs would benefit from being able to pattern match on the Fin n directly.

  In fact, there are two possible recursions that might be useful useful here (going from 0 up, or going from the last one down, changing n along the way). It would be good to have both.

• Refactoring.

  The List.Forall₂ predicate is defined inductively. It could have been defined recursively over the input lists, which would provide us with some (presumably) nice defeqs. But such a change would affect a lot of code – unless one could prove the existing constructors and induction principle with the new definition and set it up so that by induction and match work as before.

TODO (help welcome): Propose concrete syntax/commands/semantics.

Community Feedback

• Desire for inductive Fin n
• Refactoring List.Forall₂

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 with the proposal and its linked community feedback on inductive Fin n and refactoring List.Forall₂. Define concrete syntax, commands, and semantics for custom recursors, with pattern matching and induction continuing to work as described; the issue does not name implementation files or tests.