% $Id: hrefl.tex,v 1.4 2004/02/18 15:48:35 freek Exp $
\documentclass[runningheads]{llncs}
\usepackage{amssymb,url}
\usepackage[all]{xy}
\raggedbottom
\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{\eqbdi}{=}
\newcommand{\wf}{{\it wf}}
\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}}
\begin{document}
\title{Hierarchical Reflection}
\author{Lu\'\i s Cruz-Filipe\inst{1,2} \and Freek Wiedijk\inst{1}}
\institute{Department of Computer Science, University of Nijmegen\and Center for Logic and Computation, Lisboa\\ \email{$\{$lcf,freek$\}$@cs.kun.nl}}
\maketitle
\begin{abstract}
The technique of reflection is a way to automate proof construction
in type theoretical proof assistants.
Reflection is based on the definition of a type of syntactic expressions
that gets interpreted in the domain of discourse.
By allowing the interpretation function to be partial or even a relation
one gets a more general method known as ``partial reflection''.
In this paper we show how one can take advantage of the partiality of
the interpretation to uniformly define a family of tactics for equational
reasoning that will work in different algebraic structures.
These tactics then follow the hierarchy
of those algebraic structures in a natural way.
\end{abstract}
\section{Introduction}\label{intro} %F+L
\subsection{Problem}
Computers have made formalization of mathematical proof practical.
They help getting formalizations correct by
verifying all the details,
but they also make it easier to formalize
mathematics by automatically generating parts of the proofs.
One way to automate proof is the technique called
\emph{reflection}.
With reflection one describes the desired automation \emph{inside} the logic
of the theorem prover, by formalizing relevant meta-theory.
Reflection is the common approach for proof automation in type theoretical
systems like NuPRL and Coq.
Another name for reflection is ``the two-level approach''.
In Nijmegen we formalized the Fundamental Theorems of Algebra and
Calculus in Coq,
and then extended these formalizations into a structured library
of mathematics named the C-CoRN library~\cite{ccorn,lcf:geu:wie:04}.
For this library we defined a reflection tactic called {\rational}
that automatically establishes equalities of rational expressions in a field
by bringing both to the same side of the equal sign and then
multiplying everything out.
With this tactic, equalities like
$${1\over x} + {1\over y} = {x + y\over xy}$$
can be automatically proved without any human help.
The {\rational} tactic only works for expressions in a field,
but using the same idea one can define
%% there are
analogous tactics for expressions in a ring or a group.
The trivial way to define these is to duplicate the definition of the
{\rational} tactic and modify it for these simpler algebraic structures
by removing references to division or multiplication.
%This is what we did when we defined a ring version of {\rational}.
This was actually done to implement a ring version of {\rational}.
However this is not efficient, as it means duplication of the full
code of the tactic.
In particular the \emph{normalization function} that describes the simplification
of expressions, which is quite complicated, has to be defined multiple
times.
But looking at the normalization function for field expressions, it
is clear that it contains the normalization function for rings.
In this paper we study a way to \emph{integrate} these tactics for
different algebraic structures.
\subsection{Approach}
In the C-CoRN library algebraic structures like fields, rings
and groups are organized into an \emph{Algebraic Hierarchy}.
The definition of a field reuses the definition of a ring, and
the definition of a ring reuses the definition of a group.
This hierarchy means that theory about these structures
is maximally reusable.
Lemmas about groups are automatically also applicable to rings
and fields, and lemmas about rings also apply to fields.
In this paper we organize the equational tactics for fields, rings
and groups in a similar hierarchical manner.
It turns out that expression simplification in a field
can be directly applied to equational reasoning in rings and groups as well.
This is quite surprising:
the normal forms of expressions that get simplified in this theory
will contain functions like multiplication and division,
operations that do not make sense in a group.
\subsection{Related Work}
{\rational} is for the C-CoRN setoid framework what the standard Coq
tactic \tacticname{Field} is for Leibniz equality.
Both tactics were developed at about the same time.
\tacticname{Field} is a generalization of the Coq \tacticname{Ring}
tactic, so with the \tacticname{Field} and \tacticname{Ring} tactics the
duplication of effort that we try to eliminate is also present.
Also the \tacticname{Ring} tactic applies to rings as well as to
semirings (to be able to use it with the natural numbers),
so there is also this kind of duplication
within the \tacticname{Ring} tactic itself.
Reflection has also been widely used in the NuPRL system as described
originally in~\cite{ACHA90}. More recently,~\cite{HNC+03} introduces
other techniques that allow code reuse for tactics in MetaPRL,
although the ideas therein are different from ours. Since the library
of this system also includes an algebraic hierarchy built using
subtyping (see~\cite{YNKH03}), it seems reasonable to expect that the
work we describe could be easily adapted to that framework.
\subsection{Contribution}
We show that it is possible to have one unified mechanism for
simplification of expressions in different algebraic structures like
fields, rings and groups.
We also show that it is not necessary to have different normalization
functions for these expressions, but that it is possible to decide
equalities on all levels with only one normalization function.
\subsection{Outline}
In Section~\ref{reflection} we summarize the methods of reflection
and partial reflection.
In Section~\ref{normalization} we describe in detail the normalization
function of the {\rational} tactic.
Section~\ref{functions} is a small detour where we generalize the same
method to add uninterpreted function
symbols to the expressions that {\rational} understands.
In Section~\ref{hierarchical} we show how to do reflection in an
algebraic hierarchy in a hierarchical way.
Finally in Section~\ref{integration} we present a possibility
to have even tighter integration in a hierarchical reflection tactic,
which unfortunately turns out to require the so-called $K$ axiom.
\section{Reflection and Partial Reflection}\label{reflection} %F
In this section we will briefly summarize~\cite{geu:wie:zwa:00}.
That paper describes a generalization of the technique of
\emph{reflection} there called \emph{partial reflection}.
%Reflection is a technique to automate proof generation.
%It is mainly used in proof assistants that are
%based on type theory, like Coq and NuPRL.
One can give a general account of reflection in terms of
decision procedures, but here we will only present the more
specific method of reflection with
a normalization function, which is used to do equational reasoning.
In the normal, ``total'', kind of reflection
one defines a type $E$ of \emph{syntactic
expressions} for the domain $A$ that one is reasoning about,
together with an \emph{interpretation function}
$$\intfun{-} : E \to A$$
which assigns
to a syntactic expression $e$ an interpretation $\intfun{e}$.
In this, $\rho$ is a \emph{valuation} that maps the variables
in the syntactic expressions to values in $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 \emph{inside} the type
theory (this is not possible for $A$;
so the reason for introducing the type $E$ is to be able to define this $\N$).
$$\N : E \to E$$
One now proves the correctness lemma that states that the normalization function
conserves the interpretation.
$$\intfun{e} =_A \intfun{\N(e)}$$
Then, to
reason about the domain $A$ that $\inte{-}$ maps to,
one first a valuation $\rho$ and
syntactic expressions in $E$ which map under $\intfun{-}$ to the
terms that one want to reason about, and
after that one uses the lemma to do the equational reasoning.
For instance, suppose that one wants to prove $a =_A b$.
One finds $e$, $f$ and $\rho$ with $\intfun{e} \eqbdi a$ and
$\intfun{f} \eqbdi b$.
Now if $\N(e) \eqbdi \N(f)$ then
we get $a \eqbdi \intfun{e} =_A \intfun{\N(e)} \eqbdi \intfun{\N(f)} =_A \intfun{f} \eqbdi b$.
(Clearly this uses the correctness lemma twice, see Figure~\ref{fig:tactic}.)
\begin{figure}
\[
\xymatrix{
e\in E\ar[rr]^{\N\ \ \ \ }\ar@/_/[ddr]_{\intfun{-}} &&
\N(e)=\N(f)\ar[]+DL+<1cm,0pt>;[ddl]^{\intfun{-}}\ar[]+DR-<1cm,0cm>;[ddr]_{\intfun{-}} &&
f\in E\ar[ll]_{\ \ \ \ \ \N}\ar@/^/[ddl]^{\intfun{-}} \\ \\
& a\in A\ar@/_/@{-->}[uul]\ar@{<->}[rr]^{=_A} && b\in A\ar@/^/@{-->}[uur]
}
\]
\caption{Proving equalities}\label{fig:tactic}
\end{figure}
\noindent
Note that the operation of finding an expression in $E$ that
corresponds to a given expression in $A$ (dotted arrows) is not
definable in the type theory, and needs to be implemented
\emph{outside} of it. In a system like Coq it will be
implemented in ML or in the tactic language \Ltac.
Things get more interesting when the syntactic expressions in $E$ contain
\emph{partial} operations, like division.
In that case the interpretation $\intfun{e}$ will not always be defined.
To address this we generalized the method of reflection to \emph{partial
reflection}.
The naive way to do this is to define a predicate
$$\wfrho : E \to \Prop$$
that tells whether an expression is \emph{well-formed}.
Then the interpretation function takes another argument of type $\wfrho(e)$.
$$\intfun{-} : \Pi_{e:E}.\, \wfrho(e) \to F$$
The problem with this approach is that the definition of $\wf$
needs the interpretation function $\inte{-}$.
Therefore the inductive definition of $\wf$ and the recursive definition
of $\inte{-}$ need to be given simultaneously.
This is called an \emph{inductive-recursive definition}.
Inductive-recursive definitions are not supported by the Coq system,
and for a good reason:
induction-recursion makes a system significantly stronger.
In set theory it corresponds to the existence of a Mahlo
cardinal \cite{dyb:set:03}.
The solution from~\cite{geu:wie:zwa:00} for doing partial reflection without induction-recursion,
is to replace the
interpretation function with an inductively defined \emph{interpretation relation}.
$$\intrel \subseteq E \times A$$
The relation $\intfun{e} = a$ now becomes $e \intrel a$.
It means that the syntactic expression $e$ is
interpreted under the valuation $\rho$ by the object $a$.
%
The lemmas that one then proves are the following.
$$
\begin{array}{c}
e \intrel a \;\land\; e \intrel b \;\Rightarrow\; a =_A b\\
\noalign{\medskip}
e \intrel a \;\Rightarrow\; \N(e) \intrel a
\end{array}
$$
The first lemma states that the interpretation relation is \emph{functional},
and the second lemma is again the correctness of the normalization function.
Note that it is not an equivalence but just an implication.
This is the only direction that is needed.
It is easy to see that in fact in our application
the equivalence does not hold.\footnote{A simple example is $e=1/(1/0)$,
which does not relate to any $a$.
Its normal form is $0/1$, which interprets to $0$.}
For each syntactic expression $e$ that one constructs for an
object $a$,
one also needs to find an inhabitant of the statement $e \intrel a$.
In~\cite{geu:wie:zwa:00} a type $\bar E_\rho(a)$ of \emph{proof loaded syntactic
expressions} is introduced to make this easier.
These types correspond to the expressions that evaluate to $a$.
They are mapped to the normal syntactic expressions by a forgetful function
$$|\mathord{-}| : \bar E_\rho(a) \to E$$
and they satisfy the property that for all $\bar e$ in the type $\bar E_\rho(a)$
$$|{\bar e}| \intrel a.$$
In this paper we will not further go into this,
although everything that we do also works in the presence of these proof loaded
syntactic expressions.
\section{Normalization Function}\label{normalization} %L+F
We will now describe how we defined the normalization function for our
main example of \emph{rational expressions}.
Here the type E of syntactic expressions is given by the following
grammar.
\begin{eqnarray*}
E &::=& \Z \alt \V \alt E+E \alt E\cdot E \alt E/E
\end{eqnarray*}
In this $\Z$ are the integers, and $\V$ is a countable set of
\emph{variable names} (in the Coq formalization we use a copy of the natural
numbers for this).
%new (lcf)
Variables will denoted by $x,y,z$, integers by $i,j,k$.
The elements of this type $E$ are just \emph{syntactic} objects, so they are
different kind of objects
from the \emph{values} of these expressions in specific fields.
Note that in these expressions it is possible to divide by zero: $0/0$ is
one of the terms in this type.
Other algebraic operations are defined as an abbreviation
from operations that occur in the type.
For instance, subtraction is defined by
$$e - f \equiv e + (-1)\cdot f$$
%and exponentiation to a power that is a closed natural number term
%is defined as iterated multiplication
%$$e^n \equiv e\cdot e\cdot \dots\cdot e\cdot 1.$$
\noindent
We now will describe how we define the normalization function $\N(e)$
that maps an element of $E$ to a normal form.
As an example, the normal form of ${1\over x - y} + {1\over x + y}$ is
$$\N({1\over x - y} + {1\over x + y}) = {x\cdot 2 + 0\over x\cdot x\cdot 1 + y\cdot y\cdot (-1) + 0}.$$
This last expression is the ``standard form'' of the way one would normally write
this term, which is
$${2x\over x^2 - y^2}.$$
\noindent
From this example it should be clear how the normalization function works:
it multiplies everything out until there is just a quotient of two
polynomials left.
These polynomials are then in turn written in a ``standard form''.
The expressions in normal form are given by the following grammar.
\begin{eqnarray*}
F &::=& P/P \\
P &::=& M + P \alt \Z \\
M &::=& \V \cdot M \alt \Z
\end{eqnarray*}
In this grammar $F$ represents a fraction of two polynomials, $P$ are the
polynomials and $M$ are the monomials.
One should think of $P$ as a ``list of monomials'' (where $+$ is the ``cons''
and the integers take the place of the ``nil'')
and of $M$ as a ``list of variables'' (where $\cdot$ is the ``cons'' and
again the integers take the place of the ``nil'').
%changed by lcf
%We want to get uniqueness of normal forms, so we require
On the one hand we want the normalization function to terminate,
but on the other hand we want the set of normal forms to be as small
as possible.
We achieve this by requiring
% after ``;'' added by lcf
the polynomials and monomials to be \emph{sorted}; furthermore, no two
monomials in a polynomial can have exactly the same set of variables.
Thus normal forms for polynomials will be unique.
For this we have an ordering of the variable names.
So the ``list'' that is a monomial has to be sorted
according to this order on $\V$, and the ``list'' that
is a polynomial also has to be sorted, according to the
corresponding lexicographic ordering on the monomials.
If an element of $P$ or $M$ is sorted like this,
and monomials with the same set of variables have been collected
together, we say it is \emph{in normal form}.
Now to define $\N$ we have to ``program'' the multiplying out of $E$
expressions together with the sorting of monomials and polynomials,
and collecting factors and terms.
This is done in a systematic way.
Instead of first multiplying out the expressions and then sorting
them to gather common terms, we systematically combine these two things.
We recursively define the following functions
(using the \texttt{Fixpoint} operation of Coq).
$$
\begin{array}{rlcrclcl}
- &\cdot_{\it M\Z}\; - &:& M &\times& \Z &\to& M \\
- &\cdot_{\it M\V}\; - &:& M &\times& \V &\to& M \\
- &\cdot_{\it MM}\; - &:& M &\times& M &\to& M \\
- &+_{\it MM}\; - &:& M &\times& M &\to& M \\
- &+_{\it PM}\; - &:& P &\times& M &\to& P \\
- &+_{\it PP}\; - &:& P &\times& P &\to& P \\
- &\cdot_{\it PM}\; - &:& P &\times& M &\to& P \\
- &\cdot_{\it PP}\; - &:& P &\times& P &\to& P \\
- &+_{\it FF}\; - &:& F &\times& F &\to& F \\
- &\cdot_{\it FF}\; - &:& F &\times& F &\to& F \\
- &/\!_{\it FF}\; - &:& F &\times& F &\to& F
\end{array}
$$
(Actually, all these functions have all type
$$E \times E \to E$$
as we do not have separate types for $F$, $P$ and $M$.
However, the idea is that they only will be called with arguments
that are of the appropriate shape and in normal form.
In that case the functions will return the appropriate normal form.
If the other case it will return any term that is equal to
the sum or product of the arguments --- generally we just use the sum
or product of the arguments.)
%examples added by lcf
For example, the multiplication function $\cdot_{\it MM}$ looks like
%Fixpoint MM_mult [e:expr] : expr->expr := [f:expr]
%let d = (expr_mult e f) in
% Cases e f of
% (expr_mult e1 e2) f => (MV_mult (MM_mult e2 f) e1)
% | (expr_int i) f => (MI_mult f e)
% | _ _ => d
% end.
\[
e\cdot_{\it MM}f := \left\{
\begin{array}{ll}
f\cdot_{\it M\Z}i & \mbox{ if $e=i\in\Z$}\\
(e_2\cdot_{\it MM}f)\cdot_{\it MV}e_1 & \mbox{ if $e=e_1\cdot e_2$}\\
e\cdot f & \mbox{ otherwise}
\end{array}\right.
\]
\noindent and the addition function $+_{\it PM}$ is\footnote{In the fourth
case, the equality $e_1=f$ is equality \emph{as lists}, meaning that
they might differ in the integer coefficient at the end.}
%Fixpoint PM_plus [e:expr] : expr->expr := [f:expr]
%let d = (expr_plus e f) in
% Cases e f of
% (expr_plus e1 e2) (expr_int _) => (expr_plus e1 (PM_plus e2 f))
% | (expr_int i) (expr_int j) => (MM_plus e f)
% | (expr_plus e1 e2) f =>
% Cases (le_monom e1 f) of
% true =>
% Cases (eq_monom e1 f) of
% true => (PM_plus e2 (MM_plus e1 f))
% | false => (expr_plus e1 (PM_plus e2 f))
% end
% | false => (expr_plus f e)
% end
% | (expr_int i) f => (expr_plus f e)
% | _ _ => d
% end.
\[
e+_{\it PM}f := \left\{
\begin{array}{ll}
i+_{\it MM} j & \mbox{ if $e=i\in\Z$, $f=j\in\Z$} \\
f+i & \mbox{ if $e=i\in\Z$} \\
e_1+(e_2+_{\it PM} i) & \mbox{ if $e=e_1+e_2$, $f=i\in\Z$} \\
e_2+_{\it PM}(e_1+_{\it MM} f) & \mbox{ if $e=e_1+e_2$, $e_1=f$} \\
e_1+(e_2+_{\it PM} f) & \mbox{ if $e=e_1+e_2$, $e_1<_{\mathrm{lex}}f$} \\
f+e & \mbox{ if $e=e_1+e_2$, $e_1>_{\mathrm{lex}}f$} \\
e+f & \mbox{ otherwise}
\end{array}\right.
\]
%%Definition FF_plus [e:expr] : expr->expr := [f:expr]
%%let d = (expr_plus e f) in
%% Cases e f of
%% (expr_div e1 e2) (expr_div f1 f2) =>
%% (expr_div (PP_plus (PP_mult e1 f2) (PP_mult e2 f1)) (PP_mult e2 f2))
%% | _ _ => d
%% end.
%\[
%e+_{\it FF}f = \left\{
%\begin{array}{ll}
% ((e_1\cdot_{\it PP}f_2)+_{\it PP}(e_2\cdot_{\it PP}&f_1))/(e_2\cdot_{\it PP} f_2)\\ & \mbox{ if $e=e_1/e_2$ and $f=f_1/f_2$}\\
% e+f & \mbox{ otherwise}
%\end{array}\right.
%\]
\noindent where the lexicographic ordering $<_{\mathrm{lex}}$ is
used to guarantee that the monomials in the result are ordered.
Finally we used these functions to recursively ``program'' the
normalization function.
For instance the case where the argument is a division is
defined like
$$\N(e/f) := N(e) \,/\!_{\it FF} N(f).$$
%new!!! (lcf)
\noindent The base case (when $e$ is a variable) looks like
$$\N(v) := {v\cdot 1+0 \over 1}.$$
\noindent
To prove that $a=b$, then, one builds the expression corresponding to
$a-b$ and checks that this normalizes to an expression of the form
$0/e$.
(This turns out to be stronger than building expressions $e$ and $f$
interpreting to $a$ and $b$ and verifying that $\N(e)=\N(f)$, since normal
forms are in general not unique.)
\section{Uninterpreted Function Symbols}\label{functions} %L
When one starts working with the tactic defined as above, one quickly
finds out that there are situations in which it fails because two
terms which are easily seen to be equal generate two expressions whose
difference fails to normalize to $0$.
A simple example arises is when function symbols are used; for example,
trying to prove that $$f(a+b)=f(b+a)$$ will fail because $f(a+b)$ will
be syntactically represented as a variable $x$ and $f(b+a)$ as a
(different) variable $y$, and the difference between these expressions
normalizes to $${x\cdot1+y\cdot(-1)+0 \over 1},$$ which is not zero.
In this section we describe how the syntactic type $E$ and the normalization
function $\N$ can be extended to recognize and deal with function symbols.
The actual implementation includes unary and binary total functions,
as well as unary partial functions (these are binary functions whose second
argument is a proof)\footnote{Other possibilities, such as ternary functions
or binary partial functions, were not considered because this work was
done in the setting of the C-CoRN library, where these
are the types of functions which are used in practice.}.
We will discuss the case for unary total functions in detail; binary and
partial functions are treated in an analogous way.
Function symbols are treated much in the same way as variables; thus, we
extend the type $E$ of syntactic expressions with a new countable set of
\emph{function variable names} $\V_1$, which is implemented (again) as the
natural numbers.
The index $1$ stands for the arity of the function; the original set of
variables is now denoted by $\V_0$.
Function variables will be denoted $u,v$.
\begin{eqnarray*}
E &::=& \Z \alt \V_0 \alt \V_1(E) \alt E+E \alt E\cdot E \alt E/E
\end{eqnarray*}
\noindent Intuitively, the normalization function should also normalize
the arguments of function variables.
The grammar for normal forms becomes the following.
\begin{eqnarray*}
F &::=& P/P \\
P &::=& M + P \alt \Z \\
M &::=& \V_0 \cdot M \alt \V_1(F) \cdot M \alt \Z
\end{eqnarray*}
But now a problem arises: the extra condition that both polynomials and
monomials correspond to sorted lists requires ordering not only variables
in $\V_0$, but also expressions of the form $\V_1(F)$.
The simplest way to do this is by defining an ordering on the whole set $E$
of expressions.
This is achieved by ordering first the sets $\V_0$ and $\V_1$ themselves.
Then, expressions are recursively sorted by first looking at their outermost
operator $$x <_E i <_E e+f <_E e\cdot 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\cdot y)<_E v(x+3).$$
\noindent With this different ordering, the same normalization function
as before can be used with only trivial changes.
In particular, the definitions of the functions $\cdot_{\it MM}$ and
$+_{\it PM}$ stay unchanged.
Only at the very last step does one have to add a rule saying that
$$\N(v(e)) := {v(\N(e))\cdot 1+0\over 1}.$$
%nuttig?
\noindent Notice the similarity with the rule for the normal form of
variables.
The next step is to change the interpretation relation.
Instead of the valuation $\rho$, we now need two valuations
\begin{eqnarray*}
\rho_0 & : & \V_0\to A\\
\rho_1 & : & \V_1\to(A\to A)
\end{eqnarray*}
\noindent and the inductive definition of the interpretation relation
is extended with the expected constructor for interpreting expressions
of the form $v(e)$.
As before, one can again prove the two lemmas
\[
\begin{array}{c}
e \intreltwo a \;\land\; e \intreltwo b \;\Rightarrow\; a =_A b\\
\noalign{\medskip}
e \intreltwo a \;\Rightarrow\; \N(e) \intreltwo a
\end{array}
\]
\noindent Now, our original equality $f(a+b)=f(b+a)$ can easily be
solved: $f(a+b)$ can now be more faithfully represented by the
expression $v(x+y)$, where $\rho_1(v)=f$, $\rho_0(x)=a$ and
$\rho_0(y)=b$; the syntactic representation of $f(b+a)$ becomes
$v(y+x)$; and each of these normalizes to
$${v\left({x\cdot1+y\cdot1+0\over 1}\right)\cdot1+0\over 1},$$ so that
their difference normalizes to $0$ as was intended.
Adding binary functions simply requires a new sort $\V_2$ of binary
function symbols and extend the type of expressions to allow for the
like of $v(e,f)$; the normalization function and the interpretation relation
can easily be adapted, the latter requiring yet another valuation
\begin{eqnarray*}
\rho_2 & : & \V_2\to(A\times A\to A).
\end{eqnarray*}
\noindent Partial functions are added likewise, using a sort $V\pidx$
for partial function symbols and a valuation
\begin{eqnarray*}
\rho\pidx & : & \V\pidx\to(A\not\to A).
\end{eqnarray*}
\noindent As was already the case with division, one can write down
expressions like $v(e)$ even when $\rho\pidx(v)$ is not defined at
the interpretation of $e$; the definition of $\intrelfour$ ensures that
only correctly applied partial functions will be interpreted.
\section{Hierarchical Reflection}\label{hierarchical} %L
The normalization procedure described in Section~\ref{normalization}
was used to define a tactic which would prove algebraic equalities in an
arbitrary field in the context of the Algebraic Hierarchy
of~\cite{geu:pol:wie:zwa:02}.
In this hierarchy, fields are formalized as rings with an extra operation
(division) which satisfies some properties; rings, in turn, are themselves
Abelian groups where a multiplication is defined also satisfying some
axioms.
The question then arises of whether it is possible to generalize this
mechanism to the different structures of this Algebraic Hierarchy.
This would mean having three ``growing'' types of syntactic
expressions $E_G$, $E_R$ and $E_F$ (where the indices stand for
groups, rings and fields respectively) together with interpretation
relations\footnote{For simplicity we focus on the setting where
function symbols are absent; the more general situation is analogous.}.
\[
\xymatrix{
E_F \ar[rr]^(.45){\intrelF} & & F : \mbox{Field}\ar[d] \\
E_R \ar[u]^{\subseteq}\ar[rr]^(.45){\intrelR} & & R : \mbox{Ring}\ar[d] \\
E_G \ar[u]^{\subseteq}\ar[rr]^(.45){\intrelG} & & G : \mbox{Group} \\
}
\]
\noindent However one can do better.
The algorithm in the normalization function works outwards; it first
pushes all the divisions to the outside, and then proceeds to
normalize the resulting polynomials.
In other words, it first deals with the field-specific part of the expression,
and then proceeds working within a ring.
This suggests that the same normalization function could be reused to
define a decision procedure for equality of algebraic expressions within
a ring, thus allowing $E_F$ and $E_R$ to be unified.
Better yet, looking at the functions operating on the polynomials one also
quickly realizes that these will never introduce products of variables
unless they are already implicitly in the expression (in other words, a
new product expression can arise e.g.\ from distributing a sum over an
existing product, but if the original expression contains no products then
its normal form will not, either).
So our previous picture can be simplified to this one.
%\[
%\xymatrix{
% & & F : \mbox{Field}\ar[d] \\
%E \ar[drr]^{\intrelG} \ar[urr]^{\intrelF} \ar[rr]^{\intrelR} & & R : \mbox{Ring}\ar[d] \\
% & & G : \mbox{Group} \\
%}
%\]
\[
\xymatrix{
E \ar[rr]^(.45){\intrelF}
\ar`d[dr][drr]^(.4){\intrelR}
\ar`d[ddr][ddrr]^(.4){\intrelG}
& & F : \mbox{Field}\ar[d] \\
& & R : \mbox{Ring}\ar[d] \\
& & G : \mbox{Group} \\
}
\]
The key idea is to use the partiality of the interpretation
relation to be able to map $E$ into a ring $R$ or a group $G$.
In the first case, expressions of the form ${e/f}$ will not be
interpreted; in the latter, neither these nor expressions of the form
${e\cdot f}$ relate to any element of the group.
There is one problem, however.
Suppose $x$ is a variable with $\rho(x)=a$; then $a+a$ is represented
by $x+x$, but
$$
\N(x+x)={x\cdot2+0\over 1} \intrelG a+a
$$
\noindent does not hold.
In order to make sense of the normal forms defined earlier,
one needs to interpret the special cases $e/1$ in groups and rings,
as well as $e\cdot f$ with $f=i\in\Z$ in groups (assuming, of course,
that $e$ can be interpreted).
We summarize what each of the interpretation relations can interpret in
the following table.
\begin{center}
\begin{tabular}{crcccccc}
&$\qquad$&$\quad$& $\intrelG$ &$\qquad$& $\intrelR$ &$\qquad$& $\intrelF$ \\
\noalign{\smallskip}
\hline
&\vline& \\
\noalign{\vspace{-0.9em}}
$v\in\V$ &\vline&& yes && yes && yes \\
$i\in\Z$ &\vline&& if $i=0$ && yes && yes \\
$e+f$ &\vline&& yes && yes && yes \\
$e\cdot f$ &\vline&& if $f\in\Z$ && yes && yes \\
$e/f$ &\vline&& if $f=1$ && if $f=1$ && if $f\neq 0$ \\
\noalign{\vspace{-0.9em}}
&\vline& \\
\hline
\noalign{\smallskip}
\end{tabular}
\end{center}
\noindent In the last three cases the additional requirement that
$e$ and $f$ can be interpreted is implicit.
Once again, one has to prove the lemmas
$$
\begin{array}{c}
e \intrelG a \;\land\; e \intrelG b \;\Rightarrow\; a =_A b\\
\noalign{\medskip}
e \intrelG a \;\Rightarrow\; \N(e) \intrelG a
\end{array}
$$
\noindent and analogous for $\intrelR$ and $\intrelF$.
In these lemmas, one needs to use the knowledge that the auxiliary functions
will only be applied to the ``right'' arguments to be able to finish
the proofs.
This is trickier to do for groups than for rings and fields.
For example, while correctness of $\cdot_{\it MM}$ w.r.t.\ $\intrelF$
is unproblematic, as it states that
\[e\intrelF a \;\land\; f\intrelF b \;\Rightarrow\; e\cdot_{\it MM}f\intrelF a\cdot b,\]
\noindent
the analogue of this statement for $\intrelG$
cannot be written down, as $a\cdot b$ has no meaning in a group.
However, by the definition of $\intrelF$, this is equivalent to
the following.
\[e\cdot f\intrelF a\cdot b \;\Rightarrow\; e\cdot_{\it MM}f\intrelF a\cdot b\]
Now this second version does possess an analogue for $\intrelG$,
by replacing the expression $a\cdot b$ with a variable.
\[e\cdot f\intrelG c \;\Rightarrow\; e\cdot_{\it MM} f\intrelG c.\]
\noindent This is still not provable, because $\cdot_{\it MM}$ can
swap the order of its arguments.
The correct version is
\[e\cdot f\intrelG c \;\lor\; f\cdot e\intrelG c \;\Rightarrow\; e\cdot_{\it MM} f\intrelG c;\]
\noindent
the condition of this statement
reflects the fact that the normalization function will only
require computing $e\cdot_{\it MM}f$ whenever either
$e$ or $f$ is an integer.
The implementation of the tactic for the hierarchical case now becomes slightly more
sophisticated than the non-hierarchical one.
When given a goal $a=_A b$ it builds the syntactic representation of
$a$ and $b$ as before; and then looks at the type of $A$ to decide
whether it corresponds to a group, a ring or a field.
Using this information the tactic can then call the lemma stating correctness
of $\N$ w.r.t.\ the appropriate interpretation relation.
\subsection*{Optimization}
As was mentioned in Section~\ref{normalization}, normal forms for
polynomials are unique, contrarily to what happens with field expressions
in general.
This suggests that, when $A$ is a group or a ring, the decision procedure
for $a=_Ab$ can be simplified by building expressions $e$ and $f$
interpreting respectively to $a$ and $b$ and comparing their normal forms.
Clearly, this is at most as time-consuming as the previous version, since
computing $\N(e-f)$ requires first computing $\N(e)$ and $\N(f)$.
Also, since the normalization function was not defined at once, but
resorting to the auxiliary functions earlier presented, it is possible
to avoid using divisions altogether when working in rings and groups
by defining directly $\N'$ by e.g.
\[\N'(e+f)=\N'(e)+_{\it PP}\N(f)';\]
\noindent the base case now looks like
\[\N'(v)=v\cdot1+0.\]
\noindent
Notice that although we now have two different normalization functions
we still avoid duplication of the code, since they are both defined in
terms of the same auxiliary functions and these are where the real work is
done.
\section{Tighter Integration}\label{integration} %F
In the previous section we managed to avoid having different syntactic
expressions for the different kinds of algebraic structures.
We unified the types of syntactic expressions into one type $E$.
However we still had different interpretation relations $\intrelF$,
$\intrelR$ and $\intrelG$.
We will now analyze the possibility of unifying those relations
into one interpretation relation $\intrelS$.
This turns out to be possible,
but when one tries to prove the relevant lemmas for it
one runs into problems: to get the proofs finished one needs
to assume an axiom (in the type theory of Coq).
Every field, ring or group has an underlying carrier.
We will write $\crr{A}$ for the carrier of an algebraic structure $A$.
We now define an interpretation relation $\intrelS$ from the type of syntactic
expressions $E$ to an \emph{arbitrary} set\footnote{In the formalization
we actually have \emph{setoids} instead of sets, but that does not make a difference.}
$S$,
where that set is a parameter of the inductive definition.
This inductive definition quantifies
over \emph{different} kinds of algebraic structures in the clauses for the
different algebraic operations.
For instance the inductive clause for addition quantifies over groups.
$$\Pi_{G:{\rm Group}} \Pi_{e,f:E} \Pi_{a,b,c:\crr{G}} \,
(a +_G b =_G c)
\to(e\intrelX{\crr{G}} a)\to(f\intrelX{\crr{G}} b)\to
(e + f \intrelX{\crr{G}} c)$$
With this definition the diagram becomes the following.
\[
\xymatrix{
E \ar`d[dddr][dddrr]^(.4){\intrelS}
& & F : \mbox{Field}\ar[d] \\
& & R : \mbox{Ring}\ar[d] \\
& & G : \mbox{Group}\ar[d]^{\widehat{\;\mbox{\tiny\strut}\cdot\;}} \\
& & S : \mbox{Set}
}
\]
This gives a nice unification of the interpretation
relations.
However when one tries to prove the relevant lemmas
for it in Coq, the obvious way does not work.
%changed by lcf
To prove e.g.
$$
e \intrelS a \;\land\; e \intrelS b \;\Rightarrow\; a =_A b\\
$$
\noindent one needs to use inversion with respect to the inductive definition
of $\intrelS$ to get the possible ways that $e \intrelS a$ can be obtained;
but the \tacticname{Inversion} tactic of Coq then only produces
an equality between dependent pairs where what one needs is equality
between the second components of those pairs.
In Coq this is not derivable without the so-called $K$ axiom,
which states uniqueness of equality proofs.
\begin{center}
\verb|(A:Set; x:A; p:(x=x))p==(refl_equal A x)|
\end{center}
%The proofs clearly need inversion with respect to the inductive definition
%of $\intrelS$,
%but from the \tacticname{Inversion} tactic of Coq one only gets
%an equality between pairs where what one needs is equality between the second
%components of those pairs.
%In Coq this is not derivable without the so-called $K$ axiom.
\noindent We did not want to assume an axiom to be able to have our
tactic prove equalities in
algebraic structures that are clearly provable without this axiom.
For this reason we did not fully implement this more integrated version
of hierarchical reflection.
\section{Conclusion}\label{conclusion} %F+L
\subsection{Discussion}
We have shown how the {\tacticname{Rational}} tactic (first described
in~\cite{geu:wie:zwa:00}), which is used to prove equalities of expressions
in arbitrary fields, can be generalized in two distinct directions.
First, we showed in Section~\ref{functions} how this tactic could be
extended so that it would also look at the arguments of functions; the
same mechanism can be applied not only to unary total functions, as
explained, but also to binary (or $n$-ary) functions, as well as to
partial functions as defined in the C-CoRN library~\cite{ccorn}.
In Section~\ref{hierarchical} we discussed how the same syntactic type $E$
and normalization function $\N$ could be reused to define similar tactics
that will prove equalities in arbitrary rings or commutative groups.
The work here described has been successfully implemented in Coq, and
is intensively used throughout the whole C-CoRN library.
Further extensions of this tactic are possible; in particular, the same
approach easily yields a tactic that will work in commutative monoids
(e.g.\ the natural numbers with addition). For simplicity, and since
this adds nothing to this presentation, this situation was left out of
this paper.
Extending the same mechanism to non-commutative structures was not
considered. The normalization function intensively uses
commutativity of both addition and multiplication, so it cannot
be reused for structures that do not satisfy these; and the
purpose of this work was to reuse as much of the code needed for
{\tacticname{Rational}} as possible.
The correctness of the normalization function w.r.t.\ the
interpretation relation had to be proved three times, one for each
type of structure. In Section~\ref{integration} we showed one
possible way of overcoming this, that unfortunately failed because proving
correctness of the tactic would then require assuming an axiom which
is not needed to prove the actual equalities that the tactic is meant to solve.
\medskip
\noindent
A different approach to the same problem would be to use the constructor
subtyping of~\cite{bar:raa:00}.
This would allow one to define e.g.\ the interpretation relation for
rings $\intrelR$ by adding one constructor to that for groups $\intrelG$;
proving the relevant lemmas for the broader relation would then only
require proving the new case in all the inductive proofs instead of
duplicating the whole code.
Another advantage of this solution, when compared to the one explored
in Section~\ref{integration}, would be that the tactic could be programmed
and used for e.g.\ groups before rings and fields were even defined.
It would also be more easily extended to other structures.
Unfortunately, constructor subtyping for Coq is at the moment only a
theoretical possibility which has not been implemented.
\medskip
\noindent
It would be interesting to know whether the approach
from Section~\ref{integration} can be made to work without needing
the $K$ axiom for the proofs of the correctness lemmas.
\medskip
\paragraph{Acknowledgments.}
Support for the first author was provided by the Portuguese
{Fun\-da\-\c c\~ao} {pa\-ra} a {Ci\^en\-cia} e {Tec\-no\-lo\-gia,} under grant
SFRH / BD / 4926 / 2001, and by the FCT and FEDER via CLC.
\bibliographystyle{plain}
\bibliography{hrefl}
\end{document}