Document Open Access Logo

Reflexive Tactics for Algebra, Revisited

Author Kazuhiko Sakaguchi

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.29.pdf
  • Filesize: 0.82 MB
  • 22 pages

Document Identifiers

Author Details

Kazuhiko Sakaguchi
  • Unaffiliated researcher, Tokyo, Japan

Acknowledgements

The author would like to thank Enrico Tassi for his help with Coq-Elpi, particularly for adding some features and fixing performance bottlenecks, and Assia Mahboubi for providing useful examples for identifying issues in earlier versions of our ring and field tactics. The comments on earlier versions of this paper by Anne Baanen, Assia Mahboubi, Enrico Tassi, and the anonymous reviewers have also been a great help.

Cite As Get BibTex

Kazuhiko Sakaguchi. Reflexive Tactics for Algebra, Revisited. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ITP.2022.29

Abstract

Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology include decidable algebraic theories such as equational theories of commutative rings and lattices. However, such existing tools are known not to cooperate with packed classes, a methodology to define mathematical structures in dependent type theory, that allows for the sharing of vocabulary across the inheritance hierarchy. Moreover, such tools do not support homomorphisms whose domain and codomain types may differ. This paper demonstrates how to implement reflexive tactics that support packed classes and homomorphisms. As applications of our methodology, we adapt the ring and field tactics of Coq to the commutative ring and field structures of the Mathematical Components library, and apply the resulting tactics to the formal proof of the irrationality of ζ(3) by Chyzak, Mahboubi, and Sibut-Pinote. As a result, the lines of code in the proof scripts have been reduced by 8%, and the time required for proof checking has been decreased by 27%.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Theorem proving algorithms
  • Theory of computation → Automated reasoning
  • Theory of computation → Type theory
  • Theory of computation → Constraint and logic programming
