As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda's reflection mechanism provides a first-class proof search tactic for first-order Agda terms. Furthermore, the same mechanism may be used in tandem with Agda's instance arguments to implement type classes in the style of Haskell. As a result, writing proof automation tactics need not be different from writing any other program.
This repository contains the sources for the
Auto In Agda.
The paper sub-directory contains the literate Agda files that make up the paper.
The code sub-directory contains the Agda source code.
Some notes:
-
the code was written for use with Agda 2.4.2 and version 0.8.1 of the Agda standard library;
-
the code is released under an MIT license;
-
the paper is compiled using lhs2TeX;
-
compilation of the paper is facilitated using a rake build script (call
rake paper).