Equations: A Dependent Pattern-Matching Compiler

Abstract. We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functions as a set of equations, automatically find their realization in the core type theory and generate proofs to ease reasoning on them. It provides a complete package to define and reason on functions in the proof assistant, substantially reducing the boilerplate code and proofs one usually has to write, also hiding the intricacies related to the use of dependent types and complex recursion schemes.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Matthieu Sozeau
• Keywords: Coq System, Core Type Theory, ITP 2010, Mathematics, Recursive Dependently-typed Functions