\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
-\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+\newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
The user interfaces now adopted by all the proof assistants that adopt a
procedural proof language have been inspired by the CtCoq pioneering
system~\cite{ctcoq}. One succesfull incarnation of the ideas introduced
-by CtCoq is the Proof General generic interface, that has set a sort of
+by CtCoq is the Proof General generic interface~\cite{proofgeneral},
+that has set a sort of
standard way to interact with the system. Several procedural proof assistants
have either adopted or cloned Proof General as their main user interface.
\MATITA{} has also cloned the Proof General interface,
\end{center}
\end{figure}
-\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
-split in two main windows: on the left a textual widget is used to edit the
-script, on the right the list of open goal is shown using a \MATHML{} rendering
-widget. A distinguished part of the script (shaded in the screenshot) represent
-the commands already executed and can't be edited without undoing them. The
-remaining part can be freely edited and commands from that part can be executed
-moving down the execution point. An additional window --- the ``cicBrowser'' ---
-can be used to browse the library, including the proof being developed, and
-enable content based search on it. In the cicBrowser proofs are rendered in
-natural language, automatically generated from the low-level $\lambda$-terms
-using techniques inspired by \cite{natural,YANNTHESIS}.
-
-%In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
-%only seen as a convenient way to create mathematical objects. The universe of
-%all these objects makes up the \HELM{} library, which is always completely
-%visible to the user. The mathematical library is thus conceived as a global
-%hypertext, where objects may freely reference each other. It is a duty of
-%the system to guide the user through the relevant parts of the library.
-
-%This methodological assumption has many important consequences
-%which will be discussed in the next section.
-
-%on one side
-%it requires functionalities for the overall management of the library,
-%%%%%comprising efficient indexing techniques to retrieve and filter the
-%information;
-%on the other it introduces overloading in the use of
-%identifiers and mathematical notation, requiring sophisticated disambiguation
-%techniques for interpreting the user inputs.
-%In the next two sections we shall separately discuss the two previous
-%points.
-
-%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
-%organized in components which work on data in this format. For instance the
-%rendering engine, which transform $\lambda$-terms encoded as XML document to
-%\MATHML{} Presentation documents, can be used apart from \MATITA{} to print ...
-%FINIRE
-
-A final section is devoted to some innovative aspects
-of the authoring system, such as a step by step tactical execution,
-content selection and copy-paste.
-
-\subsection{Patterns}
-
-\subsubsection{Direct manipulation of terms}
+\MATITA{} has a script based user interface (UI) for proof authoring,
+based on the paradigm already exploited by other widespread user
+interfaces for theorem provers like the Proof
+General~\cite{proofgeneral} generic interface. We choosed not to
+build \MATITA{} UI over Proof General for two reasons. First because
+we had the need to integrate our rendering technologies --- mainly
+\GTKMATHVIEW{} --- based on XML markup languages whereas at the time
+of writing Proof General supports only text based
+rendering.\footnote{This may change with the future release of Proof
+General based on Eclipse, but is not yet the case.} The second reason
+is that we would like \MATITA{} UI to be built on top of a
+state-of-the-art and widespread toolkit as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} UI. As can
+be seen it is split in two main windows: on the left a textual widget
+is used to edit the script, on the right the list of open goal is
+shown using \GTKMATHVIEW. A distinguished part of the script (shaded
+in the screenshot) contains the commands already executed and can't be
+edited without undoing them. The remaining part can be freely edited
+and commands from that part can be executed moving down the execution
+point. An additional window --- the ``cicBrowser'' --- can be used to
+browse the library, including the proof being developed, and enable
+content based search over it. In the cicBrowser proofs are rendered in
+natural language, automatically generated from the low-level
+$\lambda$-terms using techniques inspired by
+\cite{natural,YANNTHESIS}.
+
+Since the concepts of script based proof authoring are well-known, the
+remaining part of this section is dedicated to the distinguishing
+features of the \MATITA{} authoring interface.
+
+\subsection{Direct manipulation of terms}
While terms are input as \TeX-like formulae in \MATITA, they're converted to a
mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
selected that way actions can be done on it like reductions or tactic
applications.
+
+\subsection{Patterns}
+
In our experience working with direct manipulation of terms is really
-effective and faster than retyping them. Nonetheless we need a way to
-encode term selections in scripts so that they can be batch compiled
-by \MATITAC. In \MATITA{} \emph{patterns} implement that encoding,
-being patterns the textual representations of \GTKMATHVIEW{} semantic
-selections. \NOTE{Zack:c'\`e scritto da qualche parte che l'utente
-non li deve necessariamente scrivere a mano, ma che pu\`o incollarli?
-Va scritto.}
+effective and is faster than typing the corresponding textual commands
+when they contain non-trivial terms. Nonetheless we need a way to
+represent term selections in scripts so that they can be batch
+compiled by \MATITAC.
+
+In \MATITA{} \emph{patterns} are such representation: each possible
+semantic selection in \GTKMATHVIEW{} can be represented as a textual
+pattern and batchly processed. Users can select using the GUI and then
+ask the system to paste the corresponding pattern in this script, but
+more often this process is transparent: once an action is performed on
+a selection, the corresponding textual command is computed and
+inserted in the script.
\subsubsection{Pattern syntax}
-A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
-$\NT{wanted}$.
-The former mocks-up a sequent, discharging unwanted subterms with $?$ and
-selecting the interesting parts with the placeholder $\%$.
-The latter is a term that lives in the context of the placeholders.
-
-The concrete syntax is reported in table \ref{tab:pathsyn}
-\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
+
+Patterns are composed of two parts: \NT{sequent\_path} and
+\NT{wanted}; their concrete syntax is reported in table
+\ref{tab:pathsyn}.
+
+\NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
+with $?$ and selecting the interesting parts with the placeholder
+$\%$. \NT{wanted} is a term that lives in the context of the
+placeholders.
+
+Since there exists a bijection between sequent paths and visual
+selections, \MATITA{} uses only the \NT{sequent\_path} part to
+represent selections in scripts. The \NT{wanted} part of the syntax
+is meant to help the users in writing concise and elegant patterns.
+
\begin{table}
\caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
\hrule
-% \[
-% \begin{array}{@{}rcll@{}}
-% \NT{pattern} &
-% ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
-% \NT{sequent\_path} &
-% ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
-% [~\verb+\vdash+~\NT{multipath}~] & \\
-% \NT{wanted} & ::= & \NT{term} & \\
-% \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
-% \end{array}
-% \]
\[
\begin{array}{@{}rcll@{}}
\NT{pattern} &
\hrule
\end{table}
-\subsubsection{Pattern concepts}
-Patterns mimic the user's selection in two steps. The first one
-selects roots (subterms) of the sequent, using the
-$\NT{sequent\_path}$, while the second
-one searches the $\NT{wanted}$ term starting from these roots. Both are
-optional steps, and by convention the empty pattern selects the whole
-conclusion.
+\subsubsection{Pattern evaluation}
+
+Patterns are evaluated in two phases. The first selects roots
+(subterms) of the sequent, using the $\NT{sequent\_path}$, while the
+second searches the $\NT{wanted}$ term starting from these roots.
+% Both are optional steps, and by convention the empty pattern selects
+% the whole conclusion.
\begin{description}
\item[Phase 1]
\end{description}
-\noindent
-Since the first step is equipotent to the composition of the two
-steps, the system uses it to represent each visual selection.
-The second step is only meant for the
-experienced user that writes patterns by hand, since it really
-helps in writing concise patterns as we will see in the
-following examples.
-
\subsubsection{Examples}
-To explain how the first step works let's give an example. Consider
+To explain how the first phase works let's give an example. Consider
you want to prove the uniqueness of the identity element $0$ for natural
-sum, and that you can relay on the previously demonstrated left
+sum, and that you can rely on the previously demonstrated left
injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
Typing
\begin{grafite}
projects / helm.git / commitdiff