Keywords
  • Coq
  • Elpi
  • λProlog
  • Mathematical Components
  • algebraic structures
  • packed classes
  • canonical structures
  • proof by reflection

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: A case study in functional analysis. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 3-20. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_1.
  2. Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William E. Aitken. The semantics of reflected proof. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 95-105. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113737.
  3. Roger Apéry. Irrationalité de ζ(2) et ζ(3). Astérisque, 61, 1979. Société Mathématique de France. Google Scholar
  4. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in unification. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 84-98. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_8.
  5. Anne Baanen. A Lean tactic for normalising ring expressions with exponents (short paper). In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 21-27. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_2.
  6. Frédéric Besson. 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, volume 4502 of Lecture Notes in Computer Science, pages 48-62. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_4.
  7. Frédéric Besson. ppsimpl: a reflexive Coq tactic for canonising goals. In The Third International Workshop on Coq for Programming Languages, CoqPL 2017, 2017. URL: https://popl17.sigplan.org/details/main/3/ppsimpl-a-reflexive-Coq-tactic-for-canonising-goals.
  8. Frédéric Besson. Fix #10779 (hnf normalisation of instance + reification of overloaded operators), 2019. Accessed: 2022-04-27. URL: https://github.com/coq/coq/pull/10787.
  9. Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial. Modular pre-processing for automated reasoning in dependent type theory, 2022. URL: https://doi.org/10.48550/ARXIV.2204.02643.
  10. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 362-377. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_26.
  11. Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Theoretical Aspects of Computer Software, Third International Symposium, TACS '97, Sendai, Japan, September 23-26, 1997, Proceedings, volume 1281 of Lecture Notes in Computer Science, pages 515-529. Springer, 1997. URL: https://doi.org/10.1007/BFb0014565.
  12. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 73-78. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  13. Thomas Braibant and Damien Pous. Tactics for reasoning modulo AC in Coq. In Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 167-182. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_14.
  14. Thomas Braibant and Damien Pous. Deciding Kleene algebras in Coq. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:16)2012.
  15. Adam Chlipala. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. URL: http://mitpress.mit.edu/books/certified-programming-dependent-types.
  16. Frédéric Chyzak, Assia Mahboubi, and Thomas Sibut-Pinote. Apery: A formal proof of the irrationality of zeta(3), the Apéry constant, 2020. Accessed: 2022-02-08. URL: https://github.com/coq-community/apery.
  17. Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi. A computer-algebra-based formal proof of the irrationality of ζ(3). In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 160-176. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_11.
  18. Cyril Cohen. Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction et théorie du premier ordre). PhD thesis, École Polytechnique, Palaiseau, France, 2012. URL: https://tel.archives-ouvertes.fr/pastel-00780446.
  19. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, volume 8307 of Lecture Notes in Computer Science, pages 147-162. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_10.
  20. Cyril Cohen and Damien Rouhling. A refinement-based approach to large scale reflection for algebra. In JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, 2017. URL: https://hal.inria.fr/hal-01414881.
  21. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  22. David Delahaye. A tactic language for the system Coq. In Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, volume 1955 of Lecture Notes in Computer Science, pages 85-95. Springer, 2000. URL: https://doi.org/10.1007/3-540-44404-1_7.
  23. Maxime Dénès, Anders Mörtberg, and Vincent Siles. A refinement-based approach to computational algebra in Coq. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, volume 7406 of Lecture Notes in Computer Science, pages 83-98. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_7.
  24. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, λProlog interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 460-468. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_32.
  25. François Garillot. Generic Proof Tools and Finite Group Theory. (Outils génériques de preuve et théorie des groupes finis). PhD thesis, École Polytechnique, Palaiseau, France, 2011. URL: https://tel.archives-ouvertes.fr/pastel-00649586.
  26. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 327-342. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_23.
  27. Paolo G. Giarrusso. ring tactic breaks on mathcomp: it requires all ring operations are defined on syntactically equal types, not definitionally equal ones, 2020. Accessed: 2021-12-07. URL: https://github.com/coq/coq/issues/11998.
  28. Georges Gonthier and Enrico Tassi. A language of patterns for subterm selection. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, volume 7406 of Lecture Notes in Computer Science, pages 361-376. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_25.
  29. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. Journal of Functional Programming, 23(4):357-401, 2013. URL: https://doi.org/10.1017/S0956796813000051.
  30. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, pages 235-246. ACM, 2002. URL: https://doi.org/10.1145/581478.581501.
  31. Benjamin Grégoire and Assia Mahboubi. 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, volume 3603 of Lecture Notes in Computer Science, pages 98-113. Springer, 2005. URL: https://doi.org/10.1007/11541868_7.
  32. Jason Gross, Andres Erbsen, and Adam Chlipala. Reification by parametricity - fast setup for proof by reflection, in two lines of Ltac. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 289-305. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_17.
  33. Benjamin S. Hvass. ring tactic for math-comp integers, 2019. Accessed: 2021-12-07. URL: https://github.com/math-comp/math-comp/issues/401.
  34. Daniel W. H. James and Ralf Hinze. A reflection-based proof tactic for lattices in Coq. In Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Komárno, Slovakia, June 2-4, 2009, volume 10 of Trends in Functional Programming, pages 97-112. Intellect, 2009. Google Scholar
  35. Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, and Derek Dreyer. Mtac2: typed tactics for backward reasoning in Coq. Proceedings of the ACM on Programming Languages, 2(ICFP):78:1-78:31, 2018. URL: https://doi.org/10.1145/3236773.
  36. Robert Y. Lewis and Paul-Nicolas Madelaine. 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), volume 2752 of CEUR Workshop Proceedings, pages 53-62, 2020. URL: http://ceur-ws.org/Vol-2752/paper4.pdf.
  37. Assia Mahboubi and Thomas Sibut-Pinote. A formal proof of the irrationality of ζ(3). Logical Methods in Computer Science, 17(1), 2021. URL: https://doi.org/10.23638/LMCS-17(1:16)2021.
  38. Assia Mahboubi and Enrico Tassi. Canonical structures for the working Coq user. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 19-34. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_5.
  39. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  40. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9781139021326.
  41. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  42. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  43. Pierre-Marie Pédrot. Ltac2: Tactical warfare. In The Fifth International Workshop on Coq for Programming Languages, CoqPL 2019, 2019. URL: https://popl19.sigplan.org/details/CoqPL-2019/8/Ltac2-Tactical-Warfare.
  44. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, pages 199-208. ACM, 1988. URL: https://doi.org/10.1145/53990.54010.
  45. Claudio Sacerdoti Coen and Enrico Tassi. ELPI - embeddable λProlog interpreter. Accessed: 2022-02-08. URL: https://github.com/LPCIC/elpi.
  46. Amokrane Saïbi. Typing algorithm in type theory with inheritance. In Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997, pages 292-301. ACM Press, 1997. URL: https://doi.org/10.1145/263699.263742.
  47. Amokrane Saïbi. Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory). PhD thesis, Pierre and Marie Curie University, Paris, France, 1999. URL: https://tel.archives-ouvertes.fr/tel-00523810.
  48. Kazuhiko Sakaguchi. Validating mathematical structures. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 138-157. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_8.
  49. Kazuhiko Sakaguchi. Algebra tactics, 2021. Accessed: 2022-02-08. URL: https://github.com/math-comp/algebra-tactics.
  50. Kazuhiko Sakaguchi. Mczify, 2021. Accessed: 2022-02-08. URL: https://github.com/math-comp/mczify.
  51. Matthieu Sozeau and Nicolas Oury. First-class type classes. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 278-293. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  52. Bas Spitters and Eelis van der Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21(4):795-825, 2011. URL: https://doi.org/10.1017/S0960129511000119.
  53. Enrico Tassi. Coq-Elpi. Accessed: 2022-02-08. URL: https://github.com/LPCIC/coq-elpi.
  54. The Coq Development Team. The Coq Proof Assistant Reference Manual, 2022. the PDF version with numbered sections is available at https://doi.org/10.5281/zenodo.1003420. URL: https://coq.inria.fr/distrib/V8.15.0/refman/.
  55. The Coq Development Team. Section 2.2.4 "syntax extensions and notation scopes", 2022. URL: https://coq.inria.fr/distrib/V8.15.0/refman/user-extensions/syntax-extensions.
  56. The Coq Development Team. Section 2.2.6 "implicit coercions", 2022. URL: https://coq.inria.fr/distrib/V8.15.0/refman/addendum/implicit-coercions.
  57. The Coq Development Team. Section 2.2.8 "canonical structures", 2022. URL: https://coq.inria.fr/distrib/V8.15.0/refman/language/extensions/canonical.
  58. The Coq Development Team. Section 3.1.5 "the ssreflect proof language", 2022. URL: https://coq.inria.fr/distrib/V8.15.0/refman/proof-engine/ssreflect-proof-language.
  59. The Coq Development Team. Section 3.2.2 "micromega: solvers for arithmetic goals over ordered rings", 2022. URL: https://coq.inria.fr/distrib/V8.15.0/refman/addendum/micromega.
  60. The Coq Development Team. Section 3.2.3 "ring and field: solvers for polynomial and rational equations", 2022. URL: https://coq.inria.fr/distrib/V8.15.0/refman/addendum/ring.
  61. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  62. Alfred van der Poorten. A proof that Euler missed: Apéry’s proof of the irrationality of ζ(3). Math. Intelligencer, 1(4):195-203, 1979. An informal report. URL: https://doi.org/10.1007/BF03028234.
  63. Beta Ziliani and Matthieu Sozeau. A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Journal of Functional Programming, 27:e10, 2017. URL: https://doi.org/10.1017/S0956796817000028.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact