← All papers
A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)
cs.LO
Jan 1, 2020 · v1
TL;DR
Implements a Lean tactic for normalizing ring expressions with natural number exponents.
Abstract
This paper presents a tactic for the Lean theorem prover that normalizes ring expressions involving exponents. The tactic extends the existing ring normalization procedure to handle expressions with natural number exponents, enabling automated reasoning about polynomial identities in commutative rings.
Problem
Lean's existing ring normalization tactic could not handle expressions involving natural number exponents, limiting automated reasoning about polynomial identities in commutative rings with exponentiation.
Approach
The paper presents a tactic for the Lean theorem prover that normalizes ring expressions involving exponents. It extends the existing ring normalization procedure to handle expressions with natural number exponents by defining an appropriate normal form for such expressions.
Results
The tactic enables automated reasoning about polynomial identities in commutative rings with exponents, closing goals that previously required manual proof steps. It integrates with Lean's existing tactic infrastructure.