\ASSIGNEDTO{zack}
\subsection{pattern}
-\ASSIGNEDTO{gares}\\
Patterns are the textual counterpart of the MathML widget graphical
selection.
\ASSIGNEDTO{gares}\\
There are mainly two kinds of languages used by proof assistants to recorder
proofs: tactic based and declarative. We will not investigate the philosophy
-aroud the choice that many proof assistant made, \MATITA{} included, and we will not compare the two diffrent approaches. We will describe the common issues of the first one and how \MATITA{} tries to solve them.
-
-First we must highlight the fact that proof scripts made using tactis are
-particularly unreadable. This 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.
-
-Another common issue for tactic based proof scripts is their mantenibility.
-Huge libraries have been developed, and backward compatibility is a really time
-consuming task. This problem is usually ameliorated with tacticals, that
-help in structuring proofs and consequently their maintenance, but have a bad
-counterpart in script readability. Since tacticals are executed atomically,
-the common practice of executing again a script to review all the proof steps
-doesn't work at all. This issue in addition to the really poor feeling that a
-list of tactics gives about the proof makes script rereading particularly hard.
-
-\MATITA{} uses a language of tactics and tacticals, but adopts a peculiar
-strategy to make this technique more user friendly without loosing in
-mantenibility or expressivity.
+aroud the choice that many proof assistant made, \MATITA{} included, and we
+will not compare the two diffrent approaches. We will describe the common
+issues of the tactic-based language approach and how \MATITA{} tries to solve
+them.
\subsubsection{Tacticals overview}
-Before describing the peculiarities of \MATITA{} tacticals we briefly introduce what tacticals are and where they can be useful.
-Tacticals first appered in LCF(cita qualcosa) and can be seen as programming
+Tacticals first appeared in LCF and can be seen as programming
constructs, like looping, branching, error recovery or sequential composition.
-For example $tac_1~.~tac_2$ executes the first tactic and applies the second
-only to the first goal opened by $tac_1$. Baranching can be used to specify a
-diffrent tactic to apply to each new goal opened by another tactic, for example
-$tac_1\verb+;[+~tac_{1.1}~\verb+|+~tac_{1.2}~\verb+|+~\cdots~|~tac_{1.n}~\verb+]+$
-applies respectively $tac_{1.i}$ to the $i$-th goal opened by $tac_1$. Looping
-can be used to iterate a tactic until it works: $\verb+repeat+~tac$ applies
-$tac$ to the current goal, and again $tac$ to the eventually resulting goals
-until all goal are closed or the tactic fails.
+The following simple example shows three tacticals in action
+\begin{grafite}
+theorem trivial:
+ \forall A,B:Prop.
+ A = B \to ((A \to B) \land (B \to A)).
+ intros (A B H).
+ split; intro;
+ [ rewrite < H. assumption.
+ | rewrite > H. assumption.
+ ]
+qed.
+\end{grafite}
+
+The first is ``\texttt{;}'' that combines the tactic \texttt{split}
+with \texttt{intro}, applying the latter to each goal opened by the
+former. Then we have ``\texttt{[}'' that branches on the goals (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{|}''. The last tactical we see here
+is ``\texttt{.}'' that is a sequential composition that selects the
+first goal opened for the following tactic (instead of applying it to
+them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
+not considered a tactical, but a sentence terminator (i.e. the
+delimiter of commands the proof assistant executes).
+
+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:
+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. We must highlight that 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 (while the
+proof is completely different).\\
+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 doesn't 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{} 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}
\begin{table}
\caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
\end{table}
\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
-While one whould expect to find structured constructs like
+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 base idea behind matita tacticals: step-by-step execution.
-\subsubsection{\MATITA{} Tinycals}
-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 two major benefits for the user, even being a so simple idea:
+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 two major benefits for the user,
+even being a so simple idea:
\begin{description}
\item[Proof structuring]
- is much easyer. Consider for example a proof by induction, and imagine you are using classical tacticals. After applying the
- induction principle, with one step tacticals, you have to choose: structure
+ is much easier. Consider for example a proof by induction, and imagine you
+ are using classical tacticals in one of the state of the
+ art graphical interfaces for proof assistant like Proof General or Coq Ide.
+ After applying the induction principle you have to choose: structure
the proof or not. If you decide for the former you have to branch with
- \verb+[+ and write tactics for all the cases separated by \verb+|+ and the
- close the tactical with
- \verb+]+. You can replace most of the cases by the identity tactic just to
+ ``\texttt{[}'' and write tactics for all the cases separated by
+ ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
+ You can replace most of the cases by the identity tactic just to
concentrate only on the first goal, but you will have to go one step back and
- one further every time you add something inside the tactical. And if you are
- boared of doing so, you will finish in giving up structuring the proof and
- write a plain list of tactics.\\
+ one further every time you add something inside the tactical. Again this is
+ caused by the one step execution of tacticals and by the fact that to modify
+ the already executed script you have to undo one step.
+ And if you are board of doing so, you will finish in giving up structuring
+ the proof and write a plain list of tactics.\\
With step-by-step tacticals you can apply the induction principle, and just
- open the branching tactical \verb+[+. Then you can interact with the system
- reaching a proof of the first case, without having to specify the whole
- branching tactical. When you have proved all the induction cases, you close
- the branching tactical with \verb+]+ and you are done with a structured proof.
+ open the branching tactical ``\texttt{[}''. Then you can interact with the
+ system reaching a proof of the first case, without having to specify any
+ tactic for the other goals. When you have proved all the induction cases, you
+ close the branching tactical with ``\texttt{]}'' and you are 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.
+
\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 baranches with a \verb+[+. 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. Again,
- executing step-by-step is the way you whould like to review the
- demonstration. Remember tha understandig 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 goning on.
+ 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}
-
-
\subsection{named variable e disambiguazione lazy}
\ASSIGNEDTO{csc}
projects / helm.git / commitdiff