From: Enrico Tassi Date: Thu, 17 Nov 2005 17:47:40 +0000 (+0000) Subject: aded a prototype of chtting aboit tacticals X-Git-Tag: V_0_7_2_3~48 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=656cb59b98db21ef50afef7677ae03282bd8aad1;p=helm.git aded a prototype of chtting aboit tacticals --- diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index 10a443280..d0305c381 100644 --- 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}