X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.tex;h=636860a822ff4ae33ef12a57c7a307d48d7c8f2f;hb=bfc419549c067ca4c90c2ddd37b17f9b70bd52c0;hp=d9a7a525f572972bb90800a547c1d25635a2a146;hpb=57f5d19fdce7c88486fe834d1150c519007d205d;p=helm.git diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index d9a7a525f..636860a82 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -749,10 +749,37 @@ can be found in~\cite{disambiguation}, where a formulation without backtracking \subsubsection{Disambiguation stages} -\subsection{notazione} +\subsection{notation} \label{sec:notation} \ASSIGNEDTO{zack} +Mathematical notation plays a fundamental role in mathematical practice: it +helps expressing in a concise symbolic fashion concepts of arbitrary complexity. +Its use in proof assistants like \MATITA{} is no exception. Formal mathematics +indeed often impose to encode mathematical concepts at a very high level of +details (e.g. Peano numbers, implicit arguments) having a restricted toolbox of +syntactic constructions in the calculus. + +Consider for example one of the point reached while proving the distributivity +of times over minus on natural numbers included in the \MATITA{} standards +library. (Part of) the reached sequent can be seen in \MATITA{} both using the +notation for various arithmetical and relational operator or without using it. +The sequent rendered without using notation would be as follows: +\sequent{ +\mathtt{H}: \mathtt{le} z y\\ +\mathtt{Hcut}: \mathtt{eq} \mathtt{nat} (\mathtt{plus} (\mathtt{times} x (\mathtt{minus} +y z)) (\mathtt{times} x z))\\ +(\mathtt{plus} (\mathtt{minus} (\mathtt{times} x y) (\mathtt{times} x z)) +(\mathtt{times} x z))}{ +\mathtt{eq} \mathtt{nat} (\mathtt{times} x (\mathtt{minus} y z)) (\mathtt{minus} +(\mathtt{times} x y) (\mathtt{times} x z))} +while the corresponding sequent rendered with notation enabled would be: +\sequent{ +H: z\leq y\\ +Hcut: x*(y-z)+x*z=x*y-x*z+x*z}{ +x*(y-z)=x*y-x*z} + + \subsection{mathml} \ASSIGNEDTO{zack} @@ -760,7 +787,6 @@ can be found in~\cite{disambiguation}, where a formulation without backtracking \ASSIGNEDTO{zack} \subsection{pattern} -\ASSIGNEDTO{gares}\\ Patterns are the textual counterpart of the MathML widget graphical selection. @@ -982,39 +1008,123 @@ using heavy math notation, would definitively be a bad choice. \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} @@ -1035,43 +1145,53 @@ until all goal are closed or the tactic fails. \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}