Document Open Access Logo

A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper)

Author Arend Mellendijk

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.35.pdf
  • Filesize: 0.57 MB
  • 8 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Theorem proving algorithms
  • Theory of computation → Automated reasoning
  • Theory of computation → Type theory
Keywords
  • Lean
  • Mathlib
  • algebraic structures
  • proof algorithms

Metrics

Abstract

This paper introduces the algebra normalizing tactic for the Lean theorem prover. This tactic expands on the existing ring tactic by additionally supporting a scalar multiplication action over a fixed commutative (semi)ring. It supports rational constants in the base ring even when the main ring is not a field, which lets us implement a suite of tactics for manipulating both univariate and multivariate polynomials. These features are implemented by adapting the existing implementation of ring while retaining support for variable exponents.

Cite As Get BibTex

Arend Mellendijk. A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 35:1-35:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.35

Author Details

Arend Mellendijk
  • University of Bonn, Germany

Supplementary Materials

References

  1. Anne Baanen. A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 21-27, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-51054-1_2.
  2. Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. Journal of Automated Reasoning, 66(4):611-637, 2022. URL: https://doi.org/10.1007/s10817-022-09644-0.
  3. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  4. Gabriel Ebner. Qq: Intuitive, type-safe expression quotations for Lean 4. URL: https://github.com/leanprover-community/quote4.
  5. Benjamin Grégoire and Assia Mahboubi. Proving Equalities in a Commutative Ring Done Right in Coq. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, pages 98-113, Berlin, Heidelberg, 2005. Springer. URL: https://doi.org/10.1007/11541868_7.
  6. John Harrison. HOL Light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design, pages 265-269, Berlin, Heidelberg, 1996. Springer. URL: https://doi.org/10.1007/BFb0031814.
  7. Robert Y. Lewis and Paul Nicolas Madelaine. Simplifying casts and coercions (Extended Abstract): Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020. PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020, pages 53-62, 2020. URL: https://www.scopus.com/pages/publications/85097274168.
  8. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, 2022. Version Number: 1.0.2. URL: https://doi.org/10.5281/zenodo.7118596.
  9. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  10. Arend Mellendijk. algebra-tactic. Software, (visited on 2026-07-13). URL: https://github.com/amellendijk/algebra-tactic
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27124
  11. Tobias Nipkow, Markus Wenzel, Lawrence C. Paulson, Gerhard Goos, Juris Hartmanis, and Jan Van Leeuwen, editors. Isabelle/HOL, volume 2283 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  12. Kazuhiko Sakaguchi. Reflexive Tactics for Algebra, Revisited. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1-29:22, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.29.
  13. Eric Wieser. Scalar actions in Lean’s mathlib, 2021. arXiv:2108.10700 [cs]. URL: https://doi.org/10.48550/arXiv.2108.10700.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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