×

Hammer for Coq: automation for dependent type theory. (English) Zbl 1448.68458

Summary: Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundations has been hindered so far by the lack of translation and reconstruction components. In this paper, we present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is “sufficiently” sound and complete to be of practical use for automated theorem provers. We also introduce a proof reconstruction mechanism based on an eauto-type algorithm combined with limited rewriting, congruence closure and some forward reasoning. The algorithm is able to re-prove in the Coq logic most of the theorems established by the ATPs. Together with machine-learning based selection of relevant premises this constitutes a full hammer system. The performance of the whole procedure is evaluated in a bootstrapping scenario emulating the development of the Coq standard library. For each theorem in the library only the previous theorems and proofs can be used. We show that 40.8% of the theorems can be proved in a push-button mode in about 40s of real time on a 8-CPU system.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Alemi, A.A., Chollet, F., Irving, G., Szegedy, C., Urban, J.: DeepMath—Deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., Luxburg, U.V., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems (NIPS 2016), pp. 2235-2243 (2016)
[2] Abel, A; Coquand, T; Norell, U; Gramlich, B (ed.), Connecting a logical framework to a first-order logic prover, 285-301, (2005), New York · Zbl 1171.68712
[3] Armand, M; Faure, G; Grégoire, B; Keller, C; Théry, L; Werner, B; Jouannaud, J (ed.); Shao, Z (ed.), A modular integration of SAT/SMT solvers to coq through proof witnesses, 135-150, (2011), New York · Zbl 1350.68223
[4] Alama, J; Heskes, T; Kühlwein, D; Tsivtsivadze, E; Urban, J, Premise selection for mathematics by corpus analysis and kernel methods, J. Autom. Reason., 52, 191-213, (2014) · Zbl 1315.68217
[5] Asperti, A; Ricciotti, W; Coen, CSacerdoti, Matita tutorial, J. Formaliz. Reason., 7, 91-199, (2014)
[6] Aspinall, D.: Proof general: a generic tool for proof development. In: Graf, S., Schwartzbach, M.I. (eds.) Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, volume 1785 of LNCS, pp. 38-42. Springer, New York (2000) · Zbl 0971.68627
[7] Asperti, A; Tassi, E; Kauers, M (ed.); Kerber, M (ed.); Miner, R (ed.); Windsteiger, W (ed.), Higher order proof reconstruction from paramodulation-based refutations: the unit equality case, 146-160, (2007), New York · Zbl 1202.68370
[8] Asperti, A., Tassi, E.: Smart matching. In: Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings, pp. 263-277 (2010) · Zbl 1286.68389
[9] Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. (2015) · Zbl 1356.68178
[10] Bancerek, G., Byliński, C., Grabowski, A. Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., Urban, J.: Mizar: State-of-the-art and beyond. In: Intelligent Computer Mathematics—International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, pp. 261-279 (2015) · Zbl 1417.68201
[11] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, New York (2004) · Zbl 1069.68095
[12] Broda, S; Damas, L, On long normal inhabitants of a type, J. Log. Comput., 15, 353-390, (2005) · Zbl 1086.03011
[13] Bove, A; Dybjer, P; Norell, U; Berghofer, S (ed.); Nipkow, T (ed.); Urban, C (ed.); Wenzel, M (ed.), A brief overview of agda—A functional language with dependent types, 73-78, (2009), New York · Zbl 1252.68062
[14] Bertot, Y; Mohamed, OA (ed.); Muñoz, CA (ed.); Tahar, S (ed.), A short presentation of coq, 12-16, (2008), New York
[15] Blanchette, JC; Greenaway, D; Kaliszyk, C; Kühlwein, D; Urban, J, A learning-based fact selector for isabelle/HOL, J. Autom. Reason., 57, 219-244, (2016) · Zbl 1386.68149
[16] Bezem, M; Hendriks, D; Nivelle, H, Automated proof construction in type theory using resolution, J. Autom. Reason., 29, 253-275, (2002) · Zbl 1015.03018
[17] Blanchette, JC; Kaliszyk, C; Paulson, LC; Urban, J, Hammering towards QED, J. Formaliz. Reason., 9, 101-148, (2016)
[18] Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. PhD thesis, Technische Universität München (2012). http://www21.in.tum.de/ blanchet/phdthesis.pdf · Zbl 1183.68560
[19] Brady, E, Idris, a general-purpose dependently typed programming language: design and implementation, J. Funct. Program., 23, 552-593, (2013) · Zbl 1295.68059
[20] Böhme, S; Weber, T; Kaufmann, M (ed.); Paulson, L (ed.), Fast LCF-style proof reconstruction for Z3, 179-194, (2010), New York · Zbl 1291.68328
[21] Ben-Yelles, C.: Type-assignment in the lambda-calculus: syntax and semantics. Ph.D. thesis, Mathematics Department, University of Wales, Swansea, UK (1979)
[22] Coquand, T; Huet, GP, The calculus of constructions, Inf. Comput., 76, 95-120, (1988) · Zbl 0654.03045
[23] Chlipala, A.: Certified Programming with Dependent Types—A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013) · Zbl 1288.68001
[24] Czajka, Ł., Kaliszyk, C.: Goal translation for a hammer for Coq (extended abstract). In: Blanchette, J.C., Kaliszyk, C. (eds.) First International Workshop on Hammers for Type Theories (HaTT 2016), Volume 210 of EPTCS, pp. 13-20 (2016)
[25] Coq Development Team: The Coq proof assistant reference manual (2016). Version 8.6 · Zbl 1356.68191
[26] Corbineau, P; Berardi, S (ed.); Coppo, M (ed.); Damiani, F (ed.), First-order reasoning in the calculus of inductive constructions, 162-177, (2003), New York
[27] Czajka, Ł.: A shallow embedding of pure type systems into first-order logic. Submitted. (2016). http://www.mimuw.edu.pl/ lukaszcz/emb.pdf · Zbl 1322.68177
[28] Moura, LM; Bjørner, N; Ramakrishnan, CR (ed.); Rehof, J (ed.), Z3: an efficient SMT solver, 337-340, (2008), New York
[29] de Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover. In: Felty, A.P., Middeldorp, A. (eds.) International Conference on Automated Deduction (CADE 2015), Volume 9195 of LNCS, pp. 378-388. Springer, New York (2015) · Zbl 1465.68279
[30] de Moura, L., Selsam, D.: Congruence closure in intensional type theory. In: Olivetti, N., Tiwari, A. (eds.) International Joint Conference on Automated Reasoning, IJCAR 2016, Volume 9706 of LNCS. Springer, New York (2016) · Zbl 1475.68452
[31] Dowek, G, A complete proof synthesis method for the cube of type systems, J. Log. Comput., 3, 287-315, (1993) · Zbl 0789.68123
[32] Dyckhoff, R, Contraction-free sequent calculi for intuitionistic logic, J. Symb. Log., 57, 795-807, (1992) · Zbl 0761.03004
[33] Filliâtre, J.-C.: One logic to use them all. In: Bonacina, M.P. (ed.) International Conference on Automated Deduction (CADE 2013), Volume 7898 of LNCS, pp. 1-20. Springer, New York (2013)
[34] Färber, M., Kaliszyk, C.: Random forests for premise selection. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems (FroCoS 2015), Volume 9322 of LNCS, pp. 325-340 (2015) · Zbl 1471.68307
[35] Filliâtre, J.-C., Paskevich, A.: Why3—Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) European Symposium on Programming (ESOP 2013), Volume 7792 of LNCS, pp. 125-128. Springer, New York (2013)
[36] Gonthier, G; Asperti, A; Avigad, J; Bertot, Y; Cohen, C; Garillot, F; Roux, SL; Mahboubi, A; O’Connor, R; Biha, SO; Pasca, I; Rideau, L; Solovyev, A; Tassi, E; Théry, L; Blazy, S (ed.); Paulin-Mohring, C (ed.); Pichardie, D (ed.), A machine-checked proof of the odd order theorem, 163-179, (2013), New York · Zbl 1317.68211
[37] Gonthier, G; Mahboubi, A, An introduction to small scale reflection in coq, J. Formaliz. Reason., 3, 95-152, (2010) · Zbl 1211.68368
[38] Gonthier, G.: The four colour theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM, Volume 5081 of LNCS, pp. 333. Springer, New York (2007) · Zbl 1166.68346
[39] Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) International Conference on Automated Deduction (CADE 2015), Volume 9195 of LNCS, pp. 246-255. Springer, New York (2015) · Zbl 1465.68284
[40] Harrison, J; Berghofer, S (ed.); Nipkow, T (ed.); Urban, C (ed.); Wenzel, M (ed.), HOL light: an overview, 60-66, (2009), New York · Zbl 1252.68255
[41] Hall, M; Frank, E; Holmes, G; Pfahringer, B; Reutemann, P; Witten, IH, The weka data mining software: an update, SIGKDD Explor. Newsl., 11, 10-18, (2009)
[42] Hindley, J.R.: Basic Simple Type Theory, Volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1997)
[43] Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), Number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56-68 (2003) · Zbl 1211.68368
[44] Harrison, J; Urban, J; Wiedijk, F; Siekmann, J (ed.), History of interactive theorem proving, 135-214, (2014), Amsterdam
[45] Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) 23rd International Conference on Automated Deduction (CADE 2011), Volume 6803 of LNCS, pp. 299-314. Springer, New York (2011) · Zbl 1341.68189
[46] Joosten, S., Kaliszyk, C., Urban, J.: Initial experiments with TPTP-style automated theorem provers on ACL2 problems. In: Verbeek, F., Schmaltz, J. (eds.) ACL2 Theorem Prover and Its Applications (ACL2 2014), Volume 152 of EPTCS, pp. 77-85 (2014) · Zbl 0761.03004
[47] Jones, KS, A statistical interpretation of term specificity and its application in retrieval, J. Doc., 28, 11-21, (1972)
[48] Komendantskaya, E. Heras, J., Grov, G.: Machine learning in Proof General: Interfacing interfaces. In: Kaliszyk, C., Lüth, C. (eds.) User Interfaces for Theorem (UITP 2012), Volume 118 of EPTCS, pp. 15-41 (2013)
[49] Kaliszyk, C. Mamane, L. Urban, J.: Machine learning of Coq proof guidance: First experiments. In: Kutsia, T., Voronkov, A. (eds.) Symbolic Computation in Software Science (SCSS 2014), Volume 30 of EPiC, pp. 27-34. EasyChair (2014)
[50] Kaliszyk, C., Urban, J.: PRocH: Proof reconstruction for HOL Light. In: Bonacina, M.P. (ed.) International Conference on Automated Deduction (CADE 2013), Volume 7898 of LNCS, pp. 267-274. Springer, New York (2013) · Zbl 1381.68271
[51] Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) Proof Exchange for Theorem Proving (PxTP 2013), Volume 14 of EPiC, pp. 87-95. EasyChair (2013)
[52] Kaliszyk, C; Urban, J, Learning-assisted automated reasoning with flyspeck, J. Autom. Reason., 53, 173-213, (2014) · Zbl 1314.68283
[53] Kaliszyk, C; Urban, J, HOL(y)hammer: online ATP service for HOL light, Math. Comput. Sci., 9, 5-22, (2015) · Zbl 1322.68177
[54] Kaliszyk, C; Urban, J, Learning-assisted theorem proving with millions of lemmas, J. Symb. Comput., 69, 109-128, (2015) · Zbl 1315.68220
[55] Kaliszyk, C; Urban, J, Mizar 40 for mizar 40, J. Autom. Reason., 55, 245-256, (2015) · Zbl 1356.68191
[56] Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 3084-3090. AAAI Press, Palo Alto (2015)
[57] Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer-Aided Verification (CAV 2013), Volume 8044 of LNCS, pp. 1-35. Springer, New York (2013) · Zbl 1291.68328
[58] Kühlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) International Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of LNCS, pp. 378-392. Springer, New York (2012) · Zbl 1358.68259
[59] Laurent, J.: Suggesting relevant lemmas by learning from successful proofs. Technical report, École normale supérieure (2016). Internship Report
[60] Letouzey, P.: Programmation fonctionnelle certifiée : L’extraction de programmes dans l’assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant). PhD thesis, University of Paris-Sud, Orsay, France, (2004)
[61] Meng, J; Paulson, LC, Translating higher-order clauses to first-order clauses, J. Autom. Reason., 40, 35-60, (2008) · Zbl 1203.68188
[62] Meng, J; Paulson, LC, Lightweight relevance filtering for machine-generated resolution problems, J. Appl. Log., 7, 41-57, (2009) · Zbl 1183.68560
[63] Paulson, L.C., Blanchette, J.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: 8th IWIL (2010)
[64] Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007), Volume 4732 of LNCS, pp. 232-245. Springer, New York (2007) · Zbl 1144.68364
[65] Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence (LPAR 2013), Volume 8312 of LNCS, pp. 735-743. Springer, New York (2013) · Zbl 1407.68442
[66] Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: Jprover : Integrating connection-based theorem proving into interactive proof assistants. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, Volume 2083 of Lecture Notes in Computer Science, pp. 421-426. Springer, New York (2001) · Zbl 0988.68609
[67] Slind, K; Norrish, M; Mohamed, OA (ed.); Muñoz, C (ed.); Tahar, S (ed.), A brief overview of HOL4, 28-32, (2008), New York · Zbl 1165.68474
[68] Sutcliffe, G; Clarke, E (ed.); Voronkov, A (ed.), The TPTP world-infrastructure for automated reasoning, 1-12, (2010), New York · Zbl 1253.68292
[69] Tammet, T; Smith, JM, Optimized encodings of fragments of type theory in first-order logic, J. Log. Comput., 8, 713-744, (1998) · Zbl 0926.03009
[70] Urban, J, MPTP—motivation, implementation, First Exp. J. Autom. Reason., 33, 319-339, (2004) · Zbl 1075.68081
[71] Urzyczyn, P, Intuitionistic games: determinacy, completeness, and normalization, Stud. Log., 104, 957-1001, (2016) · Zbl 1417.03127
[72] Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) Intelligent Computer Mathematics (CICM 2010), Volume 6167 of LNCS, pp. 132-146 (2010) · Zbl 1315.68217
[73] Wiedijk, F.: Mizar’s soft type system. In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 383-399 (2007) · Zbl 1144.68370
[74] Wenzel, M; Paulson, LC; Nipkow, T; Mohamed, OA (ed.); Muñoz, CA (ed.); Tahar, S (ed.), The isabelle framework, 33-38, (2008), New York
[75] Zielenkiewicz, M., Schubert, A.: Automata theory approach to predicate intuitionistic logic. In: Logic-Based Program Synthesis and Transformation—26th International Symposium, LOPSTR 2016, Revised Selected Papers, pp. 345-360 (2016) · Zbl 1485.03022
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.