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

Anne Baanen

doi:10.1007/978-3-030-51054-1_2

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 proceeding › Conference contribution › Academic › peer-review

49 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 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	https://doi.org/10.1007/978-3-030-51054-1_2
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!

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Access to Document

10.1007/978-3-030-51054-1_2

A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)Final published version, 306 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Baanen, A. (2020). A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). In N. Peltier, & V. Sofronie-Stokkermans (Eds.), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II (Vol. 2, pp. 21-27). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12167 LNAI). Springer. https://doi.org/10.1007/978-3-030-51054-1_2

Baanen, Anne. / A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. editor / Nicolas Peltier ; Viorica Sofronie-Stokkermans. Vol. 2 Springer, 2020. pp. 21-27 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{027c5b817e634044b9d3dde0f202e42a,

title = "A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)",

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.",

author = "Anne Baanen",

note = "The final authenticated version is available online at https://doi.org/10.1007/978-3-030-51054-1\_2.; 10th International Joint Conference on Automated Reasoning, IJCAR 2020 ; Conference date: 01-07-2020 Through 04-07-2020",

year = "2020",

doi = "10.1007/978-3-030-51054-1\_2",

language = "English",

isbn = "9783030510534",

volume = "2",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "21--27",

editor = "Nicolas Peltier and Viorica Sofronie-Stokkermans",

booktitle = "Automated Reasoning",

}

Baanen, A 2020, A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). in N Peltier & V Sofronie-Stokkermans (eds), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. vol. 2, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12167 LNAI, Springer, pp. 21-27, 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Virtual, Online, 1/07/20. https://doi.org/10.1007/978-3-030-51054-1_2

A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). / Baanen, Anne.
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. ed. / Nicolas Peltier; Viorica Sofronie-Stokkermans. Vol. 2 Springer, 2020. p. 21-27 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12167 LNAI).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Baanen, Anne

N1 - The final authenticated version is available online at https://doi.org/10.1007/978-3-030-51054-1_2.

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85088234858

UR - https://www.scopus.com/pages/publications/85088234858#tab=citedBy

U2 - 10.1007/978-3-030-51054-1_2

DO - 10.1007/978-3-030-51054-1_2

M3 - Conference contribution

SN - 9783030510534

VL - 2

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 21

EP - 27

BT - Automated Reasoning

A2 - Peltier, Nicolas

A2 - Sofronie-Stokkermans, Viorica

PB - Springer

T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020

Y2 - 1 July 2020 through 4 July 2020

ER -

Baanen A. A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). In Peltier N, Sofronie-Stokkermans V, editors, Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II. Vol. 2. Springer. 2020. p. 21-27. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2020 Jun 24. doi: 10.1007/978-3-030-51054-1_2

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

Abstract

Publication series

Conference

Bibliographical note

Funding

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this