×

Automatically proving equivalence by type-safe reflection. (English) Zbl 1367.68257

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 40-55 (2017).
Summary: One difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories, from the fact that the propositional equality enables us to prove as equal terms that are not judgementally equal, which means that the typechecker can’t always obtain equalities by reduction. As far as possible, we would like to solve such proof obligations automatically. In this paper, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. We show how defining reflected terms indexed by the original Idris expression allows us to construct and manipulate proofs. We build a hierarchy of tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs.
For the entire collection see [Zbl 1364.68010].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Agda; Coq; Irdis; Idris; Mtac
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004) · Zbl 1069.68095
[2] Brady, E.: Constructing correct circuits: verification of functional aspects of hardware specifications with dependent types. In: Trends in Functional Programming (TFP 2007) (2007)
[3] Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23, 552–593 (2013) · Zbl 1295.68059
[4] Carette, J., O’Connor, R.: Theory presentation combinators. In: Jeuring, J., Campbell, J.A., Carette, J., Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 202–215. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31374-5_14 · Zbl 1360.68802
[5] Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013) · Zbl 1288.68001
[6] Crégut, P.: Une procédure de décision reflexive pour un fragment de l’arithmétique de Presburger. In: Journées Francophones des Langages Applicatifs (2004)
[7] Delahaye, D.: A proof dedicated meta-language. Electr. Notes Theor. Comput. Sci. 70(2), 96–109 (2002) · Zbl 1270.68262
[8] Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: when achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 274–290. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-45221-5_20 · Zbl 1406.68105
[9] Delahaye, D., Mayero, M.: Field, une procédure de décision pour les nombres réels en Coq. In: Castéran, P. (ed.) Journées francophones des langages applicatifs (JFLA’01), pp. 33–48. Collection Didactique, INRIA (2001)
[10] Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning 31(1), 33–72 (2003). http://dx.doi.org/10.1023/A:1027357912519 · Zbl 1049.03011
[11] Farmer, W.M.: The formalization of syntax-based mathematical algorithms using quotation and evaluation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 35–50. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39320-4_3 · Zbl 1390.68778
[12] Gregoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Theorem Proving in Higher Order Logics (TPHOLS 2005), pp. 98–113 (2005) · Zbl 1152.68702
[13] Howard, W.: The formulae-as-types notion of construction. In: Seldin, J., Hindley, J. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, London (1980)
[14] Kokke, P., Swierstra, W.: Auto in Agda – programming proof search using reflection. In: 12th International Conference on Mathematics of Program Construction, MPC 2015, pp. 276–301 (2015) · Zbl 1432.68063
[15] 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). doi: 10.1007/11617990_10 · Zbl 1172.68615
[16] Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: 5th International Conference on Interactive Theorem Proving, ITP 2014, pp. 374–389 (2014) · Zbl 1416.68171
[17] Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)
[18] Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp. 87–100 (2013) · Zbl 1323.68236
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.