\documentclass{llncs}
\usepackage{makeidx}
\input{diagrams}
\input{extra-diagonals}
\newcommand{\bbb}{\cal}
\newcommand{\IN}{{\rm I\kern-.23em N}}
\newcommand{\N}{{\cal N}}
\newcommand{\NN}{\bar{\cal N}}
\newcommand{\hole}{-}
\newcommand{\wf}{{\rm wf}\,}
\newcommand{\lift}{{\rm lift}\,}
\newcommand{\fmult}{\cdot}
\newcommand{\emult}{*}
\newcommand{\fdiv}{\div}
\newcommand{\fdivv}{\mathbin{/\!/}}
\newcommand{\ediv}{/}
\newcommand{\eone}{{\sf u}}
\newcommand{\ezero}{{\sf z}}
\newcommand{\inte}[1]{[\![#1]\!]}
\newcommand{\intfun}[1]{[\![#1]\!]_\rho}
\newcommand{\intrel}{\mathbin{]\![_\rho}}
\newcommand{\forfun}[1]{|#1|}
\newcommand{\Pos}{{\sf Pos}}
\newcommand{\Prob}{{\sf Problem}}
\newcommand{\Prop}{{\sf Prop}}
\newcommand{\Set}{{\sf Set}}
\newcommand{\Type}{{\sf Type}}
\newcommand{\Dec}{{\sf Dec}}
\newcommand{\oftype}{{:}}
\newcommand{\arr}{{\rightarrow}}
\begin{document}
\title{Equational Reasoning via Partial Reflection}
\author{H.~Geuvers, F.~Wiedijk, J.~Zwanenburg\\
\{herman,freek,janz\}@cs.kun.nl}
\institute{Department of Computer Science, Nijmegen University, the
Netherlands}
\date{\today}
\maketitle
\begin{abstract}
We modify the reflection method to enable it to deal with partial
functions like division. The idea behind reflection is to program a
tactic for a theorem prover not in the implementation language but in
the object language of the theorem prover itself.
The main ingredients of the reflection method are a
syntactic encoding of a class of problems, an interpretation function
(mapping the encoding to the problem) and a decision
function, written on the encodings. Together with a correctness proof
of the decision function, this gives a fast method for solving
problems.
The
contribution of this work lies in the extension of the reflection
method to deal with equations in algebraic structures where some
functions may be partial. The primary example here is the theory of
fields. For the reflection method, this
yields the problem that the interpretation function
is not total. In this
paper we show how this can be overcome by defining the interpretation
as a relation.
We give
the precise details, both in mathematical terms and in Coq
syntax. It has been used to program our own tactic `Rational', for
verifying equations between field elements.
\end{abstract}
\section{Introduction}
We present a method for proving equations between field elements
(e.g.\ real numbers) in a theorem prover based on type theory. Our
method uses the {\em reflection method\/} as discussed in
\cite{how88,har95}: we encode the set of syntactic
expressions as an (inductive) data type, together with an interpretation
function $\inte{-}$ that maps the syntactic expressions to the field
elements. Then one writes a `normalization' function $\N$ that
simplifies syntactic expressions and one proves that this function is
correct, i.e.\ if $\N(t)=q$, then the interpretations of $t$ and $q$
($\inte{t}$ and $\inte{q}$) are equal in the field. Now, to prove an
equality between field elements $a$ and $b$, one has to find syntactic
expressions $t_1$ and $t_2$ such that $\N(t_1) = \N(t_2)$ and
$\inte{t_1}$ is $a$ and $\inte{t_2}$ is $b$. This method has been
applied successfully \cite{boutin97} to ring expressions in the
theorem prover Coq,
where it is implemented as the `Ring tactic': when presented with a
goal $a=b$, where $a$ and $b$ are elements of a ring, the Ring tactic
finds the underlying syntactic expressions for $a$ and $b$, executes
the normalization function and checks the equality of the normal
forms.
The application of the reflection method to the situation of fields
poses one big extra problem: syntactic expressions may not have an
interpretation, e.g.\ $\frac{1}{0}$. So, there is no interpretation
function from the syntactic expressions to the actual field
($\inte{-}$ would be partial). The solution that we propose here is to
write an interpretation {\em relation\/} instead: a binary relation
between syntactic expressions and field elements. Then we prove that
this relation is a partial function. The precise way of using this
approach is discussed below, including the technical details of its
implementation in Coq. For the precise encodings in Coq see \cite{fta}.
\subsection*{The reflection method in general}
Reflection is the method of `reflecting' part of the meta language in
the object language. Then meta theoretic results can be used to prove
results from the object language. Reflection
is also called {\em internalization\/} or the {\em two level
approach}: the {\em meta language level\/} is {\em internalised\/} in
the object language.
The reflection method can (and it has, see e.g.\ \cite{oosgeu00}) be
used in general in situations where one has a specific class of
problems with a decision function. It is also not just restricted to
the theorem prover Coq. If the theorem prover allows (A) user defined
(inductive) data types, (B) writing executable functions over these
data types and (C) user defined tactics in the meta language, then the
reflection method can be applied. The classes of problems that it can
be applied to are those where (1) there is a syntactic encoding of the
class of problems as a data type, say via the type $\Prob$, with (2) a
decoding function $\inte{-}: \Prob \rightarrow \Prop$ (where $\Prop$
is the collection of propositions in the language of our theorem
prover), (3) there is a decision function $\Dec:\Prob\rightarrow
\{0,1\}$ such that (4) one can prove $\forall p\oftype\Prob ((\Dec(p)
= 1) \rightarrow \inte{p})$. Now, if the goal is to verify whether
a problem $P$ from the class of problems holds, one has to find a
$p:\Prob$ such that $\inte{p} = P$. Then $\Dec(p)$ (together with the
proof of (4)) yields either a proof of $P$ (if $\Dec(p) =1)$ or it
`fails' (if $\Dec(p)=0$ we obtain no information about $P$). Note that
if $\Dec$ is complete, i.e.\ if $\forall p\oftype\Prob ((\Dec(p)
= 1) \leftrightarrow \inte{p})$, then $\Dec(p)=0$ yields a proof of
$\neg P$.
The construction of $p$ (the syntactic encoding) from $P$ (the
original problem) can be done in the implementation language of the
theorem prover. Therefore it is convenient that the user has access to
this implementation language; this is condition (C) above. If the user
has no access to the meta language, the reflection method still works,
but the user has to construct the encoding $p$ himself, which is very
cumbersome.
In this paper we first explain the reflection method by looking at the
example of numbers with multiplication. We point out precisely which
are the essential ingredients. Then we extend the example by looking
at numbers with multiplication and division. Here the partiality
problem arises. We explain how the reflection method can be applied
to this example. This is an illustration of what we have implemented
in Coq: a tactic for solving equations between elements of a field (a
set with multiplication, division, addition, subtraction, constants
and variables). The tactic has been applied successfully in a
formalization of real numbers in Coq that we are currently working
on.
\section{Equational reasoning using the reflection method}\label{secrefl}
We explain the reflection method by the simple example of numbers with
multiplication. Suppose we have $F:\Set$, $\fmult : F\arr F \arr F$,
$1:F$ and an equivalence relation $=_F$ on $F$ (either a built-in
equality of the theorem prover or a user defined relation) such that
\begin{enumerate}
\item[(i)] $=_F$ is a congruence for $\fmult$ (i.e.\ if $a =_F b$ and $c =_F d$,
then $a\fmult c =_F b\fmult d$),
\item[(ii)] $\fmult$ is associative and commutative,
\item[(iii)] $1$ is the unit with respect to $\fmult$.
\end{enumerate}
Phrased differently, $\langle F, \fmult, 1\rangle$ is an Abelian monoid.
When dealing with $F$, we will want to prove equations like
\begin{eqnarray}
(a\fmult c) \fmult (1 \fmult (a\fmult b)) &=_F& (a\fmult a) \fmult (b \fmult c)
\end{eqnarray}
where $a,b,c$ are arbitrary elements of $F$. To prove this equation
in a theorem prover each of the properties (i)--(iii) above has to be
used (several times). It is possible to write a `tactic' in the
theorem prover that does just that:
\begin{quote}
Apply each of the steps (i)--(iii) to rewrite the left and right hand
side
of equation (1) until the two sides of the equation are literally the
same.
\end{quote}
Obviously this is not a very smart tactic (e.g.\ it does not terminate
when the equality does not hold) and of course we can do better than
this by applying (i)--(iii) in a clever order. For the case of Abelian
monoids, this can be done by rewriting all terms into a normal form
which has the shape
$$a_1 \fmult (a_2 \fmult (\ldots \fmult (a_{n} \fmult 1)\ldots))$$
where $n\geq 0$ and $a_1, \ldots , a_n$ are elements of $F$ that can
not be decomposed, listed in alphabetic order. So $a_i$ may be a
variable of type $F$ or some other term of type $F$, that is not of
the form $-{\fmult}-$ or $1$. A tactic, which is written in the
meta language, has access to the code of $a_i$, hence it can order the
$a_i$ according to some pre-defined total order, say the lexicographic
one. (Note that a normal form as above can not be achieved via a
term rewrite system, because we have to order the variables.)
So, a more clever tactic does the following.
\begin{quote}
Rewrite the left and right hand side of equation (1) to normal form
and check if the two sides of the equation are literally the same.
\end{quote}
Following \cite{har95}, there are three ways to augment the theorem
prover with this proof technique for equational reasoning.
\begin{enumerate}
\item Add it to the primitives of the theorem prover,
\item Write (in the meta language) a tactic, built up from basic
primitive steps, that performs the normalization and checks the
equality.
\item Write a normalization function in the language of the theorem
prover itself and prove it correct inside the theorem prover; use this
as the core of the tactic.
\end{enumerate}
The first is obviously undesirable in general, as it gives no
guarantee that the method is correct (one could add any primitive rule
one likes). The second and third both have their own pros and cons,
which are discussed extensively in \cite{har95}. It is our experience
(and of others, see \cite{boutin97}) that especially for theorem
provers based on type theory, the third method is the most convenient
one if one wants to verify a large numbers of problems from one and
the same class. We will motivate why.
\subsection*{Reflection in type theory}
We still work with the Abelian monoid $\langle F, \fmult, 1\rangle$
from before and we want to verify equation (1). The equality on this
monoid will be denoted by $=_F$, which may be user defined or not, as
long as it is an equivalence relation and a congruence for
$\fmult$. Note that there is also the definitional equality, built-in
into Coq. This is usually denoted as $=_{\beta\delta\iota}$, as it is
generated from the literal ($\alpha$-) equality by adding the
computation steps $\beta$, $\delta$ (for unfolding definitions) and
$\iota$ (for recursion). Definitional equality is decidable and built
into the type checker; it is included in the equality $=_F$ (if two
terms are definitionally equal, they are equal in any respect).
We introduce an inductive type of {\em syntactic expressions}, $E$, by
$$E ::= V \mathbin{|}C \mathbin{|} E \emult E$$
where $V$ is the type of variables, let's take
$$V ::= {\IN}$$ and $C$ is the type of constant expressions,
containing in this case just one element, $\eone$. In type theory (using
Coq
syntax) the definition of $V$ and $E$ would be as follows.
\begin{verbatim}
Definition V : Set := nat.
Inductive E : Set :=
evar : V->E
| eone : E
| emult : E->E->E.
\end{verbatim}
To define the semantics of an expression $e:E$, we need a valuation
$\rho: V \to F$ to assign a value to the variables.
The interpretation function connecting the level of the syntactic
expressions $E$ and the semantics $F$ is then defined as usual by
recursion over the expression.
$$\intfun{\hole} : E \to F$$
In Coq syntax the interpretation function {\tt I} is defined as follows, given the Abelian
monoid {\tt }:
\begin{verbatim}
Variable rho : V->F.
Fixpoint I [e:E] : F :=
Cases e of
(evar v) => (rho v)
| eone => fone
| (emult e1 e2) => (fmult (I e1) (I e2))
end.
\end{verbatim}
Now we write a `normalization function':
$$\N : E \to E$$
that sorts variables, removes the unit (apart from
the tail position) and associates brackets to the left. We don't give
its encoding {\tt N : E -> E} in Coq, but give the following examples.
\begin{eqnarray*}
\N((v_0 \emult \eone) \emult (v_1 \emult v_2)) &=_{\beta\delta\iota}&
(v_0 \emult (v_1 \emult (v_2 \emult \eone))),\\
\N((v_2 \emult v_0) \emult v_1) &=_{\beta\delta\iota} & (v_0 \emult
(v_1 \emult (v_2 \emult \eone))).
\end{eqnarray*}
The equality $=_{\beta\delta\iota}$ is the internal (computational)
equality of the theorem prover: no proof is required for its
verification; a verification of such an equality is performed by the
type checker.
We prove the following key lemma for the normalization function.
$$\mbox{\it normcorrect\/} :\quad \intfun{e} =_F \intfun{\N(e)}$$
In Coq terminology: we construct a proof term
\begin{verbatim}
normcorrect : (rho: V -> F)(e:E)((I rho e) = (I rho (N e))).
\end{verbatim}
The situation is depicted in the following diagram; {\it
normcorrect\/} states that the diagram commutes.
$$\begin{diagram}
E & \rArr^{\N}& E\\
\dArr^{\inte{\hole}} & & \dArr_{\inte{\hole}} \\
F & \hLine_{=_F} & F
\end{diagram}$$
Solving equation $f =_F f'$ with $f$ and $f'$ elements of $F$ now amounts
to the following.
\begin{itemize}
\item Find ({\it by tactic\/}) $e, e'$ and $\rho$ with
$$\intfun{e} =_{\beta\delta\iota} f\mbox{ and }\intfun{e'}
=_{\beta\delta\iota} f'$$
\item Check ({\it by type checker\/}) whether
$$\N(e) =_{\beta\delta\iota} \N(e')$$
\end{itemize}
The proof of $f =_F f'$ is then found by
$$f =_{\beta\delta\iota} \intfun{e} =_F \intfun{\N(e)} =_{\beta\delta\iota}
\intfun{\N(e')} =_F \intfun{e'} =_{\beta\delta\iota} f'$$
from {\it normcorrect\/} for $e$ and $e'$ and {\it trans\/} of
$=_F$. In a diagram:
$$\begin{diagram}
E & \rArr^{\N}& E& \lArr^{\N}& E\\
\dArr^{\inte{\hole}} & & \dArr_{\inte{\hole}} &&\dArr_{\inte{\hole}} \\
F & \hLine_{=_F} & F& \hLine_{=_F} & F
\end{diagram}$$
In Coq this means that we have to construct a proof term of
type
\begin{verbatim}
f = f'
\end{verbatim}
This is done from {\tt normcorrect} using
the proofs of symmetry and transitivity of $=_F$, {\tt sym} and {\tt trans}.
\begin{verbatim}
sym : (x,y:F) (x = y) -> (y = x).
trans : (x,y,z:F) (x = y) -> (y = z) -> (x = z).
\end{verbatim}
The crucial point is that
\begin{verbatim}
(normcorrect rho e) : ((I rho e) = (I rho (N e))).
(normcorrect rho e') : ((I rho e') = (I rho (N e'))).
\end{verbatim}
can {\em only\/} be fitted together using {\tt trans},
when {\tt (N e)} and {\tt (N e')} are $\beta\delta\iota$-convertible.
In that case we find that
{\tt (I rho (N e))} is $\beta\delta\iota$-convertible with {\tt (I rho (N e'))}
as well, so if we call that {\tt g} by defining:
\begin{verbatim}
g := (I rho (N e))
\end{verbatim}
then we find that:
\begin{verbatim}
(normcorrect rho e) : (f = g).
(normcorrect rho e') : (f' = g).
\end{verbatim}
So using this, we can construct a proof term
\begin{verbatim}
(trans f g f' (normcorrect rho e) (sym f' g (normcorrect rho e')))
: f = f'.
\end{verbatim}
The important points to note here are
(1) This proof term of an equality has a relatively small size,
compared to a proof term that is spelled out completely in terms of
congruence (of $=_F$ w.r.t.\ $\cdot$) and reflexivity, symmetry and
transitivity (of $=_F$). The terms {\tt refl}, {\tt sym}, {\tt trans},
and {\tt normcorr} are just defined constants. The terms {\tt rho},
{\tt e} and {\tt e'} are generated by the tactic; {\tt rho} being of
size linear in {\tt f} and {\tt f'} with a rather small constant. A
proof term that is completely spelled out has a polynomial size in
{\tt f} and {\tt f'}.
If we unfold the definitions, we observe that the bulk of the proof
term is in {\tt normcorr}. This will be rather large but it only has
to be extended with a part of -- roughly -- the size of the input
elements themselves. So, then the proof term is still linear in the
size of the input terms.
(2) {\em Checking\/} this proof term (i.e.\ verifying whether it has
the type {\tt f = f'}) can in general take rather long. This is because
type checking now involves
serious computation, as we use the language of the theorem prover as a
small programming language. The bulk of the work for the type checker
is in verifying whether {\tt (N e)} and {\tt (N e')} are
$\beta\delta\iota$-convertible.
We compare this to the approach of using a tactic that is written
completely in the meta laguage. This tactic will do roughly the same
thing as our reflection method: reduce expressions to normal form and
generate step by step a proof term that verifies that this reduction
is correct. Checking such a proof term will take about the same time.
Some increase in speed may only be gained if we check a {\em user
generated\/} proof term, because this will (in general) avoid reducing
to full normal form (assuming the user sees the possible
`shortcuts').
(3) {\em Generating\/} the proof term is very easy, both for the
reflection method as for the tactic written in the meta language. The
tactics generate the full proof term without further interaction.
Note that a completely user generated proof term of an equality (which
may be fastest to type check, see above), is not realistic.
Here we also see why the reflection approach is particularly
appealing for theorem provers based on type theory: one has to
construct a proof term, which remains relatively small using
reflection. Moreover, these theorem provers provide the required
programming language to encode the normalization and interpretation
functions in.
Looking back at the example from the beginning, encoded in Coq, we
have as goal
\begin{verbatim}
Goal
((fmult (fmult a c) (fmult fone (fmult a b)))
= (fmult (fmult a a) (fmult b c))).
\end{verbatim}
Now the tactic generates
\begin{verbatim}
(emult (emult (evar 0) (evar 2))
(emult eone (emult (evar 0) (evar 1)))).
(* the e : E * )
(emult (emult (evar 0) (evar 0)) (emult (evar 1) (evar 2))).
(* the e' : E * )
\end{verbatim}
and a function {\tt rho : V -> F} which is defined in such a way that
\begin{verbatim}
(rho (evar 0)) = a
(rho (evar 1)) = b
(rho (evar 2)) = c
\end{verbatim}
Then it constructs a term as above,
\begin{verbatim}
(trans f g f' (normcorrect rho e) (sym f' g (normcorrect rho e')))
\end{verbatim}
where {\tt g} is {\tt (I rho (N e))}.
Note that {\tt (I rho (N e))} $=_{\beta\delta\iota}$ {\tt (I rho (N e'))}
$=_{\beta\delta\iota}$
\begin{verbatim}
(I rho (emult (evar 0) (emult (evar 0)
(emult (evar 1) (emult (evar 2) eone)))))
\end{verbatim}
$=_{\beta\delta\iota}$
{\tt (fmult a (fmult a (fmult b (fmult c fone))))}.
This term is given to the type checker. If it type checks with as type
the goal, the tactic succeeds (and it has constructed a proof term
proving the goal); if the type check fails, the tactic fails.
\section{Reflection With Partial Operations}
We explain partial reflection by adapting the example to include
division. We view division as a ternary operation:
$$a \fdiv b \fdivv p\mbox{ with } p \mbox{ a proof of }b \neq_F 0.$$
This is very much a type theoretic
view. One may alternatively write
$$a \fdiv b \mbox{ for }b \in \{ z\mathbin{|} z\neq_F 0 \},$$
but note that this also requires a proof of $b \neq_F
0$, before $\fdiv$ can be applied to it.
As a side remark, we note that we use the principle of {\em irrelevance
of proofs\/} when extending the equality on $F$ to expressions of the
form $a \fdiv b \fdivv p$. That is, if $p$ and $p'$ are both proofs of
$b\neq_F 0$, then $(a \fdiv b \fdivv p) =_F (a \fdiv b \fdivv p')$. In
our encoding in Coq, this is achieved by representing $\{ z\mathbin{|}
z\neq_F 0 \}$ by the type $\Pos$ of pairs $\langle b,p\rangle$ with $p:
(b\neq_F 0)$ {\em with the equality on $\Pos$ the one inherited from $F$}.
Then we let $\fdiv$ be a function from $F\times \Pos$ to $F$.
If we extend our structure with a zero element and a division
operator, like in fields, we encounter the problem of undefined
elements. These cause trouble in various places. First of all,
there is the question of which syntactic expression one allows: if
$1/0$ is accepted, which interpretation does it have (one has to
choose one). This is of course related to the question whether the
theorem prover allows to write down $\frac{a}{0}$ (whatever its
meaning may be).
The second problem is that a naive normalization function might
rewrite $0/(0/v)$ to $v$ (just because $x/(x/v) = x/x*v = 1*v =
v$). But then, $\frac{0}{\frac{0}{a}} = a$, which is undesirable. Note
that the `division by $0$' problem can occur in a more disguised form,
e.g.~in $\frac{y}{\frac{y}{a}} = a$, with $y$ a variable, which is
correct under the {\em side-condition\/} that $y\neq_F 0$.
So, it seems that, when normalizing an expression $e$, one would have to
take the {\em interpretation\/} $\intfun{e}$ into account (and the
interpretation of subexpressions of $e$) to verify that the
normalization steps are correct.
We have solved the problems just mentioned by
\begin{itemize}
\item Allowing syntactic expressions (like $1/0$) that have no
interpretation. So $\intfun{-}$ is defined as a relation, for which it
has to be {\em proved\/} that it is a partial function.
\item Writing the normalization function $N$ in such a way that, if
expression $e$ has an interpretation, then expression $N(e)$ has the
same interpretation as $e$.
\end{itemize}
\paragraph{Syntactic expressions}
We now define the inductive type of {\em syntactic expressions}, $E$, by
$$E ::= V \mathbin{|} C \mathbin{|} E \emult E \mathbin{|} E \ediv
E$$ where $V$ is again the type of variables, for which we take $V ::=
{\IN}$ again. $C$ is the type of constant expressions, now containing
a zero, $\ezero$, and a one expression, $\eone$. In type theory (using
Coq syntax):
\begin{verbatim}
Inductive E : Set :=
evar : V->E
| eone : E
| ezero : E
| emult : E->E->E
| ediv : E->E->E.
\end{verbatim}
Note that $E$ doesn't depend on $F$ and $\rho$; we have `light'
syntactic expressions (without any semantic information). This implies
that $1 \ediv 0$ is allowed in $E$: it is a well-formed expression.
\paragraph{Interpretation relation}
The semantics of an expression is now not given by a function but an
{\em interpretation relation}:
$$\intrel \subseteq E \times F$$
Again, we need a valuation
$\rho: V \to F$ to assign a value to the variables.
The interpretation relation can then be defined inductively as follows.
\begin{eqnarray*}
v_n\intrel f &\mbox{iff}& \rho (n) =_F f,\\
\eone \intrel f &\mbox{iff} & f =_F 1,\\
\ezero \intrel f &\mbox{iff} & f =_F 0,\\
(e_1\emult e_2)\intrel f &\mbox{iff}& \exists f_1,f_2\in F\;( e_1
\intrel f_1) \wedge (e_2 \intrel f_2) \wedge (f =_F f_1
\fmult f_2),\\
(e_1 \ediv e_2)\intrel f &\mbox{iff}& \exists f_1,f_2\in F\;( e_1
\intrel f_1) \wedge (e_2 \intrel f_2) \wedge (f_2 \neq_F 0)
\wedge (f =_F f_1\fdiv f_2).
\end{eqnarray*}
In Coq let there be given a structure {\tt }, with
\begin{verbatim}
fdiv: (x,y:F)(~(y =_F fzero))->F
\end{verbatim}
and the other operations and the equality as expected. The inductive
definition of $\intrel$ is as follows.
\begin{verbatim}
Inductive I : E->F->Prop :=
ivar : (n:V)(f:F) ((rho n) = f) -> (I (evar n) f)
| ione : (f:F) (fone = f) -> (I eone f)
| izero : (f:F) (fzero = f) -> (I ezero f)
| imult : (e,e':E)(f,f',f'':F)
((fmult f f') = f'') -> (I e f) -> (I e' f')
-> (I (emult e e') f'')
| idiv : (e,e':E)(f,f',f'':F)(nz:~(f' = fzero))
((fdiv f f' nz) = f'') -> (I e f) -> (I e' f')
-> (I (ediv e e') f'').
\end{verbatim}
Note that we do not just let {\tt ione : (I eone fone)}, but take {\tt
fone} modulo the equality on {\tt F}, and similarly for the constant,
the variables and the two operators. This is because {\tt I} should be
a partial function {\em modulo\/} the equality on {\tt F}. In more
technical terms: correctness of normalization can only be proved with
this version of {\tt I}.
\paragraph{Normalization and correctness}
The `normalization function':
$$\N : E \to E$$
now brings the expressions that have an interpretation in one of the
following two normal forms
\begin{eqnarray*}
(v_1 \emult (v_2 \emult \ldots (v_{n} \emult \eone)\ldots)) &/&
(w_1 \emult (w_2 \emult \ldots (w_{m} \emult \eone)\ldots)),\\
\ezero &/ &\eone,
\end{eqnarray*}
with $v_1, \ldots, v_n, w_1, \ldots w_m$ variables and the two lists
$v_1, \ldots, v_n$ and $w_1, \ldots w_m$ disjoint. So, $\N$ creates
two mutually exclusive lists of sorted variables, one representing the
enumerator and one representing the denominator. The sorting of these
lists is the same as for multiplicative expressions. In case $\N$
encounters a $\ezero$ in the enumerator, the whole expression is
replaced by $\ezero / \eone$ (which has interpretation
$0$). For the expressions that do not have an interpretation (those
$e\in E$ for which there are no $\rho:V\arr F, f\in F$ with $e \intrel
f$), the normalization function can return anything.
We don't give
the encoding {\tt N : E -> E} in Coq, but restrict ourselves
to some examples.
\begin{eqnarray*}
\N(v_0 \ediv(v_1\ediv v_3)) \emult v_1 &=_{\beta\delta\iota}& (v_0
\emult (v_3\emult \eone)) \ediv \eone,\\
\N((v_0 \ediv (v_1 \emult v_2)) \ediv
(v_3 \ediv v_2)) & =_{\beta\delta\iota} & (v_0 \emult \eone)\ediv
(v_1\emult (v_3\emult \eone)).
\end{eqnarray*}
We can understand the way $\N$ actually works as follows.
\begin{enumerate}
\item From an expression $e$, two sequences of variables and constants
are created $s_1$ and $s_2$, the first representing the enumerator and
the second the denominator. The intention is that, if $e$ has an
interpretation, then $s_1 \ediv s_2$ has the same interpretation.
\item These two sequences are put in normal form, following the
normalization procedure for multiplicative expressions.
\item Variables that occur both in $s_1$ and $s_2$ are canceled,
units are removed and $s_1$ is replaced by $\ezero$ if it contains a
$\ezero$.
\end{enumerate}
Note that we tacitly identify a sequence $s_1$ with the expression
that arises from consecutively applying $\emult$ to all its
components. This is also the way we have
implemented it in Coq: we do not use a separate list data structure,
but encode it via $\emult$ and $\eone$. On these lists, we define an
`append' operation, which we denote by $@$. So, if $s_1$ and $s_2$
denote two expressions in multiplicative normal form, $s_1 @ s_2$ is
the multiplicative normal form of $ s_1 \emult s_2$.
As a matter of fact, $\N$ doesn't do each of these steps sequentially,
but in a slightly smarter (and faster) way.
In proving the correctness of $\N$, one has to preserve the property
that all denominators are $\neq_F 0$. In that, the first step is the
crucial one. (The second step is only a reordering of variables; one
has to prove that this reordering preserves the $\neq_F 0$ property,
which is easy. In the third step one has to prove that $\neq_F 0$ is
preserved under cancellation, which is the case: if $a\cdot b \neq_F 0$,
then $a\neq_F 0$.) The first step has a nice recursion:
if $\N(e) = (s_1, s_2)$ and $N(e') = (s_1',s_2')$, then
\begin{eqnarray*}
\N(e \emult e') &:=& (s_1 @ s_1' , s_2 @ s_2'),\\
\N(e \ediv e') &:=& (s_1 @ s_2' , s_2 @ s_1').
\end{eqnarray*}
Now, if $e \emult e'$ has an interpretation, then (by induction) $s_2$
and $s_2'$ have an interpretation different from $0$ and hence the
interpretation of $s_2 @ s_2'$ is different from $0$. Similarly, if
$e \ediv e'$ has an interpretation, then (by induction) $s_2$, $s_1'$
and $s_2'$ have an interpretation different from $0$ and hence the
interpretation of $s_2 @ s_1'$ is different from $0$.
This is also how the correctness proof of $\N$ works: $\N$ itself
doesn't have to bother about the interpretation of the expressions it
operates on, because it is written in such a way that, the fact that
$e$ has an interpretation implies (in a rather simple way, sketched
above) that $\N(e)$ has an interpretation (which is the same as for
$e$).
Again we note that $\N$ cannot be found as a term rewriting system,
for one because it orders variables, but more importantly because it
only works properly for expressions that have an interpretation. We
can use this information, because the expression we start from is
derived from an existing $f:F$, which is well-defined (otherwise we
couldn't write it down in the theorem prover). So, we already know
that the first $e$ has an interpretation (namely $f$) and by virtue of
the construction of $\N$, this property is preserved.
We prove the following key lemmas.
$$\begin{array}{rcccl}
\mbox{\it normcorrect\/} &:&\quad e \intrel f &\Rightarrow& \N(e) \intrel
f\\
\mbox{\it extensionality\/} &:&\quad (e \intrel f) \wedge (e \intrel f')
&\Rightarrow& f =_F f'.
\end{array}$$
Extensionality states that $\intrel$ is really a partial function
(w.r.t.\ the equality $=_F$).
\paragraph{Reflection}
The reflection method for solving $f =_F f'$ is now:
\begin{itemize}
\item find ({\it by tactic\/}) $e, e'$ and $\rho$ with
$$\mbox{$e \intrel f$ and $e' \intrel f'$}$$
\item construct ({\it see below\/}) proof terms for these two statements
\item check ({\it by type checker\/}) whether
$$\N(e) =_{\beta\delta\iota} \N(e')$$
($=_{\beta\delta\iota}$ means $\beta\delta\iota$-{\it convertible\/})
\end{itemize}
The proof of $f =_F f'$ is then found by:
$$\left.\begin{array}{lll}
e \intrel f &\Rightarrow& \N(e) \intrel f\\ \\
e' \intrel f' &\Rightarrow& \N(e') \intrel f'
\end{array}\right\} \Rightarrow f = f'$$
from {\it normcorrect\/} (applied to $(e,f)$ and $(e',f')$, respectively)
and
{\it extensionality\/} (applied to $(\N(e),f,f')$).
Just as in the case for reflection in Section \ref{secrefl}, a precise
proof term can be constructed, which type checks with type $f=_F f'$
if and only if these terms are can be shown to be equal in the
equational theory. In the next Section we will exhibit such a proof term.
The main work in type checking this proof term lies
in the execution of the algorithm $\N$ (but this is done by the type
checker).
One problem remains. As we now have an interpretation {\em relation}, there
arise some {\em proof obligations}: it is not just enough to {\em
find\/} encodings $e$ and $e'$ of $f$ and $f'$; we have to {\em
prove\/} that they are encodings indeed. That is, we have as new goals
$$\mbox{$e \intrel f$ and $e' \intrel f'$}$$
Of course, we don't want the user to have to take care of these goals;
the tactic should solve them.
This problem is dealt with in the next Section.
\section{Proof Loaded Syntactic Objects}
At the second step of the partial reflection method, we need proofs of $e
\intrel f$.
One way is to let the tactic construct these; so from $f:F$, the
tactic extracts both $e:E$ and $\rho$ and a proof term $p$ with
$p:e\intrel f$. This is possible, but it is not what has been
implemented. We have chosen to have one data type for both expressions
and proofs.
The strategy for doing so (and which fits very well with the type
theoretic approach) is to create {\em syntactic expressions with
proof objects inside}
$$\bar E$$
with a {\em forgetful function\/}
$\forfun{\hole}$ and an {\em interpretation function\/}
$\intfun{\hole}$,
\begin{eqnarray*}
\forfun{\hole} &:& \bar E \to E\\
\intfun{\hole} &:& \bar E \to F
\end{eqnarray*}
The key property to be proved is then
$$\forfun{\bar e} \intrel \intfun{\bar e}$$
But note that $\bar E$ depends on $F$ and $\rho$ (it should `know'
about semantics), so $\bar E$ is a type of `heavy' syntactic
expressions (including proof terms).
This can only work if we let
$\bar E$ be a {\em dependent\/} type over $F$:
$$\bar E_f$$
which in Coq terms is defined as:
\begin{verbatim}
Inductive xE : F -> Set :=
xevar : (i:V)(xE (rho i))
| xeone : (xE fone)
| xezero : (xE fzero)
| xemult : (f,f':F)(e:(xE f))(e':(xE f'))(xE (fmult f f'))
| xediv : (f,f':F)(e:(xE f))(e':(xE f'))(nz:~(f' = fzero))
(xE (fdiv f f' nz)).
\end{verbatim}
The type $\bar E_f$ represents
the type of `heavy' syntactic expressions whose interpretation is
$f$.
The interpretation function is now
$$\intfun{\hole} : \bar E_f \to F$$
for which it should hold that
$$\intfun{\bar e} =_{\beta\delta\iota} f$$
so $\intfun{\hole}$ is constant on its domain. In Coq terms we define:
\begin{verbatim}
xI := [f:F][e:(xE f)]f : (f:F)(xE f) -> F.
\end{verbatim}
Note that we do not define the interpretation by induction on ${\tt e
:(xE f)}$, but we just return $f$ (the {\em intended\/}
interpretation). The obligation is now to prove that the underlying
`light' syntactic expression has indeed $f$ as interpretation.
The forgetful function, extracting the `light' syntactic expression, now is
$$\forfun{\hole} : \bar E_f \to E$$
It maps the `heavy' syntactic expressions to the `light' ones.
In Coq terms:
\begin{verbatim}
Fixpoint xX [f:F; e:(xE f)] : E :=
Cases e of
(xevar i) => (evar i)
| xeone => eone
| xezero => ezero
| (xemult f' f'' e' e'') => (emult (xX f' e') (xX f'' e''))
| (xediv f' f'' e' e'' p) => (ediv (xX f' e') (xX f'' e''))
end.
\end{verbatim}
which is defined by induction over {\tt (xE f)}.
The maps $\intfun{\hole}$ and $\forfun{\hole}$ `extract' the two
components (syntactic expression and semantic element) from the
`heavy' encoding. The key result now is that the second extraction is
an interpretation of the first:
$$\mbox{\it extractcorrect\/}: \quad \forall x\in \bar E_f ( \forfun{x} \intrel
\intfun{x})$$ which is just $\forall x\in \bar E_f ( \forfun{x}
\intrel f)$.
The tactic now works as follows, given a problem $f=_F f'$.
\begin{itemize}
\item find ({\it by tactic\/}) $\bar e\in \bar E_f$, $\bar e'\in \bar
E_{f'}$
and $\rho$ with
$$\mbox{$\forfun{\bar e} \intrel f$ and $\forfun{\bar e'} \intrel f'$}$$
\item obtain ({\it from extractcorrect\/}) proof terms for these two
statements
\item check ({\it by type checker\/}) whether
$$\N(\forfun{\bar e}) =_{\beta\delta\iota} \N(\forfun{\bar e'})$$
\end{itemize}
So, the tactic creates $e, e'$ of type $E$ indirectly by creating
$\bar e, \bar e'$ of types $\bar E_f, \bar E_{f'}$.
In a diagram the situation is now as follows.
$$\begin{diagram}
{\bar E_f} &\rArr^{\forfun{\hole}} & E & \rArr^{\N}& E& \lArr^{\N}& E&\lArr^{\forfun{\hole}} & {\bar E_{f'}}\\
&\SE_{\inte{\hole}} &\vLine^{\intrel} & \SWl_{\intrel} & &\SEl_{\intrel}&\vLine_{\intrel}&\SW_{\inte{\hole}}& \\
&& F & & \hLine_{=_F}& & F&&
\end{diagram}$$
The outside triangles commute due to {\it extractcorrect}; the large
middle triangle commutes due to {\it extensionality}; the other two
triangles commute due to {\it normcorrect}.
If we make the proof term given by this method explicit, it is
\begin{verbatim}
(extensionality rho ne f f'
(normcorrect rho e f (extractcorrect rho f xe ))
(normcorrect rho e' f' (extractcorrect rho f' xe')))
: f = f'
\end{verbatim}
where {\tt xe} and {\tt xe'} correspond to $\bar e$ and $\bar e'$, and
where we have defined
\begin{verbatim}
e := (xX f xe).
e' := (xX f' xe').
ne := (N e).
\end{verbatim}
This term is only well-typed when {\tt (N e)} is $\beta\delta\iota$-convertible with {\tt (N e')}.
\subsection*{Normalizing Proof Loaded Objects}
In presence of the type $\bar E_f$, we could do
without the type $E$ all-together. Then we would define a
normalization function $\NN$ to operate on the `heavy' syntactic
expressions of type $\bar E_f$. This is possible (and it yields a
simpler diagram), but it is not desirable, because then the
computation (reducing $\NN ({\bar e})$ to normal form) becomes much
heavier. Moreover, it would be more difficult to program $\NN$ (having
to take all the proof terms into account) and the two levels in the
reflection approach would be less visible, therefore slightly blurring
the exposition.
Nevertheless, for reasons of completeness we have also constructed
(see \cite{fta}) the function $\NN$ together with proofs that it is
correct. Ideally, this would amount to the following diagram
$$\begin{diagram}
\bar E_f & \rArr^{\NN} & \bar E_f & \lArr^{\NN} & \bar E_f \\
\dArr_{\inte{\hole}} & & \dArr_{\inte{\hole}} & &
\dArr_{\inte{\hole}} \\
F & & F & & F
\end{diagram}$$
However, $\NN$ can not have the dependent type $\bar E_f \rightarrow
\bar E_f$ (for $f:F$), because the value (in $F$) of the output of the
normalization function is not {\em literally\/} the same as its input
value, but only {\em provably\/} equal to it. So, we can {\em not\/}
construct $\NN$ as a term \verb! xN : (z:F) (xE z) -> (xE z)!.
Instead we construct \verb! xN : fE -> fE!, where \verb!fE! is the
type of pairs \verb!< f, e >!, with \verb!f : F! and
\verb!e : (xE f)!. (In type theoretic terms, this is the {\em
$\Sigma$-type\/} of {\em dependent pairs\/} $\langle f , e\rangle$
with $f:F$ and $e: {\bar E_f}$.) Then we have to prove that if
$\NN(\langle f, e \rangle)$ yields $\langle f', e' \rangle$, then
$f$ and $f'$ are (provably) equal in F.
If we cast this in purely mathematical terms, the situation is as
follows. Define $\bar E := \Sigma f\oftype F. \bar E_f$ and let $\wf$
be the predicate on syntactic expressions stating that it has an
interpretation (it is {\em well-formed}). It is defined as follows
(for $e:E$).
$$\wf (e) := \exists f\oftype F (e\intrel f).$$
Now there are maps $\lift: \{e:E \mathbin{|} \wf(e)\} \rightarrow \bar E$
and $\forfun{-}: {\bar E} \rightarrow \{e:E \mathbin{|} \wf(e)\}$.
Furthermore,
we can construct a proof-object
$$\mbox{\it normwf\/} \quad : \quad \forall e\oftype E (\wf (e)
\rightarrow \wf(\N (e)))\}.$$
Then we can read off the normalization function
$\bar N:\bar E \rightarrow \bar E$ from the
following diagram.
$$\begin{diagram}
\bar E & \rDasharr^{\NN} & \bar E \\
\dArr^{\forfun{-}}\uArr_{\lift} & & \dArr^{\forfun{-}}\uArr_{\lift}\\
\{e:E \mathbin{|} \wf(e)\} & \rArr_{\N}&
\{e:E \mathbin{|} \wf(e)\}\\
\end{diagram}$$
The proof term {\it normwf\/} shows that $\N$ is indeed a function
from the set of well-formed expressions to itself. The correctness of
$\NN$ is given by
$$\mbox{\it normcorrect\/} \quad : \quad \forall {\bar e}\oftype {\bar
E} (\inte{\bar e} =_F \inte{\NN({\bar e})}).$$
Here $\inte{-}: {\bar E} \rightarrow F$ is the interpretation function
mapping (heavy) syntactic expressions to elements of $F$. (As a matter
of fact, it is just the first projection.)
\section{Partial Reflection in Practice}
The approach of partial reflection is successfully used in our current
FTA project (Fundamental Theorem of Algebra).
First of all, we have a tactic called {\tt Rational} for proving equalities.
This tactic is implemented as outlined above.
But often we do not just want to prove an equality, but rather to use
an equality to {\em rewrite} a goal in a different form. In order to
explain how we have implemented rewrite tactics, we first say
something about the equality in the FTA project. Our equality is just
a congruence relation, respected by operations (such as \verb!+! and
\verb!*!) and certain predicates (such as \verb! (b (a