← All papers
Canonical for Automated Theorem Proving in Lean
cs.LO
Apr 8, 2025 · v1
TL;DR
Provides a Lean tactic invoking the Canonical solver to synthesize proof terms and programs for dependently-typed goals.
Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Problem
Type inhabitation in dependent type theory (finding a term of a given type) can be used for theorem proving and program synthesis, but existing solvers have limited support for higher-order and dependently-typed goals with structural recursion.
Approach
Canonical is a solver for type inhabitation in dependent type theory, exposed as a Lean tactic. It supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Terms are kept in beta-normal eta-long form, and a format with bindings, head, and spine enables efficient search.
Results
Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.