% $Id: hrefl-ii.tex,v 1.24 2004/07/05 09:28:06 lcf Exp $
\documentclass{article}
\usepackage{amssymb,url}
\usepackage[all]{xy}
\usepackage{a4wide}

\usepackage{theorem}
\usepackage{enumerate}

\theoremheaderfont{\scshape} \theorembodyfont{\upshape}
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{corollary}[definition]{Corollary}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{example}[definition]{Example}
\newtheorem{notation}[definition]{Notation}
\newenvironment{proof}{\smallskip\textsc{Proof.}}{\hspace*{\fill}$\Box$}

%\newcommand{\inte}[1]{[\![#1]\!]}
%\newcommand{\pidx}{_{\!\not\,1}}
%\newcommand{\intfun}[1]{\inte{#1}_\rho}
\newcommand{\intII}{\,]\![}
\newcommand{\intrel}{\mathbin{\intII_{\rho}}}
%\newcommand{\intrelG}{\mathbin{\intII_\rho^G}}
%\newcommand{\intrelF}{\mathbin{\intII_\rho^F}}
%\newcommand{\intrelR}{\mathbin{\intII_\rho^R}}
%\newcommand{\intrelS}{\mathbin{\intII_\rho^S}}
%\newcommand{\intrelX}[1]{\mathbin{\intII_\rho^{#1}}}
%\newcommand{\crr}[1]{\hat{#1}}
%\newcommand{\intreltwo}{\mathbin{\intII_{\rho_0,\rho_1}}}
%\newcommand{\intrelfour}{\mathbin{\intII_{\rho_0,\rho_1,\rho\pidx,\rho_2}}}
%\newcommand{\Ltac}{${\cal L}_{\rm tac}$}
\newcommand{\N}{{\cal N}}
\newcommand{\NF}{\ensuremath{{\cal N}_{F}}}
%\newcommand{\eqbdi}{=}
%\newcommand{\wfrho}{{\it wf\!}_\rho}
\newcommand{\Prop}{{\textsf{Prop}}}
\newcommand{\alt}{\mathrel{|}}
\newcommand{\Z}{{\mathbb Z}}
\newcommand{\V}{{\mathbb V}}
\newcommand{\tacticname}[1]{\textsf{#1}}
\newcommand{\rational}{\tacticname{rational}}

\newcommand{\zring}{\ensuremath{\mathrm{zring}}}
\newcommand{\nexp}{\ensuremath{\mathrm{nexp}}}
\newcommand{\less}{\mathrel{\prec_A}}
\newcommand{\nat}{{\mathbb N}}
\newcommand{\axiom}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\liftv}[1]{\ensuremath{\mathit{lift}_{\V_{#1}}}}
\newcommand{\lift}{\ensuremath{\mathit{lift}}}
\newcommand{\dom}{\ensuremath{\mathrm{dom}}}
\newcommand{\ord}{\ensuremath{\mathrm{ord}}}
\newcommand{\wf}{\ensuremath{\mathrm{wf}}}
\newcommand{\nf}{\ensuremath{\mathrm{nf}}}
\newcommand{\intrels}{\mathbin{\intII_{\sigma}}}
\newcommand{\intrelt}{\mathbin{\intII_{\theta}}}

\newcommand{\renamevar}[2]{\ensuremath{{#1}^{#2}}}
\newcommand{\isrenamevar}[3]{\ensuremath{{#1}=\renamevar{#2}{#3}}}
\newcommand{\idn}{()}
\newcommand{\coeff}[2]{\ensuremath{\|#2\|_{#1}}}
\newcommand{\iter}[2]{\ensuremath{{#1}\cdot{#2}}}

\newcommand{\multMZ}{\ensuremath{\cdot_{\mathrm M\Z}}}
\newcommand{\multMV}{\ensuremath{\cdot_{\mathrm M\V}}}
\newcommand{\multMM}{\ensuremath{\cdot_{\mathrm{MM}}}}
\newcommand{\plusMM}{\ensuremath{+_{\mathrm{MM}}}}
\newcommand{\plusPM}{\ensuremath{+_{\mathrm{PM}}}}
\newcommand{\plusPP}{\ensuremath{+_{\mathrm{PP}}}}
\newcommand{\multPM}{\ensuremath{\cdot_{\mathrm{PM}}}}
\newcommand{\multPP}{\ensuremath{\cdot_{\mathrm{PP}}}}
\newcommand{\starPP}{\ensuremath{\star_{\mathrm{PP}}}}
\newcommand{\plusFF}{\ensuremath{+_{\mathrm{FF}}}}
\newcommand{\multFF}{\ensuremath{\cdot_{\mathrm{FF}}}}
\newcommand{\divFF}{\ensuremath{/_{\mathrm{FF}}}}

\begin{document}

\title{\Large Equational Reasoning in Algebraic Structures: a Complete Tactic}
\author{Lu\'\i s Cruz-Filipe$^{1,2}$ and Freek Wiedijk$^1$}
\date{$^1$NIII, University of Nijmegen, Netherlands and $^2$CLC, Lisbon, Portugal}
\maketitle

\begin{abstract}
We present {\rational}, a Coq tactic for equational reasoning
in abelian groups, commutative rings, and fields.
We give an mathematical description of the method that
this tactic uses, which abstracts from Coq specifics.

We prove that the method that {\rational} uses is correct,
and that it is complete for groups and rings.
Completeness means that the method succeeds in
proving an equality if and only if that equality is provable from
the the group/ring axioms.
Finally we characterize in what way our method is incomplete for
fields.
\end{abstract}

\tableofcontents

%\section{Plan}
%
%Introduce the semantical level (fields) and the syntactical level
%(expressions).  Substitutions and interpretation, extensionality and
%replacement.  Lift function; correctness of lifting.  Normal forms,
%normalization function, correctness of $\N$ for rings.  Discussion:
%correctness of $\N$ for groups and fields.  Presentation of the
%tactic.  Completeness for rings.  Discussion: completeness for groups
%and incompleteness for fields.  Complete variant for fields without axiom
%\axiom{Set_4}.  Generalization to include full \axiom{Set_5} and
%partial functions.


\section{Introduction}

%\subsection{Problem}

One of the main aims of the Foundations group at the University of
Nijmegen is to help making formalization of mathematics practical and
attractive.
For this reason a library of formal mathematics for the Coq
system~\cite{coqmanual} -- called the C-CoRN
library~\cite{lcf:geu:wie:04} -- has been developed to exercise the
technology of proof formalization.
This library started as a formalization of the Fundamental Theorem of
Algebra in the so-called FTA project, but then was extended with a
formalization of basic analysis up to the Fundamental Theorem of
Calculus, and currently other subjects are being added to it as well.

To support the formalization work for the C-CoRN library,
a tactic called {\rational} was implemented.
It automatically proves equations from the field axioms.
Later this tactic was generalized to prove equations in
rings and groups as well.
The tactic uses the approach of \emph{reflection} from~\cite{ACHA90},
in particular the variant of reflection called \emph{partial reflection}
described in~\cite{geu:wie:zwa:00}.
The generalization to rings and groups uses the application
of partial reflection called \emph{hierarchical reflection} in~\cite{lcf:wie:04}.

The tactic has two parts: the first part is a Coq formalization of
normalization of polynomial expressions over a field, and the second
part is an ML program that constructs a proof term for a given
equation.
This means that the tactic contains two -- quite different --
programs.  On the one hand there is the program that computes the
normal form of a polynomial expression.
This program is written in the Coq type theory, and is proved correct
as part of the Coq formalization.
On the other hand there is the program that calculates a proof term
from an equation, which is written in ML.

The correctness of the {\rational} tactic is guaranteed by the way
that it works: if it finds a proof of an equation, then that proof is
automatically checked by Coq.
Failure, however, can arise from two different
situations:
\begin{enumerate}[(1)]
\item the ML program cannot find a term that corresponds to the problem.
\item the ML program returns a term that does not have the expected behavior.
\end{enumerate}
In turn, the second situation can arise in two cases:
\begin{enumerate}[(2a)]
\item although the original terms are provably equal, the normalization
procedure cannot determine that;
\item the original terms are in fact not provably equal.
\end{enumerate}
This paper studies the behavior of {\rational} from a theoretical
point of view.
\begin{itemize}
\item
It gives a mathematical description of the algorithm implicit in the
ML part of the {\rational} tactic, and proves that this algorithm is
correct.
\item
It describes under what conditions the tactic is complete.

Now completeness can mean two things here:
either one can consider the set of equations that hold in all fields,
or one can consider the equations that can be proved from the field axioms.
It happens to be the case that both sets of equations are the same \cite{cha:key:90}.

%We show that {\rational} is complete if we restrain our attention to groups
%or rings, but when we look at fields we have to drop one of the axioms.

\end{itemize}

The first point means that situation (1) cannot occur.  In the second
point, we establish completeness for groups and rings, excluding also
situation (2a).  Unfortunately this result only extends partially to
fields, but we can still give a simple condition which, if fulfilled,
also excludes this situation.

As a consequence, when a call to {\rational} fails no proof of the goal
exists that follows exclusively from the structure's axioms.  This is
extremely useful in interactive proof development, since it enables the
user to detect wrong paths much earlier.

\bigskip

The mathematics in this paper has not been formalized.
Formalizing takes an order of a magnitude more work than just doing
the proofs in the informal -- old style -- way, and it is not clear
what the benefit of formalization would be in this case (apart from
the fact that one then would be \emph{certain} that the proofs are
correct).

The description in this paper of the {\rational} tactic
is kept as independent of Coq as possible.
The algorithms and results that we describe
are not specific to Coq or even to type theory,
they can be used with any proof assistant.

This paper is self-contained in the sense that everything that
is used is defined as well.
However, it does not go into detail about partial/hierarchical reflection
or the details of the {\rational} tactic.
For this we refer to two earlier papers,~\cite{geu:wie:zwa:00}
and~\cite{lcf:wie:04}.

We begin by describing the mechanism of {\rational} in more detail.
Then we discuss the several layers of expressions we need to study
this mechanism.

Section~\ref{lifting} formally describes the ML part of the tactic and
proves a number of results about it, among which the correctness of the
code.
In Section~\ref{normalization} we introduce the normalization function for
rings and prove its completeness.  This proof generalizes almost directly
to groups, as explained in Section~\ref{groups}.  Finally,
Section~\ref{fields} analyzes the more complex case of fields, focusing
on why the previous proof cannot be adapted to this situation, and presents
an alternative completeness result.

The tactic described here is a simplified version of that
in~\cite{lcf:wie:04}, and in Section~\ref{extensions} we explain how the
same theorems can be generalized to the implemented tactic.  We conclude
with an overview of what was achieved in Section~\ref{concl}.

\subsection{Related work}

Most proof assistants have automation tools that provide the functionality
of {\rational} for rings, and many also have them for fields
(for instance, the standard library of Coq provides both these
functionalities with the
\tacticname{ring} and \tacticname{field} tactics, see~\cite{coqmanual}).
This automation is always implemented (like {\rational} is)
by putting polynomials into a normal form.

The main difference between our approach and these other implementations
of the same idea is that we do the normalization in a very structured
and systematic way.
We define addition and multiplication functions
that are meant to operate on monomials and polynomials that are already
in normal form.
These functions are then the `building blocks' of our normalization
function.
This enables us to easily prove the correctness of the normalization
function, which we need to use the reflection method.

\section{Background}

In this section we lay the bricks for the work we propose to do.  We begin
by describing the way {\rational} works in detail, after which we
summarize the parts of~\cite{geu:pol:wie:zwa:02}, \cite{geu:wie:zwa:00}
and~\cite{lcf:wie:04} that are essential for the remainder of the paper.

\subsection{The mechanism of {\rational}}\label{tactic}

The {\rational} tactic proves equalities in an algebraic
structure $A$ through the use of a type of \emph{syntactic expressions} $E$
together with an \emph{interpretation relation}.
$$\intrel \subseteq E \times A$$
In this, $\rho$ is a \emph{valuation} that maps the variables in the
syntactic expressions to values in $A$.
The relation $e \intrel a$ means that the syntactic expression
$e$ is interpreted under the valuation $\rho$ by the object $a$.

The type $E$ is an inductive type, and therefore it is possible to recursively
define a \emph{normalization function} $\N$ on the type of syntactic
expressions:
$$\N : E \to E$$
One can prove the following two lemmas
$$
\begin{array}{c}
e \intrel a \;\Rightarrow\; \N(e) \intrel a \\
\noalign{\medskip}
e \intrel a \;\land\; e \intrel b \;\Rightarrow\; a =_A b
\end{array}
$$
and together these lemmas give a method to prove equalities between terms
that denote elements of $A$.

For instance, suppose that one wants to prove $a =_A b$.
One finds $e$, $f$ and $\rho$ with $e \intrel a$ and $f \intrel b$,
and one checks whether $\N(e) = \N(f)$.
If this is the case then it follows that $a =_A b$.

For from the first lemma we find that $\N(e) \intrel a$ and $\N(f) \intrel b$,
and then the second lemma gives this desired equality.


\subsection{Object level and meta-level}\label{levels}

To describe the behavior of {\rational} we need to look at terms of
several kinds.
This section explains these different kinds of terms in turn,
so that the remainder of the paper can be easily understood.

Throughout this paper we deal with algebraic structures (groups, rings
and fields).
And, as we are working with formal systems, we also have
\emph{terms} that are interpreted in these algebraic structures.
To complicate things, we use the method of \emph{reflection}
which means that the notion of `term' both occurs on
the meta-level as well as on the object level.
In this section we will clarify this.
We will identify various instances of `number zero' as an example to explain
the situation.

Let us start with the \emph{object level}.
We have three kinds of objects that have a `zero'.
\begin{itemize}
\item
\emph{The natural numbers and the integers.}
First of all, we have the natural numbers $\nat$.
In the natural numbers there is a unique object which is the natural number
zero.

The equality that one uses for the natural numbers
is \emph{Leibniz equality}.
This means that the zero of the natural numbers does not have
different representations:
there is only one zero.

The integers are like the natural numbers:
there is exactly one integer zero, and one uses Leibniz equality
to compare integers.

\item
\emph{The elements of the algebraic structures.}
Each group, ring, or field $A$ has a zero as well.
However, as we use \emph{setoids} for these algebraic structures
(so we can model quotients
in a constructively valid way),
an algebraic structure can have more than one object
that \emph{represents} the zero of that structure.
In other words, for an algebraic structure we use \emph{setoid
equality} instead of Leibniz equality.

For instance, suppose we construct the real numbers as Cauchy
sequences of rational numbers.
Then \emph{every} Cauchy sequence that converges to zero represents the
zero of these `Cauchy reals'.
These sequences are then all `setoid equal' to each other, but can
be distinguished using Leibniz equality.

\item
\emph{Field expressions.}
Finally we have the set $E$ of terms generated by the
field operations: $+$, $-$, $\times$ and $/$.
This is an inductively generated set of syntactic objects.
In this set there is a unique term for `zero'.
For these `field expressions' we also use Leibniz equality.

Note that although these objects that we call field expressions
are terms, they exist
on the object level (as a set of mathematical objects, like
the natural numbers)
and not on the meta-level (as linguistic constructions).

\end{itemize}

\noindent
We also have the \emph{meta-level}.
In the formal language that we use to talk about all these objects,
we have terms denoting these objects.
This means there is still another kind of zero:
\begin{itemize}
\item
\emph{Terms on the meta-level.}
For the integers there is a constant in the language that
denotes the integer zero.
This symbol is a linguistic construction that differs from
the integer zero itself, in that it exists on the meta-level
instead of at the object level.

Similarly, there is a function in the language that maps each
algebraic structure to a zero element
of that structure.
Again, the symbol for this function is different from those zero elements itself,
in that it exists on the meta-level.
Note that this function denotes one specific zero of the structure
among all the elements that are setoid equal to it.

Finally, in the case of the field expressions, the basic terms denoting them
on the meta-level are very similar to the objects themselves.
Still one should distinguish the two.

\end{itemize}

\noindent
On the terms of the language there are two notions of equality.
There is \emph{syntactic identity}, and
there is \emph{$\beta\delta\iota$-equality} or \emph{convertibility}.
(These equalities are used to talk about the language, and cannot
be expressed in the language itself.)

Consider the function `$\zring$' that maps the integers into a given ring.
Then if one applies this function to the integer zero, one gets 
a term that is syntactically different from the term that denotes the zero of
the ring.
However it is convertible to this term, by $\beta\delta\iota$-reduction
($\delta$-reduction means unfolding the definition of a function, and
$\iota$-reduction means unfolding of a recursive definition.)

We will almost everywhere use syntactic identity in this paper.
The only conversion that we will refer to is $\beta\delta\iota$-reduction of a few
basic functions: subtraction, the $\zring$ function and exponentiation
with a constant natural number.
Of all other functions the definition will never be unfolded.

\medskip
\noindent
We also have two kinds of `terms', which are quite different.
There are the `field expressions' on the object level, and there are
the terms denoting elements of a field on the meta-level.
In both cases one builds these terms with the field operations:
$+$, $-$, $\times$ and $/$.
However they exist on different levels (the method of mimicking part of the meta-level on the
object level is called \emph{reflection}).
Also, the field expressions are very trivial:
they can \emph{only} involve variables and the field operations.
But the meta-level terms can involve any type of sub-term, as long as
the full term denotes an element of the field.
For instance in the field of real numbers $\sqrt{\zring(2)}$ is an acceptable
meta-level term,
but there is nothing like a square root in field expressions.

The distinction between these two different kinds of terms
can be illustrated with two relations that are defined in this
paper.
The relation $<_E$ is defined on the field expressions in Definition \ref{defn:exprorder}.
The relation $\less$ is defined on meta-level terms denoting
elements of the field $A$ in Definition \ref{defn:less}.
Note that this second relation does not respect convertibility:
${1_A}^0$ (`one to the power zero') is convertible with $1_A$, but $1_A \less {1_A}^0$ while $1_A \not\less 1_A$.

\medskip
\noindent
To summarize, we have three quite different kinds of objects that have a zero
(integers, elements in an algebraic structure, and field expressions),
and we should distinguish between these objects on the object level
and terms denoting them on the meta-level.

Also we have four kinds of equality:
between the objects on the object level we have
\emph{Leibniz equality} and \emph{setoid equality} (and we
can write those equalities in our language), while
between the terms on the meta-level we have
\emph{syntactic identity} and
\emph{$\beta\delta\iota$-equality}
(and those two relations are not in the language).


\subsection{The semantic level}\label{structures}

We now summarize the Algebraic Hierarchy of C-CoRN~\cite{geu:pol:wie:zwa:02},
on top of which {\rational} works.

\begin{definition}
A \emph{setoid structure} over $A$ is a relation
$=_A:A\to A\to\Prop$ (denoted infix) satisfying:
\begin{eqnarray*}
\axiom{Set_1} & : & \forall_{x:A}.x=_A x \\
\axiom{Set_2} & : & \forall_{x,y:A}.x=_A y\to y=_A x\\
\axiom{Set_3} & : & \forall_{x,y,z:A}.x=_A y\to y=_A z\to x=_A z\\
\end{eqnarray*}
Furthermore, we distinguish subtypes $[A\to A]$ and $[A\to A\to A]$ of
$A\to A$ and $A\to A\to A$, respectively, satisfying
\begin{eqnarray*}
\axiom{Set_4} & : &
 \forall_{f:[A\to A]}.\forall_{x,x':A}.x=_A x'\to f(x)=_A f(x')\\
\axiom{Set_5} & : & \forall_{f:[A\to A\to A]}.
 \forall_{x,x',y,y':A}.x=_A x'\to y=_A y'\to f(x,y)=_A f(x',y')
\end{eqnarray*}
We will speak of a setoid $A$ to mean a type $A$ with a setoid structure over
$A$.
\end{definition}

\begin{definition}
A \emph{group structure} over $A$ is a setoid structure over $A$ together
with a tuple $\langle 0_A,+_A,-_A\rangle$ where $0_A:A$, $+_A:[A\to
A\to A]$ and $-_A:[A\to A]$ (we will write $+_A$ using the usual infix
notation) satisfying:
\begin{eqnarray*}
\axiom{SG} & : & \forall_{x,y,z:A}.(x+_A y)+_A z=_A x+_A(y+_A z) \\
\axiom{M_1} & : & \forall_{x:A}.x+_A 0=_A x\\
\axiom{M_2} & : & \forall_{x:A}.0+_A x=_A x\\
\axiom{G_1} & : & \forall_{x:A}.x+_A (-_A x)=_A 0\\
\axiom{G_2} & : & \forall_{x:A}.(-_A x)+_A x=_A 0\\
\axiom{AG} & : & \forall_{x,y:A}.x+_A y=_A y+_A x
\end{eqnarray*}
Notice that axiom \axiom{M_2} (respectively \axiom{G_2}) can be proved
from \axiom{M_1} (resp.\ \axiom{G_1}) and \axiom{AG}.  But in the construction
of the Algebraic Hierarchy \axiom{AG} is introduced last.

By a group $A$ we mean a type $A$ with a group structure over it.
\end{definition}

\begin{definition} Let $A$ be a group.  We define $-_A:A\to A\to A$ by
\[x-_A y:= x+_A(-_A y).\]
\end{definition}

The following is trivial, and allows us to write $-_A:[A\to A\to A]$.

\begin{proposition} $-_A$ satisfies \axiom{Set_5}.
\end{proposition}

\begin{definition}
A \emph{ring structure} over $A$ is a group structure over $A$ together with
a tuple $\langle 1_A,\times_A\rangle$ where $1_A:A$, $\times_A:[A\to
A\to A]$ (we will write $\times_A$ using the usual infix notation)
satisfying the following.
\begin{eqnarray*}
\axiom{R_1} & : & \forall_{x,y,z:A}.
 (x\times_A y)\times_A z=_A x\times_A(y\times_A z) \\
\axiom{R_2} & : & \forall_{x:A}.x\times_A 1=_A x\\
\axiom{R_3} & : & \forall_{x:A}.1\times_A x=_A x\\
\axiom{R_4} & : & \forall_{x,y:A}.x\times_A y=_A y\times_A x\\
\axiom{R_5} & : & \forall_{x,y,z:A}.
 x\times_A(y+_A z)=_A(x\times_A y)+_A(x\times_A z)
\end{eqnarray*}
As before, axiom \axiom{R_3} can be proved from \axiom{R_2} and
\axiom{R_4}.

By a ring $A$ we mean a type $A$ with a ring structure over it.
\end{definition}

\begin{definition} Let $A$ be a ring.  We define two functions
$\zring_A:\Z\to A$ and $\nexp_A:A\to\nat\to A$ inductively as follows:
\begin{eqnarray}
\label{zring:0}
 \zring_A(0) & := & 0_A\\
\label{zring:pos}
 \zring_A(n+1) & := & \zring_A(n)+_A 1_A,\mbox{ for $n\geq 0$}\\
\label{zring:neg}
 \zring_A(n-1) & := & \zring_A(n)-_A 1_A,\mbox{ for $n\leq 0$}
\end{eqnarray}
\begin{eqnarray}
\label{nexp:zero}
 \nexp_A(x,0) & := & 1_A\\
\label{nexp:suc}
 \nexp_A(x,n+1) & := & x\times_A\nexp_A(x,n)
\end{eqnarray}
We denote $\zring_A(n)$ by $\underline n_A$ and $\nexp_A(x,n)$ by $x^n$.
\end{definition}

The following is again trivial to prove.
\begin{proposition} For every $n$, the function $\cdot^n:A\to A$ satisfies
\axiom{Set_4}.
\end{proposition}

Based on this result, we will often see $x^n$ as the application of
$\cdot^n:[A\to A]$ to $x$.

\begin{definition}
A \emph{field structure} over $A$ is a ring structure over $A$ together with
an operation $\cdot^{-1}:\Pi_{x:A}.x\neq 0\to A$ (we denote
$(\cdot^{-1}\ x\ H)$ simply by $x^{-1}$, leaving the proof term implicit)
satisfying
\[\axiom{F} : x\neq 0 \to x\times_A x^{-1}=_A 1_A.\]
By a field $A$ we mean a type $A$ with a field structure over it.
\end{definition}

\begin{definition} Let $A$ be a field.  We define
$/_A:A\to\Pi_{y:A}.y\neq 0\to A$ by \[x/_A y:= x\times_A(y^{-1}).\]
\end{definition}

The following is trivial:

\begin{proposition} $/_A$ satisfies \axiom{Set_5'}:
\begin{eqnarray*}
\axiom{Set_5'} & : & \forall_{x,x',y,y':A}.
 y\neq 0\to y'\neq 0\to x=_A x'\to y=_A y'\to x/_A y=_A x'/_A y'
\end{eqnarray*}
\end{proposition}
We will sometimes abuse notation and refer to \axiom{Set_5'} as an
instance of \axiom{Set_5}, and refer to $/_A$ as an operation of type
$[A\to A\to A]$.

\begin{definition}\label{defn:proof} A \emph{proof} of $t_1=_A t_2$ from
the field axioms in an environment $\Gamma$ is a sequence
$\varphi_1,\ldots,\varphi_n$ of equalities such that $\varphi_n$ is
$t_1=_A t_2$ and, for $i=1,\ldots,n$, one of the following holds.
\begin{enumerate}[--]
\item $\varphi_i$ is an instance of one of the axioms \axiom{Set_1},
\axiom{SG}, \axiom{M_1}, \axiom{M_2}, \axiom{G_1}, \axiom{G_2},
\axiom{AG} or \axiom{R_1}--\axiom{R_5}.
\item $\varphi_i$ is an instance of axiom \axiom{F} and the hypothesis
of this axiom is in $\Gamma$.
\item $\varphi_i$ is an instance of one of the axioms
\axiom{Set_2}--\axiom{Set_5} and the hypothesis(es) of the axiom are
included in $\{\varphi_1,\ldots,\varphi_{i-1}\}$.
\end{enumerate}
\end{definition}

We will often not mention $\Gamma$ explicitly, but assume that all the
proofs are done in an environment containing all the necessary inequalities.
The reason for this (and for choosing the term ``environment'' rather than
``context'') is that {\rational} only looks at the equality being proved
and assumes all needed inequalities hold anyway.

\begin{definition}\label{defn:less} Let $A$ be a type.  We define the relation
$\less$ on the terms of type $A$ as the least relation satisfying:
\begin{enumerate}
\item $t\less f(t)$ for $f:[A\to A]$ (in particular, in a group one has
$t\less -_A t$ and in a ring $t\less t^n$ for $n:\nat$);
\item $t_i\less f(t_1,t_2)$ for $f:[A\to A\to A]$ and $i=1,2$ (in
particular, $f$ can be one of $+_A$, $-_A$ or $\times_A$ in a group or
ring);
\item if $A$ is a field, then $t_i\less t_1/_A t_2$ for $i=1,2$.
%\item $\less$ is transitive.
%\item $\less$ is a congruence.
\end{enumerate}
(Notice the implicit requirement $t_2\neq 0$ in the clause
$t_i\less t_1/_A t_2$.)
\end{definition}

\begin{proposition}\label{lesswff}
$\less$ is a well founded relation.
\end{proposition}
\begin{proof}
By definition, if $t_1\less t_2$ then $t_1$ is a subterm of $t_2$; since
``being a subterm of'' is a well founded relation, so is $\less$.
\end{proof}

\begin{notation} From now on, we will omit the subscript $A$ in the
symbols denoting the algebraic operations, since no ambiguity is introduced.
However, we will write $=_A$ to emphasize the distinction between this
defined equality and the one induced by $\beta\delta\iota$-reduction on
the set of lambda terms of type $A$.
\end{notation}

\subsection{The syntactic level}\label{expressions}

We now introduce the syntactic counterpart to the type of fields, which
is the type of expressions that {\rational} works with.

\begin{definition}\label{defn:expressions}
The syntactic type $E$ of expressions is the inductive type generated by the
following grammar:
\[E ::= \Z \alt \V_0 \alt \V_1(E) \alt E+E \alt E\times E \alt E/E\]
where $\V_i=\{v^i_j|j\in\nat\}$ for $i=0,1$.
\end{definition}

\begin{definition}\label{expr:abbr}
We define the following \emph{abbreviations} on expressions:
\begin{eqnarray}
\label{expr:inv} -e & := & e\times(-1)\\
\label{expr:minus} e_1-e_2 & := & e_1+(-e_2)\\
\label{expr:exp:zero} e^0 & := & 1\\
\label{expr:exp:suc} e^{n+1} & := & e\times e^n
\end{eqnarray}
Notice that these abbreviations are done only on the meta-level; when
we write e.g.\ $e_1-e_2$ we are speaking about the expression
$e_1+(e_2\times(-1))$.
\end{definition}

At some stage we will need an order on $E$.

\begin{definition}\label{defn:exprorder}
The \emph{order} on $E$ is defined as follows, where $\star$ stands for $+$,
$\times$ or $/$.
\begin{enumerate}[(i)]
\item $v^0_i<_E v^0_j$ if $i<j$;
\item $v^0_i<_E e$ whenever $e$ is $i:\Z$, $e_1\star e_2$ or $v^1_i(e')$;
\item $i<_E j$ if $i<j$ ($i,j:\Z$);
\item $i<_E e$ whenever $e$ is $e_1\star e_2$ or $v^1_i(e')$;
\item $e_1\star e_2<_E e'_1\star e'_2$ whenever $e_1<_E e'_1$ or $e_1=e'_1$ and
$e_2<_E e'_2$ (lexicographic ordering);
\item $e_1+e_2<_E e$ whenever $e$ is $e'_1\times e'_2$, $e'_1/e'_2$
or $v^1_i(e')$;
\item $e_1\times e_2<_E e$ whenever $e$ is $e'_1/e'_2$ or $v^1_i(e')$;
\item $e_1/e_2<_E e$ whenever $e$ is $v^1_i(e')$;
\item $v^1_i(e_1)<_E v^1_j(e_2)$ whenever $i<j$ or $i=j$ and $e_1<_E e_2$.
\end{enumerate}
In other words, expressions are recursively sorted by first looking at
their outermost operator $$x <_E i <_E e+f <_E e\times f <_E e/f <_E
v(e)$$ and then sorting expressions with the same operator using a
lexicographic ordering.
For example, if $x<_{\V_0}y$ and $u<_{\V_1}v$, then
$$x<_E y<_E 2<_E 34<_E x/4<_E u(x+3)<_E u(2\times y)<_E v(x+3).$$
\end{definition}

\subsection{The interpretation relation}\label{interpretation}

The correspondence between the syntactic and the semantic levels is
made via an interpretation relation, described in detail
in~\cite{geu:wie:zwa:00} and~\cite{lcf:wie:04}.
It is this relation that allows us to speak of correctness and completeness
of {\rational}, which is what we want to do.

\subsubsection*{Substitutions}

The definition of $E$ includes families of variables so that we can
speak about arbitrary expressions in a field, and not only about those
that only mention the field operations.
Therefore, the interpretation of an expression is dependent on an assignment
of values to the variables, which we will call a substitution.

\begin{definition} A \emph{substitution} from a type of variables $\V$
to a type $T$ is a finite (partial) function from $\V$ to $T$.
\end{definition}

\begin{notation}
The domain of a substitution $\rho$ will be denoted by $\dom(\rho)$ or
simply by $\dom\rho$.

We will use the usual notation $[v:=t]$ for the substitution that
replaces $v$ with $t$.
\end{notation}

The following definitions and results are standard from the theory of
finite functions.

\begin{definition} Let $\rho,\sigma$ be substitutions from $\V$ to $T$.
If $\rho$ and $\sigma$ coincide on the intersection of their domains
(in particular, if their domains are disjoint), we define the
\emph{union} $\rho\cup\sigma$ to be the only substitution $\theta$
with domain $\dom\rho\cup\dom\sigma$ such that $\theta(v)=\rho(v)$,
for $v\in\dom\rho$, and $\theta(v)=\sigma(v)$ for $v\in\dom\sigma$.
\end{definition}

\begin{definition}\label{subst:incl} Let $\rho,\sigma$ be substitutions
from $\V$ to $T$.  We say that $\rho$ \emph{is contained} in $\sigma$, denoted
by $\rho\subseteq\sigma$, if there is a substitution $\theta$ from $\V$
to $T$ such that $\sigma=\rho\cup\theta$.
\end{definition}

\begin{proposition}\label{subst:incl:props}
For all $\V$ and $T$, $\subseteq$ is a partial order on the set of
substitutions from $\V$ to $T$.
\end{proposition}
\begin{proof} Trivial.
\end{proof}

\begin{proposition}\label{subst:incl:wdef}
Let $\rho,\sigma$ be substitutions from $\V$ to $T$ such that
$\rho\subseteq\sigma$.  Then $\sigma(v)=\rho(v)$ for every
$v\in\dom\rho$.
\end{proposition}
\begin{proof} By definition of $\subseteq$, there is a substitution $\theta$
such that $\sigma=\rho\cup\theta$; by definition of $\cup$, since
$v\in\dom\rho$, $\sigma(v)=(\rho\cup\theta)(v)=\rho(v)$.
\end{proof}

\begin{definition} A substitution $\rho$ is \emph{injective} if, for any
two distinct variables $x$ and $y$ in $\V$, the terms $\rho(x)$
and $\rho(y)$ are syntactically distinct.
\end{definition}

\bigskip From now on, we assume a fixed field $A$.

\begin{definition}\label{substpair} A \emph{substitution pair over $A$}
is a pair $\rho=\langle\rho_0,\rho_1\rangle$ where $\rho_0$ and
$\rho_1$ are injective substitutions from, respectively, $\V_0$ to $A$
and $\V_1$ to $[A\to A]$.
\end{definition}

The results about substitutions generalize in the obvious way to
substitution pairs.

\begin{definition}\label{substpair:incl}
Let $\rho$ be a substitution pair over $A$.  We say that $\rho$
\emph{is contained} in $\sigma$, denoted by $\rho\subseteq\sigma$, if
$\rho_i\subseteq\sigma_i$ for $i=0,1$.
\end{definition}

\begin{proposition}\label{substpair:incl:props}
$\subseteq$ is a reflexive and transitive relation on the set of substitution
pairs over $A$.
\end{proposition}

\begin{proposition}\label{substpair:incl:wdef}
Let $\rho,\sigma$ be substitution pairs over $A$ such that
$\rho\subseteq\sigma$.  Then $\sigma_i(v^i_k)=\rho_i(v^i_k)$ for $i=0,1$
and $v^i_k\in\dom\rho_i$.
\end{proposition}

\subsubsection*{Interpretation of expressions}

\begin{definition}\label{defn:intrel}
Let $\rho$ be a substitution pair over $A$.  The \emph{interpretation
relation} $\intrel\subseteq E\times A$ is defined inductively by:
\begin{eqnarray}
\label{intrel:var0}
\rho_0(v^0_i)=_A t & \rightarrow & v^0_i\intrel t\\
\label{intrel:int}
\underline k=_A t & \rightarrow & k\intrel t\\
\label{intrel:plus}
 e_1\intrel t_1 \wedge e_2\intrel t_2 \wedge t_1+t_2=_A t
& \rightarrow & e_1+e_2\intrel t\\
\label{intrel:mult}
 e_1\intrel t_1 \wedge e_2\intrel t_2 \wedge t_1\times t_2=_A t
& \rightarrow & e_1\times e_2\intrel t\\
\label{intrel:div}
 e_1\intrel t_1 \wedge e_2\intrel t_2 \wedge t_2\neq 0 \wedge t_1/t_2=_A t
& \rightarrow & e_1/e_2\intrel t\\
\label{intrel:var1}
 e\intrel t_1 \wedge \rho_1(v^1_i)(t_1)=_A t & \rightarrow & v^1_i(e)\intrel t
\end{eqnarray}
Notice that by omitting~(\ref{intrel:div}) we obtain an interpretation relation
over rings; omitting also~(\ref{intrel:mult}) and~(\ref{intrel:int}) for
$k\neq 0$ we obtain an interpretation relation over groups.
\end{definition}

\begin{lemma}\label{intrel:abbr} The abbreviated expressions
(Definition~\ref{expr:abbr}) satisfy the following relations.
\begin{eqnarray}
\label{intrel:inv}
e\intrel t_1 \wedge -t_1=_A t & \rightarrow & -e\intrel t\\
\label{intrel:minus}
e_1\intrel t_1 \wedge e_2\intrel t_2 \wedge t_1-t_2=_A t
 & \rightarrow & e_1-e_2\intrel t\\
\label{intrel:nexp}
e\intrel t_1 \wedge t_1^n=_A t & \rightarrow & e^n\intrel t
\end{eqnarray}
\end{lemma}
\begin{proof}
\begin{enumerate}[(1)]%
\setcounter{enumi}{\ref{intrel:inv}}\addtocounter{enumi}{-1}
\item Recall that $-e=e\times(-1)$.  By \axiom{Set_1}, $-1=_A -1$;
hence $-1\intrel -1$ by~(\ref{intrel:int}).  By hypothesis $e\intrel
t_1$.  Finally, since $-t_1=_A t$, one has $t_1\times(-1)=_A t$, whence
$e\times(-1)\intrel t$ by~(\ref{intrel:mult}).
\item By definition, $e_1-e_2=e_1+(-e_2)$.  By hypothesis, $e_1\intrel
t_1$ and $e_2\intrel t_2$.  Since $-t_2=_A -t_2$ by \axiom{Set_1}, one
has that $-e_2\intrel -t_2$ by~(\ref{intrel:inv}).  By hypothesis
$t_1-t_2=_A t$, that is (by definition of $-_A$), $t_1+(-t_2)=_A t$.
Hence, by~(\ref{intrel:plus}) $e_1+(-e_2)\intrel t$.
\item By induction on $n$.  If $n$ is $0$, then
by~(\ref{expr:exp:zero}) $e^n=1$.  By hypothesis $t_1^0=_A t$, or simply
$1=_A t$ since $t_1^0=1$ by~(\ref{nexp:zero}).  Hence $1\intrel t$
by~(\ref{intrel:int}).

Consider now $n=m+1$; then $e^n=e\times e^m$ by~(\ref{expr:exp:suc}).
By hypothesis $t_1^{m+1}=_A t$, that is to say, $t_1\times t_1^n=_A t$
according to~(\ref{nexp:suc}).  But $e\intrel t_1$ by hypothesis, and
also $e^m\intrel t_1^m$ by induction hypothesis; hence $e\times
e^m\intrel t$ by~(\ref{intrel:mult}).
\end{enumerate}
\end{proof}

\begin{lemma}\label{inclinterp}
Let $e:E$, $t:A$ and $\rho,\sigma$ be substitution pairs for $A$ with
$\rho\subseteq\sigma$ such that $e\intrel t$; then $e\intrels t$.
\end{lemma}
\begin{proof} By induction on the proof of $e\intrel t$.
\begin{enumerate}
\item $e=v^0_i$ and $\rho_0(v^0_i)=_A t$: since $\rho\subseteq\sigma$,
Proposition~\ref{substpair:incl:wdef} implies that $\sigma_0(v^0_i)=_A t$,
and by~(\ref{intrel:var0}) also $v^0_i\intrels t$.
\item $e=n$ and $\underline n=_A t$: then $n\intrels t$ follows
by~(\ref{intrel:int}).
\item $e=e_1+e_2$, $e_1\intrel t_1$, $e_2\intrel t_2$ and $t_1+t_2=_A t$;
by induction hypothesis $e_1\intrels t_1$ and $e_2\intrels t_2$, whence
$e_1+e_2\intrels t$ follows from~(\ref{intrel:plus}).
\item $e=e_1\times e_2$: analogous using~(\ref{intrel:mult}).
\item $e=e_1/e_2$: similar from~(\ref{intrel:div}), noticing that the
side condition $t_2\neq 0$ is also given by hypothesis.
\item $e=v^1_i(e')$, $e'\intrel t'$ and $\rho_1(v^1_i)(t')=_A t$: since
$\sigma_1(v^1_i)=\rho_1(v^1_i)$ by Proposition~\ref{substpair:incl:wdef},
also $\sigma_1(v^1_i)(t')=_A t$.  By induction hypothesis $e'\intrels t'$,
whence $v^1_i(e')\intrels t$ by~(\ref{intrel:var1}).
\end{enumerate}
\end{proof}

\begin{lemma}\label{intrelfunction} Let $e:E$, $t,t':A$ and $\rho$ be
a substitution pair for $A$ such that $e\intrel t$ and $e\intrel t'$.
Then the following hold.
\begin{enumerate}[(i)]
\item $t=_A t'$;
\item if $e\intrel t$ and $e\intrel t'$ can be proved without
using~(\ref{intrel:div}), and no divisions occur in either $t$ or $t'$,
then $t=_A t'$ can be proved without using the axiom \axiom{F}.
\end{enumerate}
\end{lemma}
\begin{proof} By induction on $\intrel$ (Coq checked).
\end{proof}

\section{Lifting}\label{lifting}

We now start looking at the actual implementation of {\rational}, focusing
on the ML program inside it.
%As described in Section~\ref{tactic}, 
This program computes a partial
inverse to the interpretation relation described above, that is, given
a term $t:A$, with $A$ a field, it returns an expression $e$
and a substitution pair $\rho$ such that $e\intrel t$.
In this section we formally describe this program as a function
$\lift$ and prove its correctness.

\subsection{Lifting to variables}

The first step is to define what to do when we meet a term that is not
built from the field operations, e.g. a variable $x$ or an expression
like $\sqrt 2$.

\begin{definition}\label{defn:liftv0}
Let $t:A$ and $\rho$ be a substitution pair over $A$.  Then
$\liftv0(t,\rho)=\langle v,\sigma\rangle$, $v\in\V_0$, is defined by:
\begin{itemize}
\item if there is an $i$ such that $\rho_0(v^0_i)=t$, then $v=v^0_i$ and
$\sigma=\rho$;
\item else, let $k$ be minimal such that $\rho_0(v^0_k)$ is not defined
and take $v=v^0_k$ and $\sigma_0=\rho_0\cup[v^0_k:=t]$, $\sigma_1=\rho_1$.
\end{itemize}
The behavior of $\liftv0$ can be described as follows: given a term $t$ and
a substitution $\rho$, it checks whether there is a variable $v^0_i$ such that
$\rho_0(v^0_i)=t$.  In the affirmative case, it returns this variable and
$\rho$; else it extends $\rho_0$ with a fresh variable which is interpreted
to $t$ and returns this variable and the resulting substitution.  Notice
that the result is deterministic, since there is at most one variable $i$
satisfying $\rho_0(v^0_i)=t$.
\end{definition}

\begin{lemma}\label{liftv0incl}
Let $t$ and $\rho$ be as in Definition~\ref{defn:liftv0}, and suppose
that $\liftv0(t,\rho)=\langle v,\sigma\rangle$.  Then $\rho\subseteq\sigma$.
\end{lemma}
\begin{proof}
Immediate: either $\sigma=\rho$, and we invoke reflexivity of $\subseteq$
(Proposition~\ref{substpair:incl:props}), or
$\langle\sigma_0,\sigma_1\rangle=\langle\rho_0\cup[v^0_k:=t],\rho_1\rangle$
with $v^0_k\not\in\dom\rho_0$, which directly satisfies the definition of
$\subseteq$.
\end{proof}

\begin{lemma}\label{liftv0corr}
Let $t$ and $\rho$ be as in Definition~\ref{defn:liftv0}, and suppose
that $\liftv0(t,\rho)=\langle v,\sigma\rangle$.  Then $v\intrels t$.
\end{lemma}
\begin{proof}
By definition of \liftv0, there are two cases:
\begin{itemize}
\item There is an $i$ such that $\rho_0(v^0_i)=t$, and then also
$\rho_0(v^0_i)=_A t$ by \axiom{Set_1}, whence $v^0_i\intrel t$
by~(\ref{intrel:var0}).  Since in this case $v=v^0_i$ and
$\sigma=\rho$, the thesis follows.
\item There is no such $i$; then $v=v^0_k$ where $k\not\in\dom\rho_0$,
and $\sigma_0=\rho_0\cup[v^0_k:=t]$.  Then, by definition of $\cup$,
$\sigma_0(v^0_k)=t$ and we can conclude as above that $v^0_k\intrels t$
using \axiom{Set_1} and~(\ref{intrel:var0}).
\end{itemize}
\end{proof}

\begin{definition}\label{defn:liftv1}
Let $f:[A\to A]$ and $\rho$ be a substitution pair over $A$.  Then
$\liftv1(f,\rho)=\langle v,\sigma\rangle$, $v\in\V_1$, is defined by:
\begin{itemize}
\item if there is an $i$ such that $\rho_1(v^1_i)=f$, then $v=v^1_i$ and
$\sigma=\rho$;
\item else, let $k$ be minimal such that $\rho_1(v^1_k)$ is not defined
and take $v=v^1_k$ and $\sigma_0=\rho_0$, $\sigma_1=\rho_1\cup[v^1_k:=t]$.
\end{itemize}
\end{definition}

\begin{lemma}\label{liftv1incl}
Let $t$ and $\rho$ be as in Definition~\ref{defn:liftv1}, and suppose
that $\liftv1(t,\rho)=\langle v,\sigma\rangle$.  Then $\rho\subseteq\sigma$.
\end{lemma}
\begin{proof}
Analogous to the proof of Lemma~\ref{liftv0incl}.
\end{proof}

\begin{lemma}\label{liftv1corr}
Let $f:[A\to A]$ and $\rho$ be a substitution pair over $A$ and suppose
that $\liftv1(f,\rho)=\langle v,\sigma\rangle$.  Suppose that $t\intrel e$;
then $v(t)\intrels f(e)$.
\end{lemma}
\begin{proof}
By definition of \liftv1, there are again two cases:
\begin{itemize}
\item There is an $i$ such that $\rho_1(v^1_i)=f$; then
$\rho_1(v^1_i)(t)=_A f(t)$ by \axiom{Set_1}, whence $v^1_i(e)\intrel
f(t)$ by~(\ref{intrel:var1}).  Since in this case $v=v^1_i$ and
$\sigma=\rho$, the thesis follows.
\item There is no such $i$; then $v=v^1_k$ where $k\not\in\dom\rho_1$,
and $\sigma_1=\rho_1\cup[v^1_k:=t]$.  Then, by definition of $\cup$,
$\sigma_1(v^1_k)=f$ and we can conclude as above that
$v^1_k(e)\intrels f(t)$ using \axiom{Set_1} and~(\ref{intrel:var1}).
\end{itemize}
\end{proof}

\subsection{Lifting expressions}

We can now define $\lift$.

\begin{definition}\label{defn:lift}
Let $t:A$ and $\rho$ be a substitution pair over $A$.  Then
$\lift(t,\rho)$ is recursively defined as follows.
\[
\begin{array}{rcll}
\lift(\underline n,\rho) & = & \langle n,\rho\rangle
 & \mbox{ $n:\Z$ closed}\\
\lift(t_1\star t_2,\rho) & = & \langle e_1\star e_2,\sigma\rangle
 & \mbox{where }\left\{\begin{array}l \star\in\{+,-,\times,/\}\\
                       \langle e_1,\theta\rangle=\lift(t_1,\rho)\\
                       \langle e_2,\sigma\rangle=\lift(t_2,\theta)
                       \end{array}\right. \\
\lift(-t,\rho) & = & \langle -e,\sigma\rangle
 & \mbox{ where $\langle e,\sigma\rangle=\lift(t,\rho)$}\\
\lift(t^n,\rho) & = & \langle e^n,\sigma\rangle
 & \mbox{where }\left\{\begin{array}l n:\nat\mbox{ is closed}\\
                       \langle e,\sigma\rangle=\lift(t,\rho)
                       \end{array}\right. \\
\lift(f(t),\rho) & = & \langle v^1_i(e),\theta\rangle
 & \mbox{where }\left\{\begin{array}l \langle e,\sigma\rangle=\lift(t,\rho)\\
                       \langle v^1_i,\theta\rangle=\liftv1(f,\sigma)
                       \end{array}\right. \\
\lift(t,\rho) & = & \liftv0(t,\rho) & \mbox{ otherwise}
\end{array}
\]
The two last clauses also define $\lift(\underline n,\rho)$ and
$\lift(t^n,\rho)$ when $n$ is not a closed term.

Notice that on every recursive call of $\lift$ the argument decreases
w.r.t\ $\less$; since $\less$ is well founded by
Proposition~\ref{lesswff}, this is a valid definition.
\end{definition}

\begin{lemma}\label{liftincl}
Let $\rho$ be a substitution pair for $A$.  For all $t:A$ and $e:E$, if
$\langle e,\sigma\rangle=\lift(t,\rho)$, then $\rho\subseteq\sigma$.
\end{lemma}
\begin{proof} By induction on $\less$.
\begin{enumerate}
\item $t$ is minimal for $\less$:
\begin{enumerate}
\item $t=\underline n$ with $n:\Z$ closed.  Then $\sigma=\rho$.
\item otherwise $\langle e,\sigma\rangle=\liftv0(t,\rho)$.  By
Lemma~\ref{liftv0incl}, $\rho\subseteq\sigma$.
\end{enumerate}
\item $t=f(t')$ with $f:[A\to A]$.
\begin{enumerate}
\item $f$ is $-_A$: immediate by induction hypothesis.
\item $f$ is $\cdot^n$ with $n$ is a closed term: then the result follows by
induction hypothesis.
\item otherwise, $e=v^1_i(e')$ with
$\langle e',\theta\rangle=\lift(t',\rho)$ and
$\langle v^1_i,\sigma\rangle=\liftv1(f,\theta)$.  By induction hypothesis
$\rho\subseteq\theta$; by Lemma~\ref{liftv1incl}
$\theta\subseteq\sigma$; by transitivity $\rho\subseteq\sigma$.
\end{enumerate}
\item $t=t_1\star t_2$ with $\star\in\{+,-,\times,/\}$: then
$e=e_1\star e_2$ with $\langle e_1,\theta\rangle=\lift(t_1,\rho)$
and $\langle e_2,\sigma\rangle=\lift(t_1,\theta)$.

By induction hypothesis, $\rho\subseteq\theta$ and $\theta\subseteq\sigma$;
since $\subseteq$ is transitive (Proposition~\ref{substpair:incl:props}),
$\rho\subseteq\sigma$.
\end{enumerate}
\end{proof}

The following is the main result so far: it expresses the correctness
of the ML program inherent to {\rational}.
Given a term $t$ and a substitution $\rho$, the program computes an
expression $e$ and a new substitution $\sigma$ such that $e\intrels t$.

\begin{theorem}\label{liftcorrect}
Let $t:A$ and $\rho$ be a substitution pair over $A$, and take
$\langle e,\sigma\rangle=\lift(t,\rho)$.  Then $e\intrels t$.
\end{theorem}
\begin{proof} By induction on $\less$.
\begin{enumerate}
\item $t$ is minimal for $\less$:
\begin{enumerate}
\item $t=\underline n$ with $n:\Z$ closed.  Then, by definition of
\lift, $e=n$ and $\sigma=\rho$.  By \axiom{Set_1}, $\underline
n=_A\underline n$, and by~(\ref{intrel:int}) $n\intrel\underline n$.
\item otherwise $\langle e,\sigma\rangle=\liftv0(t,\rho)$.  By
Lemma~\ref{liftv0corr}, it follows that $e\intrels t$.
\end{enumerate}
\item $t=f(t')$ with $f:[A\to A]$.
\begin{enumerate}
\item $f$ is $-_A$: then
$\langle e,\sigma\rangle=\langle -e',\sigma\rangle$ with
$\langle e',\sigma\rangle=\lift(t',\rho)$.  By induction hypothesis,
$e'\intrels t'$; since $-t'=-t'$ by \axiom{Set_1}, $-e'\intrels -t'$
by~(\ref{intrel:inv}).
\item $f$ is $\cdot^n$ with $n$ closed: then
$\langle e,\sigma\rangle=\langle (e')^n,\sigma\rangle$ with
$\langle e',\sigma\rangle=\lift(t',\rho)$.  By induction hypothesis,
$e'\intrels t'$; since $(t')^n=(t')^n$ by \axiom{Set_1},
$(e')^n\intrels(t')^n$ by~(\ref{intrel:nexp}).
\item otherwise $e=v^1_i(e')$ with
$\langle e',\theta\rangle=\lift(t',\rho)$ and
$\langle v^1_i,\sigma\rangle=\liftv1(f,\theta)$.  By induction
hypothesis $e'\intrelt t'$; Lemma~\ref{liftv1corr} allows us to
conclude that $f(e')\intrels v^1_i(t')$.
\end{enumerate}
\item $t=t_1\star t_2$ with $\star\in\{+,-,\times,/\}$ (if $\star-/$, then
also $t_2\neq 0$): then $e=e_1\star e_2$ with
$\langle e_1,\theta\rangle=\lift(t_1,\rho)$ and
$\langle e_2,\sigma\rangle=\lift(t_1,\theta)$.

By induction hypothesis, $e_1\intrelt t_1$; by Lemma~\ref{liftincl},
$\theta\subseteq\sigma$, whence by Lemma~\ref{inclinterp} also
$e_1\intrels t_1$.

Also by induction hypothesis, $e_2\intrelt t_2$.  Furthermore,
\axiom{Set_1} implies $t_1\star t_2=_A t_1\star t_2$, hence $e_1\star
e_2\intrelt t_1\star t_2$ by either~(\ref{intrel:plus}),
(\ref{intrel:minus}), (\ref{intrel:mult}) or~(\ref{intrel:div}),
according to whether $\star$ is respectively $+$, $-$, $\times$ or
$/$; in the last case, the extra condition $t_2\neq 0$ also holds.
\end{enumerate}
\end{proof}

\bigskip Notice that this result is still valid if $A$ is a group or
a ring, as can be seen by removing the corresponding cases in this proof
and checking that it remains valid.

\subsection{Properties of lifting}

The remainder of this section is concerned with other properties of
the ML program, and of $\lift$, that are needed for the rest of the
paper.

First, lifting is idempotent on the second component: if lifting $e$ with
$\rho$ returns $t$ and $\sigma$, and $\theta$ is any substitution extending
$\sigma$ (in particular, $\sigma$ itself), then
$\lift(t,\theta)=\langle e,\theta\rangle$.

\begin{lemma}\label{liftidempotent}
Let $t:A$, $e:E$ and $\rho,\sigma,\theta$ be substitution pairs over $A$
such that $\langle e,\sigma\rangle=\lift(t,\rho)$ and $\sigma\subseteq\theta$.
Then $\lift(t,\theta)=\langle e,\theta\rangle$.
\end{lemma}
\begin{proof} By induction on $\less$.
\begin{enumerate}
\item $t$ is minimal for $\less$:
\begin{enumerate}
\item $t=\underline n$ with $n:\Z$ closed.  Then
$\lift(\underline n,\rho)=\langle n,\rho\rangle$ and
$\lift(\underline n,\theta)=\langle n,\theta\rangle$; hence the thesis holds.
\item otherwise $\langle e,\sigma\rangle=\liftv0(t,\rho)$.  Then $e=v^0_i$
for some $i$, and by Lemma~\ref{liftv0corr}, $\sigma_0(v^0_i)=t$.
Since $\sigma\subseteq\theta$, $\theta_0(v^0_i)=t$ by Lemma~\ref{inclinterp},
and, according to the definition of $\liftv0$,
$\liftv0(t,\theta)=\langle v^0_i,\theta\rangle$.
\end{enumerate}
\item $t=f(t')$ with $f:[A\to A]$.
\begin{enumerate}
\item $f$ is $-_A$: then
$\langle e,\sigma\rangle=\langle -e',\sigma\rangle$ with
$\langle e',\sigma\rangle=\lift(t',\rho)$.  By induction hypothesis,
$\lift(t',\theta)=\langle e',\theta\rangle$, whence
$\lift(-t',\theta)=\langle -e',\theta\rangle$.
\item $f$ is $\cdot^n$ and $n$ is closed: then
$\langle e,\sigma\rangle=\langle (e')^n,\sigma\rangle$ with
$\langle e',\sigma\rangle=\lift(t',\rho)$.  By induction hypothesis,
$\lift(t',\theta)=\langle e',\theta\rangle$, and it follows that
$\lift((t')^n,\theta)=\langle(-e')^n,\theta\rangle$.
\item otherwise $e=v^1_i(e')$ with
$\langle e',\sigma'\rangle=\lift(t',\rho)$ and
$\langle v^1_i,\sigma\rangle=\liftv1(f,\sigma')$.  By induction
hypothesis, $\lift(t',\theta)=\langle e',\theta\rangle$; by
Lemma~\ref{liftv1corr}, $\sigma_1(v^1_i)=f$ and hence
$\theta_1(v^1_i)=f$ by Lemma~\ref{inclinterp}.  Therefore, the
definition of $\liftv1$ ensures that
$\liftv1(f,\theta)=\langle v^1_i,\theta\rangle$ and
$\lift(f(t'),\theta)=\langle v^1_i(e'),\theta\rangle$.
\end{enumerate}
\item $t=t_1\star t_2$ with $\star\in\{+,-,\times,/\}$: then
$e=e_1\star e_2$ with $\langle e_1,\sigma_1\rangle=\lift(t_1,\rho)$
and $\langle e_2,\sigma\rangle=\lift(t_1,\sigma_1)$.

By Lemma~\ref{liftincl}, $\sigma_1\subseteq\sigma$,
hence $\sigma_1\subseteq\theta$; then, by induction hypothesis,
$\lift(t_1,\theta)=\langle e_1,\theta\rangle$.  Also by induction hypothesis,
$\lift(t_2,\theta)=\langle e_2,\theta\rangle$.  It follows that
$\lift(t_1\star t_2,\theta)=\langle e_1\star e_2,\theta\rangle$.
\end{enumerate}
\end{proof}

All variables in the expression output by $\lift$ can be interpreted by
the corresponding substitution.

\begin{lemma}\label{liftdom}
Let $t:A$ and $\rho$ be a substitution pair over $A$.
If $\lift(t,\rho)=\langle e,\sigma\rangle$, then $v^i_k\in\dom(\sigma_k)$
for all variables $v^i_k$ occurring in $e$.
\end{lemma}
\begin{proof}
By induction on $t$ according to $\less$.
\begin{enumerate}
\item $t$ is minimal for $\less$.
\begin{enumerate}
\item $t=\underline n$: then $e=n$ and no variables occur in $e$, so the
result vacuously holds.
\item otherwise $\langle e,\sigma\rangle=\liftv0(t,\rho)$ and the result
is immediate by definition of $\liftv0$.
\end{enumerate}
\item $t=f(t')$ with $f:[A\to A]$.
\begin{enumerate}
\item $f$ is $-_A$: then $e=e'$ and $\lift(t',\rho)=\langle e',\sigma\rangle$.
Any variable $v^i_k$ occurring in $e$ must occur in $e'$, and by
induction hypothesis $v^i_k\in\dom(\sigma_i)$.
\item $f$ is $\cdot^n$ with $n$ closed: analogous.
\item otherwise there exist a natural number $j$, an expression $e'$
and a substitution pair $\theta$ such that
$\lift(t',\rho)=\langle e',\theta\rangle$,
$\liftv1(f,\theta)=\langle v^1_j,\sigma\rangle$ and $e=v^1_j(e')$.
If $v^i_k$ is a variable occurring in $e$, then either $v^i_k=v^1_j$ and
the result holds by definition of $\liftv1$ or $v^i_k$ occurs in $e'$;
in the latter case, by induction hypothesis $v^i_k\in\dom(\theta_i)$, and
since $\theta\subseteq\sigma$ also $v^i_k\in\dom(\sigma_i)$.
\end{enumerate}
\item $t=t_1\star t_2$ with $\star\in\{+,-,\times,/\}$: then
$e=e_1\star e_2$ and there is a substitution pair $\theta$ such that
$\lift(t_1,\rho)=\langle e_1,\theta\rangle$ and
$\lift(t_2,\theta)=\langle e_2,\sigma\rangle$.  Suppose $v^i_k$ occurs
in $e$; then it either occurs in $e_1$ or in $e_2$.  In the first
case, by induction hypothesis $v^i_k\in\dom(\theta_i)$, and since
$\theta\subseteq\sigma$ also $v^i_k\in\dom(\sigma_i)$.  The second
case follows directly from the induction hypothesis.
\end{enumerate}
\end{proof}

\subsection{Permutation of lifting}

To prove properties of {\rational}, we need to consider situations when
the same terms are lifted in different orders.
This section proves some results about the corresponding outputs: under
quite general hypotheses, they differ only in the names of the variables.

\begin{definition}\label{renamevars}
Let $\rho,\sigma$ be substitution pairs for $A$.  We say that $\sigma$ is
obtained from $\rho$ \emph{by a renaming of variables} if there is a pair
$\xi=\langle\xi_0,\xi_1\rangle$ of permutations of $\nat$ such that,
for $i=0,1$, the following conditions hold:
\begin{itemize}
\item $\xi_i(k)\neq k\rightarrow v^i_k\in\dom(\rho_i)$;
\item for all $k$, $\sigma_i\left(v^i_{\xi_i(k)}\right)\simeq\rho_i(v^i_k)$
(that is, either they are both undefined or they are both defined and
coincide).
\end{itemize}
We denote this situation by {\isrenamevar\sigma\rho\xi} and say that $\xi$ is
a renaming of variables for $\rho$ (or simply $\xi$ is a renaming of
variables, if the $\rho$ is not relevant).
Also, we will abuse notation and write $\dom(\xi_i)=\{k|\xi_i(k)\neq k\}$
for $i=0,1$; it follows that $\xi_i(j)=j$ if $j\not\in\dom(\xi_i)$.  The
first condition then becomes simply $\dom(\xi_i)\subseteq\dom(\rho_i)$.
\end{definition}

Notice that the second condition totally defines $\sigma$, since
each $\xi_i$ is a permutation.  For this reason, we will also use the
notation {\isrenamevar\sigma\rho\xi} as a definition of $\sigma$.

Another important consequence is that, if {\isrenamevar\sigma\rho\xi},
then $\dom(\sigma_i)=\dom(\rho_i)$ for $i=0,1$.
\begin{proposition}\label{renamevarsequiv}
The relation $R(\rho,\sigma)$ defined as ``$\sigma$ is obtained from $\rho$
by a renaming of variables'' is an equivalence relation.
\end{proposition}
\begin{proof}
\begin{itemize}
\item Reflexivity: just take $\xi=\langle\idn,\idn\rangle$.
\item Symmetry: suppose {\isrenamevar\sigma\rho\xi} for some $\xi$; then,
since each $\xi_i$ is a bijection, trivially
{\isrenamevar\rho\sigma{\langle\xi^{-1}_0,\xi^{-1}_1\rangle}}.
\item Transitivity: suppose {\isrenamevar\sigma\rho\xi} and
{\isrenamevar\theta\sigma{\xi'}}; then {\isrenamevar\theta\rho{\xi'\circ\xi}}
where $\xi'\circ\xi$ denotes pointwise composition.  In fact, for $i=0,1$,
and for every $k$, $\theta_i\left(v^i_{\xi'\circ\xi(k)}\right)\simeq%
\sigma_i\left(v^i_{\xi(k)}\right)\simeq\rho_i(v^i_k)$.

Finally, suppose that, for some $k$, $v^i_k\not\in\dom(\rho_i)$; then
$\xi_i(k)=k$ and, since $\dom(\sigma_i)=\dom(\rho_i)$, also
$v^i_k\not\in\dom(\sigma_i)$ and hence $\xi'_i\circ\xi_i(k)=\xi'_i(k)=k$.
But then $\xi'_i\circ\xi_i(k)\neq k\rightarrow v^i_k\in\dom(\rho_i)$.
\end{itemize}
\end{proof}

\begin{definition}
Let $\xi$ be a renaming of variables and $e,e':E$.  We say that $e'$
is obtained from $e$ by $\xi$, denoted {\isrenamevar{(e')}e\xi}, if $e'$
is obtained from $e$ by replacing each occurrence of $v^i_k$ by
$v^i_{\xi_i(k)}$, $i=0,1$.
\end{definition}

\begin{lemma}\label{renamelift}
Let $\rho$ be a substitution pair for $A$ and $\xi$ be a renaming of
variables for $\rho$.  For every $t:A$, if $\lift(t,\rho)=\langle
e,\sigma\rangle$ then $\lift(t,\renamevar\rho\xi)=%
\langle\renamevar{e}\xi,\renamevar\sigma\xi\rangle$.
\end{lemma}
\begin{proof} By induction on $\less$.
\begin{enumerate}
\item $t$ is minimal for $\less$:
\begin{enumerate}
\item $t=\underline n$: then $e=n$, $\sigma=\rho$,
$\lift(t,{\renamevar\rho\xi})=\langle n,{\renamevar\rho\xi}\rangle$ and the 
conclusion trivially holds.
\item otherwise, $e=\liftv0(t,\rho)$ and we have to distinguish two
cases.

Suppose there is an $i$ such that $\rho_0(v^0_i)=t$.  Then $e=v^0_i$ and
$\sigma=\rho$; but by Definition~\ref{renamevars}
$\renamevar\rho\xi_0\left(v^0_{\xi_0(i)}\right)=\rho_0(v^0_i)$, so
$\lift(t,\renamevar\rho\xi)=\langle v^0_{\xi_0(i)},\renamevar\rho\xi\rangle$,
and by definition {\isrenamevar{v^0_{\xi_0(i)}}{(v^0_i)}\xi}.

Otherwise, pick $k$ minimal such that $v^0_k\not\in\dom(\rho_0)$.
Then $e=v^0_k$ and $\sigma=\langle\rho_0\cup[v^0_k:=t],\rho_1\rangle$.
But then $\lift(t,{\renamevar\rho\xi})=\langle v^0_k,\sigma'\rangle$ with
$\sigma'=\langle\renamevar\rho\xi_0\cup[v^0_k:=t],\renamevar\rho\xi_1\rangle$: since
$\dom(\rho_0)=\dom(\renamevar\rho\xi_0)$ (see remark after
Definition~\ref{renamevars}), $k$ is also the minimal natural number
satisfying $v^0_k\not\in\dom(\renamevar\rho\xi_0)$; furthermore, there can be no
$i$ such that $\renamevar\rho\xi_0(v^0_i)=t$ because
$\renamevar\rho\xi_0(v^0_i)=\rho_0(v^0_{\xi^{-1}_0(i)})$.  But $k\not\in\dom(\xi_0)$,
so {\isrenamevar{v^0_k}{v^0_k}\xi} and {\isrenamevar{\sigma'}\sigma\xi}.
\end{enumerate}
\item $t=f(t')$ with $f:[A\to A]$.
\begin{enumerate}
\item $f$ is $-_A$: then there is an expression $e'$ such that
$\lift(t',\rho)=\langle e',\sigma\rangle$ and $e=-e'$.
By induction hypothesis,
$\lift(t',{\renamevar\rho\xi})=\langle\renamevar{(e')}\xi,\renamevar\sigma\xi\rangle$
and hence $\lift(t,{\renamevar\rho\xi})=\langle\renamevar e\xi,\renamevar\sigma\xi\rangle$.
\item $f$ is $\cdot^n$ with $n$ closed: analogous.
\item otherwise there exist an expression $e'$, an index $i$ and
a substitution pair $\theta$ such that
$\lift(t',\rho)=\langle e',\theta\rangle$,
$\liftv1(f,\theta)=\langle v^1_i,\sigma\rangle$ and $e=v^1_i(e')$.
By induction hypothesis, $\lift(t',{\renamevar\rho\xi})=%
\langle\renamevar{(e')}\xi,\renamevar\theta\xi\rangle$.

Suppose there is an $k$ such that $\theta_1(v^1_k)=f$.  Then $i=k$ and
$\sigma=\theta$; but by Definition~\ref{renamevars}
$\renamevar\theta\xi_1\left(v^1_{\xi_1(i)}\right)=\theta_1(v^1_i)=f$, so
$\liftv1(f,\renamevar\theta\xi)=\langle v^1_{\xi_1(i)},\renamevar\theta\xi\rangle$.
Trivially {\isrenamevar{v^1_{\xi_1(i)}}{(v^1_i)}\xi}; since $\theta=\sigma$,
$\lift(t,{\renamevar\rho\xi})=\langle\renamevar{v^1_i(e')}\xi,\renamevar\sigma\xi\rangle$,
which establishes the result.

Otherwise, $i$ is the minimal $k$ such that $v^1_k\not\in\dom(\theta_1)$
and $\sigma=\langle\theta_0,\theta_1\cup[v^1_i:=f]\rangle$.
But then $\liftv1(f,\renamevar\theta\xi)=\langle v^1_i,\sigma'\rangle$ with
$\sigma'=\langle\renamevar\theta\xi_0,\renamevar\theta\xi_1\cup[v^1_i:=f]\rangle$:
since $\dom(\theta_1)=\dom(\renamevar\theta\xi_1)$ (second condition in
Definition~\ref{renamevars}), $i$ is also the minimal $k$
satisfying $v^1_k\not\in\dom(\renamevar\theta\xi_1)$; furthermore, there can be no
$k$ such that $\renamevar\rho\xi_1(v^1_k)=f$, since
$\renamevar\theta\xi_1(v^1_k)=\theta_1(v^1_{\xi^{-1}_1(k)})$.
But then {\isrenamevar{\sigma'}\sigma\xi}; since $i=\xi_1(i)$,
we also have in this situation that
$\lift(t,{\renamevar\rho\xi})=\langle\renamevar{v^1_i(e')}\xi,\renamevar\sigma\xi\rangle$.
\end{enumerate}
\item $t=t_1\star t_2$ with $\star\in\{+,-,\times,/\}$: then there are
expressions $e_1,e_2$ and a substitution pair $\theta$ such that
$\lift(t_1,\rho)=\langle e_1,\theta\rangle$,
$\lift(t_2,\theta)=\langle e_2,\sigma\rangle$ and $e=e_1\star e_2$.

By induction hypothesis $\lift(t_1,{\renamevar\rho\xi})=%
\langle\renamevar{e_1}\xi,\renamevar\theta\xi\rangle$.
But then the induction hypothesis applies again, and
$\lift(t_2,\renamevar\theta\xi)=\langle\renamevar{e_2}\xi,%
\renamevar\sigma\xi\rangle$.  Hence, $\lift(t_1\star t_2,{\renamevar\rho\xi})=%
\langle(\renamevar{e_1}\xi)\star(\renamevar{e_2}\xi),%
\renamevar\sigma\xi\rangle$ and trivially
$(\renamevar{e_1}\xi)\star(\renamevar{e_2}\xi)=\renamevar e\xi$.
\end{enumerate}
\end{proof}

We now prove some lemmas about the order in which terms are lifted.

\begin{lemma}\label{liftv0commv1}
Let $t:A$, $f:[A\to A]$ and $\rho$ be a substitution pair for $A$.
Suppose $\liftv0(t,\rho)=\langle v^0_i,\sigma\rangle$ and
$\liftv1(f,\rho)=\langle v^1_j,\theta\rangle$.
Then
$\liftv1(f,\sigma)=\langle v^1_j,\langle\sigma_0,\theta_1\rangle\rangle$ and
$\liftv0(t,\theta)=\langle v^0_i,\langle\sigma_0,\theta_1\rangle\rangle$.
\end{lemma}
\begin{proof}
Let $\tau$ be an arbitrary substitution pair.  From the definition of
$\liftv0$ (Definition~\ref{defn:liftv0}), one sees that the result of
$\liftv0(u,\tau)$ always has $\tau_1$ as the second component of the
substitution pair in the output and the remaining values do not depend
on $\tau_1$.  Therefore, $\sigma=\langle\sigma_0,\rho_1\rangle$.

Similarly, from the definition of $\liftv1$
(Definition~\ref{defn:liftv1}), one sees that $\tau_0$ is the first
component of the substitution pair in the result of $\liftv1(g,\tau)$,
the other values being independent of $\tau_0$.  Therefore,
$\theta=\langle\rho_0,\theta_1\rangle$.

But then $\liftv1(f,\sigma)=\liftv1(f,\langle\sigma_0,\rho_1\rangle)=%
\langle v^1_j,\langle\sigma_0,\theta_1\rangle$ and $\liftv0(t,\theta)=%
\liftv0(t,\langle\rho_0,\theta_1\rangle)=%
\langle v^0_i,\langle\sigma_0,\theta_1\rangle\rangle$.
\end{proof}

\begin{lemma}\label{liftv0commv0}
Let $t_1,t_2:A$ and $\rho$ be a substitution pair for $A$.
Suppose that
\begin{eqnarray*}
\liftv0(t_1,\rho) & = & \langle v^0_i,\sigma\rangle\\
\liftv0(t_2,\sigma) & = & \langle v^0_j,\theta\rangle\\
\liftv0(t_2,\rho) & = & \langle v^0_{j'},\sigma'\rangle\\
\liftv0(t_1,\sigma') & = & \langle v^0_{i'},\theta'\rangle
\end{eqnarray*}
Then there is a renaming of variables $\xi$ for $\theta$ such that
$\xi_1=\idn$, $\dom(\xi_0)\cap\dom(\rho_0)=\emptyset$,
{\isrenamevar{\theta'}\theta\xi}, $i'=\xi_0(i)$ and $j'=\xi_0(j)$.
\end{lemma}
\begin{proof}
There are four cases to consider.

If $t_1$ and $t_2$ are (syntactically) equal, then
$\xi=\langle\idn,\idn\rangle$ trivially establishes the thesis: in this
case $j'=i$ and $\sigma'=\sigma$, whence $i'=j$ and $\theta'=\theta$;
furthermore, since we are in a special case of Lemma~\ref{liftidempotent},
also $j=i$ and $i'=j'$.

Let us now assume that $t_1$ and $t_2$ are different.
Suppose first that there is a variable $v^0_k$ such that
$\rho_0(v^0_k)=t_1$; then $i=k$ and again $\sigma=\rho$, from
which we can deduce $j'=j$ and $\sigma'=\sigma$.  But from
Lemma~\ref{liftv0incl}, $\rho\subseteq\sigma$, hence from
Lemma~\ref{liftidempotent} also $i'=i$ and $\theta'=\theta$;
therefore $\xi$ can again be taken to be
$\langle\idn,\idn\rangle$.

A symmetric argument proves the case where there is a variable $v^0_k$
such that $\rho_0(v^0_k)=t_2$.

Finally, suppose that for no $k$ either $\rho_0(v^0_k)=t_1$ or
$\rho_0(v^0_k)=t_2$.  Then $i$ is the minimal natural number satisfying
$v^0_i\not\in\dom(\rho_0)$ and
$\sigma=\langle\rho_0\cup[v^0_i:=t_1],\rho_1\rangle$.  By definition
of $\cup$, there is still no $k$ such that $\sigma_0(v^0_k)=t_2$,
whence $j$ is the least natural number such that $v^0_j\not\in\dom(\sigma_0)$
and $\theta=\langle\sigma_0\cup[v^0_j:=t_2],\sigma_1\rangle$.

On the other hand, $j'$ is also the least natural satisfying
$v^0_{j'}\not\in\dom(\rho_0)$, so $j'=i$ and
$\sigma'=\langle\rho_0\cup[v^0_i:=t_2],\rho_1\rangle$.  Then
$\dom(\sigma'_0)=\dom(\rho_0)\cup\{i\}=\dom(\sigma_0)$, whence
necessarily $i'=j$ and
$\theta'=\langle\sigma'_0\cup[v^0_j:=t_2],\sigma'_1\rangle$.
It then trivially follows that the renaming of variables
$\langle(i\ j),\idn\rangle$ satisfies all the desired conditions.
\end{proof}

\begin{lemma}\label{liftv1commv1}
Let $f_1,f_2:[A\to A]$ and $\rho$ be a substitution pair for $A$.
Suppose that
\begin{eqnarray*}
\liftv1(f_1,\rho) & = & \langle v^1_i,\sigma\rangle\\
\liftv1(f_2,\sigma) & = & \langle v^1_j,\theta\rangle\\
\liftv1(f_2,\rho) & = & \langle v^1_{j'},\sigma'\rangle\\
\liftv1(f_1,\sigma') & = & \langle v^1_{i'},\theta'\rangle
\end{eqnarray*}
Then there is a renaming of variables $\xi$ for $\theta$ such that
$\xi_0=\idn$, $\dom(\xi_1)\cap\dom(\rho_1)=\emptyset$,
{\isrenamevar{\theta'}\theta\xi}, $i'=\xi_1(i)$ and $j'=\xi_1(j)$.
\end{lemma}
\begin{proof}
The proof is exactly analogous to that of Lemma~\ref{liftv0commv0},
interchanging the indices $0$ and $1$ of the variables and substitutions.
\end{proof}

\begin{lemma}\label{liftcommv0}
Let $t_1,t_2:A$, $e_1,e'_1,e_2,e'_2:E$ and
$\rho,\sigma,\sigma',\theta,\theta'$ be substitution pairs for $A$
satisfying the following relations.
\begin{eqnarray*}
\lift(t_1,\rho) & = & \langle e_1,\sigma\rangle\\
\liftv0(t_2,\sigma) & = & \langle e_2,\theta\rangle\\
\liftv0(t_2,\rho) & = & \langle e'_2,\sigma'\rangle\\
\lift(t_1,\sigma') & = & \langle e'_1,\theta'\rangle
\end{eqnarray*}
Then there is a renaming of variables $\xi$ for $\theta$ such that:
\begin{enumerate}[(i)]
\item\label{domxi0} $\xi_1=\idn$ and
$\dom(\xi_0)\cap\dom(\rho_0)=\emptyset$;
\item\label{replxi0} {\isrenamevar{\theta'}\theta\xi} and
{\isrenamevar{e'_i}{e_i}\xi} for $i=1,2$.
\end{enumerate}
\end{lemma}
\begin{proof}
By induction on $t_1$ according to $\less$.
\begin{enumerate}
\item $t_1$ is minimal for $\less$.
\begin{enumerate}
\item $t_1=\underline n$: then $e_1=n$, $\sigma=\rho$ whence trivially
$e'_2=e_2$, $\sigma'=\theta$ and also $e'_1=e_1$ and $\theta'=\theta$;
thus $\xi=\langle\idn,\idn\rangle$ trivially
satisfies~(\ref{domxi0}) and~(\ref{replxi0}).
\item otherwise $\lift(t_1,\rho)=\liftv0(t_1,\rho)$ and
Lemma~\ref{liftv0commv0} establishes the result.
\end{enumerate}
\item $t_1=f(t)$ with $f:[A\to A]$.
\begin{enumerate}
\item $f$ is $-_A$: then $e_1=-e$ where
$\langle e,\sigma\rangle=\lift(t,\rho)$; similarly $e'_1=-e'$ where
$\langle e',\theta'\rangle=\lift(t,\sigma')$.
By induction hypothesis there is a renaming of variables $\xi$ for
$\theta$ such that $\xi_1=\idn$,
$\dom(\xi_0)\cap\dom(\rho_0)=\emptyset$,
{\isrenamevar{\theta'}\theta\xi}, {\isrenamevar{e'}e\xi} and
{\isrenamevar{e'_2}{e_2}\xi}.
The only thing left to show is that {\isrenamevar{e'_1}{e_1}\xi}; but
this is trivial, since $e_1=e$ and $e'_1=-e'$.  Therefore $\xi$ is the
desired renaming of variables.
\item $f$ is $\cdot^n$ with $n$ is closed: analogous.
\item otherwise $e_1=v^1_i(e)$ with $\lift(t,\rho)=\langle e,\tau\rangle$
and $\liftv1(f,\tau)=\langle v^1_i,\sigma\rangle$;
also $e'_1=v^1_j(e')$ with $\lift(t,\sigma')=\langle
e',\tau'\rangle$ and $\liftv1(f,\tau')=\langle v^1_j,\theta'\rangle$.

By Lemma~\ref{liftv0commv1}, $\theta=\langle\theta_0,\sigma_1\rangle$
and $\liftv0(t_2,\tau)=\langle e_2,\langle\theta_0,\tau_1\rangle\rangle$.
By induction hypothesis, there is a renaming of variables $\xi$ for
$\langle\theta_0,\tau_1\rangle$ such that $\xi_1=\idn$,
$\dom(\xi_0)\cap\dom(\rho_0)=\emptyset$,
{\isrenamevar{\tau'}{\langle\theta_0,\tau_1\rangle}\xi},
{\isrenamevar{e'}e\xi} and {\isrenamevar{e'_2}{e_2}\xi}.

It remains to show that {\isrenamevar{e'_1}{e_1}\xi}; but
{\isrenamevar{\tau'}{\langle\theta_0,\tau_1\rangle}\xi}
and $\xi_1=\idn$ imply $\tau'_1=\tau_1$.
Similar considerations as made in the proof of Lemma~\ref{liftv0commv1}
make it clear that $\theta'_1=\tau'_1$ and $j=i$.  Hence the thesis follows.
\end{enumerate}
\item $t_1=u\star v$ with $\star\in\{+,-,\times,/\}$: then there are
expressions $e_u$ and $e_v$ and a substitution pair $\tau$ such that
$\lift(u,\rho)=\langle e_u,\tau\rangle$, $\lift(v,\tau)=\langle
e_v,\sigma\rangle$ and $e=e_u\star e_v$.  Also, there are expressions
$e'_u$ and $e'_v$ and a substitution pair $\tau'$ such that
$\lift(u,\sigma')=\langle e'_u,\tau'\rangle$, $\lift(v,\tau')=\langle
e'_v,\theta'\rangle$ and $e'=e'_u\star e'_v$.

Consider now $\liftv0(t_2,\tau)=\langle e^\ast_2,\tau^\ast\rangle$.
By induction hypothesis, there is a renaming of variables $\xi$ for
$\tau^\ast$ satisfying~(\ref{domxi0}) such that
{\isrenamevar{e'_2}{e^\ast_2}\xi}, {\isrenamevar{e'_u}{e_u}\xi} and
{\isrenamevar{\tau'}{\tau^\ast}\xi}.

Let now $\lift(v,\tau^\ast)=\langle e^\ast_v,\theta^\ast\rangle$.
Induction hypothesis now implies that there is a renaming of variables
$\xi'$ for $\theta$ such that $\xi'_1=\idn$,
$\dom(\xi'_0)\cap\dom(\tau_0)=\emptyset$,
{\isrenamevar{e^\ast_2}{e_2}{\xi'}},
{\isrenamevar{e^\ast_v}{e_v}{\xi'}} and
{\isrenamevar{\theta^\ast}\theta{\xi'}} (see
Figure~\ref{fig:liftcommv0}).
\begin{figure}[htb]
\[\xymatrix{
 & \rho \ar[dl]_{u} \ar[dr]^{t_2} \\
 \tau \ar[d]_{v} \ar[dr]^{t_2} & & \sigma' \ar[d]_{u} \\
 \sigma \ar[d]_{t_2} & \tau^\ast \ar@{.>}[r]^{\xi} \ar[d]_{v}
 & \tau' \ar[d]_{v} \\
 \theta \ar@{.>}[r]^{\xi'} & \theta^\ast \ar@{.>}[r]^{\xi} & \theta' 
}\]
\caption{Induction step on the proof of Lemma~\ref{liftcommv0}.  An arrow
from $\rho$ to $\rho'$ with label $t$ means that $\rho'$ is obtained
by $\lift(t,\rho)$.}
\label{fig:liftcommv0}
\end{figure}

We now prove that $\xi\circ\xi'$ is the desired renaming of variables.
\begin{itemize}
\item Trivially, $\xi_1\circ\xi'_1=\idn$; since $\rho\subseteq\tau$,
if $v^0_k\in\dom(\rho_0)$ then $\xi_0(k)=k$ and $\xi'_0(k)=k$, hence
$\dom(\xi_0\circ\xi'_0)\cap\dom(\rho_0)=\emptyset$.
\item By hypothesis, {\isrenamevar{e'_2}{e^\ast_2}\xi} and
{\isrenamevar{e^\ast_2}{e_2}{\xi'}}, whence
{\isrenamevar{e'_2}{e_2}{\xi\circ\xi'}}.
\item By Lemma~\ref{renamelift},
$\lift(v,\tau')=\lift(v,\renamevar{(\tau^\ast)}\xi)=%
\langle\renamevar{(e^\ast_v)}\xi,\renamevar{(\theta^\ast)}\xi\rangle$,
which is
$\langle\renamevar{(\renamevar{e_v}{\xi'})}\xi,%
\renamevar{(\renamevar\theta{\xi'})}\xi\rangle$.  In other words,
$\lift(v,\tau')=\langle\renamevar{e_v}{\xi\circ\xi'},%
\renamevar\theta{\xi\circ\xi'}\rangle$.

Also, $\dom(\xi'_0)\cap\dom(\tau_0)=\emptyset$, hence no variable
occurring in $e_u$ is in the domain of $\xi_0$ by Lemma~\ref{liftdom}.
Therefore,
$e'_u=\renamevar{e_u}\xi=\renamevar{(\renamevar{e_u}{\xi'})}\xi=%
\renamevar{e_u}{\xi\circ\xi'}$, whence
{\isrenamevar{e'}e{\xi\circ\xi'}}.
\end{itemize}
Thus $\xi\circ\xi'$ is the desired renaming of variables.
\end{enumerate}
\end{proof}

\begin{lemma}\label{liftcommv1}
Let $t:A$, $f:[A\to A]$, $e,e':E$, $i,i':\nat$ and
$\rho,\sigma,\sigma',\theta,\theta'$ be substitution pairs for $A$
satisfying the following relations.
\begin{eqnarray*}
\lift(t,\rho) & = & \langle e,\sigma\rangle\\
\liftv1(f,\sigma) & = & \langle v^1_i,\theta\rangle\\
\liftv1(f,\rho) & = & \langle v^1_{i'},\sigma'\rangle\\
\lift(t,\sigma') & = & \langle e',\theta'\rangle
\end{eqnarray*}
Then there is a renaming of variables $\xi$ for $\theta$ such that:
\begin{enumerate}[(i)]
\item\label{domxi1} $\xi_0=\idn$ and
$\dom(\xi_1)\cap\dom(\rho_1)=\emptyset$;
\item\label{replxi1} {\isrenamevar{\theta'}\theta\xi},
{\isrenamevar{e'}e\xi} and $i'=\xi_1(i)$.
\end{enumerate}
\end{lemma}
\begin{proof}
By induction on $t$ according to $\less$.
\begin{enumerate}
\item $t$ is minimal for $\less$.
\begin{enumerate}
\item $t=\underline n$: then $e=n$, $\sigma=\rho$ whence trivially
$i'=i$, $\sigma'=\theta$ and also $e'=e$ and $\theta'=\theta$;
thus $\xi=\langle\idn,\idn\rangle$ trivially
satisfies~(\ref{domxi1}) and~(\ref{replxi1}).
\item otherwise $\lift(t,\rho)=\liftv0(t,\rho)$.  By
Lemma~\ref{liftv0commv1}, $\langle\idn,\idn\rangle$ also satisfies
both~(\ref{domxi1}) and~(\ref{replxi1}).
\end{enumerate}
\item $t=g(t_0)$ with $g:[A\to A]$.
\begin{enumerate}
\item $g$ is $-_A$: again analogous to the corresponding case in the
proof of Lemma~\ref{liftcommv0}.
\item $g$ is $\cdot^n$ with $n$ is closed: analogous.
\item otherwise $e=v^1_j(e_0)$ with
$\lift(t_0,\rho)=\langle e_0,\tau\rangle$ and
$\liftv1(g,\tau)=\langle v^1_j,\sigma\rangle$;
also $e'=v^1_{j'}(e'_0)$ with $\lift(t,\sigma')=\langle
e'_0,\tau'\rangle$ and $\liftv1(g,\tau')=\langle v^1_{j'},\theta'\rangle$.
\end{enumerate}
\item $t_1=u\star v$ with $\star\in\{+,-,\times,/\}$: then there are
expressions $e_u$ and $e_v$ and a substitution pair $\tau$ such that
$\lift(u,\rho)=\langle e_u,\tau\rangle$, $\lift(v,\tau)=\langle
e_v,\sigma\rangle$ and $e=e_u\star e_v$.  Also, there are expressions
$e'_u$ and $e'_v$ and a substitution pair $\tau'$ such that
$\lift(u,\sigma')=\langle e'_u,\tau'\rangle$, $\lift(v,\tau')=\langle
e'_v,\theta'\rangle$ and $e'=e'_u\star e'_v$.

If we define $\liftv1(f,\tau)=\langle v^1_{i^\ast},\tau^\ast\rangle$
and $\liftv1(g,\tau^\ast)=\langle v^1_{j^\ast},\theta^\ast\rangle$,
we can draw the picture on Figure~\ref{fig:liftcommv1}.
\begin{figure}[htb]
\[\xymatrix{
 & \rho \ar[dl]_{t_0} \ar[dr]^{f} \\
 \tau \ar[d]_{g} \ar[dr]^{f} & & \sigma' \ar[d]_{t_0} \\
 \sigma \ar[d]_{f} & \tau^\ast \ar@{.>}[r]^{\xi} \ar[d]_{g}
 & \tau' \ar[d]_{g} \\
 \theta \ar@{.>}[r]^{\xi'} & \theta^\ast \ar@{.>}[r]^{\xi} & \theta' 
}\]
\caption{Last case of the proof of Lemma~\ref{liftcommv1}.  An arrow
from $\rho$ to $\rho'$ with label $t$ means that $\rho'$ is obtained
by either $\lift(t,\rho)$ or $\liftv1(t,\rho)$.}
\label{fig:liftcommv1}
\end{figure}
Again, by induction hypothesis, there is a renaming of variables $\xi$
for $\tau^\ast$ satisfying~(\ref{domxi1}) such that $i'=\xi_1(i^\ast)$,
{\isrenamevar{e'_0}{e_0}\xi} and {\isrenamevar{\tau'}{\tau^\ast}\xi}.
By Lemma~\ref{liftv1commv1}, there is a renaming of variables
$\xi'$ for $\theta$ such that $\xi'_0=\idn$,
$\dom(\xi'_1)\cap\dom(\tau_1)=\emptyset$, $i^\ast=\xi'_1(i)$,
$j^\ast=\xi'_1(j)$ and {\isrenamevar{\theta^\ast}\theta{\xi'}}.

Once again, $\xi\circ\xi'$ is the desired renaming of variables.
\begin{itemize}
\item Trivially, $\xi_0\circ\xi'_0=\idn$; since $\rho\subseteq\tau$,
if $v^1_k\in\dom(\rho_1)$ then $\xi_1(k)=k$ and $\xi'_1(k)=k$, hence
$\dom(\xi_1\circ\xi'_1)\cap\dom(\rho_1)=\emptyset$.
\item By hypothesis, $i'=\xi_1(i^\ast)$ and $i^\ast=\xi'(i)$, whence
$i'=\xi\circ\xi'(i)$.
\item $\lift(g(t_0),\tau^\ast)=\langle v^1_{j^\ast}(e_0),\theta^\ast\rangle$:
since $\tau\subseteq\tau^\ast$ by Lemma~\ref{liftv1incl},
$\lift(t_0,\tau^\ast)=\langle e_0,\tau^\ast\rangle$ due to
Lemma~\ref{liftidempotent}; the rest follows by definition
of $\liftv1(g,\tau^\ast)$.  Similar considerations show that
$\lift(g(t_0),\tau')=\langle v^1_{j'}(e'_0),\theta'\rangle$.

By Lemma~\ref{renamelift},
$\lift(g(t_0),\tau')=\lift(g(e_0),\renamevar{\tau^\ast}\xi)=%
\langle\renamevar{v^1_{j^\ast}(e_0)}\xi,\renamevar{\theta^\ast}\xi\rangle$;
hence {\isrenamevar{\theta'}{\theta^\ast}\xi} and
{\isrenamevar{v^1_{j'}(e'_0)}{v^1_{j^\ast}(e_0)}\xi}.

From {\isrenamevar{\theta'}{\theta^\ast}\xi} and
{\isrenamevar{\theta^\ast}\theta{\xi'}} we can deduce that
{\isrenamevar{\theta'}\theta{\xi\circ\xi'}}.

Finally we show that {\isrenamevar{v^1_{j'}(e'_0)}{v^1_j(e_0)}{\xi\circ\xi'}}.
Obviously, $\renamevar{v^1_j(e_0)}{\xi\circ\xi'}=%
v^1_{\xi\circ\xi'(j)}(\renamevar{e_0}{\xi\circ\xi'})$.
From {\isrenamevar{v^1_{j'}(e'_0)}{v^1_{j^\ast}(e_0)}\xi} we get first
that $j'=\xi_1(j^\ast)$, and since $j^\ast=\xi'_1(j)$ we conclude that
$\xi_1\circ\xi'_1(j)=j'$.  Also {\isrenamevar{e'_0}{e_0}\xi}; since
$\dom(\xi'_0)\cap\dom(\tau_0)=\emptyset$, no variable occurring in
$e_0$ is in the domain of $\xi'_0$ by Lemma~\ref{liftdom}.
Therefore,
$e'_0=\renamevar{e_0}\xi=\renamevar{(\renamevar{e_0}{\xi'})}\xi=%
\renamevar{e_0}{\xi\circ\xi'}$.
\end{itemize}
Thus $\xi\circ\xi'$ is the desired renaming of variables.
\end{enumerate}
\end{proof}

\begin{lemma}\label{liftcommutes}
Let $t_1,t_2:A$, $e_1,e'_1,e_2,e'_2:E$ and
$\rho,\sigma,\sigma',\theta,\theta'$ be substitution pairs for $A$
satisfying the following relations.
\begin{eqnarray*}
\lift(t_1,\rho) & = & \langle e_1,\sigma\rangle\\
\lift(t_2,\sigma) & = & \langle e_2,\theta\rangle\\
\lift(t_2,\rho) & = & \langle e'_2,\sigma'\rangle\\
\lift(t_1,\sigma') & = & \langle e'_1,\theta'\rangle
\end{eqnarray*}
Then there is a renaming of variables $\xi$ for $\theta$ such that:
\begin{enumerate}[(i)]
\item\label{domxi} $\dom(\xi_i)\cap\dom(\rho_i)=\emptyset$ for $i=1,2$;
\item\label{replxi} {\isrenamevar{\theta'}\theta\xi} and
{\isrenamevar{e'_i}{e_i}\xi} for $i=1,2$.
\end{enumerate}
\end{lemma}
\begin{proof}
By induction on $t_1$ with respect to $\less$; most cases can be dealt
with as in the proof of Lemma~\ref{liftcommv0}.  First, notice that the
only steps where use was made of the fact
that $e_2$ was obtained from $t_2$ by $\liftv0$ were the cases where $t_1$
was minimal for $\less$ and not of the form $\underline n$ or $t_1=f(t)$.
In all other cases, proving that $\dom(\xi_0)\cap\dom(\rho_0)=\emptyset$
made use only of the induction hypothesis, so that replacing $0$ by $1$
in that subproof yields a valid proof of
$\dom(\xi_1)\cap\dom(\rho_1)=\emptyset$ from the induction hypothesis.
Therefore, we only need to consider those two cases.

If $t_1$ is minimal for $\less$ and not of the form $\underline n$,
then $\lift(t_1,\rho)=\liftv0(t_1,\rho)$ and
$\lift(t_1,\sigma')=\liftv0(t_1,\sigma')$.  Lemma~\ref{liftcommv0}
then allows us to conclude that there is a renaming of variables $\xi$
for $\theta'$ such that $\xi_1=\idn$,
$\dom(\xi_0)\cap\dom(\rho_0)=\emptyset$ and
{\isrenamevar\theta{\theta'}\xi} and {\isrenamevar{e_i}{e'_i}\xi} for $i=1,2$.
Then $\xi^{-1}$ satisfies our requirements: since $\xi_0$ is a permutation,
$\dom(\xi^{-1}_0)=\dom(\xi_0)$ and therefore
$\dom(\xi^{-1}_0)\cap\dom(\rho_0)=\emptyset$; $\dom(\idn)=\emptyset$, hence
$\dom(\xi^{-1}_0)\cap\dom(\rho_0)=\emptyset$;
{\isrenamevar{\theta'}\theta{\xi^{-1}}} follows from the second case in the
proof of Lemma~\ref{renamevarsequiv}; and {\isrenamevar{e'_i}{e_i}{\xi^{-1}}}
follows from the definition of inverse.

If $t_1=f(t)$, then there are expressions $e,e'$, natural numbers $i,i'$
and substitution pairs $\tau,\tau'$ such that
$\lift(t,\rho)=\langle e,\tau\rangle$,
$\liftv1(f,\tau)=\langle v^1_i,\sigma\rangle$, $e_1=v^1_i(e)$,
$\lift(t,\sigma')=\langle e',\tau'\rangle$,
$\liftv1(f,\tau')=\langle v^1_{i'},\theta\rangle$ and $e'_1=v^1_{i'}(e')$.

We once again let $\lift(t_2,\tau)=\langle e^\ast_2,\tau^\ast\rangle$ and
$\liftv1(f,\tau^\ast)=\langle v^1_{i^\ast},\theta^\ast\rangle$ (see
Figure~\ref{fig:liftcommutes}).
\begin{figure}[htb]
\[\xymatrix{
 & \rho \ar[dl]_{t} \ar[dr]^{t_2} \\
 \tau \ar[d]_{f} \ar[dr]^{t_2} & & \sigma' \ar[d]_{t} \\
 \sigma \ar[d]_{t_2} & \tau^\ast \ar@{.>}[r]^{\xi} \ar[d]_{f}
 & \tau' \ar[d]_{f} \\
 \theta \ar@{.>}[r]^{\xi'} & \theta^\ast \ar@{.>}[r]^{\xi} & \theta' 
}\]
\caption{Last case of the proof of Lemma~\ref{liftcommutes}.  An arrow
from $\rho$ to $\rho'$ with label $t$ means that $\rho'$ is obtained
by either $\lift(t,\rho)$ or $\liftv1(t,\rho)$.}
\label{fig:liftcommutes}
\end{figure}
By induction hypothesis there is a renaming of variables $\xi$ for
$\tau^\ast$ such that~(\ref{domxi}) holds,
{\isrenamevar{\tau'}{\tau^\ast}\xi}, {\isrenamevar{e'}e\xi} and
{\isrenamevar{e'_2}{e_2}\xi}.  By Lemma~\ref{liftcommv1} there is a
renaming of variables $\xi'$ for $\theta$ such that $\xi'_0=\idn$,
$\dom(\xi'_1)\cap\dom(\tau_1)=\emptyset$,
{\isrenamevar{\theta^\ast}\theta{\xi'}},
{\isrenamevar{e^\ast_2}{e_2}{\xi'}} and $i^\ast=\xi'_1(i)$.

In a similar way to the proof of the last case of Lemma~\ref{liftcommv1},
we can conclude that {\isrenamevar{\theta'}\theta{\xi\circ\xi'}},
$i'=\xi_1(i^\ast)$ and {\isrenamevar{e'}e{\xi\circ\xi'}}.
Then trivially {\isrenamevar{v^1_{i'}(e')}{v^1_i(e)}{\xi\circ\xi'}}.
Finally, if $v^i_k\in\dom(\rho_i)$, then $v^i_k\in\dom(\tau_i)$,
hence $\xi'_i(k)=k$, $\xi_i\circ\xi'_i(k)=\xi(k)=k$ and
$\dom(\xi_i)\cap\dom(\rho_i)=\emptyset$.
\end{proof}

\begin{lemma}\label{liftaddpred}
Let $t_1,t_2,t_3:A$, $e_1,e_2,e'_2,e_3,e'_3:E$ and
$\rho,\sigma,\sigma',\theta,\theta'$ be substitution pairs for $A$
satisfying the following relations.
\begin{eqnarray*}
\lift(t_2,\emptyset) & = & \langle e_2,\sigma\rangle\\
\lift(t_3,\sigma) & = & \langle e_3,\theta\rangle\\
\lift(t_1,\emptyset) & = & \langle e_1,\rho\rangle\\
\lift(t_2,\rho) & = & \langle e'_2,\sigma'\rangle\\
\lift(t_3,\sigma') & = & \langle e'_3,\theta'\rangle
\end{eqnarray*}
Then there exist a substitution pair $\tau$ and a renaming of variables
$\xi$ for $\tau$ such that:
\begin{enumerate}[(i)]
\item $\theta\subseteq\tau$;
\item {\isrenamevar{\theta'}\tau\xi} and {\isrenamevar{e'_i}{e_i}\xi} for $i=2,3$.
\end{enumerate}
\end{lemma}
\begin{proof}
Define $\lift(t_1,\sigma)=\langle e^\ast_1,\rho^\ast\rangle$.
By Lemma~\ref{liftcommutes}, there is a renaming of variables $\xi$ for
$\tau^\ast$ such that {\isrenamevar{\sigma'}{\rho^\ast}\xi},
{\isrenamevar{e_1}{e^\ast_1}\xi} and {\isrenamevar{e'_2}{e_2}\xi}.

Define $\lift(t_3,\rho^\ast)=\langle e^\ast_3,\theta^\ast\rangle$.
Then, by Lemma~\ref{renamelift}, {\isrenamevar{e'_3}{e^\ast_3}\xi}
and {\isrenamevar{\theta'}{\theta^\ast}\xi}.

Now take $\lift(t_1,\theta)=\langle e'_1,\tau\rangle$.
By Lemma~\ref{liftcommutes} there is a renaming of variables $\xi'$ for
$\tau$ such that also ${\isrenamevar{e^\ast_3}{e_3}{\xi'}}$ and
{\isrenamevar{\theta^\ast}\tau{\xi'}}.

It then follows that $\xi\circ\xi'$ is the desired renaming of variables.

The situation is graphically depicted in Figure~\ref{fig:liftaddpred}.
\begin{figure}[htb]
\[\xymatrix{
 & \emptyset \ar[dl]_{t_2} \ar[dr]^{t_1} \\
 \sigma \ar[d]_{t_3} \ar[dr]^{t_1} & & \rho \ar[d]_{t_2} \\
 \theta \ar[d]_{t_1} & \rho^\ast \ar@{.>}[r]^{\xi} \ar[d]_{t_3}
 & \sigma' \ar[d]_{t_3} \\
 \tau \ar@{.>}[r]^{\xi'} & \theta^\ast \ar@{.>}[r]^{\xi} & \theta'
}\]
\caption{Proof of Lemma~\ref{liftaddpred}.  An arrow from $\rho$ to
$\rho'$ with label $t$ means that $\rho'$ is obtained by $\lift(t,\rho)$.}
\label{fig:liftaddpred}
\end{figure}
\end{proof}

\section{Completeness of {\rational}: rings}\label{normalization}

We now move to the Coq portion of the tactic.
We identify a subset of the set of expressions which we call
\emph{normal forms}.  Then we define a normalization function {\N}
that assigns to any expression $e$ an expression $\N(e)$ in normal
form.  In this section we prove the fundamental properties of this function.

In this first stage we will forget about division and work only with
the subset of expressions interpretable in a ring.
Section~\ref{fields} discusses how these definitions can be
generalized for fields and how the results we show here can be
transposed to the general case.

\subsection{Normal forms}

The intuition for the normal forms is as follows.  A normal form is a
polynomial where all terms have been multiplied, so that it is written
as a sum of products of atomic terms (integers, variables of arity $0$ or
variables of arity $1$ applied to a normal form).  To guarantee uniqueness
of the normal form we further require that these terms be ordered.

We begin by defining monomials and polynomials.  These can be seen in
a precise way as lists of expressions; hence we can identify the
subset of monomials and polynomials whose lists are ordered.  These
will be our normal forms.

\begin{definition}\label{def:prenf}
The sets of \emph{monomials} and \emph{polynomials} are inductively
defined by the following grammar:
\begin{eqnarray*}
M' & ::= & \Z \alt \V_0\times M' \alt \V_1(P')\times M' \\
P' & ::= & \Z \alt M'+P'
\end{eqnarray*}
\end{definition}
Notice that $M'\subseteq E$ and $P'\subseteq E$.

\begin{definition}\label{def:monabs}
For every $m:M'$ we define:
\begin{enumerate}
\item the \emph{list of variables} of $m$, $|m|$;
\item the \emph{coefficient} of $m$, $\|m\|$.
\end{enumerate}
\[\begin{array}{rclcrcl}
|\cdot| : M' & \to & \mathrm{list}(E) & & \|\cdot\| : M' & \to & \Z \\
 i & \mapsto & [] & & i & \mapsto & i \\
 v^0_i\times m & \mapsto & v^0_i :: m & & v^0_i\times m & \mapsto & \|m\| \\
 v^1_i(p')\times m & \mapsto & v^1_i(p') :: m
  & & v^1_i(p')\times m & \mapsto & \|m\|
\end{array}\]
\end{definition}

\begin{definition}\label{def:polabs}
For every $p:P'$ we define the \emph{list of monomials} of $p$ as follows:
\begin{eqnarray*}
|\cdot| : P' & \to & \mathrm{list}(\mathrm{list}(E)) \\
 i & \mapsto & [] \\
 m+p & \mapsto & |m| :: |p|
\end{eqnarray*}
\end{definition}

\begin{definition}\label{def:prenftonf}
We define the following mutually recursive predicates over $M'$ and $P'$.
\begin{enumerate}[(i)]
\item $\ord_{M'}(m)$ holds if $|m|$ is an ordered list (with the ordering
from Definition~\ref{defn:exprorder}).
%\footnote{Saying that $|m|$ is
%ordered is different from saying that the expressions in $m$ occur in order,
%since integers are smaller than variables of type $1$.}
\item $\ord_{P'}(p)$ holds if $|p|$ is ordered (using the
lexicographic ordering for each element of $|p|$) and $|p|$ does not
contain repetitions.
\item $\wf_{M'}$ is defined recursively as follows:
\begin{itemize}
\item $\wf_{M'}(i)$ holds for $i\neq 0$;
\item $\wf_{M'}(v^0_i\times m)\iff\wf_{M'}(m)$;
\item $\wf_{M'}(v^1_i(p)\times m)\iff(\wf_{M'}(m)\wedge\nf_{P'}(p))$.
\end{itemize}
\item $\nf_{M'}(m)$ holds if either $m=0$ or $\wf_{M'}(m)\wedge\ord_{M'}(m)$
holds.
\item $\wf_{P'}$ is defined recursively as follows:
\begin{itemize}
\item $\wf_{P'}(i)$ holds for $i\in\Z$;
\item $\wf_{P'}(m+p)\iff(\wf_{P'}(p)\wedge\nf_{M'}(m))$.
\end{itemize}
\item $\nf_{P'}(p)$ holds iff $\wf_{P'}(p)\wedge\ord_{P'}(p)$ holds.
\end{enumerate}
\end{definition}

\begin{definition}\label{defn:nf}
The set $M$ of monomials \emph{in normal form} is defined as
\[M = \{m:M' \alt \nf_{M'}(m)\}.\]
The set $P$ of polynomials \emph{in normal form}, or simply of normal forms,
is defined as \[P = \{p:P' \alt \nf_{P'}(p)\}.\]
\end{definition}

We will use the definitions of $\|m\|$, $|m|$ and $|p|$ above also for
monomials and polynomials in normal form.

\begin{definition}\label{defn:coeff}
Let $m:M$ and $p:P$.  The \emph{coefficient} of $m$ in $p$, denoted by
{\coeff mp}, is recursively defined as follows.
\begin{eqnarray*}
\coeff{\underline{\ }}\cdot : P\times M & \to & \Z\\
 i, j & \mapsto & i \\
 i, m & \mapsto & 0 \\
 m'+p, m & \mapsto & \left\{%
\begin{array}{lll}\|m'\| & \mbox{if $|m'|=|m|$} \\ 
 \coeff mp & \mbox{else}\end{array}\right.
\end{eqnarray*}
The first clause in this definition may look somewhat strange; the idea is
that we only look at $|m|$ to define {\coeff mp}, and thus any integer
should correspond to the independent term of $p$.
\end{definition}

The reason for introducing the operations $|\cdot|$ and $\|\cdot\|$ is
that they totally characterize normal forms.

\begin{lemma}\label{monchar}
Let $m,m':M$.  Then $m=m'\iff \|m\|=\|m'\| \wedge |m|=|m'|$.
\end{lemma}
\begin{proof}
Straightforward.  The direct implication is immediate, since both $|\cdot|$
and $\|\cdot\|$ are functions.  For the converse, assume that $|m|=|m'|$.
Then $m$ and $m'$ share the same variables (counting repetitions); since
they are ordered, these must appear in exactly the same order.  If we
also assume that $\|m\|=\|m'\|$, then their integer coefficient is also
the same, whence $m=m'$.
\end{proof}

\begin{lemma}\label{polchar}
Let $p,q:P$.  Then $p=q\iff \forall m:M.\coeff pm=\coeff qm$.
\end{lemma}
\begin{proof}
The direct implication is again immediate, since {\coeff{\underline{\ }}\cdot}
is a function.  For the converse, assume that $\coeff pm=\coeff qm$ for
all $m$; then every monomial occurring in $p$ also occurs in $q$ with the
same coefficient, and reciprocally.  But $|p|$ and $|q|$ are both ordered,
hence $p=q$.
\end{proof}

\subsection{The normalization function}\label{normfn}

The normalization function is not defined directly, but by means of a
number of auxiliary functions.  This makes it easier to state and prove
results about it.

\begin{definition}\label{defn:multMZ} {\multMZ} is defined by:
\begin{eqnarray*}
\multMZ : M \times \Z & \to & M \\
 m, 0 & \mapsto & 0 \\
 i, j & \mapsto & i\times j \\
 x\times m, j & \mapsto & x\times (m\multMZ j)
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{multMZ}
{\multMZ} satisfies the following properties:
\begin{enumerate}[(i)]
\item $\|m\multMZ i\|=\|m\|\times i$;
\item $|m\multMZ 0|=[]$;
\item $|m\multMZ i|=|m|$ for $i\neq 0$;
\item {\multMZ} is well defined, i.e.\ its output is in $M$;
\item if $m\intrel t$, then $m\multMZ i\intrel t\times i$.
\end{enumerate}
\end{proposition}
\begin{proof}
The first two properties follow directly from the definition; for the third,
just notice that, if $i\neq 0$, then $\times_{M \Z}$ translates to the
identity on the list of variables of $m$.
From these three properties, the fourth then follows: if $i=0$, then this
is a consequence of $0:M$; else only the coefficient of $m$ changes, hence
$\nf_{M'}(m\multMZ i)$ still holds.
The last property is proved by straightforward induction (Coq checked).
\end{proof}

\begin{definition}\label{defn:multMV} {\multMV} is defined by:
\begin{eqnarray*}
\multMV : M \times (\V_0\cup\V_1(P)) & \to & M \\
 i, y & \mapsto & (y\times 1)\multMZ i \\
 x\times m, y & \mapsto & 
\left\{\begin{array}{ll}x\times(m\multMV y) & x<_E y \\
 y\times x\times m & \mbox{otherwise}\end{array}\right.
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{multMV}
{\multMV} satisfies the following properties:
\begin{enumerate}[(i)]
\item $\|m\multMV x\|=\|m\|$;
\item if $m\neq 0$, then $|m\multMV x|$ is the sorted
list obtained from $m$ and $x$;
\item {\multMV} is well defined;
\item if $m\intrel t$ and $x\intrel t'$, then
$m\multMV x\intrel t\times t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
If $m=0$ these properties follow from Proposition~\ref{multMZ}, so assume
$m\neq 0$.
The first property follows directly from the definition; for the
second, just notice that {\multMV} translates to the
algorithm of straight insertion on lists.
From these two properties, the third then follows: the elements of $|m|$
are not changed by {\multMV} and $x$ is either $v^0_i$ or
$v^1_i(p)$ with $p:P$, hence $m\multMV x$ satisfies $\wf_{M'}$.
Also the correctness of straight insertion guarantees that
$|m\multMV x|$ is sorted if $m$ is.
The last property is again proved by straightforward induction using
Proposition~\ref{multMZ} (Coq checked).
\end{proof}

\begin{definition}\label{defn:multMM} {\multMM} is defined by:
\begin{eqnarray*}
\multMM : M \times M & \to & M \\
 i, m & \mapsto & m\multMZ i \\
 x\times m, m' & \mapsto & (m\multMM m')\multMV x
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{multMM}
{\multMM} satisfies the following properties:
\begin{enumerate}[(i)]
\item $\|m\multMM m'\|=\|m\|\times\|m'\|$;
\item if $m,m'\neq 0$, then $|m\multMM m'|$ is the sorted
list obtained by merging $|m|$ with $|m'|$;
\item {\multMM} is well defined;
\item if $m\intrel t$ and $m'\intrel t'$, then
$m\multMM m'\intrel t\times t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
The first property again follows directly from the definition of {\multMM}
and Propositions~\ref{multMZ} and~\ref{multMV}.
The second holds because {\multMM} simply implements straight insertion sort
on the list obtained by appending $|m|$ to $|m'|$.
From these two the third property follows, and the last one is again proved by
straightforward induction using Propositions~\ref{multMZ} and~\ref{multMV}
(Coq checked).
\end{proof}

\bigskip

The next function is of a different nature: it takes two monomials $m$
and $m'$ that coincide as lists (that is, $|m|=|m'|$) and returns the
monomial obtained by adding them.  Obviously this is only well defined
under the assumption that $|m|=|m'|$.

\begin{definition}\label{defn:plusMM} Let $\Delta_M$ denote the subset of
$M\times M$ defined by
\[\Delta_M=\{\langle m,m'\rangle\in M\times M \alt |m|=|m'|\}.\]
{\plusMM} is defined as follows.
\begin{eqnarray*}
\plusMM : \Delta_M & \to & M \\
 i, j & \mapsto & i+j \\
 x\times m, x\times m' & \mapsto & (m\plusMM m')\multMV x
\end{eqnarray*}
Notice that this definition covers all cases because of the structure of
$\Delta_M$.
\end{definition}

\begin{proposition}\label{plusMM}
{\plusMM} satisfies the following properties:
\begin{enumerate}[(i)]
\item $\|m\plusMM m'\|=\|m\|+\|m'\|$;
\item $m\plusMM m'=0$ if $\|m\|+\|m'\|=0$;
\item $|m\plusMM m'|=|m|=|m'|$ otherwise;
\item {\plusMM} is well defined;
\item if $m\intrel t$ and $m'\intrel t'$, then $m\plusMM m'\intrel t+t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
The first condition is straightforward from the definition of {\plusMM}.
The second and third follow from this definition and
Proposition~\ref{multMV}; and from these the fourth is a direct consequence.
Finally the last point is again proved by induction using
Proposition~\ref{multMV} (Coq checked).
\end{proof}

\bigskip

In the sequence we will need the following notations.
We will denote by $<_M$ the lexicographic ordering on $\mathrm{list}(E)$
obtained from $<_E$.
Given two lists $l,w$ of expressions, we write $l\subseteq w$ to mean
that $l$ is a sublist of $w$, i.e.\ all elements of $l$ occur in $w$ and
in the same order.

\begin{definition}\label{defn:plusPM} {\plusPM} is defined as follows.
\begin{eqnarray*}
\plusPM : P\times M & \to & P \\
 i, j & \mapsto & i+j \\
 i, m & \mapsto & m+i \\
 m+p, j & \mapsto & m+(p\plusPM j) \\
 m+p, m' & \mapsto &
\left\{\begin{array}{ll} m+(p\plusPM m') & |m|<_M|m'| \\
 p\plusPM(m\plusMM m') & |m|=|m'| \\
 m'+m+p & \mbox{else}\end{array}\right.
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{plusPM}
{\plusPM} satisfies the following properties:
\begin{enumerate}[(i)]
\item if $|m|=|m'|$, then $\coeff{m'}{p\plusPM m}=\coeff{m'}p+\|m\|$;
\item if $|m|\neq|m'|$, then $\coeff{m'}{p\plusPM m}=\coeff{m'}p$;
\item $|p\plusPM m|\subseteq l$, where $l$ is the list obtained by appending
$|m|$ to $|p|$ and sorting the result;
\item {\plusPM} is well defined;
\item if $p\intrel t$ and $m'\intrel t'$, then $p\plusPM m'\intrel t+t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
The two first properties follow from the definition of {\plusPM} (in the
first case also appealing to Proposition~\ref{plusMM}).

The third property is proved by induction.  The basis is trivial; for
the induction step we need to consider two cases.  Let $p=m'+p'$; if
$|m|\neq|m'|$, then the algorithm reduces again to straight insertion
of an element in a list (since the only difference is in the case
$|m|=|m'|$).  If $|m|=|m'|$, then $|m'\plusMM m|=|m|$ by
Proposition~\ref{plusMM}, so we can use the induction hypothesis to
conclude that this call returns a $q$ such that $|q|$ is the straight
insertion of $|m'|$ in $|p'|$, which is $|m'|::|p'|$ (since $m'+p:P$),
and this is a sublist of $|m|::|m|::|p'|$, which would be the outcome of
the straight insertion of $|m|$ in $|m'|::|p'|$ (since $|m|=|m'|$).
Hence also in this case the thesis holds.

The fourth property is a consequence of the previous ones, since a sublist
of an ordered list is ordered.  The last property is proved by induction
(Coq checked).
\end{proof}

\begin{definition}\label{defn:plusPP} {\plusPP} is defined as follows.
\begin{eqnarray*}
\plusPP : P\times P & \to & P \\
 i, q & \mapsto & q\plusPM i \\
 m+p, q & \mapsto & (p\plusPP q)\plusPM m
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{plusPP}
{\plusPP} satisfies the following properties:
\begin{enumerate}[(i)]
\item for all $m$, $\coeff m{p\plusPP q}=\coeff mp+\coeff mq$;
\item $|p\plusPP q|\subseteq l$, where $l$ is the list obtained by appending
$|q|$ to $|p|$ and sorting the result;
\item {\plusPP} is well defined;
\item if $p\intrel t$ and $q\intrel t'$, then $p\plusPP q\intrel t+t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
The first property is proved by induction on $p$.  If $p=i$, then
either $m=j$ for some $j\in\Z$ and the thesis holds by the first part
of Proposition~\ref{plusPM} or else $|m|\neq|i|$ and the thesis holds
by the second part of Proposition~\ref{plusPM}.  If $p=m'+p'$, then
by induction hypothesis $\coeff m{p'\plusPP q}=\coeff m{p'}+\coeff mq$
and there are two cases.  If $|m'|=|m|$, then $\coeff mp=\|m'\|$ and
$\coeff m{p'}=0$ (since $|p|$ does not have repetitions), and by the
first part of Proposition~\ref{plusPM}
$\coeff m{(p'\plusPP q)\plusPM m'}%\
=\coeff m{p'\plusPP q}+\|m'\|%
=\coeff m{p'}+\coeff mq+\|m'\|%
=\coeff mq+\|m'\|%
=\coeff mq+\coeff mp$.
If $|m'|\neq|m|$ then $\coeff mp=\coeff m{p'}$ and by the second part
of Proposition~\ref{plusPM}
$\coeff m{(p'\plusPP q)\plusPM m'}%
=\coeff m{p'}+\coeff mq=%
\coeff mp+\coeff mq$.

The second and third properties are proved from
Proposition~\ref{plusPM} by straightforward induction.  The last
property is similar (Coq checked).
\end{proof}

\bigskip

The last operations have no analogue in sorting algorithms.
We will use juxtaposition to denote the sorted merge of two lists.

\begin{definition}\label{defn:multPM} {\multPM} is defined as follows.
\begin{eqnarray*}
\multPM : P\times M & \to & P \\
 i, m' & \mapsto & 0\plusPM (m'\multMZ i) \\
 m+p, m' & \mapsto & (p\multPM m')\plusPM (m\multMM m')
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{multPM}
{\multPM} satisfies the following properties:
\begin{enumerate}[(i)]
\item for all $m$, $\coeff m{p\multPM m'}=\coeff{m^\ast}p\times\|m'\|$ if
there is\footnote{Notice that there may exist at most one such $m^\ast$.}
an $m^\ast$ such that $|m|=|m^\ast||m'|$ and $0$ otherwise;
\item $p\multPM 0=0$;
\item if $m'\neq 0$, then $|p\multPM m'|$ is the sorted list whose
elements are obtained by appending $|m'|$ to each element of $p$ and
sorting the result;
\item {\multPM} is well defined;
\item if $p\intrel t$ and $m'\intrel t'$, then $p\multPM m'\intrel t\times t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
The first property is a straightforward induction on $p$ using
Propositions~\ref{plusPM} and~\ref{multMM} (notice that {\multMZ} is
a special case of {\multMM}).  The second property can be proved directly
by induction, since $0\multMM0=0$ and $0\plusPM 0$.

The third property is also proved by induction on $p$.  If $p=i$
then the result follows from Propositions~\ref{multMZ} and~\ref{plusPM}.
If $p=m+p'$, then $(m+p')\multPM m'=(p\multPM m')\plusPM (m\multMM m')$.
Since $|p'|$ does not have any repeated elements, by induction hypothesis
neither does $|p\multPM m'|$ (since its elements are the image of the
elements of $|p|$ via an injective function).  By Proposition~\ref{multMM},
$|m\multMM m'|$ is the sorted list whose elements are either in $|m|$ or in
$|m'|$, and this does not occur in $|p\multPM m'|$.  Hence the thesis
follows from Proposition~\ref{plusPM}.

The fourth property is straightforward since {\multMM} and {\plusPM} are
both well defined.  The last one is again proved by induction on $p$
(Coq checked).
\end{proof}

\begin{definition}\label{defn:multPP} {\multPP} is defined as follows.
\begin{eqnarray*}
\multPP : P\times P & \to & P \\
 i, q & \mapsto & q\multPM i \\
 m+p, q & \mapsto & (q\multPM m)\plusPP (p\multPP q)
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{multPP}
{\multPP} satisfies the following properties:
\begin{enumerate}[(i)]
\item for all $m\in M$, $\coeff m{p\multPP q}=\sum\coeff{m_1}p\coeff{m_2}q$,
where the sum ranges over all $m_1\in|p|\cup\{1\}$ and
$m_2\in|q|\cup\{1\}$ for which $|m|=|m_1||m_2|$;
\item {\multPP} is well defined;
\item if $p\intrel t$ and $q\intrel t'$, then $p\multPP q\intrel t\times t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
We prove the first property by induction.  If $p=i$ then the result follows
from Proposition~\ref{multPM}, since then $m_1$ can only be $1$ ($|p|$ is the
empty list).
If $p=m'+p'$, then by Proposition~\ref{plusPP}
$\coeff m{(q\multPM m')\plusPP(p'\multPP q)}=%
\coeff m{q\multPM m'}+\coeff m{p'\multPP q}$; the result now follows from
induction hypothesis and Proposition~\ref{multPM}.

The second property is trivial; the last is proved by induction (Coq checked).
\end{proof}

\begin{definition}\label{defn:NormR}
The normalization function $\N$ is defined as follows, where $E^\ast$ denotes
the type of expressions that do not use division.
\begin{eqnarray*}
\N : E^\ast & \to & P \\
 i & \mapsto & i \\
 v^0_i & \mapsto & v^0_i\times 1+0 \\
 e+f & \mapsto & \N(e)\plusPP\N(f) \\
 e\times f& \mapsto & \N(e)\multPP\N(f) \\
 v^1_i(e) & \mapsto & v^1_i(\N(e))\times 1+0
\end{eqnarray*}
\end{definition}
\begin{proposition}\label{NormR} {\N} satisfies the following properties:
\begin{enumerate}[(i)]
\item {\N} is well defined;
\item\label{normpresint} if $e\intrel t$ then $\N(e)\intrel t$.
\end{enumerate}
\end{proposition}
\begin{proof}
The first part is a straightforward induction.  $\N(i)$ and $\N(v^0_i)$ are
in normal form by definition of $P$; $\N(e+f)$ and $\N(e\times f)$ are
in normal form by induction hypothesis and Propositions~\ref{plusPP}
and~\ref{multPP}; and $\N(v^1_i(e))$ is in normal form by definition of $P$
and induction hypothesis.

The second property is a straightforward induction (Coq checked).
\end{proof}

\begin{corollary}\label{correctness}
Let $t,t':A$ and define $\langle e,\rho\rangle=\lift(t,\emptyset)$ and
$\langle e',\sigma\rangle=\lift(t',\rho)$.  If $\N(e)=\N(e')$, then
$t=_A t'$ can be proved from the ring axioms and unfolding of
the definitions of $-$, {\zring} and {\nexp}.
\end{corollary}
\begin{proof}
Let $e$ and $e'$ be as defined above and suppose that $\N(e)=\N(e')$.
By Lemma~\ref{liftcorrect}, both $e\intrel t$ and $e'\intrel t'$.
By Proposition~\ref{NormR} also $\N(e)\intrel t$ and $\N(e')\intrel t'$.
Since $\N(e)=\N(e')$, we have that $\N(e)\intrel t$ and $\N(e)\intrel t'$,
whence $t=_A t'$ by Lemma~\ref{intrelfunction}.
\end{proof}

\subsection{Properties of $P$ and $\N$}\label{PNprops}

We now show that $\langle P,\plusPP,0,\multPP,1\rangle$ is a ring
(w.r.t.\ syntactic equality).
This will be essential later on, where we will use the properties
of these operations without comment.

\begin{lemma}\label{multMMcomm}
For all $m,m':M$, $m\multMM m'=m'\multMM m$.
\end{lemma}
\begin{proof}
By Lemma~\ref{monchar}, it is sufficient to show that 
$\|m\multMM m'\|=\|m'\multMM m\|$ and $|m\multMM m'|=|m'\multMM m|$.  But
both of these are consequences of Proposition~\ref{multMM}, commutativity
of addition and uniqueness of sort.
\end{proof}

\begin{lemma}\label{plusPPprops}
Let $p,q,r:P$.  Then the following hold:
\begin{enumerate}[(i)]
\item $p\plusPP0=p$
\item $p\plusPP (q\plusPP r)=(p\plusPP q)\plusPP r$
\item $p\plusPP q=q\plusPP p$
\item $p\plusPP (p\multPP(-1))=0$
\end{enumerate}
\end{lemma}
\begin{proof} Remember that $p=q\iff \forall m:M.\coeff pm=\coeff qm$
(Proposition~\ref{polchar}).  Let $m:M$ be arbitrary; then, by
Proposition~\ref{plusPP}, the following are immediate:
\begin{enumerate}[(i)]
\item 
 $\coeff m{p\plusPP0}%
=\coeff mp+\coeff m0%
=\coeff mp$
\item
 $\coeff m{p\plusPP (q\plusPP r)}%
=\coeff mp+\coeff m{q\plusPP r}%
=\coeff mp+\coeff mq+\coeff mr%
=\coeff m{p\plusPP q}+\coeff mr%
=\coeff m{(p\plusPP q)\plusPP r}$.
\item
 $\coeff m{p\plusPP q}%
=\coeff mp+\coeff mq%
=\coeff mq+\coeff mp%
=\coeff m{q\plusPP p}$.
\item Given $m:M$,
$\coeff m{p\plusPP(p\multPP(-1))}=\coeff mp+\coeff m{p\multPP(-1)}$, so
it suffices to show that $\coeff m{p\multPP(-1)}=-\coeff mp$.
By Proposition~\ref{multPP},
$\coeff m{p\multPP(-1)}=\sum\coeff{m_1}p\coeff{m_2}{-1}$.
Now in this sum $m_2$ can only assume value $1$, whence $m_1=m$ and
the previous expression reduces to $\coeff mp(-1)=-\coeff mp$.
\end{enumerate}
\end{proof}

\begin{lemma}\label{multPPprops}
Let $p,q,r:P$.  Then the following hold:
\begin{enumerate}[(i)]
\item $p\multPP0=0$
\item $p\multPP1=p$
\item $p\multPP (q\multPP r)=(p\multPP q)\multPP r$
\item $p\multPP q=q\multPP p$
\end{enumerate}
\end{lemma}
\begin{proof} Again we appeal to Proposition~\ref{polchar}.

We begin by proving commutativity.  For any $m:M$,
$\coeff m{p\multPP q}=%
\sum\coeff{m_1}p\coeff{m_2}q=%
\sum\coeff{m_2}q\coeff{m_1}p=%
\coeff m{q\multPP p}$
where the sums range over all $m_1\in|p|\cup\{1\}$ and $m_2\in|q|\cup\{1\}$
for which $|m|=|m_1||m_2|$; the equalities hold by Proposition~\ref{multPP}.

$p\multPP0=0$ is proved straightforwardly by induction, using
Proposition~\ref{multPM}.

Next, $p\multPP1=1\multPP p=p\multPM1$.  For any $m:M$, $|m|=|m||1|$, hence
by Proposition~\ref{multPM}
$\coeff m{p\multPM1}=\coeff mp\times\|1\|=\coeff mp$, hence $p\multPP1=p$.

Finally, for associativity, we again obtain from Proposition~\ref{multPP}
that, for $m:M$,
$\coeff m{p\multPP(q\multPP r)}=%
\sum\coeff{m_1}p\coeff{m_2}{q\multPP r}=%
\sum\coeff{m_1}p\left(\sum\coeff{m_2^1}q\coeff{m_2^2}r\right)=%
\sum\coeff{m_1}p\coeff{m_2^1}q\coeff{m_2^2}r$

The last expression is completely symmetric on $p$, $q$ and $r$, since the
last sum in fact ranges over all $m_1$, $m_2^1$ and $m_2^2$ such that
$|m|=|m_1||m_2^1||m_2^2|$ with $m_1\in|p|\cup\{1\}$, $m_2^1\in|q|\cup\{1\}$
and $m_2^2\in|r|\cup\{1\}$.
Therefore, from associativity and commutativity of sums and products of
integers, we immediately get that
$\coeff m{p\multPP(q\multPP r)}=\coeff m{r\multPP(p\multPP q)}$, and
applying commutativity of {\multPP} twice we get the desired result.
\end{proof}

\begin{lemma}\label{multPPdistplusPP} Let $p,q,r:P$.  Then
$p\multPP(q\plusPP r)=(p\multPP q)\plusPP(p\multPP r)$.
\end{lemma}
\begin{proof}
Once again, if $m:M$ then
$\coeff m{p\multPP(q\plusPP r)}=%
\sum\coeff{m_1}p\coeff{m_2}{q\plusPP r}=%
\sum\coeff{m_1}p(\coeff{m_2}q+\coeff{m_2}r)=%
\sum\coeff{m_1}p\coeff{m_2}q+\sum\coeff{m_1}p\coeff{m_2}r=%
\coeff m{(p\multPP q)\plusPP(p\multPP r)}$
\end{proof}

\begin{lemma}\label{NormRmon} Let $m:M\setminus\Z$ and $p:P$.
Then $\N(m)=m+0$ and $\N(p)=p$.
\end{lemma}
\begin{proof}
We prove both results by simultaneous induction on $m$ and $p$.

If $m=v^0_i\times i$ then
$\N(m)%
=\N(v^0_i)\multPP\N(i)%
=(v^0_i\times1+0)\multPP i%
=v^0_i\times i+0%
=m+0$,
where the last-but-one equality is simply computation of {\multPP}.
If $m=v^1_i(p)\times i$ then
$\N(m)%
=\N(v^1_i(p))\multPP\N(i)%
=(v^1_i(\N(p))\times1+0)\multPP i%
=v^1_i(p)\times i+0%
=m+0$,
where the last-but-one equality follows from computation and induction
hypothesis for $p$.

If $m=v^0_i\times m'$, then notice first that $m'\multMM(v^0_i\times 1)=m$:
$\|m'\multMM(v^0_i\times1)\|=\|m'\|\times1=\|m'\|$ by Proposition~\ref{multMM}
and $|m'\multMM(v^0_i\times 1)|$ is the list obtained by inserting $v^0_i$ at
the right position in $|m'|$, which is by definition $|m|$ (since this list is
sorted), hence by Lemma~\ref{monchar} the result holds.
Using this fact, the induction hypothesis and Lemmas~\ref{multPPprops}
and~\ref{plusPPprops}, we see that the thesis holds.
\begin{eqnarray*}
\N(m) & = & \N(v^0_i)\multPP\N(m') \\
 & = & (v^0_i\times1+0)\multPP(m'+0) \\
 & = & (m'+0)\multPM(v^0_i\times1)\plusPP(0\multPP(e'+0))\\
 & = & (m'+0)\multPM(v^0_i\times1)\plusPP0\\
 & = & (m'+0)\multPM(v^0_i\times1)\\
 & = & 0\multPM(v^0_i\times 1)\plusPM m'\multMM(v^0_i\times1)\\
 & = & (0\plusPM(v^0_i\times1)\multMZ0)\plusPM m'\multMM(v^0_i\times1)\\
 & = & (0\plusPM0)\plusPM(m'\multMM(v\times 1))\\
 & = & 0\plusPM m\\
 & = & m+0.
\end{eqnarray*}
If $m=v^1_i(p)\times m'$, then by induction hypothesis
$\N(v^1_i(p))%
=v^1_i(\N(p))\times1+0%
=v^1_i(p)+0$
and the previous chain of equalities holds replacing $v^1_i(p)+0$ for
$v^0_i$ everywhere.

Now suppose that $p$ is an integer; then $\N(p)=p$ by definition.
Else take $p=m+q$; by induction hypothesis $\N(q)=q$ and $\N(m)=m+0$, hence
\begin{eqnarray*}
\N(m+q) & = & \N(m)\plusPP\N(q) \\
 & = & (m+0)\plusPP q\\
 & = & (0\plusPP q)\plusPM m\\
 & = & q\plusPM m
\end{eqnarray*}
by Lemma~\ref{plusPPprops}; but by definition of $P$, $|m|$ cannot occur
in $|q|$ and must be smaller (w.r.t.\ $<_M$), hence the last expression
reduces to $m+q$, or $p$.
\end{proof}

\begin{corollary}\label{NormRidemp} $\N$ is idempotent, i.e.,\ for every
$e:E^\ast$, $\N(\N(e))=\N(e)$.
\end{corollary}
\begin{proof}
Since $\N(e):P$, the previous lemma is applicable, yielding the result.
\end{proof}

\subsection{The substitution lemma}

In this subsection, we show that the following ``substitution lemma''
holds: if, in two expressions that normalize to the same, some variables
get uniformly renamed, then the resulting expressions also normalize to
the same term.

This is proven in two steps.
\begin{lemma}\label{substlemmaaux} Let $e:E$ and $\xi$ be a renaming of
variables.  Then $\N(\renamevar e\xi)=\N(\renamevar{\N(e)}\xi)$.
\end{lemma}
\begin{proof}
By induction on $e$.

Suppose $e=i$; then
$\N(\renamevar{\N(i)}\xi)%
=\N(\renamevar i\xi)%
=\N(i)%
=\N(\renamevar i\xi)$.

Now let $e=v^0_i$.  Then
$\N(\renamevar{\N(e)}\xi)%
=\N(\renamevar{(v^0_i\times1+0)}\xi)%
=\N(v^0_{\xi_0(i)}\times1+0)%
=\N(v^0_{\xi_0(i)})\multPP1\plusPP0%
=\N(v^0_{\xi_0(i)}))%
=\N(\renamevar{(v^0_i)}\xi)$
by virtue of Propositions~\ref{plusPPprops} and~\ref{multPPprops}.

If $e=v^1_i(e')$, then we use the induction hypothesis to show that
\begin{eqnarray*}
\N(\renamevar{\N(v^1_i(e'))}\xi)
 & = & \N(\renamevar{(v^1_i(\N(e'))\times1+0)}\xi)\\
 & = & \N(v^1_{\xi_1(i)}(\renamevar{\N(e')}\xi)\times1+0) \\
 & = & \N(v^1_{\xi_1(i)}(\renamevar{\N(e')}\xi))\multPP1\plusPP0 \\
 & = & \N(v^1_{\xi_1(i)}(\renamevar{\N(e')}\xi)) \\
 & = & v^1_{\xi_1(i)}(\N(\renamevar{\N(e')}\xi))\times1+0 \\
 & \stackrel{IH}= & v^1_{\xi_1(i)}(\N(\renamevar{e'}\xi))\times1+0 \\
 & = & \N(v^1_{\xi_1(i)}(\renamevar{e'}\xi)) \\
 & = & \N(\renamevar{(v^1_i(e'))}\xi)
\end{eqnarray*}

For the case $e=e_1\star e_2$, with $\star=+,\times$, we need besides the
induction hypothesis the equality
\begin{equation}\label{eqn:nvsstar}
\N(\renamevar{(p\star q)}\xi)=\N(\renamevar{(p\starPP q)}\xi)
\end{equation}
for all $p,q:P$.  The proof of this is included in the Appendix; its use is
marked here by $\ast$.
\begin{eqnarray*}
\N(\renamevar{\N(e_1\star e_2)}\xi)
 & = & \N(\renamevar{(\N(e_1)\starPP\N(e_2))}\xi) \\
 & \stackrel\ast= & \N(\renamevar{(\N(e_1)\star\N(e_2))}\xi) \\
 & = & \N(\renamevar{\N(e_1)}\xi\star\renamevar{\N(e_2)}\xi) \\
 & = & \N(\renamevar{\N(e_1)}\xi)\starPP\N(\renamevar{\N(e_2)}\xi) \\
 & \stackrel{IH}= & \N(\renamevar{e_1}\xi)\starPP\N(\renamevar{e_2}\xi) \\
 & = & \N(\renamevar{e_1}\xi\star\renamevar{e_2}\xi) \\
 & = & \N(\renamevar{(e_1\star e_2)}\xi) \\
\end{eqnarray*}
\end{proof}

With this we can prove the main result of this section:

\begin{theorem}\label{substlemma}
Let $e,e':E$ be expressions such that $\N(e)=\N(e')$ and let $\xi$ be
a renaming of variables.  Then $\N(\renamevar e\xi)=\N(\renamevar{e'}\xi)$.
\end{theorem}
\begin{proof}
According to the previous lemma,
$\N(\renamevar e\xi)%
=\N(\renamevar{N(e)}\xi)%
=\N(\renamevar{N(e')}\xi)%
=\N(\renamevar{e'}\xi)$.
\end{proof}

\subsection{Completeness}

We are now ready to state our main result.

\begin{theorem}\label{completeness}
Let $t,t':A$ be such that the equality $t=_A t'$ can be proved (in the
sense of Definition~\ref{defn:proof}) only from the ring axioms and
unfolding of the definitions of $-$, $\zring$ and $\nexp$ in $t$ and
$t'$.  Define $\langle e,\rho\rangle=\lift(t,\emptyset)$ and
$\langle e',\sigma\rangle=\lift(t',\rho)$.  Then $\N(e)=\N(e')$.
\end{theorem}

The proof of this is split in several stages.

\begin{lemma}\label{unfolding}
Let $t,t':A$ be terms such that $t'$ is obtained from $t$ by unfolding
the definitions of $-$, $\zring$ and $\cdot^n$ ($n$ closed) in $t$.
Let $\lift(t,\rho)=\langle e,\sigma\rangle$ and
$\lift(t',\rho)=\langle e',\sigma'\rangle$.  Then $\sigma=\sigma'$ and
$\N(e)=\N(e')$.
\end{lemma}
\begin{proof}
For $-$ and $\cdot^n$ this is immediate,
since terms using these constructors are lifted to expressions using the
corresponding abbreviations whose definition coincides with those of $-$
and $\cdot^n$.

For $\zring$ the proof is by induction\footnote{In this paragraph we
write $+_\Z$ to emphasize the distinction between addition of integers and
addition of expressions.}: $\underline0$ unfolds
to $0$, both of which are lifted to $0$; $\underline{n+1}$ is lifted to
$n+_\Z1$, which is in normal form, whereas $\underline{n}+1$ is lifted
to $n+1$ which normalizes to $\N(n)\plusPP1=n+_\Z1$; finally,
$\underline{n-1}$ is lifted to $n+1\times(-1)$, which normalizes to
$\N(n)\plusPP1\multPP(-1)=n-_\Z1$.
\end{proof}

\begin{lemma}\label{axioms}
Let $t,t':A$ be such that $t=_A t'$ is an instance of one of the axioms
\axiom{Set_1}, \axiom{SG}, \axiom{M_1}, \axiom{M_2}, \axiom{G_1}, \axiom{G_2},
\axiom{AG} or \axiom{R_i} with $1\leq i\leq5$.
Define
$\langle e,\tau\rangle=\lift(t,\emptyset)$ and
$\langle e',\tau'\rangle=\lift(t',\tau)$.  Then $\N(e)=\N(e')$.
\end{lemma}
\begin{proof}
All these proofs are very similar, being a consequence of
Lemmas~\ref{plusPPprops} and~\ref{multPPprops}.  We detail a few:
\begin{description}
\item[\axiom{Set_1}] Then $t=t'$; by Lemma~\ref{liftidempotent}
$e'=e$, and obviously $\N(e)=\N(e)$.
\item[\axiom{SG}] Then $t=(t_1+t_2)+t_3$ and $t'=t_1+(t_2+t_3)$.
Let $\lift(t_1,\emptyset)=\langle e_1,\rho\rangle$,
$\lift(t_2,\rho)=\langle e_2,\sigma\rangle$ and
$\lift(t_3,\sigma)=\langle e_3,\theta\rangle$.  Then
$\lift(t_1+t_2,\emptyset)=\langle e_1+e_2,\sigma\rangle$ and
$\lift((t_1+t_2)+t_3,\emptyset)=\langle (e_1+e_2)+e_3,\theta\rangle$.

Furthermore, since $\rho\subseteq\sigma\subseteq\theta$ by
Lemma~\ref{liftincl}, Lemma~\ref{liftidempotent} yields
$\lift(t_1,\theta)=\langle e_1,\theta\rangle$,
$\lift(t_2,\theta)=\langle e_2,\theta\rangle$ and
$\lift(t_3,\sigma)=\langle e_3,\theta\rangle$, whence
$\lift(t_2+t_3,\theta)=\langle e_2+e_3,\theta\rangle$ and
$\lift(t_1+(t_2+t_3),\theta)=\langle e_1+(e_2+e_3),\theta\rangle$.

Then
$\N((e_1+e_2)+e_3)%
=\N(e_1+e_2)\plusPP\N(e_3)%
=(\N(e_1)\plusPP\N(e_2))\plusPP\N(e_3)%
=\N(e_1)\plusPP(\N(e_2)\plusPP\N(e_3))%
=\N(e_1)\plusPP\N(e_2+e_3)%
=\N(e_1+(e_2+e_3))$.
\item[\axiom{G_1}] Then $t=t_1+(-t_1)$ and $t'=0$.  Let
$\lift(t_1,\emptyset)=\langle e_1,\rho\rangle$; then by
Lemma~\ref{liftidempotent} also $\lift(t_1,\rho)=\langle e_1,\rho\rangle$,
hence $e=e_1+(e_1\times(-1))$; by definition
$\lift(0,\rho)=\langle 0,\rho\rangle$, so $e'=0$.

Now
$\N(e_1+(e_1\times(-1)))%
=\N(e_1)\plusPP(\N(e_1)\multPP(-1))%
=0%
=\N(0)$,
according to Lemma~\ref{plusPPprops}.
\item[\axiom{R_5}] In this case $t=t_1\times(t_2+t_3)$ and
$t'=(t_1\times t_2)+(t_1\times t_3)$.  Reasoning in an analogous way to
the case of \axiom{SG} above, we conclude that $e=e_1\times(e_2+e_3)$ and
$e'=(e_1\times e_2)+(e_1\times e_3)$.  By Lemma~\ref{multPPprops},
$\N(e_1\times(e_2+e_3))%
=\N(e_1)\multPP(\N(e_2)\plusPP\N(e_3))%
=\N(e_1)\multPP\N(e_2)\plusPP\N(e_1)\multPP\N(e_3)%
=\N((e_1\times e_2)+(e_1\times e_3))$.
\end{description}
\end{proof}

\begin{lemma}\label{set2}
Let $t_1,t_2:A$ be such that, if $\langle e_1,\rho\rangle=\lift(t_1,\emptyset)$
and $\langle e_2,\sigma\rangle=\lift(t_2,\rho)$, then $\N(e_1)=\N(e_2)$.
Define $\langle e'_2,\sigma'\rangle=\lift(t_2,\emptyset)$
and $\langle e'_1,\rho'\rangle=\lift(t_1,\sigma')$.  Then $\N(e'_1)=\N(e'_2)$.
\end{lemma}
\begin{proof}
Let $e_1,e'_1,e_2$ and $e'_2$ be as given.  By
Lemma~\ref{liftcommutes} there is a renaming of variables $\xi$ such
that {\isrenamevar{e'_i}{e_i}\xi} for $i=1,2$; but then
\[\N(e'_1)=\N\left(\renamevar{e_1}\xi\right)=%
\N\left(\renamevar{e_2}\xi\right)=\N(e'_2)\] using the hypothesis
$\N(e_1)=\N(e_2)$ and Theorem~\ref{substlemma}.
\end{proof}

\begin{lemma}\label{set3}
Let $t_1,t_2,t_3:A$ and define
\[\begin{array}{ccc}
\langle e_1,\rho\rangle=\lift(t_1,\emptyset)
 & & \langle e'_2,\sigma'\rangle=\lift(t_2,\emptyset) \\
\langle e_2,\sigma\rangle=\lift(t_2,\rho)
 & & \langle e'_3,\theta'\rangle=\lift(t_3,\sigma')
\end{array}\]
Assume that $\N(e_1)=\N(e_2)$ and $\N(e'_2)=\N(e'_3)$.  Define
$\langle e_3,\theta\rangle=\lift(t_3,\rho)$.  Then $\N(e_1)=\N(e_3)$.
\end{lemma}
\begin{proof}
Let $e_1,e_2,e'_2,e_3$ and $e'_3$ be as given and define
$\langle e''_3,\theta''\rangle=\lift(t_3,\sigma)$.
By Lemma~\ref{liftaddpred},
there exists a renaming of variables $\xi$ such that
$\isrenamevar{e''_3}{e'_3}\xi$ and $\isrenamevar{e_2}{e'_2}\xi$.
By Lemma~\ref{liftcommutes} there is another renaming of variables $\xi'$
such that $\isrenamevar{e_3}{e''_3}{\xi'}$ and
$\dom(\xi'_i)\cap\dom(\rho_i)=\emptyset$ (see Figure~\ref{fig:set3}).
\begin{figure}[htb]
\[\xymatrix{
 & \emptyset \ar[dl]_{t_2} \ar[dr]^{t_1} \\
 \sigma' \ar[d]_{t_3}\ar@{.>}[dr]^{\xi} & & \rho \ar[dl]_{t_2} \ar[d]_{t_3} \\
 \theta'\ar@{.>}[dr]^{\xi} & \sigma \ar[d]_{t_3} & \theta \\
 & \theta''\ar@{.>}[ur]^{\xi'}
}\]
\caption{Proof of Lemma~\ref{set3}}\label{fig:set3}
\end{figure}
Then,
\[\N(e_3)%
=\N\left(\renamevar{e''_3}{\xi'}\right)%
=\N\left(\renamevar{e'_3}{\xi'\circ\xi}\right)%
=\N\left(\renamevar{e'_2}{\xi'\circ\xi}\right)%
=\N\left(\renamevar{e_2}{\xi'}\right)%
=\N\left(\renamevar{e_1}{\xi'}\right)%
=\N(e_1)\]
using the hypotheses $\N(e_1)=\N(e_2)$ and $\N(e'_2)=\N(e'_3)$ together with 
Theorem~\ref{substlemma} and the equalities above stated.  The last equality
follows from the fact that $\dom(\xi'_i)\cap\dom(\rho_i)=\emptyset$: by
Lemma~\ref{liftdom} every variable $v^i_k$ occurring in $e_1$ is in
$\dom(\rho_i)$, so {\isrenamevar{e_1}{e_1}{\xi'}}.
\end{proof}

\begin{lemma}\label{set4}
Let $t_1,t_2:A$ be such that, if $\langle e_1,\rho\rangle=\lift(t_1,\emptyset)$
and $\langle e_2,\sigma\rangle=\lift(t_2,\rho)$, then $\N(e_1)=\N(e_2)$.
Let $f:[A\to A]$ be other than $\cdot^n$ with $n$ closed and define
$\langle e'_1,\rho'\rangle=\lift(f(t_1),\emptyset)$ and
$\langle e'_2,\sigma'\rangle=\lift(f(t_2),\emptyset)$.
Then $\N(e'_1)=\N(e'_2)$.
\end{lemma}
\begin{proof}
We have to consider two cases.  If $f$ is the unary inverse ($-$), then
immediately $e'_1=-e_1$, $\rho'=\rho$ and hence $e'_2=-e_2$; in this case,
$\N(e'_1)=\N(-e_1)=\N(e_1\times(-1))=\N(e_1)\multPP(-1)=\N(e_2)\multPP(-1)=%
\N(e_2\times(-1))=\N(-e_2)=\N(e'_2)$.

Else, $e'_1=v^1_i(e_1)$ with $\liftv1(f,\rho)=\langle v^1_i,\rho'\rangle$
and $e'_2=v^1_i(e''_2)$, with $\lift(t_2,\rho')=\langle e''_2,\sigma'\rangle$
(since by Lemma~\ref{liftincl} $\rho'\subseteq\sigma'$, $\sigma'_1(v^1_i)=f$
and thus $\liftv1(f,\sigma')=\langle v^1_i,\sigma\rangle$).

By Lemma~\ref{liftcommv1} there is a renaming of variables $\xi$ such
that {\isrenamevar{e''_2}{e_2}\xi} and $\dom(\xi_i)\cap\dom(\rho_i)=\emptyset$.
Hence
$\N(e'_2)%
=\N(v^1_i(e''_2))%
=v^1_i(\N(e''_2))\times1+0%
=v^1_i(\N(\renamevar{e_2}\xi))\times1+0%
=v^1_i(\N(\renamevar{e_1}\xi))\times1+0%
=v^1_i(\N(e_1))\times1+0%
=\N(v^1_i(e_1))%
=\N(e'_1)$,
using Theorem~\ref{substlemma} together with the assumption
$\N(e_1)=\N(e_2)$ and the fact that {\isrenamevar{e_1}{e_1}\xi} by
virtue of Lemma~\ref{liftdom} and
$\dom(\xi_i)\cap\dom(\rho_i)=\emptyset$.
\end{proof}

\begin{lemma}\label{set5}
Let $t_1,t_2,t_3,t_4:A$ and define
\[\begin{array}{ccc}
\langle e_1,\rho\rangle=\lift(t_1,\emptyset)
 & & \langle e_3,\theta\rangle=\lift(t_3,\emptyset) \\
\langle e_2,\sigma\rangle=\lift(t_2,\rho)
 & & \langle e_4,\tau\rangle=\lift(t_4,\theta)
\end{array}\]
Assume that $\N(e_1)=\N(e_2)$ and $\N(e_3)=\N(e_4)$ and let
\[\begin{array}{ccc}
\langle e,\gamma\rangle=\lift(t_1\star t_3)
 & & \langle e',\gamma'\rangle=\lift(t_2\star t_4)
\end{array}\]
where $\star$ is $+$ or $\times$.  Then $\N(e)=\N(e')$.
\end{lemma}
\begin{proof}
By definition of {\lift}, $e=e_1\star e'_3$ with
$\langle e'_3,\gamma\rangle=\lift(t_3,\rho)$.
Also, $e'=e'_2\star e'_4$, with
$\langle e'_2,\gamma''\rangle=\lift(t_2,\gamma)$
and $\langle e'_4,\gamma'\rangle=\lift(t_4,\gamma'')$.


Take $\lift(t_4,\gamma)=\langle e''_4,\gamma'''\rangle$.

According to Lemma~\ref{liftaddpred}, there exists a renaming of variables
$\xi$ such that {\isrenamevar{e'_3}{e_3}\xi} and
{\isrenamevar{e''_4}{e_4}\xi}.  By Lemma~\ref{liftcommutes}, there
is a renaming of variables $\xi'$ such that {\isrenamevar{e'_2}{e_2}{\xi'}}
and $\dom(\xi'_i)\cap\dom(\rho_i)=\emptyset$ (and hence
{\isrenamevar{e_1}{e_1}{\xi'}} due to Lemma~\ref{liftdom}).
Again by Lemma~\ref{liftcommutes}, there exists a renaming of
variables $\xi''$ such that {\isrenamevar{e'_4}{e''_4}{\xi''}}
and $\dom(\xi''_i)\cap\dom(\gamma_i)=\emptyset$ (so that
{\isrenamevar{e'_3}{e'_3}{\xi''}}) (see Figure~\ref{fig:set5}).
\begin{figure}
\[\xymatrix{
 & & \emptyset \ar[dl]_{t_1} \ar[dr]^{t_3} \\
 & \rho \ar[dl]_{t_2} \ar[dr]^{t_3}
 & & \theta \ar[dr]^{t_4} \ar@{.>}[dl]_{\xi} \\
 \sigma \ar@{.>}[dr]^{\xi'}
 & & \gamma \ar[dl]_{t_2} \ar[dr]^{t_4}
 & & \tau \ar@{.>}[dl]_{\xi} \\
 & \gamma'' \ar[dr]^{t^4}
 & & \gamma''' \ar@{.>}[dl]_{\xi''} \\
 & & \gamma'
}\]
\caption{Proof of Lemma~\ref{set5}}\label{fig:set5}
\end{figure}

Then,
$\N(e')%
=\N(e'_2\star e'_4)%
=\N(e'_2)\starPP\N(e'_4)%
=\N(\renamevar{e_2}{\xi'})\starPP\N(\renamevar{e''_4}{\xi''})%
=\N(\renamevar{e_2}{\xi'})\starPP\N(\renamevar{e_4}{\xi''\circ\xi})%
=\N(\renamevar{e_1}{\xi'})\starPP\N(\renamevar{e_3}{\xi''\circ\xi})%
=\N(e_1)\starPP\N(\renamevar{e'_3}{\xi''})=\N(e_1)\starPP\N(e'_3)%
=\N(e_1\star e'_3)%
=\N(e)$
using the hypotheses and Theorem~\ref{substlemma}.
\end{proof}

\begin{definition}\label{defn:normalproof} A \emph{normal proof} of $t=_A t'$
is a proof of $t=_A t'$ where \axiom{Set_4} is never applied with
$\cdot^n$ ($n$ closed) and \axiom{Set_5} is never applied with $-$.
\end{definition}

\begin{lemma}\label{normalproof} Suppose that $t=_A t'$ can be proved
only from the ring axioms and unfolding of the definitions of $-$,
$\zring$ and $\nexp$ in $t$ and $t'$.  Then there exists a normal proof
of $t=_A t'$.
\end{lemma}
\begin{proof}
By induction on the length of the proof of $t=_A t'$.  The only non-trivial
cases are those when the last axiom to be applied is \axiom{Set_4} with
$\cdot^n$ ($n$ closed) or \axiom{Set_5} with $-$.

Suppose we prove $t_1^n=_A t_2^n$ from $t_1=_A t_2$ using
\axiom{Set_4}.  We proceed by induction.  If $n=0$, then we can
replace the whole proof by $(\axiom{Set_1}\ 1)$, and folding produces
$t_1^0=_A t_2^0$.  If $n=k+1$, we first find a normal proof of
$t_1^k=_A t_2^k$ using the induction hypothesis (for $n$) and a normal
proof of $t_1=_A t_2$ using the induction hypothesis for the lemma.
Then we apply \axiom{Set_5} to get $t_1\times t_1^k=_A t_2\times
t_2^k$; folding $\cdot^{k+1}$ on the last equality produces the
desired proof.

Finally, if we prove $t_1-t_3=_A t_2-t_4$ from $t_1=_A t_2$ and
$t_3=_A t_4$ using \axiom{Set_5}, we first find normal proofs of
$t_1=_A t_2$ and $t_3=_A t_4$ (induction hypothesis), apply \axiom{Set_4}
to the latter to get $-t_3=_A -t_4$ and apply \axiom{Set_5} to get
$t_1+(-t_3)=_A t_2+(-t_4)$, which is the desired equality with the
definition of $-$ unfolded.
\end{proof}

\begin{theorem}\label{completenormal} 
Let $t,t':A$ and $e,e':E$ be as in Theorem~\ref{completeness} and
assume furthermore that there is a normal proof of the equality $t=_A t'$.
Then $\N(e)=\N(e')$.
\end{theorem}
\begin{proof}
By induction on the length of the normal proof of $t=_A t'$.

If $t=_A t'$ is an instance of one of the axioms \axiom{Set_1},
\axiom{SG}, \axiom{M_1}, \axiom{M_2}, \axiom{G_1}, \axiom{G_2},
\axiom{AG} or \axiom{R_i} with $1\leq i\leq5$, then by Lemma~\ref{axioms}
$\N(e)=\N(e')$.

Suppose $t=_A t'$ is proved by \axiom{Set_2} from $t'=_A t$.  Then we
can apply Lemma~\ref{set2} and the induction hypothesis to conclude that
the thesis holds.

Suppose $t=_A t'$ is proved by \axiom{Set_3} from $t=_A t_1$ and
$t_1=_A t'$.  Then we can apply Lemma~\ref{set3} and the induction
hypothesis to conclude that the thesis holds.

Suppose $t=_A t'$ is proved from $t_1=_A t_2$ by \axiom{Set_4} and
$f$ is not $\cdot^n$ with $n$ closed.  Then by Lemma~\ref{set4} and the
induction hypothesis the thesis holds.

Suppose $t=_A t'$ is proved from $t_1=_A t_2$ and $t_3=_A t_4$ by
\axiom{Set_5} and $f$ is not $-$.  Then by Lemma~\ref{set5} and the
induction hypothesis the thesis holds.

If $t_1$ and $t_2$ can be obtained from $t$ and $t'$ by unfolding the
definitions of $-$, $\cdot^n$ and $\zring$, then by Lemma~\ref{unfolding}
$\lift(t_1,\emptyset)=\lift(t,\emptyset)=\langle e,\rho\rangle$
and $\lift(t_2,\rho)=\lift(t',\rho)=\langle e',\sigma\rangle$, hence the
induction hypothesis immediately asserts the thesis.
\end{proof}

\bigskip

We are now ready to prove Theorem~\ref{completeness}.

\begin{proof}\emph{(Completeness Theorem~\ref{completeness})}
Assume there is a proof of $t=_A t'$.  By Lemma~\ref{normalproof} there is
also a normal proof of $t=_A t'$, so by Theorem~\ref{completenormal}
$\N(e)=\N(e')$.
\end{proof}

\section{Completeness of {\rational}: groups}\label{groups}

We now show how we can get a completeness theorem for groups similar
to Theorem~\ref{completeness}.  We begin by observing that the theory
developed above is not enough as is: if $G$ is a group, $a:G$ and
$v^0_0\intrel a$, then $v^0_0+v^0_0\intrel a+a$, but
$\N(v^0_0+v^0_0)=v^0_0\times 2+0$ which cannot be interpreted in $G$,
so part~(\ref{normpresint}) of Lemma~\ref{NormR} fails to hold.
Therefore we begin by extending the interpretation relation in a
conservative way.

\begin{definition}\label{defn:iter} Let $G$ be a group, $n:\Z$ and $a:G$.
Then {\iter na} is inductively defined as follows.
\begin{eqnarray}
\label{iter:0}
 \iter0a & := & 0\\
\label{iter:pos}
 \iter{(n+1)}a & := & \iter na+a, \mbox{ for $n\geq 0$}\\
\label{iter:neg}
 \iter{(n-1)}a & := & \iter na-a, \mbox{ for $n\leq 0$}
\end{eqnarray}
\end{definition}

\begin{proposition} Let $R$ be a ring.  Then, for all $n:\Z$ and $a:R$,
$\iter na=_R \underline n\times a$ is provable.
\end{proposition}
\begin{proof}
Straightforward induction.  If $n=0$ then $\iter na=0$ and $\underline0=0$,
so the equality reduces to $0\times a=_R 0$, which is provable.
Assume that $\iter na=_R\underline n\times a$ for $n\geq 0$; then
$\iter{(n+1)}a%
=\iter na+a%
=_R\underline n \times a+a%
=_R(\underline n+1) \times a%
=\underline{n+1} \times a$.
Similarly, if $n\leq 0$ then
$\iter{(n-1)}a%
=\iter na-a%
=_R\underline n \times a-a%
=_R(\underline n-1) \times a%
=\underline{n-1} \times a$.
\end{proof}

\begin{lemma}\label{intrel:iterprop} Let $\rho$ be a substitution pair for
a ring $A$.  The interpretation relation satisfies the following rule:
\begin{eqnarray*}
e\intrel t_1 \wedge \iter n{t_1}=_A t & \rightarrow & e\times n\intrel t
\end{eqnarray*}
where $n:\Z$.
\end{lemma}
\begin{proof} By the previous proposition
$\iter n{t_1}=_A \underline n\times t_1$ is provable, whence
$\underline n\times t_1=_A t$ is provable by hypothesis, \axiom{Set_2} and
\axiom{Set_3}.  Furthermore, $\underline n\intrel n$ by \axiom{Set_1}
and~(\ref{intrel:int}).  By hypothesis $e\intrel t_1$.  Therefore,
by~(\ref{intrel:mult}), $e\times n\intrel t$.
\end{proof}

\bigskip

Hence, this clause can be added to the inductive definition of
the interpretation relation without changing it when defined over a
ring or field but extending it in the case of groups.
We also need the case $k=0$ of~(\ref{intrel:int}).  That is, we
consider the interpretation relation as defined in
Definition~\ref{defn:intrel} extended with the two following clauses.
\begin{eqnarray}
\label{intrel:zero}
0=_G t & \rightarrow & 0\intrel t\\
\label{intrel:iter}
e\intrel t_1 \wedge \iter n{t_1}=_G t & \rightarrow & e\times n\intrel t
\end{eqnarray}
Notice that conditions~(\ref{intrel:inv}) and~(\ref{intrel:minus}) in
Lemma~(\ref{intrel:abbr}) can be proved from these clauses, so that
they also hold for groups with this extended interpretation relation.
This allows us to prove the following version of Lemma~\ref{intrelfunction}.

\begin{lemma}\label{intrelfunction:group} Let $e:E$, $t,t':G$ and $\rho$ be
a substitution pair for $G$ such that $e\intrel t$ and $e\intrel t'$.
Then $t=_G t'$.
\end{lemma}
\begin{proof} By induction on $\intrel$ (Coq checked).
\end{proof}

\bigskip

We can now prove the following results, which are group analogues of those
proved in Subsection~\ref{normfn}.

\begin{lemma}\label{groupprops}
Let $G$ be a group and $\rho$ be a substitution pair for $G$.
The auxiliary normalization functions satisfy the following properties.
\begin{enumerate}[(i)]
\item if $m\intrel t$ then $m\multMZ i\intrel\iter it$;
\item if $x\times m\intrel t$ then $m\multMV x\intrel t$;
\item if $m\times m'\intrel t$ or $m'\times m\intrel t$ then
$m\multMM m'\intrel t$;
\item if $m\intrel t$ and $m'\intrel t'$ then $m\plusMM m'\intrel t+t'$;
\item if $p\intrel t$ and $m'\intrel t'$ then $p\plusPM m'\intrel t+t'$;
\item if $p\intrel t$ and $p'\intrel t'$ then $p\plusPP p'\intrel t+t'$;
\item if $p\times m'\intrel t$ or $m'\times p\intrel t$ then
$p\multPM m'\intrel t$;
\item if $p\times p'\intrel t$ then $p\multPP p'\intrel t$.
\end{enumerate}
\end{lemma}
\begin{proof} By induction (Coq checked).
\end{proof}

\bigskip
Some of the hypotheses in the previous lemma may seem a bit strange.  The
problem is, we cannot say as before that ``if $m\intrel t$ and $m'\intrel t'$
then $m\multMM m'\intrel t\times t'$'' because in $G$ there is no
multiplication.  Hence, we replace this by the equivalent (in a ring) form
``if $m\times m'\intrel t$ then $m\multMM m'\intrel t$''.  However, this
is still not enough, since {\multMM} may switch the order of its arguments;
hence the disjunction in the actual lemma, which in fact says that one of
the arguments to {\multMM} is an integer.

Similar remarks hold for {\multPM}.  In the case of {\multMV} we already
know that the second argument is a variable, so one of the clauses of the
disjunction never holds and we can erase it.  As for {\multPP}, it will only
be called by $\N$ when a product appears in the original expression, which
is clearly impossible if this is the result of lifting a term in $G$;
it is however needed in the proof of the following lemma.

\begin{lemma}\label{NormG} Let $e:E$ and $t:G$.  If $e\intrel t$ then
$\N(e)\intrel t$.
\end{lemma}
\begin{proof}
By induction (Coq checked).  Since products in expressions can now only be
interpreted by means of~(\ref{intrel:iter}), the stronger hypotheses
in Lemma~\ref{groupprops} are seen to be satisfied by analyzing the proof
of $e\intrel t$.
\end{proof}

\begin{corollary}\label{correctness:group}
Let $t,t':G$ and define $\langle e,\rho\rangle=\lift(t,\emptyset)$ and
$\langle e',\sigma\rangle=\lift(t',\rho)$.  If $\N(e)=\N(e')$, then
$t=_G t'$ can be proved from the group axioms and unfolding of
the definition of $-$.
\end{corollary}
\begin{proof}
Let $e$ and $e'$ be as defined above and suppose that $\N(e)=\N(e')$.
By Lemma~\ref{liftcorrect}, both $e\intrel t$ and $e'\intrel t'$.
By Proposition~\ref{NormG} also $\N(e)\intrel t$ and $\N(e')\intrel t'$.
Since $\N(e)=\N(e')$, we have that $\N(e)\intrel t$ and $\N(e)\intrel t'$,
whence $t=_G t'$ by Lemma~\ref{intrelfunction:group}.
\end{proof}

\begin{theorem}\label{completeness:group}
Let $t,t':G$ be such that the equality $t=_G t'$ can be proved
only from the group axioms and unfolding of the definition of $-$.  Define
$\langle e,\rho\rangle=\lift(t,\emptyset)$ and
$\langle e',\sigma\rangle=\lift(t',\rho)$.  Then $\N(e)=\N(e')$.
\end{theorem}
\begin{proof}
Immediate from Theorem~\ref{completeness}, since the group axioms are a
proper subset of the ring axioms.
\end{proof}

\section{Partial completeness of {\rational}: fields}\label{fields}

We now try to extend the results in the previous sections to an
arbitrary field structure $A$.

We begin by extending the type of normal forms and the normalization function.

\begin{definition}\label{defn:NF} The set $F$ of field expressions in
normal form is the set $\{p/q|p,q\in P\}$.
\end{definition}

\begin{definition}\label{defn:plusFF} {\plusFF} is defined as follows.
\begin{eqnarray*}
\plusFF : F\times F & \to & F \\
 e_1/e_2, f_1/f_2 & \mapsto &
 \left((e_1\multPP f_2)\plusPP(e_2\multPP f_1)\right)/(e_2\multPP f_2)
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{plusFF}
{\plusFF} satisfies the following properties:
\begin{enumerate}[(i)]
\item {\plusFF} is well defined;
\item if $p\intrel t$ and $q\intrel t'$, then $p\plusFF q\intrel t+t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
Direct consequence of the definition of $F$ and Propositions~\ref{plusPP}
and~\ref{multPP} (the second is Coq checked).
\end{proof}

\begin{definition}\label{defn:multFF} {\multFF} is defined as follows.
\begin{eqnarray*}
\plusFF : F\times F & \to & F \\
 e_1/e_2, f_1/f_2 & \mapsto & (e_1\multPP f_1)/(e_2\multPP f_2)
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{multFF}
{\multFF} satisfies the following properties:
\begin{enumerate}[(i)]
\item {\multFF} is well defined;
\item if $p\intrel t$ and $q\intrel t'$, then $p\multFF q\intrel t\times t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
Direct consequence of the definition of $F$ and Proposition~\ref{multPP}
(the second is Coq checked).
\end{proof}

\begin{definition}\label{defn:divFF} {\divFF} is defined as follows.
\begin{eqnarray*}
\divFF : F\times F & \to & F \\
 e_1/e_2, f_1/f_2 & \mapsto & (e_1\multPP f_2)/(e_2\multPP f_1)
\end{eqnarray*}
\end{definition}

\begin{proposition}\label{divFF}
{\divFF} satisfies the following properties:
\begin{enumerate}[(i)]
\item {\divFF} is well defined;
\item if $p\intrel t$ and $q\intrel t'\neq 0$, then $p\divFF q\intrel t/t'$.
\end{enumerate}
\end{proposition}
\begin{proof}
Direct consequence of the definition of $F$ and Propositions~\ref{plusPP}
and~\ref{multPP} (the second is Coq checked).
\end{proof}

\begin{definition}\label{defn:NormF}
The normalization function $\NF$ is defined as follows.
\begin{eqnarray*}
\NF : E & \to & P \\
 i & \mapsto & i \\
 v^0_i & \mapsto & \left(v^0_i\times 1+0\right)/1 \\
 e+f & \mapsto & \NF(e)\plusFF\NF(f) \\
 e\times f& \mapsto & \NF(e)\multFF\NF(f) \\
 e/f& \mapsto & \NF(e)\divFF\NF(f) \\
 v^1_i(e) & \mapsto & \left(v^1_i(\NF(e))\times 1+0\right)/1
\end{eqnarray*}
\end{definition}
\begin{proposition}\label{NormF} {\NF} satisfies the following properties:
\begin{enumerate}[(i)]
\item {\NF} is well defined;
\item\label{NFpresint} if $e\intrel t$ then $\NF(e)\intrel t$.
\end{enumerate}
\end{proposition}
\begin{proof}
As before, the first part is a straightforward induction, similar to the proof
of Proposition~\ref{NormR}.

The second property is proved by induction (Coq checked); notice that the
hypothesis $e\intrel t$ is essential to guarantee that {\NF} will not
introduce divisions by zero (compare with the situation for groups).
\end{proof}

\subsection{Correctness and completeness}

Unfortunately, {\rational} as described above does not work so well
with this normalization function as before, as the following (simple)
example shows.

\begin{example} Let $x:A$ be a variable such that $x\neq 0$.
Then $x\times 1/x =_A1$ is a special case of axiom \axiom{F}.

A simple calculation shows that
\begin{eqnarray*}
\lift(x\times 1/x,\emptyset) & = &
  \langle v^0_0\times 1/v^0_0,[v^0_0:=x]\rangle \\
\lift(1,[v^0_0:=x]) & = &
  \langle 1,[v^0_0:=x]\rangle
\end{eqnarray*}
but $\NF(v^0_0\times 1/v^0_0)=(v^0\times 1+0)/(v^0\times 1+0)$, while
$\NF(1)=1$.
\end{example}

The problem lies in the algebraic structure of $F$ with the operations
above defined, and in trying to generalize the properties in
Section~\ref{PNprops}.
Although $\langle F,\plusFF,0/1,\multFF,1/1\rangle$ is a ring, it is not
an integral domain: \emph{any} expression of the form $0/e$ is an additive
unit, and therefore $F$ does not become a field when we add $\divFF$ as
a division operator.

The crux of the matter is that terms in $F$ are not restricted to
irreducible fractions (with the intuitive meaning of what ``irreducible''
should mean).
Adding this restriction is also far from trivial: rewriting quotients of
polynomials to irreducible fractions is known to be an extremely difficult
problem, and implementing such an algorithm in {\NF} would make {\rational}
extremely slow.

Therefore, we will use a different approach.
Going back to the example, it is easy to check that
$\NF(v^0_0\times 1/v^0_0-1)=0/(v^0_0\times 1+0)$.
Therefore, we will use the following modified version of {\rational}
for fields: instead of comparing the normal form of the two expressions
$e$ and $f$, we compute the normal form of $e-f$ and check that it has
the form $0/e'$.
This is correct.

\begin{corollary}\label{correctnessF1}
Let $t,t':A$ and define $\langle e,\rho\rangle=\lift(t,\emptyset)$ and
$\langle e',\sigma\rangle=\lift(t',\rho)$.  If $\NF(e-e')=0/e''$, where
$e''$ is an arbitrary expression, then $t=_A t'$ can be proved from the
field axioms and unfolding of the definitions of $-$, {\zring} and {\nexp}.
\end{corollary}
\begin{proof}
Let $e$ and $e'$ be as defined above and suppose that $\N(e-e')=0/e''$ for
some $e''$.
By Lemma~\ref{liftcorrect}, both $e\intrel t$ and $e'\intrel t'$.
By Proposition~\ref{NormR} also $\N(e)\intrel t$ and $\N(e')\intrel t'$.
Since $\N(e-e')=\N(e)\plusFF \N(e')\multFF(-1)$, Lemmas~\ref{plusFF}
and~\ref{multFF} together with~(\ref{intrel:int}) imply that
$\N(e-e')\intrel t+t'\times -1$; but $\N(e-e')=0/e''$, hence $0/e''$ can
be interpreted, and therefore $0/e''\intrel 0$ by~(\ref{intrel:div})
and~(\ref{intrel:int}).  By Lemma~\ref{intrelfunction} it then follows
that $t+t'\times -1=_A 0$, from which the thesis follows.
\end{proof}

The only drawback of this approach is that the completeness proof does not
go through.
A proof analogous to that of Theorem~\ref{completeness}, obtained by
replacing ``$\N(e)=\N(e')$'' with ``$\N(e-e')=0/e''$'' everywhere, fails
on the induction step for \axiom{Set_4}, since the induction hypothesis
will not be strong enough to prove an equivalent of Lemma~\ref{set4}.
All other proofs can be adapted, though, thus yielding the following
(partial) completeness result.

\begin{theorem}\label{completeness:field}
Let $t,t':A$ be such that the equality $t=_A t'$ can be proved
only from the field axioms and unfolding of the definitions of $-$,
$\zring$ and $\nexp$ in $t$ and $t'$, without using \axiom{Set_4} except
for $-$ and $\cdot^n$ ($n$ closed).  Define
$\langle e,\rho\rangle=\lift(t,\emptyset)$ and
$\langle e',\sigma\rangle=\lift(t',\rho)$.  Then $\N(e-e')$ has the form
$0/e''$ for some expression $e''$.
\end{theorem}
\begin{proof}
Similar to the proof of Theorem~\ref{completeness}.
\end{proof}

\bigskip
To see that the extra hypothesis is really needed, consider
$f(x)=_Af(x/2+x/2)$, which is clearly provable.  Then
\begin{eqnarray*}
\lift(f(x),\emptyset) & = &
  \langle v^1_0(v^0_0),\langle[v^0_0:=x],[v^1_0:=f]\rangle\rangle \\
\lift(f(x/2+x/2),\langle[v^0_0:=x],[v^1_0:=f]\rangle) & = &
  \langle v^1_0(v^0_0/2+v^0_0/2),\langle[v^0_0:=x],[v^1_0:=f]\rangle\rangle \\
\end{eqnarray*}
and
$\NF(v^1_0(v^0_0)-v^1_0(v^0_0/2+v^0_0/2))=%
(v^1_0((v^0_0\times 1+0)/1)\times1+v^1_0((v^0_0\times 4+0)/4)\times(-1)+0)/1%
\neq0$.

In practice, though, the difference in strength between
Theorem~\ref{completeness} and Theorem~\ref{completeness:field} is not
very serious.  In most situations axiom \axiom{Set_4} is not needed,
and in several where it is used {\rational} still works (this will be
the case whenever the hypothesis of this axiom can be proved just from
the ring axioms).  In particular, {\rational} still works on goals
like $f(x+x)/4+f(2x)/4=f(x+x+0)/2$, and this is usually enough.
Throughout C-CoRN, less than five situations were found where this
limitation of {\rational} made an alternative proof necessary.

\section{Remarks on the implementation}\label{extensions}

As mentioned in the Introduction, the theoretical treatment of {\rational}
we made considered a simplified version of the tactic.
The actual implementation covers all the expressions considered in the
type of setoids in C-CoRN, in particular binary functions and partial unary
functions, the latter being implemented as functions of a setoid element
and a proof term.

These extra cases pose no new difficulties.
There is one new axiom \axiom{Set'_4}, stating a similar version of
\axiom{Set_4} for partial functions.
The type of expressions needs to be extended with two new constructors
for variables representing these functions, and the interpretation and
lift must be adapted accordingly.
As a consequence several new cases need to be considered when proving
results about the order in which terms are lifted, but these can be
treated in a similar way to the like cases for variables in $\V_1$
(unlike variables in $\V_0$, which behave differently).
The completeness results for groups and rings still hold; as for
fields, as would be expected, the hypothesis of
Theorem~\ref{completeness:field} has to be strengthened since
\axiom{Set'_4} and \axiom{Set_5} cannot be used either in the proof of
$t=t'$.

\section{Conclusions}\label{concl}

In this paper we formally described {\rational} and undertook a study
of its behavior as a decision procedure.  It was shown to be correct
and complete for groups and rings, which is very useful information in
interactive proof development, and correct and partially complete for
fields, which is also very useful, as explained in Section~\ref{fields}.

Furthermore, we hope to use the completeness of {\rational} to take the
tactic a step further.  By the completeness of the theory of fields we
also know that for every equality $t=t'$ that cannot be proved from the
axioms there is a field where $t\neq t'$ holds.  We hope to use the
information provided by {\rational} upon failure (namely, an expression
in normal form that does not equal zero) to construct such a model
\emph{within} Coq, thus reflecting completeness within the system.

Although {\rational} is designed for Coq, we conducted this study at a
level of abstraction that should make it easy to develop similar
(partially) complete tactics for other proof assistants based on type
theory.  It is also possible that {\rational} can be adapted to other
systems.

\section*{Acknowledgments}

The authors wish to thank Henk Barendregt and Herman Geuvers for their
helpful suggestions and support.

This work was partially supported by the European Project 
IST-2001-33562 MoWGLI
and by FCT and FEDER under POCTI, namely through CLC project FibLog
FEDER POCTI / 2001 / MAT / 37239.

%\bibliographystyle{plain}
%\bibliography{hrefl-ii}

\begin{thebibliography}{1}

\bibitem{ACHA90}
Stuart~F. Allen, Robert~L. Constable, Douglas~J. Howe, and William Aitken.
\newblock {The Semantics of Reflected Proof}.
\newblock In {\em Proceedings of the 5th Symposium on Logic in Computer
  Science}, pages 95--197, Philadelphia, Pennsylvania, June 1990. IEEE, IEEE
  Computer Society Press.

\bibitem{cha:key:90}
C.~C. Chang and H.~Jerome Keisler.
\newblock {\em Model Theory}.
\newblock North-Holland, 1990.

\bibitem{coqmanual}
The {C}oq Development Team.
\newblock {\em {The {C}oq Proof Assistant Reference Manual}}, April 2004.
\newblock Version $8.0$.

\bibitem{lcf:geu:wie:04}
L.~Cruz-Filipe, H.~Geuvers, and F.~Wiedijk.
\newblock {C-CoRN: the Constructive Coq Repository at Nijmegen}.
\newblock In {\em MKM 2004}, LNCS. Springer Verlag, 2004.
\newblock To appear.

\bibitem{lcf:wie:04}
L.~Cruz-Filipe and F.~Wiedijk.
\newblock {Hierarchical Reflection}.
\newblock In {\em Theorem Proving in Higher Order Logics, 17th International
  Conference, TPHOLs 2004}, LNCS. Springer Verlag, 2004.
\newblock To appear.

\bibitem{geu:pol:wie:zwa:02}
H.~Geuvers, R.~Pollack, F.~Wiedijk, and J.~Zwanenburg.
\newblock {The Algebraic Hierarchy of the {FTA} {P}roject}.
\newblock {\em Journal of Symbolic Computation, Special Issue on the
  Integration of Automated Reasoning and Computer Algebra Systems}, pages
  271--286, 2002.

\bibitem{geu:wie:zwa:00}
H.~Geuvers, F.~Wiedijk, and J.~Zwanenburg.
\newblock {Equational Reasoning via Partial Reflection}.
\newblock In M.~Aagaard and J.~Harrison, editors, {\em Theorem Proving in
  Higher Order Logics, 13th International Conference, TPHOLs 2000}, volume 1869
  of {\em LNCS}, pages 162--178, Berlin, Heidelberg, New York, 2000. Springer
  Verlag.

\end{thebibliography}

\appendix

\section{Proof of Equality~(\ref{eqn:nvsstar})}

Throughout this section, $\xi$ is a (fixed) renaming of variables.
We prove the following equality, valid for all $p,q:P$:
\[\N(\renamevar{(p\star q)}\xi)=\N(\renamevar{(p\starPP q)}\xi).\]

We will only deal with the case $\star=+$, since the case $\star=\times$
is similar.  We prove this in a series of steps.

\begin{lemma}\label{multMVsubst0} Let $m:M$ and $v^0_i:\V_0$.  Then
$\N(\renamevar{(m\multMV v^0_i)}\xi)=\N(\renamevar m\xi)\multPP%
\N(\renamevar{v^0_i}\xi)$.
\end{lemma}
\begin{proof}
By induction on $m$.  If $m\in\Z$, then trivially
\begin{eqnarray*}
\N(\renamevar{(m\multMV v^0_i)}\xi) & = & \N(\renamevar{(v^0_i\times m)}\xi) \\
 & = & \N(\renamevar{v^0_i}\xi\times m) \\
 & = & \N(\renamevar{v^0_i}\xi)\multPP\N(m) \\
 & = & \N(m)\multPP\N(\renamevar{v^0_i}\xi) \\
 & = & \N(m\times\renamevar{v^0_i}\xi) \\
 & = & \N(\renamevar{(m\times v^0_i)}\xi)
\end{eqnarray*}
Suppose now that $m=v^0_j\times e$.  If $i\leq j$, the previous proof
still holds replacing $m$ with {\renamevar m\xi} in the third through
sixth expression; else the following shows the equality.
\begin{eqnarray*}
\N(\renamevar{((v^0_j\times e)\multMV v^0_i)}\xi)
 & = & \N(\renamevar{(v^0_j\times(e\multMV v^0_i))}\xi) \\
 & = & \N(\renamevar{v^0_j}\xi)\multPP\N(\renamevar{(e\multMV v^0_i)}\xi) \\
 & \stackrel{IH}= & \N(\renamevar{v^0_j}\xi)\multPP\left(%
   \N(\renamevar e\xi)\multPP\N(\renamevar{v^0_i}\xi)\right) \\
 & = & \left(\N(\renamevar{v^0_j}\xi)\multPP\N(\renamevar e\xi)\right)%
   \multPP\N(\renamevar{v^0_i}\xi) \\
 & = & \N(\renamevar{(v^0_j\times e)}\xi)\multPP\N(\renamevar{v^0_i}\xi)
\end{eqnarray*}
Finally, if $m=v^1_j(p)\times e$ then again the first argument holds.
\end{proof}

\begin{lemma}\label{multMVsubst1} Let $m:M$, $v^1_i:\V_1$ and $p:P$.  Then
$\N(\renamevar{(m\multMV v^1_i(p))}\xi)%
=\N(\renamevar m\xi)\multPP\N(\renamevar{v^1_i(p)}\xi)$.
\end{lemma}
\begin{proof}
Analogous to the previous.
\end{proof}

\begin{lemma}\label{plusMMsubst} Let $m_1,m_2:M$ be such that $|m_1|=|m_2|$.
Then $\N(\renamevar{(m_1\plusMM m_2)}\xi)%
=\N(\renamevar{m_1}\xi)\plusPP\N(\renamevar{m_2}\xi)$.
\end{lemma}
\begin{proof}
By induction on $m_1$.

If $m_1=i\in\Z$, then also $m_2=j\in\Z$ because $|m_1|=|m_2|$.  Then
both sides of the equality reduce to $i+j$.

If $m_1=v^0_i\times e$, then also $m_2=v^0_i\times e'$, whence
\begin{eqnarray*}
\N(\renamevar{(v^0_i\times e\plusMM v^0_i\times e')}\xi)
 & = & \N(\renamevar{((e\plusMM e')\multMV v^0_i)}\xi) \\
 & \stackrel{\star}= &
       \N(\renamevar{(e\plusMM e')}\xi)\multPP\N(\renamevar{v^0_i}\xi) \\
 & \stackrel{IH}= & \left(\N(\renamevar e\xi)\plusPP%
       \N(\renamevar{e'}\xi)\right)\multPP\N(\renamevar{v^0_i}\xi) \\
 & = & \N(\renamevar{v^0_i}\xi)\multPP\N(\renamevar e\xi)\plusPP%
       \N(\renamevar{v^0_i}\xi)\multPP\N(\renamevar{e'}\xi) \\
 & = & \N(\renamevar{(v^0_i\times e)}\xi)\plusPP
       \N(\renamevar{(v^0_i\times e')}\xi)
\end{eqnarray*}
where $\star$ denotes application of Lemma~\ref{multMVsubst0}.

The case $m_1=v^1_i(p)\times e$ is analogous resorting to
Lemma~\ref{multMVsubst1}.
\end{proof}

\begin{lemma}\label{plusPMsubst} Let $p:P$ and $m:M$.  Then
$\N(\renamevar{(p\plusPM m)}\xi)%
=\N(\renamevar p\xi)\plusPP\N(\renamevar m\xi)$.
\end{lemma}
\begin{proof}
By induction on $p$ and $m$.

Suppose $p=i\in\Z$.  If $m=j\in\Z$, then both expressions reduce to $i+j$;
else
$\N(\renamevar{(i\plusPM m)}\xi)%
=\N(\renamevar{(m+i)}\xi)%
=\N(\renamevar m\xi)\plusPP\N(\renamevar i\xi)%
=\N(\renamevar i\xi)\plusPP\N(\renamevar m\xi)$.

Suppose now that $p=e_1+e_2$.  There are several cases to consider.
\begin{itemize}
\item if $m=i\in\Z$ or $|e_1|<_M|m|$, then
\begin{eqnarray*}
\N(\renamevar{((e_1+e_2)\plusPM m)}\xi)
 & = & \N(\renamevar{(e_1+(e_2\plusPM m))}\xi) \\
 & = & \N(\renamevar{e_1}\xi)\plusPP\N(\renamevar{(e_2\plusPM m)}\xi) \\
 & \stackrel{IH}= & \N(\renamevar{e_1}\xi)\plusPP\left(%
   \N(\renamevar{e_2}\xi)\plusPP\N(\renamevar m\xi)\right) \\
 & = & \left(\N(\renamevar{e_1}\xi)\plusPP\N(\renamevar{e_2}\xi)\right)%
   \plusPP\N(\renamevar m\xi)\\
 & = & \N(\renamevar{(e_1+e_2)}\xi)\plusPP\N(\renamevar m\xi)
\end{eqnarray*}
\item if $|e_1|=|m|$, then
\begin{eqnarray*}
\N(\renamevar{((e_1+e_2)\plusPM m)}\xi)
 & = & \N(\renamevar{(e_2\plusPM(e_1\plusMM m))}\xi) \\
 & \stackrel{IH}= & \N(\renamevar{e_2}\xi)\plusPP%
   \N(\renamevar{(e_1\plusMM m)}\xi) \\
 & \stackrel{\star}= & \N(\renamevar{e_2}\xi)\plusPP\left(%
   \N(\renamevar{e_1}\xi)\plusPP\N(\renamevar m\xi)\right) \\
 & = & \left(\N(\renamevar{e_1}\xi)\plusPP\N(\renamevar{e_2}\xi)\right)\plusPP%
   \N(\renamevar m\xi) \\
 & = & \N(\renamevar{(e_1+e_2)}\xi)\plusPP\N(\renamevar m\xi)
\end{eqnarray*}
where $\star$ denotes application of Lemma~\ref{plusMMsubst}.
\item if $|e_1|\geq_M|m|$, then
\begin{eqnarray*}
\N(\renamevar{(p\plusPM m)}\xi)
 & = & \N(\renamevar{(m+p)}\xi) \\
 & = & \N(\renamevar m\xi)\plusPP\N(\renamevar p\xi) \\
 & = & \N(\renamevar p\xi)\plusPP\N(\renamevar m\xi)
\end{eqnarray*}
\end{itemize}
\end{proof}

\begin{lemma}\label{plusPPsubst} Let $p,q:P$.  Then
$\N(\renamevar{(p\plusPP q)}\xi)%
=\N(\renamevar p\xi)\plusPP\N(\renamevar q\xi)$.
\end{lemma}
\begin{proof}
By induction on $p$.  If $p=i\in\Z$ then
$\N(\renamevar{(i\plusPP q)}\xi)%
=\N(\renamevar{(q\plusPM i)}\xi)%
=\N(\renamevar q\xi)\plusPP\N(\renamevar i\xi)%
=\N(\renamevar i\xi)\plusPP\N(\renamevar q\xi)$
by Lemma~\ref{plusPMsubst}.

Finally, if $p=e_1+e_2$ then the following reasoning proves the desired
equality.
\begin{eqnarray*}
\N(\renamevar{((e_1+e_2)\plusPP q)}\xi)
 & = & \N(\renamevar{((e_2\plusPP q)\plusPM e_1)}\xi) \\
 & \stackrel\star= & \N(\renamevar{(e_2\plusPP q)}\xi)\plusPP%
   \N(\renamevar{e_1}\xi) \\
 & \stackrel{IH}= & \left(\N(\renamevar{e_2}\xi)\plusPP%
   \N(\renamevar q\xi)\right)\plusPP\N(\renamevar{e_1}\xi) \\
 & = & \left(\N(\renamevar{e_1}\xi)\plusPP\N(\renamevar{e_2}\xi)\right)%
   \plusPP\N(\renamevar q\xi) \\
 & = & \N(\renamevar{(e_1+e_2)}\xi)\plusPP\N(\renamevar q\xi) \\
\end{eqnarray*}
\end{proof}

\begin{corollary}\label{plusPPsubstvars} Let $p,q:P$.  Then
$\N(\renamevar{(p\plusPP q)}\xi)=\N(\renamevar{(p+q)}\xi)$.
\end{corollary}
\begin{proof}
$\N(\renamevar{(p+q)}\xi)=\N(\renamevar p\xi)\plusPP\N(\renamevar q\xi)$,
and by Lemma~\ref{plusPPsubst} we are done.
\end{proof}

\end{document}