Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Authors: 
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre VialAuthors Info & Claims
Pages 63 - 77
Abstract
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones.
This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.
References
[1]
Qinxiang Cao Andrew W. Appel, Lennart Beringer and Josiah Dodds. 2022. Verifiable C. https://github.com/PrincetonUniversity/VST/raw/master/doc/VC.pdf
[2]
Andrew W. Appel. 2011. Verified Software Toolchain - (Invited Talk). In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, Gilles Barthe (Ed.) (Lecture Notes in Computer Science, Vol. 6602). Springer, 1–17. https://doi.org/10.1007/978-3-642-19718-5_1
[3]
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark W. Barrett. 2019. Extending SMT Solvers to Higher-Order Logic. In Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Pascal Fontaine (Ed.) (Lecture Notes in Computer Science, Vol. 11716). Springer, 35–54. https://doi.org/10.1007/978-3-030-29436-6_3
[4]
Frédéric Besson. 2006. Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, Thorsten Altenkirch and Conor McBride (Eds.) (Lecture Notes in Computer Science, Vol. 4502). Springer, 48–62. https://doi.org/10.1007/978-3-540-74464-1_4
[5]
Frédéric Besson. 2017. ppsimpl: a reflexive Coq tactic for canonising goals. In Coq Workshop on Programming Languages. https://popl17.sigplan.org/details/main/3/ppsimpl-a-reflexive-Coq-tactic-for-canonising-goals
[6]
Frédéric Besson. 2021. Itauto: An Extensible Intuitionistic SAT Solver. In 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), Liron Cohen and Cezary Kaliszyk (Eds.) (LIPIcs, Vol. 193). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 9:1–9:18. https://doi.org/10.4230/LIPIcs.ITP.2021.9
[7]
Valentin Blot, Louise Dubois de Prisque, Chantal Keller, and Pierre Vial. 2021. General Automation in Coq through Modular Transformations. In Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021, Chantal Keller and Mathias Fleury (Eds.) (EPTCS, Vol. 336). 24–39. https://doi.org/10.4204/EPTCS.336.3
[8]
François Bobot and Andrey Paskevich. 2011. Expressing Polymorphic Types in a Many-Sorted Language. In Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, Cesare Tinelli and Viorica Sofronie-Stokkermans (Eds.) (Lecture Notes in Computer Science, Vol. 6989). Springer, 87–102. https://doi.org/10.1007/978-3-642-24364-6_7
[9]
Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, and Pascal Fontaine. 2009. veriT: An Open, Trustable and Efficient SMT-Solver. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, Renate A. Schmidt (Ed.) (Lecture Notes in Computer Science, Vol. 5663). Springer, 151–156. https://doi.org/10.1007/978-3-642-02959-2_12
[10]
Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. isbn:978-0-262-02665-9 http://mitpress.mit.edu/books/certified-programming-dependent-types
[11]
Lukasz Czajka. 2018. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 97). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 9:1–9:39. isbn:978-3-95977-065-1 issn:1868-8969 https://doi.org/10.4230/LIPIcs.TYPES.2016.9
[12]
Lukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason., 61, 1-4 (2018), 423–453. https://doi.org/10.1007/s10817-018-9458-4
[13]
Enzo Crance Denis Cousineau and Assia Mahboubi. 2022. Trakt: a generic pre-processing tactic for theory-based proof automation. Abstract and talk at the Coq Workshop 2022, https://www.youtube.com/watch?v=dZyylCY1seE
[14]
Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, and Makarius Wenzel. 2022. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, June Andronick and Leonardo de Moura (Eds.) (LIPIcs, Vol. 237). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 8:1–8:18. https://doi.org/10.4230/LIPIcs.ITP.2022.8
[15]
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Rupak Majumdar and Viktor Kuncak (Eds.) (Lecture Notes in Computer Science, Vol. 10427). Springer, 126–133. https://doi.org/10.1007/978-3-319-63390-9_7
[16]
Benjamin Grégoire and Assia Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Joe Hurd and Thomas F. Melham (Eds.) (Lecture Notes in Computer Science, Vol. 3603). Springer, 98–113. https://doi.org/10.1007/11541868_7
[17]
Amélie Ledein and Catherine Dubois. 2020. FaCiLe en Coq : vérification formelle des listes d’intervalles. In JFLA’20 : Journées Francophones sur les Langages Applicatifs (Annual Workshop). INRIA.
[18]
Xavier Leroy and Sandrine Blazy. 2008. Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason., 41, 1 (2008), 1–31. https://doi.org/10.1007/s10817-008-9099-0
[19]
Robert Y. Lewis and Paul-Nicolas Madelaine. 2020. Simplifying Casts and Coercions (Extended Abstract). In Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual), Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, and Sophie Tourret (Eds.) (CEUR Workshop Proceedings, Vol. 2752). CEUR-WS.org, 53–62. http://ceur-ws.org/Vol-2752/paper4.pdf
[20]
Assia Mahboubi and Enrico Tassi. 2013. Canonical Structures for the Working Coq User. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.) (Lecture Notes in Computer Science, Vol. 7998). Springer, 19–34. https://doi.org/10.1007/978-3-642-39634-2_5
[21]
Assia Mahboubi and Enrico Tassi. 2021. Mathematical Components. Zenodo. https://doi.org/10.5281/zenodo.4457887
[22]
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. 2019. Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Luís Caires (Ed.) (Lecture Notes in Computer Science, Vol. 11423). Springer, 30–59. https://doi.org/10.1007/978-3-030-17184-1_2
[23]
Conor McBride, Healfdene Goguen, and James McKinna. 2004. A Few Constructions on Constructors. In Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner (Eds.) (Lecture Notes in Computer Science, Vol. 3839). Springer, 186–200. https://doi.org/10.1007/11617990_12
[24]
Sean McLaughlin and John Harrison. 2005. A Proof-Producing Decision Procedure for Real Arithmetic. In Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, Robert Nieuwenhuis (Ed.) (Lecture Notes in Computer Science, Vol. 3632). Springer, 295–314. https://doi.org/10.1007/11532231_22
[25]
Dale Miller. 2000. Abstract Syntax for Variable Binders: An Overview. In Computational Logic - CL 2000, First International Conference, London, UK, 24-28 July, 2000, Proceedings, John W. Lloyd, Verónica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey (Eds.) (Lecture Notes in Computer Science, Vol. 1861). Springer, 239–253. https://doi.org/10.1007/3-540-44957-4_16
[26]
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. 2018. Logical Foundations. Electronic textbook. Version 5.5. http://www.cis.upenn.edu/ bcpierce/sf
[27]
Kazuhiko Sakaguchi. 2012-2020. A Formalization of Typed and Untyped λ -Calculi in Coq and Agda2. https://github.com/pi8027/lambda-calculus
[28]
Kazuhiko Sakaguchi. 2019-2022. Micromega tactics for Mathematical Components. https://github.com/math-comp/mczify
[29]
Kazuhiko Sakaguchi. 2022. Reflexive Tactics for Algebra, Revisited. In 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, June Andronick and Leonardo de Moura (Eds.) (LIPIcs, Vol. 237). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 29:1–29:22. https://doi.org/10.4230/LIPIcs.ITP.2022.29
[30]
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2020. The MetaCoq Project. J. Autom. Reason., 64, 5 (2020), 947–999. https://doi.org/10.1007/s10817-019-09540-0
[31]
Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (Eds.) (Lecture Notes in Computer Science, Vol. 5170). Springer, 278–293. https://doi.org/10.1007/978-3-540-71067-7_23
[32]
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-monadic effects in F. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256–270. https://doi.org/10.1145/2837614.2837655
[33]
Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. 2021. The Marriage of Univalence and Parametricity. J. ACM, 68, 1 (2021), Article 5, jan, 44 pages. issn:0004-5411 https://doi.org/10.1145/3429979
[34]
Enrico Tassi. 2019. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019), John Harrison, John O’Leary, and Andrew Tolmach (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 141). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 29:1–29:18. isbn:978-3-95977-122-1 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ITP.2019.29
[35]
The Coq Development Team. 2022. The Coq Proof Assistant. https://doi.org/10.5281/zenodo.5846982
Index Terms
- Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Recommendations
Completeness and Decidability Results for CTL in Constructive Type Theory
We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our main result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system ...
Learning-Assisted Automated Reasoning with Flyspeck
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the Flyspeck proofs, producing an AI system capable of proving a ...
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
AbstractWe illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive Constructions, by taking advantage of natural deduction semantics and ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2023
347 pages
ISBN:9798400700262
DOI:10.1145/3573105
- General Chairs:
- Robbert Krebbers,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Steve Zdancewic
Copyright © 2023 ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 January 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
CPP '23
Sponsor:
CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 16 - 17, 2023
MA, Boston, USA
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 104Total Downloads
- Downloads (Last 12 months)17
- Downloads (Last 6 weeks)2
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in