ring_exp_paper.tex

\documentclass{llncs}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[backend=biber,style=lncs,doi=true]{biblatex}
\usepackage[
   a4paper,
   xetex,
   pdftitle={A Lean tactic for normalising ring expressions with exponents},
   pdfauthor={Anne Baanen},
   pdfkeywords={},
   pdfborder={0 0 0},
   draft=false,
   bookmarksnumbered,
   bookmarks,
   bookmarksdepth=2,
   bookmarksopenlevel=2,
   bookmarksopen]{hyperref}
\usepackage{makecell}
\usepackage{xcolor}
\usepackage{xspace}

\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstset{language=lean}

\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.4, 0.4, 0.4}    % grey
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green

\renewcommand\UrlFont{\color{blue}\rmfamily}

\title{A Lean tactic for normalising ring\\ expressions with exponents (short paper)}
\titlerunning{A Lean tactic for normalising ring expressions with exponents}
\author{Anne Baanen\orcidID{0000-0001-8497-3683}}
\authorrunning{T. Baanen}
\institute{Vrije Universiteit Amsterdam, Amsterdam, The Netherlands\\\email{t.baanen@vu.nl}}

\newcommand{\N}{\mathbb{N}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\lean}[1]{\texttt{#1}\xspace} % for writing Lean expressions
\newcommand{\ex}{\lean{ex}}
\newcommand{\mathlib}{\texttt{mathlib}\xspace}
\newcommand{\pow}{{${}^\wedge$}\xspace}
\newcommand{\ring}{\lean{ring}}
\newcommand{\ringexp}{\lean{ring\_exp}}

\addbibresource{lean.bib}

\begin{document}
\maketitle

\begin{abstract}
This paper describes the design of the normalising tactic \ringexp 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.
\end{abstract}

\section{Introduction}

In interactive theorem proving, normalising tactics are powerful tools to prove equalities.
Given an expression $a$, these tactics return an expression $a'$ in normal form together with a proof that $a = a'$.
%Such tactics are metaprograms which can be applied to an expression $a$,
%and return an expression $a'$ in normal form, together with a proof term showing $a = a'$;
%to prove $a = b$ it suffices to normalise $a'$ and $b'$ and show $a' = b'$.
For instance, in \mathlib~\cite{mathlib}, the mathematical library for the Lean theorem prover~\cite{lean-prover},
%several normalising tactics are included~\cite{mathlib}.
%Among others,
%\lean{norm\_cast} normalises type coercions in an expression,
%\lean{abel} normalises expressions in an Abelian group,
the \ring tactic normalises % polynomials, i.e.
expressions in a commutative (semi)ring.
Analogous tactics or conversions exist in many theorem provers \cite{hol_light, isabelle_hol, agda-stdlib}.
The \ring tactic in Lean can be directly invoked by the user
and is called by the decision procedure \lean{linarith}.
The utility of \ring is evident from the fact that it is invoked over 300 times in \mathlib.

The \ring tactic in Lean, and the tactic in Coq it is based on,
use a Horner normal form representation of polynomials~\cite{ring-tactic}.
%The Horner normal form for univariate polynomials over $\Q$ can be given as an inductive datatype \lean{horner} with two constructors \lean{const} and \lean{xadd};
%$\lean{const}\ c$ for $c : \Q$ represents a constant polynomial $f(x) = c$,
%and $\lean{xadd}\ g\ c$ for $g : \lean{horner}, c : \Q$ represents the polynomial $f(x) = g(x) * x + c$.
The Horner form represents a polynomial $f(x)$ with one of two cases:
either it is constant ($f(x) = c$) or it is of the form $f(x) = c + x * g(x)$.
This representation
% generalised to multivariate polynomials over arbitrary semirings
allows \ring to uniquely and efficiently represent any polynomial,
i.e. any expression consisting of the operators $+$ and $*$, numerals and variables.
Problems arise when expressions include other operators than $+$ and $*$, such as the exponentiation operator \pow.
The Horner form fundamentally assumes the degree of a term is a constant integer,
so it cannot be simply modified to represent variable exponents,
or more generally to represent \pow applied to compound expressions.
The analogous procedures in other theorem provers have the same restriction.
Adding rewrite rules such as $x^{n+1} \mapsto x * x^n$ is not a universal solution.
This rule would unfold the expression $x^{100}$ into a large term composed of repeated multiplications,
reducing the performance of the procedure significantly.
The result is that \ring cannot prove that $2^{n+1} - 1 = 2 * 2^n - 1$ for a free variable $n : \mathbb{N}$.

The \ringexp tactic uses a new extensible normal form, currently supporting the operators $+$, $*$ and \pow, numerals and variables.
Its domain is a strict superset of the domain of previous semiring tactics,
without sacrificing too much of the efficiency of \ring.
This paper describes the design and engineering challenges encountered in implementing \ringexp.

The version of \ringexp discussed in this paper was merged into \mathlib in commit \texttt{5c09372658}.\footnote{\url{https://github.com/leanprover-community/mathlib/tree/5c09372658}}
Additional code and setup instructions are available online.\footnote{\url{https://github.com/lean-forward/ring_exp}}

\section{Design Overview}

The \ringexp tactic uses a normalisation scheme similar to the original \ring tactic.
The input from the tactic system is an abstract syntax tree representing the expression to normalise.
% Lean makes the syntax available for metaprogramming as terms of type \lean{expr}.
An \lean{eval} function maps inputs to a type \lean{ex} of normalised expressions.
The normal form should be designed in such a way that values of type \lean{ex} are equal
if and only if the input expressions can be proved equal using the axioms of commutative semirings.
From the \lean{ex} representation, the normalised output expression is constructed by a function \lean{simple}.
Both \lean{eval} and \lean{simple} additionally return a proof showing that the input and output expressions are equal.

The \ringexp tactic does not use reflection but directly constructs proof terms to be type checked by Lean's kernel,
as is typical for tactics in \mathlib~\cite{mathlib}.
Reflective tactics avoid the construction and checking of a large proof term
by performing most computation during proof checking, running a verified program~\cite{reflection-tactics}.
If the proof checker performs efficient reduction, this results in a significant speed-up of the tactic,
at the same time as providing more correctness guarantees.
Unfortunately, the advantages of reflection do not translate directly to Lean.
Tactic execution in Lean occurs within a fast interpreter,
while the kernel used in proof checking is designed for simplicity instead of efficient reduction~\cite{lean-tactics}.
Achieving an acceptable speed for \ringexp requires other approaches to the benefits that reflection brings automatically.

The language of semirings implemented by \ring, with binary operators $+$, $*$ and optionally $-$ and $/$,
is extended in \ringexp with a binary exponentiation operator \pow.
The input expression can consist of these operators applied to other expressions,
with two base cases: natural numerals such as $0$ and $37$, and \emph{atoms}.
An atom is any expression which is not of the above form, e.g. a variable name $x$ or a function application $\sin (y - z)$.
It is treated as an opaque variable in the expression.
Two such expressions are considered equal if in every commutative semiring they evaluate to equal values, for any assignment to the atoms.
% The theory should not be confused with that of `exponential rings', which extends $+$ and $*$ with a unary operator $E$. %, which is a ring $(R, +, *)$ equipped with a unary operator $E$ which is a monoid homomorphism $(R, +) \to (R^*, *)$.

%For instance, each expression in the language of monoids (with associative operator $*$ and neutral element $1$) has a list of atoms as normal form;
%the conversion interprets $*$ as list concatenation `++` and $1$ as the empty list `nil`.
%Adding an associative, distributive $+$ operator will give the language of semirings,
%and by distributivity, we can always rewrite in such a way that the arguments to $*$ are not sums.
%This allows us to write a polynomial as a sum of monomials, which are themselves products of atoms.
%The exponentation operator, however, does not have such nice associativity or distributivity properties:
%in general, only `(a ^ b)^c = a ^ (b * c)` and `(a * b)^c = a^c * b^c` hold.

\begin{figure}
\begin{lstlisting}
inductive ex_type : Type
| sum | prod | exp | base
inductive ex : ex_type → Type
| zero  : ex_info →                     ex sum     -- 0
| sum   : ex_info → ex prod →  ex sum → ex sum     -- +
| coeff : ex_info →             coeff → ex prod    -- numerals
| prod  : ex_info → ex exp  → ex prod → ex prod    -- *
| exp   : ex_info → ex base → ex prod → ex exp     -- ^
| var   : ex_info →              atom → ex base    -- atoms
| sum_b : ex_info →            ex sum → ex base
\end{lstlisting}
\caption{Definition of \lean{ex\_type} and \ex}
\label{fig:def_ex}
\end{figure}
Using a suitable representation of the normal form is crucial to easily guarantee correctness of the normaliser.
%For expressions in the language of rings, i.e. polynomials,
%there are various possible representations with their own strengths.
%Apart from the Horner form used in the \ring tactic,
%the Lean mathematical library contains the type \lean{mv\_polynomial} representing multivariate polynomials
%as a map from monomials to coefficients, where monomials themselves are maps from the variables to their exponent, as a natural number.
%Neither representation can be easily extended with new operators,
%so \ringexp introduces its own representation of expressions named \ex. 
Since there is no clear way to generalise the Horner form,
\ringexp instead represents its normal form \ex as a tree with operators at the nodes and atoms at the leaves.
Certain classes of non-normalised expressions are prohibited by restricting which sub-node can occur for each node.
% Compared with the abstract syntax tree, this will prohibit certain non-normalised subexpressions.
%For example, associativity allows rewriting $(a * b) * c$ to $a * (b * c)$ and distributivity allows rewriting $(a + b) * c$ to $(a * c) + (b * c)$,
%which leads to the rule that the left argument to $*$ cannot be of the form $a + b$ or $a * b$.
The \ex type captures these restrictions through a parameter in the enum \lean{ex\_type},
creating an inductive family of types.
Each constructor allows specific members of the \ex family in its arguments
and returns a specific type of \ex.
The full definition is given in Figure \ref{fig:def_ex}.
%Here, the `sum` constructor represents $+$, `prod` represents $*$ and `exp` represents $\^$,
%the `zero` and `coeff` constructors represent zero and non-zero numeric coefficients,
%the `var` constructor represents an atom and
The additional \lean{ex\_info} record passed to the constructors contains auxiliary information used to construct correctness proofs.
The \lean{sum\_b} constructor allows sums as the base of a power, analogously to the parentheses in $(a + b) ^ c$.

For readability, we will write the \ex representation in symbols instead of the constructors of \ex.
Thus, the term \lean{sum (prod (exp (var n) (coeff 1)) (coeff 1)) zero} (with \lean{ex\_info} fields omitted) is written as $n^1 * 1 + 0$,
and the normalised form of $2^n - 1$ is written $(2+0)^{n^1 * 1} * 1 + (-1) + 0$.

\begin{table}
\centering
\caption{Associativity and distributivity properties of the $+$, $*$ and \pow operators}
\label{tab:assoc-distrib}
{
\setlength{\tabcolsep}{1em} % Add horizontal padding (absolute amount)
\renewcommand{\arraystretch}{1.7}% Add vertical padding (relative amount)
\begin{tabular}{l | c c c}
	& $+$	& $*$	& \pow	\\ \hline
$+$	& $(a + b) + c = a + (b + c)$	& ---	& --- 	\\
$*$	& \makecell{$(a + b) * c = a * c + b * c$; \\ $a * (b + c) = a * b + a * c$}	& $(a * b) * c = a * (b * c) $	& --- 	\\
\pow	& $a ^ {b + c} = a ^ b * a ^ c$	& $(a * b) ^ c = a^c * b^c$	& $\left(a^b\right)^c = a^{b * c}$	\\
\end{tabular}
}
\end{table}
%Thus, the restriction that $+$ and $*$ cannot occur as the left argument to $*$,
%is reflected by the first argument to `prod` being `ex exp`, which must be of the form $a ^ b$.
%Similarly, the `sum` constructor has arguments `ex prod` and `ex sum`, reflecting that the $+$ operator is re-associated to the right in the normal form.
% Some further examples on how the equalities are reflected in the types?
The types of the arguments to each constructor are determined by the associativity and distributivity properties of the operators involved,
summarised in Table \ref{tab:assoc-distrib}.
Since addition does not distribute over either other operator (as seen from the empty entries on the $+$ row),
an expression with a sum as outermost operator cannot be rewritten so that another operator is outermost.
%The empty sum is the representation of $0$, with constructor \lean{zero}.
Thus, the set of all expressions should be represented by \lean{ex sum}.
Since $*$ distributes over $+$ but not over \pow, the next outermost operator after $+$ will be $*$.
By associativity (the diagonal entries of the table) the left argument to $+$ should have $*$ as outermost operator;
otherwise we can apply the rewrite rule $(a + b) + c \mapsto a + (b + c)$.
Analogously, the left argument to the \lean{prod} constructor is not an \lean{ex prod} but an \lean{ex exp},
% and the right argument to the \lean{exp} constructor is not an \lean{ex exp} but an \lean{ex prod}.
and the left argument to \lean{exp} is an \lean{ex base}.

%\begin{align*}
%	0 &\mapsto 0\\
%	1 &\mapsto 1 + 0\\
%	x &\mapsto x^1 * 1 + 0\\
%	\frac{2}{3} y^{2^k} z - x &\mapsto x^1 * (-1) + \left(y^{(2 + 0)^{k * 1} * 1} * z^1 * \frac{2}{3} + 0\right)
%\end{align*}

% Although the \ring tactic described by \citeauthor{ring-tactic} is based on reflection,
% kernel computation in Lean is relatively slow.
% Thus, the \ringexp tactic follows the Lean \ring tactic in constructing its proof directly.
The \lean{eval} function interprets each operator in the input expression as a corresponding operation on \ex,
building a normal form for the whole expression out of normalised subexpressions.
The operations on \ex build the correctness proof of normalisation out of the proofs for subexpressions
using a correctness lemma: for example, the lemma \lean{add\_pf\_z\_sum : ps = 0 → qs = qs' → ps + qs = qs'} is used on the input expression \lean{ps + qs} when \lean{ps} normalises to $0$.
% These correctness proofs are stored in the \lean{ex\_info} record. % so they can be easily passed to other operations.

Adding support for a new operator would take relatively little work:
after extending the table of associativity and distributivity relations,
one can insert the constructor in \ex using the table to determine the relevant \lean{ex\_type},
and add an operation on \ex that interprets the operator.

% Finally, the \lean{tactic.interactive.ring\_exp} function ties the various parts together.
% It reads the expression(s) to normalise from the tactic state,
% parses them into an \ex,
% reads out the normalisation proofs from the \lean{ex\_info},
% and uses these proofs to rewrite the expressions.

\section{Intricacies}

The \ex type enforces that distributivity and associativity rules are always applied,
but commutative semirings have more equations.
% For instance, the $+$ and $*$ operators are also commutative:
% but this is not reflected in this definition of the \ex type:
% if $a, b : \lean{ex prod}$, $a + (b + 0)$ and $b + (a + 0)$ represent the same expression.
% $a + (b + 0)$ and $b + (a + 0)$ represent equal expressions.
In a normal form, arguments to commutative operators should be sorted according to some linear order $\prec$: if $a \prec b$, then $a + (b + 0)$ is normalised and $b + (a + 0)$ is not.
Defining a linear order on \ex requires an order on atoms; definitional equality of atoms is tested (with user control over the amount of definitional unfolding) in the \lean{tactic} monad~\cite{lean-tactics},
so a well-defined order on atoms cannot be easily expressed on the type level.
% Unfortunately, operations on expressions such as testing for definitional equality requires the usage of the \lean{tactic} monad~\cite{lean-tactics},
% making it unfeasible to enforce invariants on the type level.
% Thus, a well-defined linear order with respect to definitional equality of atoms is not expressible:
% sortedness is an invariant that cannot be checked on the type level.
Additionally, the recursive structure of expressions
means any expression $a$ can also be represented as $(a)^1*1 + 0$;
if the left argument to \pow is $0$ or $a * b + 0$, the expression is not in normal form.
Although these invariants can also be encoded in a more complicated \lean{ex} type,
they are instead maintained by careful programming.
A mistake in maintaining these invariants is not fatal: invariants only protect completeness, not soundness, of \ringexp.

Efficient handling of numerals in expressions, using the \lean{coeff} constructor, is required for acceptable running time without sacrificing completeness.
The tactic should not unfold expressions like $x * 1000$ as $1000$ additions of the variable $x$.
Representing numerals with the \lean{coeff} constructor requires an extra step to implement addition.
When terms overlap, differing only in the coefficients as for $a * b^2 * 1 + a * b^2 * 2$,
their sum is given by adding their coefficients: $a * b^2 * 3$.
Moreover, when the coefficients add up to $0$, the correct representation is not $a * b^2 * 0 : \lean{ex prod}$ but $0 : \lean{ex sum}$.
Coefficients must be treated similarly in exponents: $x ^ {a * b^2 * 1} * x ^ {a * b^2 * 2} %
% = x ^ {a * b^2 * 1 + a * b^2 * 2}
= x ^ {a * b^2 * 3}$.
Both cases are handled by a function \lean{add\_overlap} which returns the correct sum if there is overlap,
or indicates that there is no such overlap.
By choosing the order on expressions such that overlapping terms will appear adjacent in a sum,
\lean{add\_overlap} can be applied in one linear scan.

A subtle complication arises when normalising in the exponent of an expression \lean{a \pow b}:
the type of \lean{a} is an arbitrary commutative semiring, but \lean{b} must be a natural number.
To correctly compute a normalised expression for \lean{b},
the tactic needs to keep track of the type of \lean{b}.
The calculations of the \lean{eval} function are thus done in an extension of the \lean{tactic} monad%~\cite{lean-tactics}
, called the \lean{ring\_exp\_m} monad.
Using a reader monad transformer~\cite{monad-transformers},
\lean{ring\_exp\_m} stores the type of the current expression
as a variable which can be replaced locally when operating on exponents.

Implementing subtraction and division also requires more work,
since semirings in general do not have well-defined $-$ or $/$ operators.
The tactic uses typeclass inference to determine whether the required extra structure exists on the type.
When this is the case, the operators can be rewritten:
$a - b$ becomes $a + (-1) * b$ in a ring
and $a / b$ becomes $a * b^{-1}$ in a field.
Otherwise, the subtraction or division is treated as an atom.
Conditionally rewriting avoids the need for an almost-ring concept to treat semirings and rings uniformly~\cite{ring-tactic}.
Cancellation of multiplication and division, such as $a * b / a = b$, is not supported by the tactic,
since such lemmas require an $a \ne 0$ side condition, which is not supported by \ringexp.
In future work, extending the \lean{ex} type with a negation or multiplicative inverse constructor could allow for handling of these operators in more general cases.

%Expressions that \ringexp cannot fully parse can still be usefully normalised:
%$(\cos x + \sin x)^2$ can still be normalised to $\cos^2 x + \sin^2 x + 2 \cos x \sin x$,
%even though $\cos$ and $\sin$ are not (yet) operators supported by \ringexp.
%Any such unparseable subexpression is considered an \emph{atom} by the tactic,
%and each atom is manipulated like a variable in a polynomial.
For completeness, atoms should be considered up to definitional equality:
\lean{($\lambda$ x, x) a} and \lean{($\lambda$ x y, x) a b} reduce to the same value \lean{a},
so % for completeness
they should be treated as the same atom.
The \lean{ring\_exp\_m} monad contains a state monad transformer to keep track of which atoms are definitionally equal.
The state consists of a list of all distinct atoms encountered in the whole input expression,
and any comparisons between atoms are instead made by comparing their indices in the list.
As an additional benefit, the indices induce an order on atoms, which is used to sort arguments to commutative operators.
% whereas Lean's built-in order can vary between executions
Within atoms, there may be subexpressions that can be normalised as well.
%For example, the argument to $\cos$.
Instead of running the normaliser directly, \ringexp calls the built-in tactic \lean{simp} with the normaliser as an argument.
The \lean{simp} tactic calls a given normaliser on each subexpression,
rewriting it when the normaliser succeeds.

\section{Optimisations}

An important practical consideration in implementing \ringexp is its efficiency, especially running time.
Among the approximately 300 calls to \ring in \mathlib, about half are invocations on linear expressions by the tactic \lean{linarith}.
Since \ringexp is intended to work as a drop-in replacement for \lean{ring},
its performance characteristics, especially for linear expressions, should be comparable.

Optimising the code was a notable part of the implementation of \ringexp.
% guided by Lean's built-in profiler.
%Originally, the tactic used Lean's elaborator to fill in implicit arguments and typeclass instances when constructing terms.
%Profiling revealed that up to 90\% of running time could be spent in elaboration.
Profiling revealed that up to 90\% of running time could be spent on inferring implicit arguments and typeclass instances.
The solution was to pass all arguments explicitly and maintain a cache of typeclass instances,
also caching the expressions for the constants \lean{0} and \lean{1}.
It was possible to apply this solution without large changes to the codebase,
because the required extra fields were hidden behind the \lean{ring\_exp\_m} and \lean{ex\_info} types.

%Since the tactic works bottom up,
%constructing normal forms by applying each operator to the normal form of its operands,
%after each operation the sub-proofs can be discarded.
%Each \lean{ex} value carries its proof of normalisation,
%but when it does not appear as a subterm of the normal form, such as $a$ in $a * 0 = 0$,
%the normalisation proofs of $a$ is no longer needed and are deleted.
%Similarly, any proof that reduces to reflexivity is deleted.
%This results in smaller proof terms, reducing memory usage and type checking time.
%The final benefit is for debugging: the representation of \lean{ex} is simpler.

%Another test involved replacing all calls to \ring with \ringexp in the compilation of \mathlib.
%The compilation time in both cases was approximately the same:

The result of these optimisations can be quantified by comparing the running time of \ring and \ringexp on randomly generated expressions.%
\footnote{The benchmark program and analysis scripts are available at \url{https://github.com/lean-forward/ring_exp}.}
The performance measure is the tactic execution time reported by the Lean profiler,
running on a 3 GHz Intel\textregistered\xspace Core\texttrademark\xspace i5-8500 CPU with 16 GB of RAM.
On arbitrary expressions, the benchmark indicates that \ringexp is a factor of approximately $3.9$ times slower than \ring;
on linear expressions such as are passed by \lean{linarith},
\ringexp is $1.7$ times slower than \ring.

Compared to a constant factor difference in the average cases,
\ringexp has an advantage on problems requiring efficient handling of numeric exponents.
The \ringexp tactic is a factor 20 faster than \ring when showing $x^{50} * x^{50} = x^{100}$ in an arbitrary ring.
A similar speedup for \ringexp was found in practice, for the goal $(1 + x^2 + x^4 + x^6) * (1 + x) = 1 + x + x^2 + x^3 + x^4 + x^5 + x^6 + x^7$.
The Horner normal form used by \ring is optimal for representing expressions with additions and multiplications,
so a constant-factor slowdown compared to \ring on simpler goals is traded off for faster and more powerful handling of more complicated goals.

% The benchmark also serves as a correctness test for \ringexp, checking that arbitrary expressions are correctly handled.

%Apart from checking running time, these tests served to verify that \ringexp can parse arbitrary expressions.
% During development, \mathlib was compiled with all calls to \ring replaced with \ringexp.
% This ensured that \ringexp serves as a drop-in replacement for \ring.
% with ring: lean --make src/all.lean  3444.96s user 6.63s system 556% cpu 10:19.94 total
% 

%\begin{figure}
%\input{linexpr.tex}
%\caption{Running time of \ring and \ringexp on linear expressions.}
%\end{figure}
%\begin{figure}
%\input{expr-small.tex}
%\caption{Running time of \ring and \ringexp on arbitrary expressions.}
%\end{figure}

%\begin{figure}
%\centering
%\subfloat[Running time of \ring and \ringexp on linear expressions.]{\resizebox{0.3\textwidth}{!}{\input{linexpr.tex}}} \hspace{0.05\textwidth}
%\subfloat[Running time of \ring and \ringexp on arbitrary expressions.]{\resizebox{0.3\textwidth}{!}{\input{expr-large.tex}}} \hspace{0.05\textwidth}
%\subfloat[Running time of \ring and \ringexp on arbitrary expressions (detail).]{\resizebox{0.3\textwidth}{!}{\input{expr-small.tex}}}
%\end{figure}

\section{Discussion}

The \ring tactic for Coq and Lean can efficiently convert expressions in commutative semirings to normal form.
%HOL Light has the normalising procedure \texttt{SEMIRING\_NORMALIZERS\_CONV} for expressions in $+$ and $*$ (which also supports exponentiation with a constant exponent), analogous to \ring.
% This procedure powers \texttt{NUM\_NORMALIZE\_CONV} and \texttt{REAL\_POLY\_CONV}.
A normalizing procedure for polynomials is also included with the Agda standard library~\cite{agda-stdlib}, HOL Light~\cite{hol_light} and Isabelle/HOL~\cite{isabelle_hol},
and decision procedures exist that support exponential functions~\cite{resolution-rcf};
there is no single normalisation procedure supporting compound expressions in exponents.
% \cite{coq-assoc-comm} is acrefl for coq, \cite{coq-lattices} uses a decision procedure without normalisation.
% Term rewriting systems support compound exponents by adding the relevant equations,
% but typically lack support for numerals.

Compared with the \ring tactic, the \ringexp tactic can deal with a strict superset of expressions,
and can do so without sacrificing too much speed.
The extensible nature of the \ex type should make it simple to add support for more operators to \ringexp.
% including those not arising from algebra, such as casts~\cite{norm-cast}.
Independently, it should be possible to adapt the \ex type to other algebraic structures
such as lattices or vector spaces.
Although more optimisations are needed to fully equal \ring in average case efficiency,
the \ringexp tactic already achieves its goal of being a useful, more general normalisation tactic.
These results are as much a consequence of engineering effort as of theoretical work.

%An interesting question is whether it is possible to automatically derive an appropriate \ex type
%and its operations, given a set of distributivity, associativity and commutativity relations.

\paragraph{Acknowledgements}
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!

\printbibliography
\end{document}