\newcommand{\OP}[1]{``\texttt{#1}''}
\newcommand{\FILE}[1]{\texttt{#1}}
\newcommand{\TAC}[1]{\texttt{#1}}
-\newcommand{\NOTE}[1]{\ednote{#1}{}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\sequent}[2]{
\savebox{\tmpxyz}[0.9\linewidth]{
\begin{minipage}{0.9\linewidth}
- \texttt{#1} \\
+ \ensuremath{#1} \\
\rule{3cm}{0.03cm}\\
- \texttt{#2}
+ \ensuremath{#2}
\end{minipage}}\setlength{\fboxsep}{3mm}%
\begin{center}
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\listoffigures
\listoftables
-\TODO{rivedere tutti gli usi di \TEXMACRO{NOTE}}
-
\section{Introduction}
\label{sec:intro}
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:
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.
\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
literal of included explicit disambiguation preferences
(see Sect.~\ref{sec:disambaliases}).
-\TODO{da rivedere: da dove salta fuori ``regenerating content''?}
-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}
user, the latter is automatically invoked by \MATITA{}
to regenerate parts of the library previously invalidated.
-\TODO{come sopra: ``content of a script''?}
While they share the same engine for generation and invalidation, they
provide different granularity. \MATITAC{} is only able to re-execute a
-whole script and similarly to invalidate the whole content of a script
-(together with all the other scripts that rely on a concept defined
+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}
theorem example1:
\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;
+intros; demodulate; reflexivity
qed.
\end{grafite}
Take for instance the statement:
\begin{grafite}
- \forall n: nat. n = plus n O
+\forall n: nat. n = plus n O
\end{grafite}
Possible legal names are: \texttt{plus\_n\_O}, \texttt{plus\_O},
\texttt{eq\_n\_plus\_n\_O} and so on.
in this case, is the following. You should start with defining the
symmetric property for relations:
\begin{grafite}
-definition symmetric =
+definition symmetric \def
\lambda A: Type. \lambda R. \forall x, y: A.
- R x y \to R y x
+ R x y \to R y x.
\end{grafite}
Then, you may state the symmetry of equality as:
\begin{grafite}
$\NT{multipath}$ is omitted the whole assumption is selected. Remember that
the user can be mostly unaware of patterns concrete syntax, since the system
is able to write down a \NT{sequent\_path} starting from a graphical
- selection.\NOTE{Questo ancora non va in matita}
+ selection.
A \NT{multipath} is a CIC term in which a special constant \OP{\%} is allowed.
The roots of discharged subterms are marked with \OP{?}, while \OP{\%} is used
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
-\subsubsection{Tactics supporting patterns}
-
-\TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
-
-\TODO{mergiare con il successivo facendo notare che i patterns sono una
-interfaccia comune per le tattiche}
-
-In \MATITA{} all the tactics that can be restricted to subterms of the current
-sequent accept the pattern syntax. These tactics are:
-\TAC{simplify}, \TAC{change}, \TAC{fold}, \TAC{unfold}, \TAC{generalize},
-\TAC{replace} and \TAC{rewrite}.
+\subsubsection{Comparison with \COQ{}}
-\NOTE{attualmente rewrite e fold non supportano fase 2. per
-supportarlo bisogna far loro trasformare il pattern phase1+phase2
-in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
-con una pattern\_of(select(pattern))}
+In \MATITA{} all the tactics that act on subterms of the current sequent
+accept pattern arguments. Additional arguments can be disambiguated in the
+contexts of the terms selected by the pattern
+(\emph{context-dependent arguments}).
-\subsubsection{Comparison with \COQ{}}
+%\NOTE{attualmente rewrite e fold non supportano fase 2. per
+%supportarlo bisogna far loro trasformare il pattern phase1+phase2
+%in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
+%con una pattern\_of(select(pattern))}
\COQ{} has two different ways of restricting the application of tactics to
subterms of the current sequent, both relying on the same special syntax to
adopting a method for restricting tactics application domain that discourages
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~\cite{lcf} as higher order tactics.
They can be seen as control flow constructs like looping, branching,
error recovery and sequential composition.
Qed.
\end{grafite}
-The third command is an application of the sequencing tactical \OP{..~;~..},
+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{..~;[~..~|~..~|~..~]} to other tactics or tacticals.
+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{} 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-based proof languages}
-We will examine the two main problems of tactic-based proof scripts:
+\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 the primary way of making
scripts more maintainable. They also have the well-known duty of
To show the intermediate steps, the proof must be de-structured on the
fly, for example replacing \OP{;} with \OP{.} 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.
-
\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}
\begin{table}
::= & \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 the base idea of \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 \OP{[}. Then he can interact with the
-system until the proof of the first case is terminated. After that
-\OP{|} is used to move to the next goal, until all goals are
-closed. After the last goal, the user closes the branching tactical with
-\OP{]} and he just finished 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 un-structured
-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}
\theendnotes
-\TODO{rivedere bibliografia, \'e un po' povera}
-
\bibliography{matita}
\end{document}
projects / helm.git / commitdiff