A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)

Anne Baanen*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

32 Downloads (Pure)

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 languageEnglish
Title of host publicationAutomated Reasoning
Subtitle of host publication10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II
EditorsNicolas Peltier, Viorica Sofronie-Stokkermans
PublisherSpringer
Pages21-27
Number of pages7
Volume2
ISBN (Electronic)9783030510541
ISBN (Print)9783030510534
DOIs
Publication statusPublished - 2020
Event10th International Joint Conference on Automated Reasoning, IJCAR 2020 - Virtual, Online
Duration: 1 Jul 20204 Jul 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12167 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th International Joint Conference on Automated Reasoning, IJCAR 2020
CityVirtual, Online
Period1/07/204/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!

Fingerprint

Dive into the research topics of 'A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)'. Together they form a unique fingerprint.

Cite this