From 4fa098d44a4f6f88fe09597abf6ad2af726cbff0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 Jan 2006 13:20:37 +0000 Subject: [PATCH 1/1] reshaped the "authoring interface" part --- helm/papers/matita/matita2.tex | 164 +++++++++++++++------------------ 1 file changed, 74 insertions(+), 90 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 192117af5..802bcfa37 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -60,7 +60,7 @@ \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}''} @@ -228,7 +228,8 @@ for human audiences). 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, @@ -1205,51 +1206,38 @@ expression and the suffix \verb+_to_Prop+. In the above example, \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 @@ -1289,38 +1277,42 @@ latter denotes an incomplete $\Pi$-binder. Once a (sub)term has been 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} & @@ -1335,13 +1327,13 @@ The concrete syntax is reported in table \ref{tab:pathsyn} \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] @@ -1381,18 +1373,10 @@ conclusion. \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} -- 2.39.2