Abstract
This paper describes the design of the normalising tactic ring_exp for the Lean prover. This tactic improves on existing tactics by extending commutative rings with a binary exponent operator. An inductive family of types represents the normal form, enforcing various invariants. The design can also be extended with more operators.
Original language | English |
---|---|
Title of host publication | Automated Reasoning |
Subtitle of host publication | 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II |
Editors | Nicolas Peltier, Viorica Sofronie-Stokkermans |
Publisher | Springer |
Pages | 21-27 |
Number of pages | 7 |
Volume | 2 |
ISBN (Electronic) | 9783030510541 |
ISBN (Print) | 9783030510534 |
DOIs | |
Publication status | Published - 2020 |
Event | 10th International Joint Conference on Automated Reasoning, IJCAR 2020 - Virtual, Online Duration: 1 Jul 2020 → 4 Jul 2020 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12167 LNAI |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 10th International Joint Conference on Automated Reasoning, IJCAR 2020 |
---|---|
City | Virtual, Online |
Period | 1/07/20 → 4/07/20 |
Bibliographical note
The final authenticated version is available online at https://doi.org/10.1007/978-3-030-51054-1_2.Funding
The author has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Floris van Doorn, Mario Carneiro and Robert Y. Lewis reviewed the code and suggested improvements. Brian Gin-Ge Chen, Gabriel Ebner, Jasmin Blanchette, Kevin Buzzard, Robert Y. Lewis, Sander Dahmen and the anonymous reviewers read this paper and gave useful suggestions. Many thanks for the help!