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.
-For 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 iw
+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 whe he shows his work to someone else.
+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
-contibute structuring proofs, but rise one more difficulty for the user that
-want to read a proof, since they are executed in an atomic way, making the
-user loose intermediate steps.
+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
\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 constructs, like
-looping, branching, error recovery or sequential composition.
+Tacticals first appered in LCF(cita qualcosa) 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.
-\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
\begin{table}
\caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
\hrule
\hrule
\end{table}
+\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
While one whould 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 execute 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. After applying the
+ 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
the proof or not. If you decide for the former you have to branch with
- \verb+[+ and write tactics for all the cases and the close the tactical 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
- concentrate only on the first goal, but you will have to one step back and
+ 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.
+ 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
+ without the.
\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 subdivided all
+ 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
projects / helm.git / commitdiff