{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:06:54Z","timestamp":1784844414866,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Equations are ubiquitous in mathematical reasoning. Often, however, they only hold under certain conditions. As these conditions are usually clear from context, mathematicians regularly omit them when performing equational reasoning on paper. In contrast, interactive theorem provers pedantically insist on every detail to be convinced that a theorem holds, hindering equational reasoning at the more abstract level of pen-andpaper mathematics. In this paper, we address this issue by raising the level of equational reasoning to enable pen-and-paper style in interactive theorem provers. We achieve this by interpreting theorems as conditional rewrite rules, and use equality saturation to automatically derive equational proofs. Conditions that cannot be automatically proven may be surfaced as proof obligations. Concretely, we present how to interpret theorems as conditional rewrite rules for a significant class of theorems. Handling these theorems goes beyond simple syntactic rewriting, and deals with aspects like propositional conditions and type classes. We evaluate our approach by implementing it as a tactic in Lean, using the egg library for equality saturation with e-graphs. We show four use cases demonstrating the efficacy of this higher level of abstraction for equational reasoning.<\/jats:p>","DOI":"10.1145\/3776667","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"718-747","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-3567-6890","authenticated-orcid":false,"given":"Marcus","family":"Rossel","sequence":"first","affiliation":[{"name":"Barkhausen Institut, Dresden, Germany"},{"name":"Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9151-773X","authenticated-orcid":false,"given":"Rudi","family":"Schneider","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8461-8075","authenticated-orcid":false,"given":"Thomas","family":"K\u0153hler","sequence":"additional","affiliation":[{"name":"ICube Lab - CNRS - Universit\u00e9 de Strasbourg, Strasbourg, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-1363","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Goens","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Amsterdam, Netherlands"},{"name":"Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_3_1","unstructured":"Emmanuel Anaya Gonzalez Cole Kurashige Aditya Giridharan and Polikarpova Nadia. 2023. Optimizing Beta Reduction in E-Graphs. (2023). https:\/\/pldi23.sigplan.org\/details\/egraphs-2023-papers\/12\/Optimizing-Beta-Reduction-in-E-GraphsEGRAPHS2023."},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80027-5"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"e_1_3_2_7_1","article-title":"The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale","author":"Bolan Matthew","year":"2026","unstructured":"Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andr\u00e9s Goens, Aaron Hill, Harald Husum, Hern\u00e1n Ibarra Mejia, Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, J\u00e9r\u00e9my Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. 2026. The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. In preparation.","journal-title":"In preparation"},{"key":"e_1_3_2_8_1","volume-title":"Specification and verification of sequential machines in rule-based hardware languages. Ph.D. Dissertation","author":"Bourgeat Thomas","year":"2023","unstructured":"Thomas Bourgeat. 2023. Specification and verification of sequential machines in rule-based hardware languages. Ph.D. Dissertation. MIT, USA. https:\/\/hdl.handle.net\/1721.1\/150194"},{"key":"e_1_3_2_9_1","first-page":"486","volume-title":"Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973","author":"Boyer Robert S.","year":"1973","unstructured":"Robert S. Boyer and J Strother Moore. 1973. Proving Theorems about LISP Functions. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973, Nils J. Nilsson (Ed.). William Kaufmann, 486\u2013493. http:\/\/ijcai.org\/Proceedings\/73\/Papers\/053.pdf"},{"key":"e_1_3_2_10_1","volume-title":"The Type Theory of Lean","author":"Carneiro Mario","year":"2019","unstructured":"Mario Carneiro. 2019. The Type Theory of Lean. Master\u2019s thesis. Carnegie Mellon University."},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2403.14064"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9225-2"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2019.2"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14418-9_11"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9458-4"},{"key":"e_1_3_2_18_1","unstructured":"NG de Bruijn. 1968. Automath: a language for mathematics. (1968)."},{"key":"e_1_3_2_19_1","first-page":"141","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"De Bruijn Nicolaas Govert","year":"1994","unstructured":"Nicolaas Govert De Bruijn. 1994. A survey of the project AUTOMATH. In Studies in Logic and the Foundations of Mathematics. Vol. 133. Elsevier, 141\u2013161."},{"key":"e_1_3_2_20_1","unstructured":"Leonardo de Moura and Kim Morrison. 2025. The Lean Language Reference: The grind tactic. https:\/\/lean-lang.org\/doc\/reference\/latest\/The--grind--tactic\/#grind"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_2_25_1","doi-asserted-by":"crossref","DOI":"10.1007\/1-84628-490-2","volume-title":"Introduction to Lie algebras","author":"Erdmann Karin","year":"2006","unstructured":"Karin Erdmann and Mark J Wildon. 2006. Introduction to Lie algebras. Vol. 122. Springer."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_13"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408974"},{"key":"e_1_3_2_29_1","unstructured":"Muhammad Humayoun. 2010. Mathnat-mathematical text in a controlled natural language. Special issue: Natural Language Processing and its\u2026 (2010)."},{"key":"e_1_3_2_30_1","first-page":"97","volume-title":"Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Kom\u00e1rno, Slovakia, June 2-4, 2009 (Trends in Functional Programming, Vol. 10)","author":"James Daniel W. H.","year":"2009","unstructured":"Daniel W. H. James and Ralf Hinze. 2009. A Reflection-based Proof Tactic for Lattices in Coq. In Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Kom\u00e1rno, Slovakia, June 2-4, 2009 (Trends in Functional Programming, Vol. 10), Zolt\u00e1n Horv\u00e1th, Vikt\u00f3ria Zs\u00f3k, Peter Achten, and Pieter W. M. Koopman (Eds.). Intellect, 97\u2013112."},{"key":"e_1_3_2_31_1","volume-title":"The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023","author":"Jiang Albert Qiaochu","year":"2023","unstructured":"Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth \u00e9e Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net. https:\/\/openreview.net\/forum?id=SMa9EAovKMC"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.5525\/GLA.THESIS.83323"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632900"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/909447"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_3_2_36_1","unstructured":"Lawrence C. Paulson. 1993. Isabelle: The Next 700 Theorem Provers. CoRR cs.LO\/9301106 (1993). https:\/\/arxiv.org\/abs\/cs\/9301106"},{"issue":"2","key":"e_1_3_2_37_1","first-page":"91","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov Alexandre","year":"2002","unstructured":"Alexandre Riazanov and Andrei Voronkov. 2002. The design and implementation of VAMPIRE. AI Commun. 15, 2-3 (2002), 91\u2013110. http:\/\/content.iospress.com\/articles\/ai-communications\/aic259","journal-title":"AI Commun"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Rocq Dev Team. 2025. The Rocq Prover. doi:10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17696648"},{"key":"e_1_3_2_40_1","volume-title":"A first course in abstract algebra: with applications","author":"Rotman Joseph J","year":"2006","unstructured":"Joseph J Rotman. 2006. A first course in abstract algebra: with applications. Pearson."},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729326"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_8"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.34727\/2024\/ISBN.978-3-85448-065-5_13"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"issue":"4","key":"e_1_3_2_45_1","doi-asserted-by":"crossref","first-page":"703","DOI":"10.2307\/2371008","article-title":"Postulates for Boolean algebras and generalized Boolean algebras","volume":"57","author":"Stone Marshall H","year":"1935","unstructured":"Marshall H Stone. 1935. Postulates for Boolean algebras and generalized Boolean algebras. American Journal of Mathematics 57, 4 (1935), 703\u2013732.","journal-title":"American Journal of Mathematics"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_47_1","first-page":"26","volume-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, CA, USA, August 1985","author":"Trybulec Andrzej","year":"1985","unstructured":"Andrzej Trybulec and Howard A. Blair. 1985. Computer Assisted Reasoning with MIZAR. In Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, CA, USA, August 1985, Aravind K. Joshi (Ed.). Morgan Kaufmann, 26\u201328. http:\/\/ijcai.org\/Proceedings\/85-1\/Papers\/006.pdf"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.5445\/IR\/1000161074"},{"key":"e_1_3_2_49_1","volume-title":"Isabelle, Isar - a versatile environment for human readable formal proof documents. Ph. D. Dissertation","author":"Wenzel Markus","year":"2002","unstructured":"Markus Wenzel. 2002. Isabelle, Isar - a versatile environment for human readable formal proof documents. Ph. D. Dissertation. Technical University Munich, Germany. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.pdf"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11542384"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-42753-4_15"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704913"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","unstructured":"Philip Zucker. 2025. Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching. CoRR abs\/2504.14340 (2025). arXiv:2504.14340 doi:10.48550\/ARXIV.2504.14340","DOI":"10.48550\/ARXIV.2504.14340"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:45:09Z","timestamp":1784209509000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776667"],"URL":"https:\/\/doi.org\/10.1145\/3776667","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}