Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux
cs.LO
May 16, 2015 · v2
TL;DR
Describes the elaboration algorithm implemented in the Lean theorem prover for dependent type theory.
Abstract
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is left implicit in a quasi-formal expression and resolving ambiguities. We call the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean's elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and we describe the central design goals that guide our implementation.
Problem
Interactive theorem provers need convenient and efficient means of writing expressions, definitions, and proofs. Passing from quasi-formal, partially-specified expressions to completely precise formal ones (elaboration) requires inferring implicit information and resolving ambiguities, which is challenging in dependent type theory.
Approach
The authors describe an elaboration algorithm for dependent type theory implemented in the Lean theorem prover. The elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, and the use of tactics. The algorithm handles the interaction between these features in a unified framework.
Results
The elaboration algorithm is implemented in the Lean theorem prover, supporting the full range of features needed for practical use: higher-order unification, type class inference, ad hoc overloading, coercion insertion, and tactic integration.
