liufengyun
commented
4 years ago Multiple binders are indeed annoying, I don't know any good reference about this.
Instead, I think the mechanization can try to simplify the pattern language so that it only has single binder and try to keep the same expressiveness. This is one area, where pen & paper systems look better esthetically.
The annoying case is application. If we assume the pattern for application is always App[T] f x, where f and x are bound variables, will simplify the problem? By doing so, patterns are no longer composable, but they can nest patmat to have the same expressiveness.
radeusgd
Patterns may contain multiple binders, for example we may have a pattern (x1 x2) (matching an application and extracting each term into x1 and x2 respectively).
The number of binders can be arbitrary in a pattern (from 0 to any positive integer).
When using DeBruijn indices for encoding binders, we need to know how many binders are added in the inner term so that when we refer to outer variables we know which index to use.
Another thing is order of the binders - we need to have some notion of order to be able to address binders in the pattern by an index (but this is not a big issue as probably something like index of inorder traversal of the pattern tree could be used).
The issue is however, that autosubst seems to only handle single-level binders, like in a lambda - we can bind one argument. I'm not sure if we can directly achieve multi-level binders for a fixed level, like a lambda taking 2 arguments at once. Binders parametrized by an arbitrary natural number (which seems required for handling patterns) seem completely out of question.
This is however based on my current view of autosubst and I may be wrong about it. I couldn't find any information in the manual or examples hinting that this was possible.