aded a prototype of chtting aboit tacticals

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index 10a44328010fb13b84dad5f9f15c26c63df36f86..d0305c38167a1a76899cbdafb691a3f4f016c6ae 100644 (file)
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -37,6 +37,16 @@
 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
 \newcommand{\UWOBO}{UWOBO}
 \newcommand{\WHELP}{Whelp}
+\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
+\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
+\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
+\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
+\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
+\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
+\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
+\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
+\newcommand{\SKIP}{\MATHTT{skip}}
+\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
 
 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
@@ -56,7 +66,7 @@
 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
 \newcommand{\FILE}[1]{\texttt{#1}}
 % \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
-\newcommand{\NOTE}[1]{\ednote{x~\hspace{-10cm}y#1}{foo}}
+\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
 
 \newsavebox{\tmpxyz}
@@ -352,6 +362,54 @@ will be used later on, checking its consistency by construction.
 \label{sec:disambiguation}
 \ASSIGNEDTO{zack}
 
+ \begin{table}
+  \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in
+  notation\strut}
+ \hrule
+ \[
+ \begin{array}{@{}rcll@{}}
+   \NT{term} & ::= & & \mbox{\bf terms} \\
+     &     & x & \mbox{(identifier)} \\
+     &  |  & n & \mbox{(number)} \\
+     &  |  & s & \mbox{(symbol)} \\
+     &  |  & \mathrm{URI} & \mbox{(URI)} \\
+     &  |  & \verb+_+ & \mbox{(implicit)}\TODO{sync} \\
+     &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+     &  |  & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
+     &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
+     &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
+     &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
+     &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
+     &  |  & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
+     &     & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
+             ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
+     &     & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
+     &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
+     &  |  & \verb+(+~\NT{term}~\verb+)+ \\
+   \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
+     &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
+   \NT{fun} & ::= & & \mbox{\bf functions} \\
+     &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
+   \NT{binder} & ::= & & \mbox{\bf binders} \\
+     &     & \verb+\forall+ \mid \verb+\lambda+ \\
+   \NT{arg} & ::= & & \mbox{\bf single argument} \\
+     &     & \verb+_+ \mid x \\
+   \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
+     &     & \NT{arg} \\
+     &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
+   \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
+     &     & \NT{arg} \\
+     &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
+   \NT{kind} & ::= & & \mbox{\bf induction kind} \\
+     &     & \verb+rec+ \mid \verb+corec+ \\
+   \NT{rule} & ::= & & \mbox{\bf rules} \\
+     &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
+ \end{array}
+ \]
+ \hrule
+ \end{table}
+ 
+
 \subsubsection{Term input}
 
 The primary form of user interaction employed by \MATITA{} is textual script
@@ -833,18 +891,83 @@ One of the goals of \MATITA{} is to use modern publishing techiques, and
 adopting a method for restricting tactics application domain that discourages 
 using heavy math notation, would definitively be a bad choice.
 
-\subsection{tatticali}
-\ASSIGNEDTO{gares}
-\begin{verbatim}
-- problemi principali dei PA basati su tattiche
- o illeggibilita' dello script
- o scarsa strutturazione dello script e mantenibilita'
-   - ameliorate by tacticals
-- intro sui tatticali esistenti
-- peculiarita' di matita
-  - passo passo
-  - nice handling of sideeffects (see later on metavariables)
-\end{verbatim}
+\subsection{Tacticals}
+\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.
+
+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
+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.
+
+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.
+
+\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.
+
+\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. 
+
+\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
+\begin{table}
+ \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+  \NT{punctuation} & 
+    ::= & \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} & 
+    ::= & \verb+begin+ ~|~ \verb+end+ & \\
+  \NT{tactical} & 
+    ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+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:
+\begin{description}
+\item[Proof structuring] 
+  is much easyer. Consider for example a proof by induction. 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+]+. 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
+  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.
+\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
+  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.
+\end{description}
+
+
 
 \subsection{named variable e disambiguazione lazy}
 \ASSIGNEDTO{csc}