Abstract
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. As a result, writing proof automation tactics need not be different from writing any other program.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Note that Agda’s reflection mechanism should not be confused with ‘proof by reflection’ – the technique of writing a verified decisionprocedure for some class of problems.
- 3.
Syntax for Agda tactics was added in Agda 2.4.2.
References
Agda development team. Agda release notes documenting the reflection mechanism. The Agda Wiki (2013). http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-8 and http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-3-0. Accessed 9 Feb 2013
Allais, G.: Proof automatization using reflection (implementations in Agda). MSc Intern report, University of Nottingham (2010)
Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 9, 23:552–593 (2013). doi:10.1017/S095679681300018X
Braibant, T.: Emancipate yourself from LTac (2012). http://gallium.inria.fr/blog/your-first-coq-plugin/
Chapman, J.: Type checking and normalisation. Ph.D. thesis, University of Nottingham (2009)
Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2013)
Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93–109. Springer, Heidelberg (2007). doi:10.1145/2500365.2500575
Coq development team. The Coq proof assistant reference manual. Logical Project (2004)
Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). ACM, September 2013. doi:10.1145/2500365.2500575
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)
Lindblad, F., Benke, M.: A tool for automated theorem proving in Agda. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 154–169. Springer, Heidelberg (2006)
Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 374–389. Springer, Heidelberg (2014)
Martin-Löf, P.: Constructive mathematics and computer programming. In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp. 167–184. Prentice-Hall Inc. (1985)
McBride, C.: First-order unification by structural recursion. J. Funct. Program. 11, 13:1061–1075 (2003). doi:10.1017/S0956796803004957
McBride, C.: Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In: Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming, WGP 2010, pp. 1–12. ACM, New York (2010). doi:10.1145/1863495.1863497
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2007)
Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009a)
Norell, U.: Playing with Agda. Invited talk at TPHOLS (2009b)
Oury, N., Swierstra, W.: The power of Pi. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pp. 39–50 (2008). doi:10.1145/1411204.1411213
Jones, S.P. (ed.): Haskell 98 Language and Libraries: the Revised report. Cambridge University Press, Cambridge (2003)
Pitman, K.M.: Special forms in LISP. In: Proceedings of the 1980 ACM Conference on LISP and Functional Programming, pp. 179–187. ACM (1980)
Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pp 1–16 (2002). doi:10.1145/581690.581691
Stutterheim, J., Swierstra, W., Swierstra, D.: Forty hours of declarative programming: teaching prolog at the junior college Utrecht. In: Proceedings First International Workshop on Trends in Functional Programming in Education, Electronic Proceedings in Theoretical Computer Science, University of St. Andrews, Scotland, UK, 11 June 2012, vol. 106, pp 50–62 (2013)
Swierstra, W.: More dependent types for distributed arrays. High.-Ord. Symbol. Comput. 23(4), 489–506 (2010)
Swierstra, W., van Noort, T.: A library for polymorphic dynamic typing. J. Funct. Program. 23, 229–248 (2013). doi:10.1017/S0956796813000063
Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 1997 (1997). doi:10.1145/258993.259019
van der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013)
van der Walt, P.: Reflection in Agda. Master’s thesis, Department of Computer Science, Utrecht University, Utrecht, The Netherlands (2012). http://igitur-archive.library.uu.nl/student-theses/2012-1030-200720/UUindex.html
Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp 87–100 (2013). doi:10.1145/2500365.2500579
Acknowledgements
We would like to thank the Software Technology Reading Club at the Universiteit Utrecht, and all our anonymous reviewers for their helpful feedback – we hope we have done their feedback justice.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Kokke, W., Swierstra, W. (2015). Auto in Agda. In: Hinze, R., Voigtländer, J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science(), vol 9129. Springer, Cham. https://doi.org/10.1007/978-3-319-19797-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-19797-5_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19796-8
Online ISBN: 978-3-319-19797-5
eBook Packages: Computer ScienceComputer Science (R0)