\usepackage[show]{ed}
\usepackage{draftstamp}
+\newcommand{\musing}{\texttt{musing}}
+\newcommand{\musings}{\texttt{musings}}
\newcommand{\ws}{Web-Service}
\newcommand{\wss}{Web-Services}
\newcommand{\hbugs}{H-Bugs}
The \ws{} approach at software development seems to be a working solution for
getting rid of a wide range of incompatibilities between communicating
software applications. W3C's efforts in standardizing related technologies
- grant longevity and implementations availability for frameworks based on \wss{}\
- for information exchange. As a direct conseguence, the number of such
+ grant longevity and implementations availability for frameworks based on
+ \wss{} for information exchange. As a direct conseguence, the number of such
frameworks is increasing and the World Wide Web is moving from a disorganized
repository of human-understandable HTML documents to a disorganized repository
of applications working on machine-understandable XML documents both for input
il concetto di broker non e' definito da W3C e co} of the \wss{}/brokers
approach, is working on the development of a framework aimed at providing a
set of software tools for the advertisement and discovering of mathematical
- web services.
+ \wss{}.
%CSC This framework turns out to be strongly based on both \wss{} and brokers.
Several groups have already developed \wss{} providing both computational and
reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
- dalle conferenze calculemus}: the first ones are implemented on top of
- Computer Algebra Systems; the last ones provide interfaces to well-known
- theorem provers. Proof-planners, proof-assistants, CAS themselves and
+ dalle conferenze calculemus}: the formers are implemented on top of
+ Computer Algebra Systems; the latters provide interfaces to well-known
+ theorem provers. Proof-planners, proof-assistants, CAS and
domain-specific problem solvers are natural candidates to be client of these
services. Nevertheless, so far the number of examples in the literature has
been extremely low and the concrete benefits are still to be assessed.
come ws client si}
{
Despite of that the proof assistant case seems to be well suited to
- investigate the usage of many different mathematical \wss{}. Indeed: most proof
- assistants are still based on non-client/server architectures, are
+ investigate the usage of many different mathematical \wss{}. Indeed: most
+ proof assistants are still based on non-client/server architectures, are
application-centric instead of document-centric, offer a scarce level of
automation leaving entirely to the user the choice of which macro (usually
called \emph{tactic}) to use in order to make progress in a proof.
The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
- Each actor present one or more \ws{} interface to its neighbours \hbugs{}
+ Each actor present one or more \ws{} interfaces to its neighbours \hbugs{}
actors.
- In this section we will detail the role and requiremente of each kind of
+ In this section we will detail the role and requirements of each kind of
actors and discuss about the correspondencies between them and the MONET
entities described in \cite{MONET-Overview}.
An \hbugs{} client is a software component able to produce \emph{proof
status} and to consume \emph{hints}.
- \ednote{"status" ha il plurale?}
+ \ednote{Zack: "status" ha il plurale? CSC: no}
A proof status is a representation of an incomplete proof and is supposed to
be informative enough to be used by an interactive proof assistant. No
- additional requirement exists on the proof status, but there should be an
+ additional requirements exist on the proof status, but there should be an
agreement on its format between clients and tutors. An hint is a
- representation of a step that can be performed in order to proceed in an
- incomplete proof. Usually it represents a tactic available on some proof
- assistant along with instantiation of its parameters for tactics which
- require them.
+ representation\ednote{non c'\'e un sinonimo pi\'u carino?}
+ of a step that can be performed in order to proceed in an
+ incomplete proof. Usually it represents a reference to a tactic available
+ on some proof assistant along with an instantiation for its formal
+ parameters. More structured hints can also be used: an hint can be
+ as complex as a whole proof-plan.
Clients act both as \ws{} provider and requester (using W3C's terminology
\cite{ws-glossary}). They act as providers for the broker (to receive hints)
- ans as requesters again for the broker (to submit new status). Clients
+ and as requesters (to submit new status). Clients
additionally use broker service to know which tutors are available and to
subscribe to one or more of them.
dialog box or enlightening a tactic button).
\hbugs{} clients act as MONET clients and ask broker to provide access to a
- set of services (the tutors). \hbugs{} has no actors corresponding to MONET's
- Broker Locating Service (since the client is supposed to know the URI of at
- least one broker) and Mathematical Object Manager (since proof status are
- built on the fly and not stored).
+ set of services (the tutors). \hbugs{} has no actors corresponding to
+ MONET's Broker Locating Service (since the client is supposed to know the
+ URI of at least one broker) and Mathematical Object Manager (since proof
+ status are built on the fly and not stored).
\paragraph{Brokers}
\hbugs{} brokers are the key actors of the \hbugs{} architecture since they
- act as intermediaries between clients and tutors. They act both as \ws{}
- provider and requester \emph{both} for clients and tutors.
+ act as intermediaries between clients and tutors. They behave as \ws{}
+ providers and requesters for \emph{both} clients and tutors.
- With respect to client, a broker act as \ws{} provider receiving status and
- forwarding them to one or more tutors. They act as \ws{} requester sending
- hints to client as soon as they are available from tutors.
+ With respect to client, a broker act as \ws{} provider, receiving the
+ proof status and forwarding it to one or more tutors.
+ It also acts as a \ws{} requester sending
+ hints to client as soon as they are available from the tutors.
With respect to tutors, the \ws{} provider role is accomplished by receiving
- hints as soon as they are produced; the \ws{} requester one is accomplished
- by requesting computations (\emph{musings} in \hbugs{} terminology) on status
- received by clients and stopping out of date ongoing musings.
+ hints as soon as they are produced; as a requester one is accomplished
+ by requesting computations (\emph{musings} in \hbugs{} terminology) on
+ status received by clients and by stopping already late but still
+ ongoing \musings{}
+ \ednote{Sta frase va comunque riscritta perch\'e non si capisce una mazza}.
- Additionally brokers keep track of available tutors and subscription of each
- client.
+ Additionally brokers keep track of available tutors and clients
+ subscriptions.
\hbugs{} brokers act as MONET brokers implementing the following components:
Client Manager, Service Registry Manager (keeping track of available
\paragraph{Tutors}
Tutors are software component able to consume proof status producing hints.
- \hbugs{} doesn't specify by which means hints should be produced, tutors can
+ \hbugs{} doesn't specify by which means hints should be produced: tutors can
use any means necessary (heuristics, external theorem prover or CAS, ...).
The only requirement is that exists an agreement on the formats of proof
status and hints.
- tutors act both as \ws{} providers and requesters for broker. As providers,
- they wait for commands requesting to start a new musing on a given proof
- status or to stop an old, out of date, musing. As requesters, they signal to
- the broker the end of a musing along with its outcome (an hint in case of
- success or a notification of failure).
+ Tutors act both as \ws{} providers and requesters for the broker. As
+ providers, they wait for commands requesting to start a new \musing{} on
+ a given proof status or to stop an old, out of date, \musing{}. As
+ requesters, they signal to the broker the end of a \musing{} along with its
+ outcome (an hint in case of success or a notification of failure).
\hbugs{} tutors act as MONET services.
XML format as the target format for the serialization.
A schematic representation of the gTopLevel internal status is depicted in
- Fig. \ref{status}. Each proof is representated by a 4-tuple: \emph{uri},
- \emph{metasenv}, \emph{proof}, \emph{term}.
+ Fig. \ref{status}. Each proof is representated by a tuple of four elements:
+ \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
\myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
status}
\begin{description}
\item[uri]: an URI chosen by the user at the beginning of the proof
process. Once (and if) proved, that URI will globally identify the term
- inside the \helm{} framework (given that the user decide to save it).
- \item[metasenv]: a list of opened \emph{goals}, in order to complete the
- proof the user has to fill them all. Each of them is identified by an
- integer index, has a context (\emph{meta}) and a type (\emph{goal}). The
- context is in turn represented as a list of named hypotheses
- (declarations and definitions).
+ inside the \helm{} library (given that the user decides to save it).
+ \item[thesis]: the thesis of the ongoing proof
\item[proof]: the current incomplete proof tree. It can contain
- metavariables (\emph{holes}) that need to be proved in order to complete
- the proof. Each metavariables appearing in the tree reference one
- element of the current metasenv.
- \item[term]: the term that the ongoing proof aims to prove
+ \emph{metavariables} (holes) that stands for the parts of the proof
+ that are still to be completed. Each metavariables appearing in the
+ tree references one element of the metavariables environment
+ (\emph{metasenv}).
+ \item[metasenv]: the metavariables environment is a list of
+ \emph{goals} (unproved conjectures).
+ In order to complete the proof, the user has to instantiate every
+ metavariable in the proof with a proof of the corresponding goal.
+ Each goal is identified by an unique identifier and has a context
+ and a type ( the goal thesis). The context is a list of named
+ hypotheses (declarations and definitions). Thus the context and the goal
+ thesis form a sequent, which is the statement of the proof that will
+ be used to instatiate the metavariable occurrences.
\end{description}
Each of these information is represented in XML as described in
- \cite{csc-thesis}. Additionally \hbugs{} status carry an integer value
- referencing one of the opened goal; using this value is possible to
- implement different client side strategies: the user could ask the tutors to
- work on the same goal as the user or to work on ``background'' goals.
+ \cite{csc-thesis}. Additionally, an \hbugs{} status carry the unique
+ identifier of the current goal, which is the goal the user is currently
+ focused on. Using this value it is possible to implement different client
+ side strategies: the user could ask the tutors to work on the goal
+ she is considering or to work on the other ``background'' goals.
\paragraph{Hints}
An hint in the \hbugs{} architecture should carry enough information to
- permit to the client to make progress in the current proof. In our
- implementation each hint reference one of the tactic available to the user
- in gTopLevel.
+ permit the client to progress in the current proof. In our
+ implementation each hint corresponds to either one of the tactics available
+ to the user in gTopLevel (together with its actual arguments) or a set
+ of alternative suggestions (a list of hints).
For tactics that don't require any particular argument (like tactics that
apply type constructors or try to automatically conclude equality goals)
- only the tactic name is represented in the hint. For tactic that need terms
+ only the tactic name is represented in the hint. For tactics that need terms
as arguments (for example the \emph{Apply} tactic) the hint includes a
textual representation of them, using the same representation used by the
- interactive proof assistent when querying user for terms.
+ interactive proof assistant when querying user for terms. In order to be
+ trasmitted between \wss, hints are serialized in XML.
- Hints are serialized to an XML format for the same reasons reported for the
- proof status.
-
- Actually is also possible for a tutor to return more hints at once, grouping
- them in a particular XML element. This feature turns out to be particulary
- useful for the \emph{searchPatternApply} tutor (Sect. \ref{tutors}) that
+ Actually it is also possible for a tutor to return more hints at once,
+ grouping them in a particular XML element.
+ This feature turns out to be particulary useful for the
+ \emph{searchPatternApply} tutor (Sect. \ref{tutors}) that
query a term database and return to the client a list of all terms that
could be used to complete the proof. This particular hint is encoded as a
list of Apply hints, each of them having one of the results as term
argument.
- We would like to stress once more that neither the hint nor the status
- representation are fixed by the \hbugs{} architecture. Is only necessary
- that a common format exists and is understood by both clients and tutors.
+ We would like to stress that the \hbugs{} architecture has no dependency
+ on either the hint or the status representation: the only message parts
+ that are fixed are those representing the administrative messages
+ (the envelops in the \wss terminology). In particular, the broker can
+ manage at the same time several sessions working on different status/hints
+ formats. Of couse, there must be an agreement between the clients
+ and the tutors on the format of the data exchanged.
- Additionally, please note that there is no ``trust'' assumed on tutors'
- hints. Being encoded as references to available tactics and argument imply
+ In our implementation the client does not trust the tutors' hints:
+ being encoded as references to available tactics imply
that an \hbugs{} client, on receipt of an hint, simply try to reply the work
done by a tutor on the local copy of the proof. The application of the hint
can even fail to type check and the client copy of the proof can be left
- undamaged after spotting the error (assuming that client's type checking
- implementation is correct, though).
+ undamaged after spotting the error. Note, however, that it is still
+ possible to implement a complex tutor that looks for a possible proof and
+ send back to the client an hint whose argument is a witness (a trace) of
+ the proof found: the client applies the hint reconstructing (and checking
+ the correctness of) the proof from the witness, without having to
+ re-discover the proof itself.
+
+ An alternative implementation where the tutors are trusted would simply
+ send back to the client a new proof-status. Upong receiving the
+ proof-status, the client would just override its current proof status with
+ the suggested one. In the case of those clients which are implemented
+ using proof-objects (as the Coq proof-assistant, for instance), it is
+ still possible for the client to type-check the proof-object and reject
+ wrong hints. The systems that are not based on proof-objects
+ (as PVS, NuPRL, etc.), instead, have to trust the new proof-status. In this
+ case the \hbugs{} architecture needs to be extended with clients-tutors
+ autentication.
- Other choices of hints encoding (like sending the \emph{result} of the hint
- application), even if reducing total computation time, don't benefit of this
- nice property.
-
\paragraph{Registries}
Being central in the \hbugs{} architecture, the broker is also responsible
of accounting operations both for clients and tutors. These operations are
implemented using three different data structures called \emph{registries}:
- clients registry, tutors registry and musings registry.
+ clients registry, tutors registry and \musings{} registry.
In order to use the suggestion engine a client should register itself to the
broker and subscribe to one or more tutors. The registration phase is
- triggered by the client using the \emph{Register\_client} method of the
- broker to send him an unique identifier and the base URI at which client's
- \ws{} is available. After the registration, the client can use broker's
- \emph{List\_tutors} method to get a list of available tutors. Eventually the
+ triggered by the client using the \texttt{Register\_client} method of the
+ broker to send him an unique identifier and its base URI as a
+ \ws{}. After the registration, the client can use broker's
+ \texttt{List\_tutors} method to get a list of available tutors.
+ Eventually\ednote{CSC: Vuoi veramente dire eventually qui?} the
client can subscribe to one or more of these using broker's \emph{Subscribe}
method. Clients can also unregister from brokers using
- \emph{Unregister\_client} method.
+ \texttt{Unregister\_client} method.
The broker keeps track of both registered clients and clients' subscriptions
in the clients registry.
In order to be advertised to clients during the subscription phase, tutors
- should register to the broker using broker's \emph{Register\_tutor} method.
- This method is really similar to the already seen Register\_client: tutors
- are required to send an unique identify and a base URI for their \ws{}.
+ should register to the broker using broker's \texttt{Register\_tutor}
+ method. This method is really similar to the \texttt{Register\_client}
+ one: tutors are required to send an unique identify and a base URI for
+ their \ws{}.
Additionally tutors are required to send an human readable description of
- their capabilities, this information could be used by client's user to
- decide which tutors he need to subscribe to. Like clients, tutors can
- unregister from brokers using \emph{Unregister\_broker} method.
+ their capabilities; this information could be used by client's user to
+ decide which tutors he needs to subscribe to. Like clients, tutors can
+ unregister from brokers using \texttt{Unregister\_broker} method.
- Track of available tutors is kept in the tutors registry.
+ Track of available tutors is kept in the tutors
+ registry.\ednote{Non si mette mai un paragrafo lungo meno di una linea!}
- Each time a new status is available from the client, it is sent to the
+ Each time the client status change, the status is sent to the
broker using its \emph{Status} method. Using both clients registry (to
lookup client's subscription) and tutors registry (to check if some tutors
- has unsubscribed), the broker is able to decide to which tutor forward the
- new status just received.
-
- The forwarding operation is performed using tutors' \emph{Start\_musing}
- method, that is a request to start a new computation (\emph{musing}) on a
- given status. The return value for Start\_musing method is a musing
- identifier that is saved in the musings registry along with the identifier
- of the client that triggered the starting of the musing.
-
- As soon as a musing is completed, the owning tutor informs the broker using
- its \emph{Musing\_completed} method, the broker can now remove the musing
- entry from the musings registry and, depending on its outcome, inform the
- client. In case of success one of the Musing\_completed arguments is an hint
- to be sent to the client, otherwise there's no need to inform him and the
- Musing\_completed method is just to update the musings registry.
-
- Consulting the musings registry, the tutor is able to know, at each time,
- which musings are in execution on which tutor. This peculiarity is exploited
- by the broker on invocation of Status method. Receiving a new status from
- the client imply indeed that the previous status no longer exists and all
- musings working on it should be stopped. Additionally to the already
- described behaviour (i.e. starting new musings on the received status), the
- tutor takes also care of stopping ongoing computation invoking
- \emph{Stop\_musing} tutors' method.
+ has unsubscribed), the broker is able to decide to which tutors the
+ new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
+ della possibilit\'a di avere un vero brocker che multiplexi le richieste
+ del tutor localizzando i servizi, etc.}
+
+ The forwarding operation is performed using tutors' \texttt{Start\_musing}
+ method, that is a request to start a new computation (\emph{\musing{}}) on a
+ given status. The return value for \texttt{Start\_musing} method is a
+ \musing{} identifier that is saved in the \musings{} registry along with
+ the identifier of the client that triggered the starting of the \musing{}.
+
+ As soon as a \musing{} is completed, the owning tutor informs the broker
+ using its \texttt{Musing\_completed} method; the broker can now remove the
+ \musing{} entry from the \musings{} registry and, depending on its outcome,
+ inform the client. In case of success one of the \texttt{Musing\_completed}
+ arguments is an hint to be sent to the client, otherwise there's no need to
+ inform him and the \texttt{Musing\_completed} method is called
+ just to update the \musings{} registry.
+
+ Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
+ stai delirando?} is able to know, at each time,
+ which \musings{} are in execution on which tutor. This peculiarity is
+ exploited by the broker on invocation of Status method. Receiving a new
+ status from the client imply indeed that the previous status no longer
+ exists and all \musings{} working on it should be stopped: additionally to
+ the already described behaviour (i.e. starting new \musings{} on the
+ received status), the tutor takes also care of stopping ongoing computation
+ invoking \texttt{Stop\_musing} tutors' method.
\paragraph{\wss{}}
As already discussed, all \hbugs{} actors act as \wss{} offering one or more
services to neighbour actors. To grant as most accessibility as possible to
our \wss{} we have chosen to bind them using the HTTP/POST bindings
- described in \cite{????}.
-
- Given that our proof assistant was entirely developed in the Objective Caml
- language, we have chosen to develop also \hbugs{} in that language in order
- to maximize code reuse. To develop \wss{} in Objective Caml we have
- developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
- write HTTP 1.1 web servers and abstract over GET/POST parsing. This library
- supports different kind of web servers architecture, including multi-process
- and multi-threaded ones.
+ described in \cite{????}\footnote{Given that our proof assistant was
+ entirely developed in the Objective Caml language, we have chosen to
+ develop also \hbugs{} in that language in order to maximize code reuse. To
+ develop \wss{} in Objective Caml we have developed an auxiliary generic
+ library (\emph{O'HTTP}) that can be used to write HTTP 1.1 web servers and
+ abstract over GET/POST parsing. This library supports different kinds of web
+ servers architecture, including multi-process and multi-threaded ones.}.
\paragraph{Tutors}
Each tutor expose a \ws{} interface and should be able to work, not only for
many different clients referring to a common broker, but also for many
- different brokers. The potential number of clients is therefore very high
- and is simply too non scalable to think at a single-process architecture.
-
- Our choice was for a multi threaded architecture exploiting capabilities of
- the O'HTTP library. Each tutor is composed by two thread always running plus
- an additional thread for each running musing. One thread is devoted to
- listening for incoming \ws{} request, upon correct receiving requests it
+ different brokers. The potential high number of concurrent clients imposes
+ a multi-threaded or multi-process architecture.
+
+ Our current implementation is based on a multi threaded architecture
+ exploiting the capabilities of the O'HTTP library. Each tutor is composed
+ by two thread always running plus
+ an additional thread for each running \musing{}. One thread is devoted to
+ listening for incoming \ws{} request; upon correct receiving requests it
pass the control to the second always-running thread which handle the pool
- of running musings. When a new musing is requested, a new thread is spawned
- to work them out; when a request to interrupt an old musing is received, the
- thread actually running them is killed freeing its resources.
-
- This architecture turns out to be scalable and permit at the running threads
- to share the type checker cache \ednote{Zack: brrrr ... abbiamo il coraggio
- di dirlo?, mai provato :-)}. This feature turns out to be really useful
- expecially for reflexive tactics, like Ring and Fourier, that ``reflect''
- terms of some domain (e.g. polynomials over real numbers) in other abstract
- domain. Type checking of most of the terms and operation in the abstract
- domain can be indeed cached and shared by all the threads.
+ of running \musings{}. When a new \musing{} is requested, a new thread is
+ spawned to work them out; when a request to interrupt an old \musing{} is
+ received, the thread actually running them is killed freeing its
+ resources.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
+ ricordo male al problema dell'uccisione dei thread. Ora o si spiega
+ il motivo di questa architettura o si glissa/bluffa.}
+
+ This architecture turns out to be scalable and allows the running threads
+ to share the cache of loaded (and type-checked) theorems.
+ As we will explain in Sect. \ref{tutors}, this feature turns out to be
+ really useful for tactics that rely on a huge but fixed set of lemmas,
+ as every reflexivite tactic.
The implementation of a tutor with the described architecture is not that
difficult having a language with good threading capabilities (as OCaml has)
- and a pool of implemented tactics (as gTopLevel has). Still working with
- threads is known to be really error prone due to concurrent programming
- intrinsic complexity.
-
- To get rid of this technical problem we have written (and thoroughly tested)
- a ``generic'' implementation of a tutor, and templated (using O'Caml
- functors) them over some parameters like the tactic to be invoked, the hint
- to send in case of success and a textual description of the tutor. This
- generic implementation use O'HTTP to implement the \ws{} part of the tutor
- and some generic routines we have implemented to handle deserialization of
- received status and serialization of generated hints.
-
- Having a list of available tactics and hints we are able to generate
- automatically source code that implement all the requested tutors.
- Obviously, this approach works only for the implementation of ``simple'' (or
- ``stupid'', if you like) tutors that simply interface an already existing
- proof assistant tactic and can't be used to implement more raffinate
- decision procedures. Nonetheless, given that the number of available tactics
- was quite high, it offered a lot of practical advantages.
-
-\section{The \hbugs Tutors}
+ and a pool of already implemented tactics (as gTopLevel has).
+ Still working with threads is known to be really error prone due to
+ concurrent programming intrinsic complexity. Moreover, there is a
+ non-neglectable part of code that needs to be duplicated in every tutor:
+ the code to register the tutor to the broker and to handle HTTP requests;
+ the code to manage the creation and termination of threads; and the code for
+ parsing the requests and serializing the answers. As a consequence we
+ have written a generic implementation of a tutor which is parameterized
+ over the code that actually propose the hint and some administrative
+ data (as the port the tutor will be listening to).
+
+ The generic tutor skeleton is really helpful in writing new tutors.
+ Nevertheless, the code obtained by converting existing tactics into tutors
+ is still quite repetitive: every tutor that wraps a tactic has to
+ instantiate its own copy of the proof-engine kernel and, for each request,
+ it has to override its status, guess the tactic arguments, apply the tactic
+ and, in case of success, send back an hint with the tactic name and the
+ chosen arguments. Of course, the complex part of the work is guessing the
+ right arguments. For the simple case of tactics that do not require
+ any argument, though, we are able to automatically generate the whole
+ tutor code given the tactic name. Concretely, we have written a
+ tactic-based tutor template and a script that parses an XML file with
+ the specification of the tutor and generates the tutor's code.
+ The XML file holds the tutor's port, the code to invoke the tactic,
+ the hint that is sent back upon successfull application and a
+ human readable explanation of the tactic implemented by the tutor.
+
+\section{The Implemented \hbugs Tutors}
\label{tutors}
-To test the \hbugs architecture and to assess the utility of a suggestion
+To test the \hbugs{} architecture and to assess the utility of a suggestion
engine for the end user, we have implemented several tutors. In particular,
we have investigated three classes of tutors:
\begin{enumerate}
belong to this class:
\begin{itemize}
\item \emph{Assumption Tutor}: it ends the proof if the thesis is
- equivalent\footnote{The equivalence relation is convertibility. In some
- cases, expecially when non-trivial computations are involved, the user
- is totally unable to figure out the convertibility of two terms.
- In these cases the tutor becomes handy also for expert users.}
- to one of the hypotheses.
+ equivalent\footnote{In our implementation, the equivalence relation
+ imposed by the logical framework is \emph{convertibility}. Two
+ expressions are convertible when they reduce to the same normal form.
+ Two ``equal'' terms depending on free variables can be non-convertible
+ since free variables stop the reduction. For example, $2x$ is convertible
+ with $(3-1)x$ because they both reduce to the same normal form
+ $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
+ already in normal form.}
+ to one of the hypotheses\footnote{
+ In some cases, expecially when non-trivial computations are involved,
+ the user is totally unable to figure out the convertibility of two terms.
+ In these cases the tutor becomes handy also for expert users.}.
\item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
adsurdum} if one hypothesis is equivalent to $False$.
\item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
suggests to apply the commutative property.
- \item \emph{Left/Right/Exists/Split/Constructor Tutors}: the Constructor
- Tutor suggests to proceed in the proof by applying one or more
- constructors when the goal thesis is an inductive type or a
- proposition inductively defined according to the declarative style.
- Since disjunction, conjunction and existential quantifications are
- particular cases of inductive propositions,
- all the other tutors of this class implements restrictions of the
+ \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
+ the Constructor Tutor suggests to proceed in the proof by applying one
+ or more constructors when the goal thesis is an inductive type or a
+ proposition inductively defined according to the declarative
+ style\footnote{An example of a proposition that can be given in
+ declarative style is the $\le$ relation: $\le$ is the smallest relation
+ such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
+ that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
+ of $n \le n$ is simply the application of the first constructor to
+ $n$ and a proof of $n \le m$ is the application of the second
+ constructor to $n,m$ and a proof of $n \le m$.}.
+ Since disjunction, conjunction, existential quantification and
+ Leibniz equality are particular cases of inductive propositions,
+ all the other tutors of this class are restrictions of the
the Constructor tactic: Left and Right suggest to prove a disjunction
by proving its left/right member; Split reduces the proof of a
conjunction to the two proof of its members; Exists suggests to
prove an existential quantification by providing a
- witness\footnote{This task is left to the user.}.
+ witness\footnote{This task is left to the user.}; Reflexivity proves
+ an equality whenever the two sides are convertible.
\end{itemize}
Beginners, when first faced with a tactic-based proof-assistant, get
lost quite soon since the set of tactics is large and their names and
instead of wasting efforts trying to remember the interface to the system.
\item{Tutors for Computationally Expensive Tactics}. Several tactics have
an unpredictable behaviour, in the sense that it is unfeasible to understand
- wether they will succeed or they will failt when applied and what will be
+ wether they will succeed or they will fail when applied and what will be
their result. Among them, there are several tactics either computationally
expensive or resources consuming. In the first case, the user is not
willing to try a tactic and wait for a long time just to understand its
obtained applying a lemma can be authomatically proved or, even better,
auhomatically disproved to reject the lemma.}, it is not unusual for
the tutor to come up with precious hints that can save several minutes of
- works that would be spent in proving again already proven results or
+ work that would be spent in proving again already proven results or
figuring out where the lemmas could have been stored in the library.
\end{enumerate}
-Once the code that implements a tactic or decision procedure is available,
-transforming it into a tutor is not a difficult task, but it is surely
-repetitive and error prone.\ednote{Zack: perche' hai messo qui questa parte?
-Vuoi riportare qui la generazione automatica dei tutor? per ora lo messo nella
-sezione implementazione}
-
\section{???}
\label{conclusions}
-% \section{Introduction}
-% Since the development of the first proof-assistants based on the
-% Curry-Howard isomorphism, it became clear that directly writing
-% lambda-terms (henceforth called simply terms) was a difficult, repetitive,
-% time-expensive and error prone activity; hence the introduction of
-% meta-languages to describe procedures that are able to automatically
-% generate the low-level terms.
-% Nowadays, almost all the proof-assistants
-% using terms description of proofs have many levels of abstractions, i.e.
-% meta-languages, to create the terms, with the only remarkable exception
-% of the ALF family \cite{ALF} in which terms are still directly written
-% without any over-standing level of abstraction.
-%
-% In particular, there are
-% usually at least two levels, that of tactics and that of the language in
-% which the whole system and hence the tactics are written; once the tactics
-% are implemented, to do a proof the user enters to the system a sequence of
-% tactics, called a script; the script is then executed to create the term
-% encoding of the proof, which is type-checked by the kernel of the
-% proof-assistant. Writing a script interactively is much simpler than
-% writing the term by hands; once written, though, it becomes impossible
-% to understand a script without replaying it interactively. For this reason,
-% we can hardly speak of the language of tactics as a high level language,
-% even if it is ``compiled'' to the language of terms.
-%
-% To avoid confusion, in the rest of this paper we will
-% avoid the use of the term ``proof'', using only ``script'' and ``term'';
-% moreover, we will avoid also the terms ``proof-checking'' and ``type-checking'',
-% replacing them with ``retyping'' to mean the type-checking of an already
-% generated term; finally, we will use the term ``compiling'' to mean the
-% execution of a script. Usually, compilation ends with
-% the type-checking of the generated term; hence the choice of ``retyping'' for
-% the type-checking of an already generated term.
-%
-% A long term consequence of the introduction of tactics has been the
-% progressive lowering of interest in terms. In particular, users of
-% modern proof-assistants as Coq \cite{Coq} may even ignore the existence of
-% commands to show the terms generated by their scripts. These terms are
-% usually very huge and quite unreadable, so they don't add any easily
-% accessible information to the scripts. Hence implementors have loosed
-% interest in terms too, as far as their size and compilation time are
-% small enough to make the system response-time acceptable.
-% When this is not the case, it is sometimes possible to trade space
-% with time using reflexive tactics, in which the potentiality of complex
-% type-systems to speak about themselves are exploited: reflexive tactics
-% usually leads to a polynomial asympotical reduction in the size of the
-% terms, at the cost of an increased reduction time during retyping and
-% compilation. Often, though, reflexive tactics could not be used; moreover,
-% reflexive tactics suffer of the same implementative problems of other tactics
-% and so could be implemented in such a way to create huger than
-% needed terms, even if asymptotically smaller than the best ones created
-% without reflection.
-%
-% The low level of interest in terms of the implementors of
-% tactics often leads to naive implementations (``If it works, it is OK'') and
-% this to low-quality terms, which:
-% \begin{enumerate}
-% \item are huger than needed because particular cases are not taken
-% into account during tactic development
-% \item require more time than needed for retyping due to
-% their size
-% \item are particularly unreadable because they don't
-% correspond to the ``natural'' way of writing the proof by hand
-% \end{enumerate}
-% To cope with the second problem, retyping is usually avoided allowing
-% systems to reload saved terms without retyping them and using a
-% checksum to ensure that the saved file has not been modified. This is
-% perfectly reasonable accordingly to the traditional application-centric
-% architecture of proof-assistants in which you have only one tool integrating
-% all the functionalities and so you are free to use a proprietary format for data
-% representation.
-%
-% In the last months, though, an ever increasing number of people and projects
-% (see, for example, HELM \cite{EHELM}, MathWeb \cite{MATHWEB} and
-% Formavie \cite{FORMAVIE})
-% have been interested to switch from the application-centric model to the
-% newer content-centric one, in which information is stored in
-% standard formats (that is, XML based) to allow different applications to work
-% on the same set of data. As a consequence, term size really becomes an
-% important issue, due to the redundancy of standard formats, and retyping
-% is needed because the applications can not trust each other, hence needing
-% retyping and making retyping time critical.
-% Moreover, as showed by Yann Coscoy in its PhD.
-% thesis \cite{YANNTHESIS} or by the Alfa interface to the Agda system
-% \cite{ALFA}, it is perfectly reasonable and also feasible to try
-% to produce descriptions in natural languages of formal proofs encoded as
-% terms.
-% This approach, combined with the further possibility of applying the usual
-% two-dimensional mathematic notation to the formulas that appears in the
-% terms, is being followed by projects HELM \cite{HELM}, PCOQ \cite{PCOQ} and
-% MathWeb \cite{MATHWEB} with promising results. It must be understood, though,
-% that the quality (in terms of naturality and readability) of this kind of
-% proofs rendering heavily depends on the quality of terms, making also
-% the third characteristic of low-quality terms a critical issue.
-%
-% A totally different scenario in which term size and retyping time are
-% critical is the one introduced by Necula and Lee \cite{Necula} under
-% the name Proof Carrying Code (PCC). PCC is a technique that can be used
-% for safe execution of untrusted code. In a typical instance of PCC, a code
-% receiver establishes a set of safety rules that guarantee safe behavior
-% of programs, and the code producer creates a formal safety proof that
-% proves, for the untrusted code, adherence to the safety rules. Then, the
-% proof is transmitted to the receiver together with the code and it is
-% retyped before code execution. While very compact representation of the
-% terms, highly based on type-inference and unification, could be used
-% to reduce the size and retyping time \cite{Necula2}, designing proof-assistants
-% to produce terms characterized by an high level of quality is still necessary.
-%
-% In the next section we introduce a particular class of metrics for
-% tactics evaluation. In section \ref{equivalence} we consider the
-% notion of tactics equivalence and we describe one of the bad habits
-% of tactics implementors, which is overkilling; we also provide and analyze
-% a simple example of overkilling tactic. In the last section we describe
-% a concrete experience of fixing overkilling in the implementation of a
-% reflexive tactic in system Coq and we analyze the gain with respect to
-% term-size, retyping time and term readability.
-%
-% \section{From Metrics for Terms Evaluation to Metrics for Tactics Evaluation}
-% The aim of this section is to show how metrics for term evaluation could
-% induce metrics for tactic evaluation. Roughly speaking, this allows us to
-% valuate tactics in terms of the quality of the terms produced. Even if
-% we think that these kinds of metrics are interesting and worth studying,
-% it must be understood that many other valuable forms of metrics could be
-% defined on tactics, depending on what we are interested in. For example,
-% we could be interested on compilation time, that is the sum of the time
-% required to generate the term and the retyping time for it. Clearly, only
-% the second component could be measured with a term metric and a good
-% implementation of a tactic with respect to the metric considered could
-% effectively decide to sacrifice term quality (and hence retyping time) to
-% minimize the time spent to generate the term. The situation is very close to
-% the one already encountered in compilers implementation, where there is
-% always a compromise, usually user configurable, between minimizing compiling
-% time and maximizing code quality.
-%
-% The section is organized as follows: first we recall the definition of
-% tactic and we introduce metrics on terms; then we give the definition
-% of some metrics induced by term metrics on tactics.
-%
-% \begin{definition}[Of tactic]
-% We define a \emph{tactic} as a function that, given a goal $G$ (that is, a local
-% context plus a type to inhabit) that satisfies a list of assumptions
-% (preconditions) $P$,
-% returns a couple $(L,t)$ where
-% $L = {L_1,\ldots,L_n}$ is a (possible empty) list of proof-obligations
-% (i.e. goals) and $t$ is a function that, given a list $l = {l_1,\ldots,l_n}$
-% of terms such that $l_i$ inhabits\footnote{We say, with a small abuse of
-% language, that a term $t$ inhabits a goal $G=(\Gamma,T)$ when $t$ is of type
-% $T$ in the context $\Gamma$.} $L_i$ for each $i$ in ${1,\ldots,n}$, returns a
-% term $t(l)$ inhabiting $G$.
-% \end{definition}
-%
-% % You can get another looser definition of tactic just saying that a tactic
-% % is a partial function instead than a total one. In this paper when referring
-% % to tactics we always refer to the first definition.
-%
-% \begin{definition}[Of term metric]
-% For any goal $G$, a term metric $\mu_G$ is any function in
-% $\mathbb{N}^{\{t/t\;\mbox{inhabits}\;G\}}$.
-% Two important class of term metrics are functional metrics and monotone
-% metrics:
-% \begin{enumerate}
-% \item {\bf Functional metrics:} a metric $\mu_G$ is \emph{functional}
-% if for each term context (=term with an hole) $C[]$ and for all terms
-% $t_1$,$t_2$ if $\mu_G(t_1)=\mu_G(t_2)$ then $\mu_G(C[t_1])=\mu_G(C[t_2])$.
-% An equivalent definition is that a metric $\mu_G$ is functional
-% if for each term context $C[]$ the function
-% $\lambda t.\mu_G(C[\mu_G^{-1}(t)])$ is well defined.
-% \item {\bf Monotone metrics:} a metric $\mu_G$ is \emph{monotone} if for
-% each term context $C[]$ and for all terms $t_1$,$t_2$ if
-% $\mu_G(t_1)\le\mu_G(t_2)$ then $\mu_G(C[t_1])\le\mu_G(C[t_2])$.
-% An equivalent definition is that a metric $\mu_G$ is functional if
-% for each term context $C[]$ the function
-% $\lambda t.\mu_G(C[\mu_G^{-1}(t)])$ is well defined and monotone.
-% \end{enumerate}
-%
-% % Vecchie definizioni
-% %\begin{enumerate}
-% %\item {\bf Monotony:} a metric $\mu_G$ is \emph{monotone} if for each term
-% %context (=term with an hole) $C[]$ and for all terms $t_1$,$t_2$ if
-% %$\mu_G(t_1)\le\mu_G(t_2)$ then $\mu_G(C[t_1])\le\mu_G(C[t_2])$
-% %\item {\bf Strict monotony:} a monotone metric $\mu_G$ is \emph{strictly
-% %monotone} if for each term context $C[]$ and
-% %for all terms $t_1$,$t_2$ if $\mu_G(t_1)=\mu_G(t_2)$ then
-% %$\mu_G(C[t_1])=\mu_G(C[t_2])$
-% %\end{enumerate}
-% \end{definition}
-%
-% Typical examples of term metrics are the size of a term, the time required
-% to retype it or even an estimate of its ``naturality'' (or simplicity) to be
-% defined somehow; the first two are also examples of monotone metrics
-% and the third one could probably be defined as to be. So, in the rest
-% of this paper, we will restrict to monotone metrics, even if the
-% following definitions also work with weaker properties for general metrics.
-% Here, however, we are not interested in defining such metrics, but in showing
-% how they naturally induce metrics for tactics.
-%
-% Once a term metric is chosen, we get the notion of a best term (not unique!)
-% inhabiting a goal:
-% \begin{definition}[Of best terms inhabiting a goal]
-% the term $t$ inhabiting a goal $G$ is said to be a best term inhabiting $G$
-% w.r.t. the metric $\mu_G$ when
-% $\mu_G(t) = min\{\mu_G(t') / t'\;\mbox{inhabits}\;G\}$.
-% \end{definition}
-%
-% Using the previous notion, we can confront the behavior of two tactics
-% on the same goal:
-%
-% \begin{definition}
-% Let $\tau_1$ and $\tau_2$ be two tactics both applyable to a goal $G$
-% such that $\tau_1(G) = (L_1,t_1)$ and $\tau_2(G) = (L_2,t_2)$.
-% We say that $\tau_1$ is better or equal than $\tau_2$ for the goal $G$
-% with respect to $\mu_G$ if, for all $l_1$ and $l_2$ lists of best terms
-% inhabiting respectively $L_1$ and $L_2$, $\mu_G(t_1(l_1)) \le \mu_G(t_2(l_2))$
-% holds.
-% \end{definition}
-% Note that confronting in this way ``equivalent'' tactics
-% (whose definition is precised in the next section) gives us information
-% on which implementation is better; doing the same thing on tactics that
-% are not equivalent, instead, gives us information about what tactic to
-% apply to obtain the best proof.
-%
-% A (functional) metric to confront two tactics only on a particular goal
-% has the nice property to be a total order, but is quite useless. Hence,
-% we will now
-% define a bunch of different tactic metrics induced by term metrics
-% that can be used to confront the behavior of tactics when applied to
-% a generic goal. Some of them will be \emph{deterministic} partial orders;
-% others will be total orders, but will provide only a \emph{probabilistic}
-% estimate of the behavior. Both kinds of metrics are useful in practice
-% when rating tactics implementation.
-% \begin{definition}[Of locally deterministic better or equal tactic]
-% $\tau_1$ is a locally deterministic (or locally
-% uniform) better or equal tactic
-% than $\tau_2$ w.r.t. $\mu$ (and in that case we write $\tau_1 \le_{\mu} \tau_2$
-% or simply $\tau_1 \le \tau_2$), when
-% for all goals $G$ satisfying the preconditions of both tactics we have that
-% $\tau_1$ is better or equal than $\tau_2$ w.r.t. the metric $\mu_G$.
-% \end{definition}
-%
-% \begin{definition}[Of locally deterministic better tactic]
-% $\tau_1$ is a locally deterministic (or locally uniform)
-% better tactic than $\tau_2$
-% w.r.t. $\mu$ (and in that case we write $\tau_1 <_{\mu} \tau_2$
-% or simply $\tau_1 < \tau_2$), when $\tau_1 \le_{\mu} \tau_2$ and
-% exists a goal $G$ satisfying the preconditions of both tactics such that
-% $\tau_1$ is better (but not equal!) than $\tau_2$ w.r.t. the metric $\mu_G$.
-% \end{definition}
-%
-% \begin{definition}[Of locally probabilistic better or equal tactic of a factor K]
-% $\tau_1$ is said to be a tactic locally probabilistic better or equal of a
-% factor $0.5 \le K \le 1$ than $\tau_2$ w.r.t. $\mu$ and a particular expected
-% goals distribution when the probability of having $\tau_1$ better or equal than
-% $\tau_2$ w.r.t. the metric $\mu_G$ is greater or equal to $K$ when $G$ is
-% chosen randomly according to the distribution.
-% \end{definition}
-% The set of terms being discrete, you can note that a deterministically better
-% or equal tactic is a tactic probabilistically better or equal of a factor 1.
-%
-%
-% To end this section, we can remark the strong dependence of the $\le$
-% relation on the choice of metric $\mu$, so that it is easy to find
-% two metrics $\mu_1,\mu_2$ such that $\tau_1 <_{\mu_1} \tau_2$ and
-% $\tau_2 <_{\mu_2} \tau_1$. Luckily, tough, the main interesting metrics,
-% term size, retyping time and naturality, are in practice highly correlated,
-% though the correlation of the third one with the previous two could be a
-% bit surprising. So, in the following section, we
-% will not state what is the chosen term metric; you may think as
-% any of them or even at some kind of weighted mean.
-%
-%
-% \section{Equivalent Tactics and Overkilling}
-% \label{equivalence}
-% We are now interested in using the metrics defined in the previous section
-% to confront tactics implementation. Before doing so, though, we have to
-% identify what we consider to be different implementations of the
-% same tactic. Our approach consists in identifying every implementation
-% with the tactic it implements and then defining appropriate notions of
-% equivalence for tactics: two equivalent tactics will then be considered
-% as equivalent implementations and will be confronted using metrics.
-%
-% Defining two tactics as equivalent when they can solve exactly the same
-% set of goals generating the same set of proof-obligations seems quite natural,
-% but is highly unsatisfactory if not completely wrong. The reason is that, for
-% equivalent tactics, we would like to have the \emph{property of substitutivity},
-% that is substituting a tactic for an equivalent one in a script should give
-% back an error-free script\footnote{A weaker notion of substitutivity is that
-% substituting the term generated by a tactic for the term generated by an
-% equivalent one in a generic well-typed term should always give back a
-% well-typed term.}. In logical frameworks with dependent types,
-% without proof-irrelevance and with universes as CIC \cite{Werner} though,
-% it is possible for a term to inspect the term of a previous proof, behaving
-% in a different way, for example, if the constructive proof of a conjunction
-% is made proving the left or right side.
-% So, two tactics, equivalent w.r.t. the previous
-% definition, that prove $A \vee A$ having at their disposal an
-% hypothesis $A$ proving the first one the left and the second one
-% the right part of the conjunction, could not be substituted one for the
-% other if a subsequent term inspects the form of the generated proof.
-%
-% Put in another way, it seems quite reasonable to derive equivalence for
-% tactics from the definition of an underlying equivalence for terms.
-% The simplest form of such an equivalence relation is convertibility
-% (up to proof-irrelevance) of closed terms and this is the relation
-% we will use in this section and the following one. In particular,
-% we will restrict ourselves to CIC and hence to
-% $\beta\delta\iota$-convertibility\footnote{The Coq proof-assistant
-% introduces the notion of \emph{opaque} and \emph{transparent} terms,
-% differing only for the possibility of being inspected. Because the
-% user could change the opacity status at any time, the notion of
-% convertibility we must conservatively choose for the terms of Coq is
-% $\beta\delta\iota$-convertibility after having set all the definitions
-% as transparent.}.
-% Convertibility, though, is a too restrictive notion that does not take
-% in account, for example, commuting conversions. Looking for more suitable
-% notions of equivalence is our main open issue for future work.
-%
-% \begin{definition}[Of terms closed in a local environment]
-% A term $t$ is \emph{closed} in a local environment $\Gamma$ when $\Gamma$
-% is defined on any free variable of $t$.
-% \end{definition}
-%
-% \begin{definition}[Of equivalent tactics]
-% We define two tactics $\tau_1$ and $\tau_2$ to be equivalent (and
-% we write $\tau_1 \approx \tau_2$) when for each goal $G = (\Gamma,T)$ and for
-% each list of terms closed in $\Gamma$ and inhabiting the proof-obligations
-% generated respectively by $\tau_1$ and $\tau_2$, we have that the result terms
-% produced by $\tau_1$ and $\tau_2$ are $\beta\delta\iota$-convertible.
-% \end{definition}
-%
-% Once we have the definition of equivalent tactics, we can use metrics,
-% either deterministic or probabilistic, to confront them. In particular,
-% in the rest of this section and in the following one we will focus on the
-% notion of deterministically overkilling tactic, defined as follows:
-%
-% \begin{definition}[Of overkilling tactics]
-% A tactic $\tau_1$ is (deterministically) overkilling w.r.t. a metric
-% $\mu$ when there exists another tactic $\tau_2$ such that
-% $\tau_1 \approx \tau_2$ and $\tau_2 <_\mu \tau_1$.
-% \end{definition}
-%
-% Fixing an overkilling tactic $\tau_1$ means replacing it with the
-% tactic $\tau_2$ which is the witness of $\tau_1$ being overkilling.
-% Note that the fixed tactic could still be overkilling.
-%
-% The name overkilling has been chosen because most of the time overkilling
-% tactics are tactics that do not consider special cases, following the general
-% algorithm. While in computer science it is often a good design pattern to
-% prefer general solutions to ad-hoc ones, this is not a silver bullet:
-% an example comes another time from compiler technology, where
-% ad-hoc cases, i.e. optimizations, are greatly valuable if not necessary.
-% In our context, ad-hoc cases could be considered either as optimizations,
-% or as applications of Occam's razor to proofs to keep the simplest one.
-%
-% \subsection{A Simple Example of Overkilling Tactic}
-% A first example of overkilling tactic in system Coq is
-% \emph{Replace}, that works in this way: when the current goal
-% is $G = (\Gamma,T)$, the
-% tactic ``{\texttt Replace E$_1$ with E$_2$.}'' always produces a new
-% principal proof-obligation $(\Gamma, T\{E_2/E_1\})$ and an auxiliary
-% proof-obligation $(\Gamma, E_1=E_2)$ and uses the elimination scheme
-% of equality on the term $E_1 = E_2$ and the two terms that inhabit the
-% obligations to prove the current goal.
-%
-% To show that this tactic is overkilling, we will provide an example
-% in which the tactic fails to find the best term, we will
-% propose a different implementation that produces the best term and we will
-% show the equivalence with the actual one.
-%
-% The example consists in applying the tactic in the case in which $E_1$ is
-% convertible to $E_2$: the tactic proposes to the user the two
-% proof-obligations and then builds the term as described above. We claim
-% that the term inhabiting the principal proof-obligation also inhabits
-% the goal and, used as the generated term, is surely smaller
-% and quicker to retype than the one that is generated in the
-% implementation; moreover, it
-% is also as natural as the previous one, in the sense that the apparently
-% lost information has simply become implicit in the reduction and could
-% be easily rediscovered using type-inference algorithms as the one described
-% in Coscoy's thesis \cite{YANNTHESIS}. So, a new implementation could
-% simply recognize this special case and generate the better term.
-%
-% We will now show that the terms provided by the two implementations are
-% $\beta\delta\iota$-convertible.
-% Each closed terms in $\beta\delta\iota$-normal form
-% inhabiting the proof that $E_1$ is equal to $E_2$ is equal to the only
-% constructor of equality applied to a term convertible to the type of
-% $E_1$ and to another term convertible to $E_1$; hence, once the principle
-% of elimination of equality is applied to this term, we can first apply
-% $\beta$-reduction and then $\iota$-reduction to obtain the term inhabiting
-% the principal proof-obligation in which $E_1$ has been replaced by $E_2$.
-% Since $E_1$ and $E_2$ are $\beta\delta\iota$-convertible by hypothesis and
-% for the congruence properties of convertibility in CIC, we have that the
-% generated term is $\beta\delta\iota$-convertible to the one inhabiting the
-% principal proof-obligation.
-%
-% %The simplest example is when $E_1$ and $E_2$ are syntactically equal:
-% %in this case the principal obligation proposed is identical to the current goal
-% %and the equality elimination introduced could be replaced by the proof of
-% %this obligation, leading to a smaller, quicker to retype and also more
-% %natural\footnote{Even if naturality is in some way a subjective metric,
-% %who would dare say that a proof in which you rewrite an expression with
-% %itself is natural?} term. To show that handling this special case in this
-% %way is equivalent to the current solution, we have to show that the two
-% %terms are $\beta\delta\iota$-convertible when so are the subterms inhabiting
-% %the obligations.
-% %The only closed term in $\beta\delta\iota$-normal form
-% %inhabiting the proof that $E_1$ is equal to $E_1$ is the only constructor
-% %of equality applied to the type of $E_1$ and to $E_1$; hence we can
-% %first apply $\beta$-reduction and then $\iota$-reduction to obtain
-% %the second proof in which $E_1$ has been replaced by $E_1$, i.e. the
-% %second proof.
-%
-% %So, for this example, the simple fix to avoid overkilling is checking
-% %if $E_1$ and $E_2$ are syntactically equal and in case omitting the elimination;
-% %curiously, this is done in Coq in the implementation of a very similar tactic
-% %called \emph{Rewriting}.
-%
-%
-% %A second, more involved, example is when $E_1$ and $E_2$ are not
-% %syntactically equal, but $E_1$ reduces to $E_2$. Even in this case
-% %the elimination could simply be avoided because the typing rules of
-% %the logical system ensures us that a term that inhabits the principal
-% %obligation also inhabits the current goal: the proof is equivalent to the
-% %previous one, but for the last step in which $E_2$ is actually substituted for
-% %$E_1$; by hypothesis, though, the two terms are $\beta\delta\iota$-convertible
-% %and hence the thesis.
-%
-% %Surely smaller and faster to retype, the new term is also as natural
-% %as the previous one, in the sense that the apparently lost information has
-% %simply become implicit in the reduction and could be easily rediscovered
-% %using type-inference algorithms as the one described in chapter ???
-% %of Coscoy's thesis \ref{YANNTHESIS}.
-%
-% This example may seem quite stupid because, if the user is already able to
-% prove the principal proof-obligation and because this new goal is totally
-% equivalent to the original one, the user could simply redo the same steps
-% without applying the rewriting at all. Most of the time, though, the
-% convertibility of the two terms could be really complex to understand,
-% greatly depending on the exact definitions given; indeed, the user could
-% often be completely unaware of the convertibility of the two terms. Moreover,
-% even in the cases in which the user understands the convertibility, the
-% tactic has the important effect of changing the form of the current
-% goal in order to simplify the task of completing the proof, which is the reason
-% for the user to apply it.
-%
-% ~\\
-%
-% The previous example shows only a very small improvement in the produced
-% term and could make you wonder if the effort of fixing overkilling and
-% more in general if putting more attention to terms when implementing
-% tactics is really worth the trouble. In the next section we describe as
-% another example a concrete experience of fixing a complex reflexive tactic
-% in system Coq that has lead to really significant improvements in term
-% size, retyping time and naturality.
-%
-% \section{Fixing Overkilling: a Concrete Experience}
-% Coq provides a reflexive tactic called \emph{Ring} to do associative-commutative
-% rewriting in ring and semi-ring structures. The usual usage is,
-% given the goal $E_1 = E_2$ where $E_1$ and $E_2$ are two expressions defined
-% on the ring-structure, to prove the goal reducing it to proving
-% $E'_1 = E'_2$ where $E'_i$ is the normal form of $E_i$. In fact, once
-% obtained the goal $E'_1 = E'_2$, the tactic also tries to apply simple
-% heuristics to automatically solve the goal.
-%
-% The actual implementation of the tactic by reflexion is quite complex and
-% is described in \cite{Ring}. The main idea is described in Fig. \ref{ring1}:
-% first of all, an inductive data type to describe abstract polynomial is
-% made available. On this abstract polynomial, using well-founded recursion in
-% Coq, a normalization function named $apolynomial\_normalize$ is defined;
-% for technical reasons, the abstract data type of normalized polynomials
-% is different from the one of un-normalized polynomials. Then, two
-% interpretation functions, named $interp\_ap$ and $interp\_sacs$ are given
-% to map the two forms of abstract polynomials to the concrete one. Finally,
-% a theorem named $apolynomial\_normalize\_ok$ stating the equality of
-% the interpretation of an abstract polynomial and the interpretation of
-% its normal form is defined in Coq using well-founded induction. The above
-% machinery could be used in this way: to prove that $E^I$ is equal to its
-% normal form $E^{IV}$, the tactic computes an abstract polynomial $E^{II}$ that,
-% once interpreted, reduces to $E^{I}$, and such that the interpretation
-% of $E^{III} = (apolynomial\_normalize E^{II})$ could be shown to be equal
-% to $E^{IV}$ applying $apolynomial\_normalize\_ok$.
-%
-% %such that $(interp\_ap\;E^{II})$ could be proved (theorem
-% %$apolynomial\_normalize\_ok$) in Coq to be equal to
-% %$(interp\_sacs\;E^{III})$ where
-% %$E^{III} = (apolynomial\_normalize E^{II})$ is another abstract polynomial
-% %in normal form and the three functions $interp\_ap$, $interp\_sacs$ and
-% %$apolynomial\_normalize$ could all be defined inside Coq using well-founded
-% %recursion/induction on the abstract polynomial definition.
-%
-% % \myincludegraphics{ring1}{t}{12cm}{Reflexion in Ring}{Reflexion in Ring}
-% % \myincludegraphics{ring2}{t}{10cm}{Ring implementation (first half)}{Ring implementation (first half)}
-%
-% In Fig. \ref{ring2} the first half of the steps taken
-% by the Ring tactic to prove $E_1 = E_2$ are shown\footnote{Here $E_1$
-% stands for $E^I$.}.
-% The first step is replacing $E_1 = E_2$ with $(interp\_ap\;E^{II}_1) = E_2$,
-% justifying the rewriting using the only one constructor of equality due to
-% the $\beta\delta\iota$-convertibility of $(interp\_ap\;E^{II}_1)$ with $E_1$.
-% The second one is replacing $(interp\_ap\;E^{II})$ with
-% $(interp\_sacs\;E^{III})$, justifying the rewriting using
-% $apolynomial\_normalize\_ok$.
-%
-% Next, the two steps are done again on the left part of the equality,
-% obtaining $(interp\_sacs\;E^{III}_1) = (interp\_sacs\;E^{III}_2)$,
-% that is eventually solved trying simpler tactics as \emph{Reflexivity} or left
-% to the user.
-%
-% The tactic is clearly overkilling, at least due to the usage of rewriting for
-% convertible terms. Let's consider as a simple example the session in Fig.
-% \ref{session}:
-% \begin{figure}[t]
-% %\begin{verbatim}
-% \mbox{\hspace{3cm}\tt Coq $<$ Goal ``0*0==0``.}\\
-% \mbox{\hspace{3cm}\tt 1 subgoal}\\
-% ~\\
-% \mbox{\hspace{3cm}\tt ~~=================}\\
-% \mbox{\hspace{3cm}\tt ~~~~``0*0 == 0``}\\
-% ~\\
-% \mbox{\hspace{3cm}\tt Unnamed\_thm $<$ Ring.}\\
-% \mbox{\hspace{3cm}\tt Subtree proved!}
-% %\end{verbatim}
-% \caption{A Coq session.}
-% \label{session}
-% \end{figure}
-% in Fig. \ref{before} the $\lambda$-term created by the
-% original overkilling implementation of Ring is shown. Following the previous
-% explanation, it should be easily understandable. In particular, the
-% four rewritings are clearly visible as applications of $eqT\_ind$, as
-% are the two applications of $apolynomial\_normalize\_ok$ and the
-% three usage of reflexivity, i.e. the two applications of $refl\_eqT$
-% to justify the rewritings on the left and right members of the equality
-% and the one that ends the proof.
-%
-% Let's start the analysis of overkilling in this implementation:
-% \begin{description}
-% \item[Always overkilling rewritings:] as already stated, four of the rewriting
-% steps are always overkilling because the rewritten term is convertible to
-% the original one due to the tactic implementation.
-% As proved in the previous section, all these rewritings could be simply
-% removed obtaining an equivalent tactic.
-% \item[Overkilling rewritings due to members already normalized:] it may happen,
-% as in our example, that one (or even both) of the two members is already in
-% normal form. In this case the two rewriting steps for that member could be
-% simply removed obtaining an equivalent tactic as shown in the previous section.
-% \item[Rewriting followed by reflexivity:] after having removed all
-% the overkilling rewritings, the general form of the $\lambda$-term produced
-% for $E_1 = E_2$ is the application of two rewritings ($E'_1$ for $E_1$ and
-% $E'_2$ for $E_2$), followed by a proof of $E'_1 = E'_2$. In many cases,
-% $E'_1$ and $E'_2$ are simply convertible and so the tactic finishes the
-% proof with an application of reflexivity to prove the equivalent goal
-% $E'_1 = E'_1$.
-% A smaller and also more natural solution is just to
-% rewrite $E'_1$ for $E_1$ and then proving $E'_1 = E_2$ applying the lemma
-% stating the symmetry of equality to the proof of $E_2 = E'_2$.
-% The equivalence to the original
-% tactic is trivial by $\beta\iota$-reduction because the lemma is proved
-% exactly doing the rewriting and then applying reflexivity:
-% $$
-% \begin{array}{l}
-% \lambda A:Type.\\
-% \hspace{0.2cm}\lambda x,y:A.\\
-% \hspace{0.4cm}\lambda H:(x==y).\\
-% \hspace{0.6cm}(eqT\_ind~A~x~ [x:A]a==x~(refl\_eqT~A~x)~y~H)
-% \end{array}
-% $$
-% \end{description}
-% In Fig. \ref{after} is shown the $\lambda$-term created by the same
-% tactic after having fixed all the overkilling problems described above.
-%
-% \begin{figure}
-% \begin{verbatim}
-% Unnamed_thm < Show Proof.
-% LOC:
-% Subgoals
-% Proof:
-% (eqT_ind R
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% (APmult AP0 AP0)) [r:R]``r == 0``
-% (eqT_ind R
-% (interp_sacs R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% Nil_varlist) [r:R]``r == 0``
-% (eqT_ind R
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R) AP0)
-% [r:R]
-% ``(interp_sacs R Rplus Rmult 1 r Ropp (Empty_vm R) Nil_varlist)
-% == r``
-% (eqT_ind R
-% (interp_sacs R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% Nil_varlist)
-% [r:R]
-% ``(interp_sacs R Rplus Rmult 1 r Ropp (Empty_vm R)
-% Nil_varlist) == r`` (refl_eqT R ``0``)
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R) AP0)
-% (apolynomial_normalize_ok R Rplus Rmult ``1`` ``0`` Ropp
-% [_,_:R]false (Empty_vm R) RTheory AP0)) ``0``
-% (refl_eqT R ``0``))
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% (APmult AP0 AP0))
-% (apolynomial_normalize_ok R Rplus Rmult ``1`` ``0`` Ropp
-% [_,_:R]false (Empty_vm R) RTheory (APmult AP0 AP0))) ``0*0``
-% (refl_eqT R ``0*0``))
-% \end{verbatim}
-% \caption{The $\lambda$-term created by the original overkilling implementation}
-% \label{before}
-% \end{figure}
-%
-% \begin{figure}
-% \begin{verbatim}
-% Unnamed_thm < Show Proof.
-% LOC:
-% Subgoals
-% Proof:
-% (sym_eqT R ``0`` ``0*0``
-% (apolynomial_normalize_ok R Rplus Rmult ``1`` ``0`` Ropp
-% [_,_:R]false (Empty_vm R) RTheory (APmult AP0 AP0)))
-% \end{verbatim}
-% \caption{The $\lambda$-term created by the new implementation}
-% \label{after}
-% \end{figure}
-%
-% \clearpage
-% \subsection{A Quantitative Analysis of the Gain Obtained}
-% Let's now try a quantitative analysis of the gain with respect to term size,
-% retyping time and naturality, considering the two interesting cases of
-% no member or only one member already in normal form\footnote{If the two
-% members are already in normal form, the new implementation simply applies
-% once the only constructor of the equality to one of the two members. The tactic
-% is also implemented to do the same thing also when the two members are not yet
-% in normal forms, but are already convertible. We omit this other improvement
-% in our analysis.}.
-%
-% \subsubsection{Term Size.}
-% \paragraph{Terms metric definition:} given a term $t$, the metric $|.|$ associates to it its number of nodes $|t|$.
-% \paragraph{Notation}: $|T|$ stands for the number of nodes in the actual parameters
-% given to $interp\_ap$, $interp\_sacs$ and $apolynomial\_normalize\_ok$ to
-% describe the concrete (semi)ring theory and the list of non-primitive
-% terms occurring in the goal to solve. In the example in figures \ref{before}
-% and \ref{after}, $|T|$ is the number of nodes in
-% \begin{texttt}[R Rplus Rmult ``1`` ``0`` Ropp (Empty\_vm R)]\end{texttt}.
-% $|R|$ stands for the number of nodes in the term which is the carrier
-% of the ring structure. In the same examples, $|R|$ is simply 1, i.e.
-% the number of nodes in \begin{texttt}R\end{texttt}.
-%
-% \begin{displaymath}
-% \begin{array}{l}
-% \mbox{\bf Original version:}\\
-% \begin{array}{ll}
-% 1 + (|E^{II}_1| + |T| + 1) + |E_2| + |E_1| + &
-% \mbox{(I rewriting Left)} \\
-% 1 + |E_1| + &
-% \mbox{(justification)} \\
-% 1 + (|E^{III}_1| + |T| + 1) + |E_2| + (|E^{II}_1| + |T| + 1) + &
-% \mbox{(II rewriting Left)} \\
-% (|E^{II}_1| + |T| + 1) + &
-% \mbox{(justification)} \\
-% 1 + (|E^{II}_2| + |T| + 1) + (|E^{III}_1| + |T| + 1) + |E_2| + &
-% \mbox{(I rewriting Right)} \\
-% 1 + |E_2| + &
-% \mbox{(justification)} \\
-% 1 + (|E^{III}_2| + |T| + 1) + (|E^{III}_1| + |T| + 1) + &
-% \mbox{(II rewriting Right)} \\
-% ~(|E^{II}_2| + |T| + 1) +& \\
-% (|E^{II}_2| + |T| + 1) + &
-% \mbox{(justification)} \\
-% 1 + |E_1| = &
-% \mbox{(reflexivity application)} \\
-% \hline
-% 4|E_1| + 2|E_2| + 3|E^{II}_1| + 3|E^{II}_2| + 3|E^{III}_1| + |E^{III}_2| +~ &
-% \mbox{\bf Total number} \\
-% ~10|T| + 17 &
-% \end{array}
-% \end{array}
-% \end{displaymath}
-%
-% \begin{displaymath}
-% \begin{array}{l}
-% \mbox{\bf New version, both members not in normal form:}\\
-% \begin{array}{ll}
-% 1 + |R| + |E_1| + |E'_2| + &
-% \mbox{(Rewriting Right)} \\
-% 1 + |T| + |E^{II}_2| + &
-% \mbox{(justification)} \\
-% 1 + |R| + |E'_2| + |E'_1| + |E_2| + &
-% \mbox{(Symmetry application)} \\
-% 1 + |T| + |E^{II}_1| = &
-% \mbox{(justification)} \\
-% \hline
-% 2|E_1| + |E_2| + |E^{II}_1| + |E^{II}_2| + 2|E'_2| + 2|T| +~ &
-% \mbox{\bf Total number} \\
-% ~2|R| + 4 & \\
-% ~ &
-% \end{array}
-% \end{array}
-% \end{displaymath}
-% \begin{displaymath}
-% \begin{array}{l}
-% \mbox{\bf New version, only the first member not in normal form:}\\
-% \begin{array}{ll}
-% 1 + |R| + |E_1| + |E'_2| + &
-% \mbox{(Rewriting)} \\
-% 1 + |T| + |E^{II}_2| = &
-% \mbox{(justification)} \\
-% \hline
-% |E_1| + |E'_2| + |E^{II}_2| + |T| + |R| + 2~~~ &
-% \mbox{\bf Total number} \\
-% ~ &
-% \end{array}
-% \end{array}
-% \end{displaymath}
-%
-% While the overall space complexity of the terms generated by the new
-% implementation is asymptotically equal to the one of the old implementation,
-% all the constants involved are much smaller, but for the one of
-% $E'_2$ (the two normal forms) that before was 0 and now is
-% equal to 2. Is it possible to have goals for which the new implementation
-% behaves worst than the old one? Unfortunately, yes. This happens when
-% the size of the two normal forms $E'_1$ and $E'_2$ is greatly huger than
-% ($E^{II}_1 + |T| + 1)$ and $(E^{II}_2 + |T| + 1)$. This happens when
-% the number of occurrences of non-primitive terms is much higher than
-% the number of non-primitive terms and the size of them is big. More
-% formally, being $m$ the number of non-primitive terms, $d$ the average
-% size and $n$ the number of occurrences, the new implementation creates bigger
-% terms than the previous one if
-% \begin{displaymath}
-% n \log_2 m + m d < n d
-% \end{displaymath}
-% where the difference between the two members is great enough to hide the gain
-% achieved lowering all the other constants.
-% The logarithmic factor in the previous
-% formula derives from the implementation of the map of variables to
-% non-primitive terms as a tree and the representation of occurrences with
-% the path inside the tree to retrieve the term.
-%
-% To fix the problem, for each non-primitive term occurring more than once
-% inside the normal forms, we can use a \emph{let \ldots in} local definition
-% to bind it to a fresh identifier; then we replace every occurrence of
-% the term inside the normal forms with the appropriate
-% identifier\footnote{This has not yet been implemented in Coq.}.
-% In this way, the above inequation becomes
-% \begin{displaymath}
-% n \log_2 m + m d < n + m d
-% \end{displaymath}
-% that is never satisfied.
-%
-% Here it is important to stress how the latest problem was easily
-% overlooked during the implementation and has been discovered
-% only during the previous analysis, strengthening our belief in
-% the importance of this kind of analysis for tactic implementations.
-%
-% In the next two paragraphs we will consider only the new implementation
-% with the above fixing.
-%
-% \subsubsection{Retyping Time.}
-% \paragraph{Terms metric definition:} given a term $t$, the metric $|.|$ associates to it the time $|t|$ required to retype it.
-%
-% Due to lack of space, we will omit a detailed analysis as the one given
-% for terms size. Nevertheless, we can observe that the retyping time required
-% is surely smaller because all the type-checking operations required for
-% the new implementation are already present in the old one, but for the
-% type-checking of the two normal forms, that have fewer complexity
-% than the type-checking of the two abstract normal forms, and the
-% \emph{let \ldots in} definitions that have the same complexity of the
-% type-checking of the variable map. Moreover, the quite expensive operation
-% of computing the two normal forms is already done during proof construction.
-%
-% %In the case in which both the members of the equality are not in normal form,
-% %we can't expect a great improvement in retyping time but for very cheap
-% %normalizations; this because retyping time is dominated by the factor due to
-% %$apolynomial\_normalize$ that is present in both implementations and is
-% %usually much higher than the factor due to the removed applications of
-% %$interp\_ap$, $interp\_sacs$ and the eliminations of equality.
-%
-% %The situation is very different if one of the two members is already
-% %convertible to its normal form and the reduction involved in the normalization
-% %is expensive. In this rather unlikely case, the new implementation
-% %avoids the reduction at all, roughly halving the overall retyping time.
-%
-% In section \ref{benchmarks} we present some benchmarks to give an idea of
-% the real gain obtained.
-%
-% \subsubsection{Naturality.}~\\~\\
-% The idea behind the \emph{Ring} tactic is to be able to prove
-% an equality showing that both members have the same normal form.
-% This simply amounts to show that each member is equal to the same
-% normal form, that is exactly what is done in the new implementation.
-% Indeed, every step that belonged to the old implementation and has been
-% changed or removed to fix overkilling used to lead to some unnatural step:
-% \begin{enumerate}
-% \item The fact that the normalization is not done on the concrete
-% representation, but passing through two abstract ones that are
-% interpreted on the concrete terms is an implementative detail that
-% was not hidden as much as possible as it should be.
-% \item Normalizing a member of the equality that is already in normal form,
-% is illogical and so unnatural. Hence it should be avoided, but it was not.
-% \item The natural way to show $A=B$ under the hypothesis $B=A$ is just
-% to use the symmetric property of equality. Instead, the old implementation
-% rewrote $B$ with $A$ using the hypothesis and proved the goal by reflexivity.
-% \item Using local definitions (\emph{let \ldots in}) as abbreviations
-% rises the readability of the proof by shrinking its size removing
-% subexpressions that are not involved in the computation.
-% \end{enumerate}
-%
-% \subsection{Some Benchmarks}
-% \label{benchmarks}To understand the actual gain in term size and retyping
-% time on real-life examples, we have done some benchmarks on the whole set
-% of theorems in the standard library of Coq that use the Ring tactic. The
-% results are shown in table~\ref{benchs}.
-%
-% Term size is the size of the disk dump of the terms. Re-typing time is the
-% user time spent by Coq in proof-checking already parsed terms. The reduction
-% of the terms size implies also a reduction in Coq parsing time, that is
-% difficult to compute because Coq files do not hold single terms, but whole
-% theories. Hence, the parsing time shown is really the user time spent by Coq
-% to parse not only the terms on which we are interested, but also all the
-% terms in their theories and the theories on which they depend. So, this last
-% measure greatly under-estimates the actual gain.
-%
-% Every benchmark has been repeated 100 times under different load conditions on
-% a 600Mhz Pentium III bi-processor equipped with 256Mb RAM. The timings shown
-% are mean values.
-%
-% \begin{table}
-% \begin{center}
-% \begin{tabular}{|l|c|c|c|}
-% \hline
-% & ~Term size~ & Re-typing time & Parsing time\\
-% \hline
-% Old implementation & 20.27Mb & 4.59s & 2.425s \\
-% \hline
-% New implementation & 12.99Mb & 2.94s & 2.210s \\
-% \hline
-% Percentage reduction & 35.74\% & 35.95\% & 8.87\% \\
-% \hline
-% \end{tabular}
-% \end{center}
-% \caption{Some benchmarks}
-% \label{benchs}
-% \end{table}
-%
-% \section{Conclusions and Future Work}
-% Naive ways of implementing tactics lead to low quality terms that are
-% difficult to inspect and process. To improve the situation, we show
-% how metrics defined for terms naturally induce metrics for tactics and
-% tactics implementation and we advocate the usage of such metrics for
-% tactics evaluation and implementation. In particular, metrics could
-% be used to analyze the quality of an implementation or could be used at run
-% time by a tactic to choose what is the best way to proceed.
-%
-% To safely replace a tactic implementation with another one, it is important
-% to define when two tactics are equivalent, i.e. generate equivalent terms.
-% In this work, the equivalence relation chosen for terms has simply been
-% $\beta\delta\iota$-convertibility, that in many situations seems too strong.
-% Hence, an important future work is the study of weaker forms of term
-% equivalence and the equivalence relations they induce on tactics. In particular,
-% it seems that proof-irrelevance, $\eta$-conversion and commuting conversions
-% must all be considered in the definition of a suitable equivalence relation.
-
\begin{thebibliography}{01}
% \bibitem{ALF} The ALF family of proof-assistants:\\
projects / helm.git / commitdiff