X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=494b1c25a7bf2bd5ba54a37b4cc595b9cb023f32;hb=d04c51d4a69b0dc4838f46a41b4018835b252ff8;hp=65b5882af121a964c1c2ec38d7c98055b0c4852f;hpb=ed308fc03be5397081ac0e00bbc73b3f71da1e67;p=helm.git diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 65b5882af..494b1c25a 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -60,7 +60,7 @@ \newcommand{\URI}[1]{\texttt{#1}} \newcommand{\OP}[1]{``\texttt{#1}''} \newcommand{\FILE}[1]{\texttt{#1}} -\newcommand{\NOTE}[1]{\ednote{#1}{}} +\newcommand{\TAC}[1]{\texttt{#1}} \newcommand{\TODO}[1]{\textbf{TODO: #1}} \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black @@ -134,12 +134,13 @@ features. \subsection{Historical perspective} The origins of \MATITA{} go back to 1999. At the time we were mostly -interested to develop tools and techniques to enhance the accessibility -via Web of libraries of formal mathematics. Due to its dimension, the -library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems) +interested in developing tools and techniques to enhance the accessibility +via Web of libraries of formalized mathematics. Due to its dimension, the +library of the \COQ~\cite{CoqManual} proof assistant (of the order of +35'000 theorems) was chosen as a privileged test bench for our work, although experiments have been also conducted with other systems, and notably -with \NUPRL~\cite{nuprl-book}.\TODO{citare la tesi di vincenzo(?)} +with \NUPRL~\cite{nuprl-book}. The work, mostly performed in the framework of the recently concluded European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the following steps: @@ -150,7 +151,7 @@ following steps: the time an emerging standard, we naturally adopted that technology, fostering a content-centric architecture~\cite{content-centric} where the documents of the library were the the main components around which - everything else has to be build; + everything else has to be built; \item developing indexing and searching techniques supporting semantic queries to the library; @@ -273,7 +274,7 @@ assistants. Among them, the advanced indexing tools over the library and the parser for ambiguous mathematical notation. The size and complexity improvements over \COQ{} must be understood -historically. \COQ{} is a quite old +historically. \COQ{}\cite{CoqArt} is a quite old system whose development started 20 years ago. Since then, several developers have took over the code and several new research ideas that were not considered in the original architecture have been experimented @@ -465,7 +466,8 @@ presentation level terms. Omitted subterms can bear no information at all or they may be associated to a sequent. The formers are called \emph{implicit terms} and they occur only linearly. The latters may occur multiple times and are called -\emph{metavariables}. An \emph{explicit substitution} is applied to each +\emph{metavariables}~\cite{geuvers-jojgov,munoz}. +An \emph{explicit substitution} is applied to each occurrence of a metavariable. A metavariable stands for a term whose type is given by the conclusion of the sequent. The term must be closed in the context that is given by the ordered list of hypotheses of the sequent. @@ -479,9 +481,9 @@ metavariables and that can introduce \emph{implicit coercions}~\cite{barthe95implicit} to make a partially specified term well-typed. The refiner of \MATITA{} is implemented in the \texttt{cic\_unification} \component. As the type checker is based on -the conversion check, the refiner is based on \emph{unification} that is -a procedure that makes two partially specified term convertible by instantiating -as few as possible metavariables that occur in them. +the conversion check, the refiner is based on \emph{unification}~\cite{strecker} +that is a procedure that makes two partially specified term convertible by +instantiating as few as possible metavariables that occur in them. Since terms are used in CIC to represent proofs, correct incomplete proofs are represented by refinable partially specified terms. The metavariables @@ -530,7 +532,7 @@ properties of addition over the binary representation are very different from those of addition over the unary representation. And addition over two natural numbers is definitely different from addition over two real numbers. -Formal mathematics cannot hide these differences and obliges the user to be +Formalized mathematics cannot hide these differences and obliges the user to be very precise on the types he is using and their representation. However, to communicate formulae with the user and with external tools, it seems good practice to stick to the usual imprecise mathematical ontology. In the @@ -720,26 +722,22 @@ A proof assistant provides both an interface to interact with its library and an \emph{authoring} interface to develop new proofs and theories. According to its historical origins, \MATITA{} strives to provide innovative functionalities for the interaction with the library. It is more traditional -in its script based authoring interface. - -In the remaining part of the paper we focus on the user view of \MATITA. -This section is devoted to the aspects of the tool that arise from the -document centric approach to the library. Sect.~\ref{sec:authoring} describes -the peculiarities of the authoring interface. +in its script based authoring interface. In the remaining part of the paper we +focus on the user view of \MATITA. The library of \MATITA{} comprises mathematical concepts (theorems, axioms, definitions) and notation. The concepts are authored sequentially using scripts that are (ordered) sequences of procedural commands. -However, once they are produced we store them independently in the library. +Once they are produced we store them independently in the library. The only relation implicitly kept between the concepts are the logical, acyclic dependencies among them. This way the library forms a global (and distributed) hypertext. \begin{figure}[!ht] \begin{center} - \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-browsing} + \includegraphics[width=0.45\textwidth]{pics/cicbrowser-screenshot-browsing} \hspace{0.05\textwidth} - \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-query} + \includegraphics[width=0.45\textwidth]{pics/cicbrowser-screenshot-query} \caption{Browsing and searching the library\strut} \label{fig:cicbrowser1} \end{center} @@ -762,7 +760,7 @@ explored (on the left of Fig.~\ref{fig:cicbrowser1}), the natural language rendering of proofs can be inspected (Fig.~\ref{fig:cicbrowser2}), and content based searches on the library can be performed (on the right of Fig.~\ref{fig:cicbrowser1}). -Available content based searches are described in +Content based searches are described in Sect.~\ref{sec:indexing}. Other examples of library operations are disambiguation of content level terms (see Sect.~\ref{sec:disambiguation}) and automatic proof searching (see @@ -823,8 +821,8 @@ set, and the searching facilites built on top of them --- collected in the so called \WHELP{} search engine --- have been extensively described in~\cite{whelp}. Let us just recall here that the \WHELP{} metadata model is essentially based a single ternary relation -\REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a - given position $p$, where the position specify the place of the +\REF{p}{s}{t} stating that a concept $s$ refers a concept $t$ at a +given position $p$, where the position specify the place of the occurrence of $t$ inside $s$ (we currently work with a fixed set of positions, discriminating the hypothesis from the conclusion and outermost form innermost occurrences). This approach is extremely @@ -839,7 +837,7 @@ sections rely in a direct or indirect way on its metadata system and the search features. Here, we shall just recall some of its most direct applications. -A first, very simple but not negligeable feature is the check for duplicates. +A first, very simple but not negligeable feature is the \emph{duplicate check}. As soon as a theorem is stated, just before starting its proof, the library is searched to check that no other equivalent statement has been already proved @@ -859,7 +857,8 @@ statements (see Sect.~\ref{sec:naming}) that greatly simplifies the effort of recalling names, the naming discipline remains one of the most annoying aspects of formal developments, and \HINT{} provides a very friendly solution. -In the near feature, we expect to extend the \HINT{} operation to + +In the near future, we expect to extend the \HINT{} query to a \REWRITEHINT, resulting in all equational statements that can be applied to rewrite the current goal. @@ -876,9 +875,9 @@ concrete syntax corresponding to presentation level terms) and are then translated (in multiple steps) to partially specified terms as sketched in Sect.~\ref{sec:contentintro}. -The key component of the translation is the generic disambiguation algorithm +The key ingredient of the translation is the generic disambiguation algorithm implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries} -and presented in~\cite{disambiguation}. In this section we present how to use +and presented in~\cite{disambiguation}. In this section we detail how to use that algorithm in the context of the development of a library of formalized mathematics. We will see that using multiple passes of the algorithm, varying some of its parameters, helps in keeping the input terse without sacrificing @@ -887,7 +886,7 @@ expressiveness. \subsubsection{Disambiguation aliases} \label{sec:disambaliases} -Consider the following command to state a theorem over integer numbers: +Consider the following command that states a theorem over integer numbers: \begin{grafite} theorem Zlt_compat: @@ -902,7 +901,7 @@ refinable partially specified terms could be associated to it. posing the same question in case of a future re-execution (e.g. undo/redo), the choice must be recorded. Since scripts need to be re-executed after invalidation, the choice record must be permanently stored somewhere. The most -natural place is in the script itself. +natural place is the script itself. In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}. They are mappings, stored in the library, from ambiguity sources @@ -968,7 +967,8 @@ preferences. Several disambiguation parameters can vary among passes. With respect to preference handling we implemented three passes. In the first pass, called \emph{mono-preferences}, we consider only the aliases corresponding to the -current preferences. In the second pass, called \emph{multi-preferences}, we +current set of preferences. In the second pass, called +\emph{multi-preferences}, we consider every alias corresponding to a current or past preference. For instance, in the example above disambiguation succeeds in the multi-preference pass. In the third pass, called \emph{library-preferences}, all aliases @@ -994,8 +994,9 @@ has two \emph{instances}) and two different interpretations for it have to be used in order to obtain a refinable partially specified term. To address this issue, we have the ability to consider each instance of a single -symbol as a different ambiguous expression in the content level term, and thus -we can use a different alias for each of them. Exploiting or not this feature is +symbol as a different ambiguous expression in the content level term, +enabling the use of a different alias for each of them. +Exploiting or not this feature is one of the disambiguation pass parameters. A disambiguation pass which exploit it is said to be using \emph{fresh instances} (opposed to a \emph{shared instances} pass). @@ -1003,9 +1004,9 @@ instances} pass). Fresh instances lead to a non negligible performance loss (since the choice of an alias for one instance does not constraint the choice of the others). For this reason we always attempt a fresh instances pass only after attempting a -non-fresh one. +shared instances pass. -\paragraph{One-shot preferences} Disambiguation preferecens as seen so far are +\paragraph{One-shot preferences} Disambiguation preferences as seen so far are instance-independent. However, implicit preferences obtained as a result of a disambiguation pass which uses fresh instances ought to be instance-dependent. Informally, the set of preferences that can be respected by the disambiguator on @@ -1029,15 +1030,16 @@ and assume that in the library there is an alias mapping \OP{\^} to a partially specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the right hand side of the equality need to be ``injected'' from \texttt{nat} to -\texttt{R}. The refiner of \MATITA{} supports \emph{implicit coercions} for +\texttt{R}. The refiner of \MATITA{} supports +\emph{implicit coercions}~\cite{barthe95implicit} for this reason: given as input the above presentation level term, it will return a partially specified term where in place of \texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears (assuming such a coercion has been defined in advance). -Coercions are not always desirable. For example, in disambiguating +Implicitc coercions are not always desirable. For example, in disambiguating \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses -two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up +2 coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up among the possible partially specified term choices. For this reason we always attempt a disambiguation pass which require the refiner not to use the coercions before attempting a coercion-enabled pass. @@ -1049,7 +1051,8 @@ instances. In case there exists a coercion from natural numbers to (positive) integers (which indeed does), the theorem can be disambiguated using twice that coercion on the left hand side of the implication. The obtained partially specified term however would not -probably be the expected one, being a theorem which prove a trivial implication. +probably be the expected one, being a theorem which proves a trivial +implication. Motivated by this and similar examples we choose to always prefer fresh instances over implicit coercions, i.e. we always attempt disambiguation passes with fresh instances @@ -1060,8 +1063,8 @@ and no implicit coercions before attempting passes with implicit coercions. According to the criteria described above, in \MATITA{} we perform the disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In -our experience that choice gives reasonable performance and minimize the need of -user interaction during the disambiguation. +our experience that choice gives reasonable performance and minimizes the need +of user interaction during the disambiguation. \begin{table}[ht] \caption{Disambiguation passes sequence\strut} @@ -1119,9 +1122,8 @@ library. Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases. The first one is the calculation of all the concepts that recursively -depend on the ones we are invalidating. The calculation of the -reverse dependencies can be computed using the relational database -that stores metadata. +depend on the ones we are invalidating. It can be performed +using the relational database that stores the metadata. This technique is the same used by the \emph{Dependency Analyzer} and is described in~\cite{zack-master}. @@ -1136,23 +1138,25 @@ metadata included. %the library is preserved. To regenerate an invalidated part of the library \MATITA{} re-executes -the script files that produced the invalidated concepts. The main +the scripts that produced the invalidated concepts. The main problem is to find a suitable order of execution of the scripts. For this purpose we provide a tool called \MATITADEP{} that takes in input the list of scripts that compose the development and -outputs their dependencies in a format suitable for the GNU \texttt{make} tool. +outputs their dependencies in a format suitable for the GNU \texttt{make} +tool.\footnote{\url{http://www.gnu.org/software/make/}} The user is not asked to run \MATITADEP{} by hand, but simply to tell \MATITA{} the root directory of his development (where all script files can be found) and \MATITA{} will handle all the generation related tasks, including dependencies calculation. To compute dependencies it is enough to look at the script files for -disambiguation preferences declared or imported from other scripts -(see \ref{sec:disambaliases}). +literal of included explicit disambiguation preferences +(see Sect.~\ref{sec:disambaliases}). -Regenerating the content of a modified script file involves the preliminary -invalidation of all its old content. +The re-execution of a script to regenerate part of the library +requires the preliminary invalidation of the concepts generated by the +script. \subsubsection{Batch vs Interactive} @@ -1161,38 +1165,40 @@ invalidation of all its old content. Only the former is intended to be used directly by the user, the latter is automatically invoked by \MATITA{} -to try to regenerate parts of the library previously invalidated. +to regenerate parts of the library previously invalidated. While they share the same engine for generation and invalidation, they -provide different granularity. \MATITAC{} is only able to reexecute a -whole script and similarly to invalidate the whole content of a script -(together with all the other scripts that rely on an concept defined +provide different granularity. \MATITAC{} is only able to re-execute a +whole script and similarly to invalidate all the concepts generated +by a script (together with all the other scripts that rely on a concept defined in it). \subsection{Automation} \label{sec:automation} -In the long run, one would expect to work with a Proof Assistant -like Matita, using only three basic tactics: Intro, Elim, and Auto -(possibly integrated by a moderate use of Cut). The state of the art + +In the long run, one would expect to work with a proof assistant +like \MATITA, using only three basic tactics: \TAC{intro}, \TAC{elim}, +and \TAC{auto} +(possibly integrated by a moderate use of \TAC{cut}). The state of the art in automated deduction is still far away from this goal, but -this is one of the main development direction of Matita. +this is one of the main development direction of \MATITA. -Even in this field, the underlying phisolophy of Matita is to +Even in this field, the underlying philosophy of \MATITA{} is to free the user from any burden relative to the overall management -of the library. For instance, in Coq, the user is responsible to +of the library. For instance, in \COQ, the user is responsible to define small collections of theorems to be used as a parameter -by the Auto tactic; -in Matita, it is the system itself that authomatically retrieves, from +by the \TAC{auto} tactic; +in \MATITA, it is the system itself that automatically retrieves, from the whole library, a subset of theorems worth to be considered according to the signature of the current goal and context. -The basic tactic merely performs an iterated use of the Apply tactic -(with no Intro). The research tree may be pruned according to two -main parameters: the {\em depth} (whit the obvious meaning), and the -{\em width} that is the maximum number of (new) open goals allowed at -any instant. Matita has only one notion of metavariable, corresponding -to the so called existential variables of Coq; so, Matita's Auto tactic -should be compared with Coq's EAuto. +The basic tactic merely iterates the use of the \TAC{apply} tactic +(with no \TAC{intro}). The search tree may be pruned according to two +main parameters: the \emph{depth} (whit the obvious meaning), and the +\emph{width} that is the maximum number of (new) open goals allowed at +any instant. \MATITA{} has only one notion of metavariable, corresponding +to the so called existential variables of Coq; so, \MATITA's \TAC{auto} +tactic should be compared with \COQ's \TAC{EAuto} tactic. Recently we have extended automation with paramodulation based techniques. At present, the system works reasonably well with @@ -1201,140 +1207,160 @@ and can be specified by the user: the system only requires a proof of {\em reflexivity} and {\em paramodulation} (or rewriting, as it is usually called in the proof assistant community). -Given an equational goal, Matita recovers all known equational facts +Given an equational goal, \MATITA{} recovers all known equational facts from the library (and the local context), applying a variant of -the so called {\em given-clause algorithm} \cite{paramodulation}, -that is the the procedure currently used by the majority of modern theorem -provers. +the so called {\em given-clause algorithm}~\cite{paramodulation}, +that is the the procedure currently used by the majority of modern +automatic theorem provers. The given-clause algorithm is essentially composed by an alternation -of a {\em saturation} phase, deriving new facts by a set of active -facts and a new {\em given} clause suitably selected from a set of passive -equations, -and a {\em demodulation} phase that tries to simplify the equations -orienting them according to a suitable weight associated with terms. -Matita currently supports several different weigthing functions +of a \emph{saturation} phase and a \emph{demodulation} phase. +The former derives new facts by a set of active +facts and a new \emph{given} clause suitably selected from a set of passive +equations. The latter tries to simplify the equations +orienting them according to a suitable weight associated to terms. +\MATITA{} currently supports several different weigthing functions comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo), -that integrates particualry well with normalization. +that integrates particularly well with normalization. Demodulation alone is already a quite powerful technique, and -it has been turned into a tactic by itself: the {\em demodulate} -tactic, which can be seen as a kind of generalization of {\em simplify}. +it has been turned into a tactic by itself: the \TAC{demodulate} +tactic, which can be seen as a kind of generalization of \TAC{simplify}. The following portion of script describes two interesting cases of application of this tactic (both of them relying on elementary arithmetic equations): -\begin{verbatim} +\begin{grafite} theorem example1: - \forall x:nat. (x+1)*(x-1)=x*x - 1. + \forall x: nat. (x+1)*(x-1) = x*x - 1. intro. -apply (nat_case x) -[simplify;reflexivity -|intro;demodulate;reflexivity] +apply (nat_case x); + [ simplify; reflexivity + | intro; demodulate; reflexivity ] qed. +\end{grafite} +\begin{grafite} theorem example2: - \forall x,y:nat. (x+y)*(x+y) = x*x + 2*x*y + y*y. -intros;demodulate;reflexivity. + \forall x, y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y. +intros; demodulate; reflexivity qed. -\end{verbatim} +\end{grafite} In the future we expect to integrate applicative and equational rewriting. In particular, the overall idea would be to integrate applicative rewriting with demodulation, treating saturation as an operation to be performed in batch mode, e.g. during the night. - - \subsection{Naming convention} \label{sec:naming} A minor but not entirely negligible aspect of \MATITA{} is that of -adopting a (semi)-rigid naming convention for identifiers, derived by +adopting a (semi)-rigid naming convention for concept names, derived by our studies about metadata for statements. -The convention is only applied to identifiers for theorems -(not definitions), and relates the name of a proof to its statement. +The convention is only applied to theorems +(not definitions), and relates theorem names to their statements. The basic rules are the following: \begin{itemize} -\item each identifier is composed by an ordered list of (short) -names occurring in a left to right traversal of the statement; -\item all identifiers should (but this is not strictly compulsory) -separated by an underscore, -\item identifiers in two different hypothesis, or in an hypothesis -and in the conclusion must be separated by the string ``\verb+_to_+''; -\item the identifier may be followed by a numerical suffix, or a -single or double apostrophe. + + \item each name is composed by an ordered list of (short) + identifiers occurring in a left to right traversal of the statement; + + \item all names should (but this is not strictly compulsory) + separated by an underscore; + + \item names occurring in two different hypotheses, or in an hypothesis + and in the conclusion must be separated by the string \texttt{\_to\_}; + + \item the identifier may be followed by a numerical suffix, or a + single or double apostrophe. \end{itemize} -Take for instance the theorem -\[\forall n:nat. n = plus \; n\; O\] -Possible legal names are: \verb+plus_n_O+, \verb+plus_O+, -\verb+eq_n_plus_n_O+ and so on. -Similarly, consider the theorem -\[\forall n,m:nat. n m + n = n0) n - ============================ - m = 0 -\end{grafite} - -where $H$ is $\beta$-expanded over the second $n$ +\sequent{n: nat\\m : nat\\H: (fun n0: nat => m + n = n0) n}{m = 0} +where \texttt{H} is $\beta$-expanded over the second \texttt{n} occurrence. -At this point, since \COQ{} unification algorithm is essentially -first-order, the application of an elimination principle (of the -form $\forall P.\forall x.(H~x)\to (P~x)$) will unify -$x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}. +At this point, since \COQ{} unification algorithm is essentially first-order, +the application of an elimination principle (of the form $\forall P.\forall +x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with +\texttt{(fun n0: nat => m + n = n0)}. -Since rewriting, replacing and several other tactics boils down to +Since \TAC{rewrite}, \TAC{replace} and several other tactics boils down to the application of the equality elimination principle, the previous -trick deals the expected behaviour. +trick implements the expected behaviour. The idea behind this way of identifying subterms in not really far from the idea behind patterns, but fails in extending to -complex notation, since it relays on a mono-dimensional sequent representation. +complex notation, since it relies on a mono-dimensional sequent representation. Real math notation places arguments upside-down (like in indexed sums or integrations) or even puts them inside a bidimensional matrix. In these cases using the mouse to select the wanted term is probably the @@ -1612,31 +1601,32 @@ more effective way to tell the system what to do. One of the goals of \MATITA{} is to use modern publishing techniques, and adopting a method for restricting tactics application domain that discourages -using heavy math notation, would definitively be a bad choice. +using heavy math notation would have definitively been a bad choice. + +In \MATITA{}, tactics accepting pattern arguments can be more expressive than +the equivalent tactics in \COQ{} since variables bound in the pattern context, +can occurr in context-dependent arguments. For example, consider the sequent: +\sequent{n: nat\\x: nat\\H: \forall m. n + m*n = x + m}{m = O} +In \MATITA{} the user can issue the command: +\begin{grafite} +change in H: \forall _. (? ? % ?) with (S m) * n. +\end{grafite} +to change $n+m*n$ with $(S~m)*n$. To achieve the same effect in \COQ, the +user is obliged to change the whole hypothesis rewriting its right hand side +as well. \subsection{Tacticals} \label{sec:tinycals} -%There are mainly two kinds of languages used by proof assistants to recorder -%proofs: tactic based and declarative. We will not investigate the philosophy -%around the choice that many proof assistant made, \MATITA{} included, and we -%will not compare the two different approaches. We will describe the common -%issues of the tactic-based language approach and how \MATITA{} tries to solve -%them. - The procedural proof language implemented in \MATITA{} is pretty standard, with a notable exception for tacticals. -%\subsubsection{Tacticals overview} - -Tacticals first appeared in LCF as higher order tactics. They can be -seen as control flow constructs, like looping, branching, error -recovery or sequential composition. - - -The following simple example -shows a Coq script made of four dot-terminated commands +Tacticals first appeared in LCF~\cite{lcf} as higher order tactics. +They can be seen as control flow constructs like looping, branching, +error recovery and sequential composition. +The following simple example shows a \COQ{} script made of four dot-terminated +commands: \begin{grafite} Theorem trivial: forall A B:Prop, @@ -1649,85 +1639,27 @@ Theorem trivial: Qed. \end{grafite} -The third command is an application of the sequencing tactical -``$\ldots$\texttt{;}$\ldots$'', that combines the tactic -\texttt{split} with the application of the branching tactical -``$\ldots$\texttt{;[}$\ldots$\texttt{|}$\ldots$\texttt{|}$\ldots$\texttt{]}'' -to other tactics and tacticals. +The third command is an application of the sequencing tactical \OP{$\ldots$~;~$\ldots$}, +that combines the tactic \TAC{split} with the application of the branching +tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]} to other tactics or tacticals. The usual implementation of tacticals executes them atomically as any -other command. In \MATITA{} thi is not true since each punctuation is -executed as a single command. +other command. In \MATITA{} this is not the case: each punctuation +symbol is executed as a single command. -%The latter is applied to all the goals opened by \texttt{split} -% -%(here we have two goals, the two sides of the logic and). The first -%goal $B$ (with $A$ in the context) is proved by the first sequence of -%tactics \texttt{rewrite} and \texttt{assumption}. Then we move to the -%second goal with the separator ``\texttt{|}''. -% -%Giving serious examples here is rather difficult, since they are hard -%to read without the interactive tool. To help the reader in -%understanding the following considerations we just give few common -%usage examples without a proof context. -% -%\begin{grafite} -% elim z; try assumption; [ ... | ... ]. -% elim z; first [ assumption | reflexivity | id ]. -%\end{grafite} -% -%The first example goes by induction on a term \texttt{z} and applies -%the tactic \texttt{assumption} to each opened goal eventually recovering if -%\texttt{assumption} fails. Here we are asking the system to close all -%trivial cases and then we branch on the remaining with ``\texttt{[}''. -%The second example goes again by induction on \texttt{z} and tries to -%close each opened goal first with \texttt{assumption}, if it fails it -%tries \texttt{reflexivity} and finally \texttt{id} -%that is the tactic that leaves the goal untouched without failing. -% -%Note that in the common implementation of tacticals both lines are -%compositions of tacticals and in particular they are a single -%statement (i.e. derived from the same non terminal entry of the -%grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{} -%this is not true, since each atomic tactic or punctuation is considered -%a single statement. - -\subsubsection{Common issues of tactic(als)-based proof languages} -We will examine the two main problems of tactic(als)-based proof script: +\subsubsection{Common issues of tacticals} +We will examine the two main problems of procedural proof languages: maintainability and readability. -%Huge libraries of formal mathematics have been developed, and backward -%compatibility is a really time consuming task. \\ -%A real-life example in the history of \MATITA{} was the reordering of -%goals opened by a tactic application. We noticed that some tactics -%were not opening goals in the expected order. In particular the -%\texttt{elim} tactic on a term of an inductive type with constructors -%$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1} -%\ldots, g_2$. The library of \MATITA{} was still in an embryonic state -%but some theorems about integers were there. The inductive type of -%$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the -%induction proofs on this type where written without tacticals and, -%obviously, considering the three induction cases in the wrong order. -%Fixing the behavior of the tactic broke the library and two days of -%work were needed to make it compile again. The whole time was spent in -%finding the list of tactics used to prove the third induction case and -%swap it with the list of tactics used to prove the second case. If -%the proofs was structured with the branch tactical this task could -%have been done automatically. -% -%From this experience we learned that the use of tacticals for -%structuring proofs gives some help but may have some drawbacks in -%proof script readability. - Tacticals are not only used to make scripts shorter by factoring out -common cases and repeating commands. They are a primary way of making -scripts more mainteable. Moreover, they also have the well-known -role of structuring the proof. +common cases and repeating commands. They are the primary way of making +scripts more maintainable. They also have the well-known duty of +structuring the proof using the branching tactical. However, authoring a proof structured with tacticals is annoying. Consider for example a proof by induction, and imagine you -are using one of the state of the art graphical interfaces for proof assistant -like Proof General. After applying the induction principle you have to choose: +are using one of the state of the art graphical interfaces for proof assistant: +Proof General. After applying the induction principle you have to choose: immediately structure the proof or postpone the structuring. If you decide for the former you have to apply the branching tactical and write at once tactics for all the cases. Since the user does not even know the @@ -1746,42 +1678,13 @@ intermediate proof status. Tacticals make this operation uncomfortable. Indeed, a tactical is executed atomically, while it is obvious that it performs lot of smaller steps we are interested in. To show the intermediate steps, the proof must be de-structured on the -fly, for example replacing ``\texttt{;}'' with ``\texttt{.}'' where -possible.\\ - -%Proof scripts -%readability is poor by itself, but in conjunction with tacticals it -%can be nearly impossible. The main cause is the fact that in proof -%scripts there is no trace of what you are working on. It is not rare -%for two different theorems to have the same proof script.\\ -%Bad readability is not a big deal for the user while he is -%constructing the proof, but is considerably a problem when he tries to -%reread what he did or when he shows his work to someone else. The -%workaround commonly used to read a script is to execute it again -%step-by-step, so that you can see the proof goal changing and you can -%follow the proof steps. This works fine until you reach a tactical. A -%compound statement, made by some basic tactics glued with tacticals, -%is executed in a single step, while it obviously performs lot of proof -%steps. In the fist example of the previous section the whole branch -%over the two goals (respectively the left and right part of the logic -%and) result in a single step of execution. The workaround does not work -%anymore unless you de-structure on the fly the proof, putting some -%``\texttt{.}'' where you want the system to stop.\\ - -%Now we can understand the tradeoff between script readability and -%proof structuring with tacticals. Using tacticals helps in maintaining -%scripts, but makes it really hard to read them again, cause of the way -%they are executed. +fly, for example replacing \OP{;} with \OP{.} where possible. \MATITA{} has a peculiar tacticals implementation that provides the same benefits as classical tacticals, while not burdening the user during proof authoring and re-playing. -%\MATITA{} uses a language of tactics and tacticals, but tries to avoid -%this tradeoff, alluring the user to write structured proof without -%making it impossible to read them again. - -\subsubsection{The \MATITA{} approach: Tinycals} +\subsubsection{The \MATITA{} approach} \begin{table} \caption{Concrete syntax of tacticals\strut} @@ -1793,69 +1696,52 @@ during proof authoring and re-playing. ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\ \NT{block\_kind} & ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\ - \NT{block\_delimiter} & + \NT{block\_delim} & ::= & \verb+begin+ ~|~ \verb+end+ & \\ - \NT{tactical} & - ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\ + \NT{command} & + ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delim} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} \\ \end{array} \] \hrule \end{table} \MATITA{} tacticals syntax is reported in Tab.~\ref{tab:tacsyn}. -While one would expect to find structured constructs like -$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written. -This is essential for the base idea behind \MATITA{} tacticals: step-by-step -execution. - -The low-level tacticals implementation of \MATITA{} allows a step-by-step -execution of a tactical, that substantially means that a $\NT{block\_kind}$ is -not executed as an atomic operation. This has major benefits for the -user during proof structuring and re-playing. +LCF tacticals have been replaced by unstructured more primitive commands; +every LCF tactical is semantically equivalent to a sequential composition of +them. As usual, each command is executed atomically, so that a sequence +corresponding to an LCF tactical is now executed in multiple steps. For instance, reconsider the previous example of a proof by induction. -With step-by-step tacticals the user can apply the induction principle, and just -open the branching tactical ``\texttt{[}''. Then he can interact with the -system until the proof of the first case is terminated. After that -``\texttt{|}'' is used to move to the next goal, until all goals are -closed. After the last goal, the user closes the branching tactical with -``\texttt{]}'' and is done with a structured proof. \\ -While \MATITA{} tacticals help in structuring proofs they allow you to -choose the amount of structure you want. There are no constraints imposed by -the system, and if the user wants he can even write completely plain proofs. - -Re-playing a proof is also made simpler. There is no longer any need -to destructure the proof on the fly since \MATITA{} executes each -tactical not atomically. - -%\item[Rereading] -% is possible. Going on step by step shows exactly what is going on. Consider -% again a proof by induction, that starts applying the induction principle and -% suddenly branches with a ``\texttt{[}''. This clearly separates all the -% induction cases, but if the square brackets content is executed in one single -% step you completely loose the possibility of rereading it and you have to -% temporary remove the branching tactical to execute in a satisfying way the -% branches. Again, executing step-by-step is the way you would like to review -% the demonstration. Remember that understanding the proof from the script is -% not easy, and only the execution of tactics (and the resulting transformed -% goal) gives you the feeling of what is going on. -%\end{description} +In \MATITA{} the user can apply the induction principle, and just +open the branching punctuation symbol \OP{[}. Then he can interact with the +system (applying tactics and so forth) until he decides to move to the +next branch using \OP{|}. After the last branch, the punctuation symbol +\OP{]} must be used to collect goals possibly left open, accordingly to +the semantics of the LCF branching tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]}. The result effortlessly obtained is a structured script. + +The user is not forced to fully structure his script. If he wants, he +can even write completely unstructured proofs using only the \OP{.} +punctuation symbol. + +Re-playing a proof is also straightforward since there is no longer any need +to manually destructure the proof. \section{Standard library} \label{sec:stdlib} -\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} -can be read, checked and referenced in further developments. -However, in order to test the actual usability of the system, a -new library of results has been started from scratch. In this case, -of course, we wrote (and offer) the source script files, -while, in the case of \COQ, \MATITA{} may only rely on XML files of -\COQ{} objects. +\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} can be +read, checked and referenced in further developments. However, in order to test +the actual usability of the system, a new library of results has been started +from scratch. In this case, of course, we wrote (and offer) the source scripts, +while in the case of \COQ{} \MATITA{} may only rely on XML files of \COQ{} +objects. + The current library just comprises about one thousand theorems in elementary aspects of arithmetics up to the multiplicative property for Eulers' totient function $\phi$. + The library is organized in five main directories: \texttt{logic} (connectives, -quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type +quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q} (rationals). The most complex development is \texttt{nat}, organized in 25 scripts, listed in Tab.~\ref{tab:scripts}. @@ -1879,7 +1765,7 @@ scripts, listed in Tab.~\ref{tab:scripts}. We do not plan to maintain the library in a centralized way, as most of the systems do. On the contrary we are currently -developing wiki-technologies to support a collaborative +developing wiki-technologies to support collaborative development of the library, encouraging people to expand, modify and elaborate previous contributions. @@ -1897,10 +1783,6 @@ and V.~Tamburrelli. \theendnotes -\TODO{rivedere bibliografia, \'e un po' povera} - -\TODO{aggiungere entry per le coercion implicite} - \bibliography{matita} \end{document}