\subsubsection{Disambiguation aliases}
\label{sec:disambaliases}
-Let's start with the definition of the ``strictly greater then'' notion over
+Let us start with the definition of the ``strictly greater then'' notion over
(Peano) natural numbers.
\begin{grafite}
\subsubsection{Operator instances}
-Let's suppose now we want to define a theorem relating ordering relations on
+Let us suppose now we want to define a theorem relating ordering relations on
natural and integer numbers. The way we would like to write such a theorem (as
we can read it in the \MATITA{} standard library) is:
an \emph{i}-th instance of a symbol should be mapped to a given partially
specified term. Instance-depend aliases are meaningful only for the term whose
disambiguation generated it. For this reason we call them \emph{one-shot
-aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the
+aliases} and \MATITA{} does not use it to disambiguate further terms down in the
script.
\subsubsection{Implicit coercions}
-Let's now consider a theorem about derivation:
+Let us now consider a theorem about derivation:
\begin{grafite}
theorem power_deriv:
(assuming it has been defined as such of course).
Nonetheless coercions are not always desirable. For example, in disambiguating
-\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
among the possible partially specified term choices. For this reason in
\MATITA{} we always try first a disambiguation pass which require the refiner
\section{The authoring interface}
\label{sec:authoring}
-\begin{figure}[t]
+The authoring interface of \MATITA{} is very similar to Proof General. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW{}. 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 wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
+as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
+featuring two windows. The background one is very like to the Proof General
+interface. The main difference is that we use the \GTKMATHVIEW{} widget to
+render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
+advantage of the whole bidimensional mathematical notation.
+
+The foreground window, also implemented around \GTKMATHVIEW, is called
+``cicBrowser''. It is used to browse the library, including the proof being
+developed, and enable content based search over it. Proofs are rendered in
+natural language, automatically generated from the low-level lambda-terms,
+using techniques inspired by \cite{natural,YANNTHESIS} and already described
+in~\cite{remathematization}.
+
+Note that the syntax used in the script view is \TeX-like, however unicode is
+fully supported so that mathematical glyphs can be input as such.
+
+\begin{figure}[!ht]
\begin{center}
\includegraphics[width=0.95\textwidth]{matita-screenshot}
\caption{\MATITA{} look and feel}
\end{center}
\end{figure}
-The authoring interface of \MATITA{} is very similar to Proof General.
-We chose not to
-build the \MATITA{} UI over Proof General for two reasons. First of all we
-wanted to integrate our XML-based 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
+While terms are input as \TeX-like formulae in \MATITA, they are converted to a
mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
-\GTKMATHVIEW. This mixed choice~\cite{latexmathml} enables both high-quality
-bidimensional rendering of terms (including the use of fancy layout schemata
-like radicals and matrices~\cite{mathml}) and the use of a concise and
-widespread textual syntax.
-
-\begin{figure}[t]
- \begin{center}
- \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
- \hspace{0.05\textwidth}
- \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
- \caption{Semantic selection and hyperlinks}
- \label{fig:directmanip}
- \end{center}
-\end{figure}
+\GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
+high-quality bidimensional rendering of terms (including the use of fancy
+layout schemata like radicals and matrices) and the use of a
+concise and widespread textual syntax.
Keeping pointers from the presentations level terms down to the
partially specified ones \MATITA{} enable direct manipulation of
rendered (sub)terms in the form of hyperlinks and semantic selection.
+
\emph{Hyperlinks} have anchors on the occurrences of constant and
inductive type constructors and point to the corresponding definitions
in the library. Anchors are available notwithstanding the use of
encoding complex notations retain all the hyperlinks of constants or
constructors used in the notation.
-\emph{Semantic selection} enable the selection of mixed
+\emph{Semantic selection} enables the selection of mixed
\MATHML+\BOXML{} markup, constraining the selection to markup
representing meaningful CIC (sub)terms. In the example on the left of
Fig.~\ref{fig:directmanip} is thus possible to select the subterm
$\mathrm{prime}~n$, whereas it would not be possible to select
-$\forall~n:nat$ since the former denotes an application while the
-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
+$\to n$ since the former denotes an application while the
+latter it not a subterm. Once a meaningful (sub)term has been
+selected actions can be done on it like reductions or tactic
applications.
+\begin{figure}[t]
+ \begin{center}
+ \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
+ \hspace{0.05\textwidth}
+ \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
+ \caption{Semantic selection and hyperlinks}
+ \label{fig:directmanip}
+ \end{center}
+\end{figure}
+
+
\subsection{Patterns}
-In our experience working with direct manipulation of terms is really
-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 several situations working with direct manipulation of terms is
+simpler and faster than typing the corresponding textual
+commands~\cite{proof-by-pointing}.
+Nonetheless we need to record actions and selections in scripts.
-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.
+In \MATITA{} \emph{patterns} are textual representations of selections.
+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}
$\%$. \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.
+Textual patterns produced from a graphical selection are made of the
+\NT{sequent\_path} only. Such patterns can represent every selection,
+but are quite verbose. The \NT{wanted} part of the syntax is meant to
+help the users in writing concise and elegant patterns by hand.
\begin{table}
\caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
the source of an arrow and the head of the application that is
found in the arrow target.
- The first phase selects not only terms (roots of subterms) but also
- their context that will be eventually used in the second phase.
+ The first phase not only selects terms (roots of subterms) but
+ determines also their context that will be eventually used in the
+ second phase.
\item[Phase 2]
plays a role only if the $[~\verb+match+~\NT{wanted}~]$
part is specified. From the first phase we have some terms, that we
will see as subterm roots, and their context. For each of these
contexts the $\NT{wanted}$ term is disambiguated in it and the
- corresponding root is searched for a subterm $\alpha$-equivalent to
+ corresponding root is searched for a subterm that can be unified to
$\NT{wanted}$. The result of this search is the selection the
pattern represents.
\end{description}
\subsubsection{Examples}
-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 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}
-theorem valid_name: \forall n,m. m + n = n \to m = O.
- intros (n m H).
-\end{grafite}
-\noindent
-leads you to the following sequent
+%To explain how the first phase works let us give an example. Consider
+%you want to prove the uniqueness of the identity element $0$ for natural
+%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}
+%theorem valid_name: \forall n,m. m + n = n \to m = O.
+% intros (n m H).
+%\end{grafite}
+%\noindent
+Consider the following sequent
\sequent{
n:nat\\
m:nat\\
m=O
}
\noindent
-where you want to change the right part of the equivalence of the $H$
-hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
+To change the right part of the equivalence of the $H$
+hypothesis with $O + n$ the user selects and pastes it as the pattern
+in the following statement.
\begin{grafite}
change in H:(? ? ? %) with (O + n).
\end{grafite}
\noindent
-This pattern, that is a simple instance of the $\NT{sequent\_path}$
-grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
-and discharges the head of the application and the first two arguments with a
-$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
-but the user can simply select with the mouse the right part of the equivalence
-and left to the system the burden of writing down in the script file the
-corresponding pattern with $?$ and $\%$ in the right place (that is not
-trivial, expecially where implicit arguments are hidden by the notation, like
-the type $nat$ in this example).
-
-Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
-works too and can be done, by the experienced user, writing directly
-a simpler pattern that uses the second phase.
+To understand the pattern (or produce it by hand) the user should be
+aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
+that the pattern selects only the third argument of $eq$.
+
+The experienced user may also write by hand a concise pattern
+to change at once all the occcurrences of $n$ in the hypothesis $H$:
\begin{grafite}
change in H match n with (O + n).
\end{grafite}
\noindent
In this case the $\NT{sequent\_path}$ selects the whole $H$, while
-the second phase searches the wanted $n$ inside it by
-$\alpha$-equivalence. The resulting
-equivalence will be $m+(O+n)=O+n$ since the second phase found two
-occurrences of $n$ in $H$ and the tactic changed both.
+the second phase locates $n$.
-Just for completeness the second pattern is equivalent to the
-following one, that is less readable but uses only the first phase.
+The latter pattern is equivalent to the following one, that the system
+can automatically generate from the selection.
\begin{grafite}
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
\noindent
\subsubsection{Tactics supporting patterns}
+MERGIARE CON IL SUCCESSIVO FACENDO NOTARE CHE I PATTERNS SONO UNA
+INTERFACCIA OCMUNE PER LE TATTICHE
+
In \MATITA{} all the tactics that can be restricted to subterm of the working
sequent accept the pattern syntax. In particular these tactics are: simplify,
change, fold, unfold, generalize, replace and rewrite.
con una pattern\_of(select(pattern))}
\subsubsection{Comparison with \COQ{}}
-\COQ{} has a two diffrent ways of restricting the application of tactis to
+\COQ{} has a two different ways of restricting the application of tactis to
subterms of the sequent, both relaying on the same special syntax to identify
a term occurrence.
-The first way is to use this special syntax to specify directly to the
-tactic the occurrnces of a wanted term that should be affected, while
-the second is to prepare the sequent with another tactic called
-pattern and the apply the real tactic. Note that the choice is not
+The first way is to use this special syntax to tell the
+tactic what occurrences of a wanted term should be affected.
+The second is to prepare the sequent with another tactic called
+pattern and then apply the real tactic. Note that the choice is not
left to the user, since some tactics needs the sequent to be prepared
with pattern and do not accept directly this special syntax.
\end{grafite}
\noindent
meaning that in the hypothesis $H$ the $n$ we want to change is the
-second we encounter proceeding from left toright.
+second we encounter proceeding from left to right.
The tactic pattern computes a
$\beta$-expansion of a part of the sequent with respect to some
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
+and) result in a single step of execution. The workaround does not work
anymore unless you de-structure on the fly the proof, putting some
``\texttt{.}'' where you want the system to stop.\\
projects / helm.git / commitdiff