Скачать или смотреть Generalization of meta programs with dependent types in mtac2 with mtac2

https://icfp20.sigplan.org/details/ty...



Meta-languages are becoming an essential part of proof assistants, as they enable the proof developer to automate her proofs. Hence, an increasing number of provers are adopting different meta-languages. The Mtac and Mtac2 meta-languages code meta-programs within a monad in Coq to obtain typed meta-programs. That is, an Mtac2 meta-program with type M A will ensure that the value returned will indeed have type A.

However, the combination of monads and dependent types presents an interesting challenge: The convoy pattern—an extremely useful and often necessary tool for dependent programming in Coq—is not automatically supported. The convoy pattern is necessary when dependent pattern matching inspects values on which \emph{the types} of other values depend.

In this work we present a new meta-meta-program lift that provides a semi-automatic solution: given any meta-program or operator (like bind) and a list of dependencies (what lies behind the last arrow in the type of mfix above), it generates a new operator that can be used in a context where such dependencies are expected. It is important to mention that \textbf{we use Mtac as is as its own meta-language!}