The authoring interface of \MATITA{} is very similar to Proof
General~\cite{proofgeneral}. 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, in the UI.
+of all we wanted to integrate in the UI our rendering technologies, mainly
+\GTKMATHVIEW, to render sequents exploiting the bidimensional mathematical layouts
+of \MATHML-Presentation.
At the time of writing Proof General supports only text based
rendering.\footnote{This may change with future releases of Proof General
-based on Eclipse (\url{http://www.eclipse.org/}), but is not yet the
-case.} The second reason is that we wanted
+based on Eclipse (\url{http://www.eclipse.org/}).} The second reason is that we wanted
to build the \MATITA{} UI on top of a state-of-the-art and widespread graphical
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
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface.
+The foreground
window is an instance of the cicBrowser (see Sect.~\ref{sec:library}) used to
-render in natural language the proof being developed.
+render in natural language the proof under development.
Note that the syntax used in the script view is \TeX-like, but
Unicode\footnote{\url{http://www.unicode.org/}} is
\end{figure}
Since the concepts of script based proof authoring are well-known, the
-remaining part of this section is dedicated to the distinguishing
+remaining part of this section is devoted to the distinguishing
features of the \MATITA{} authoring interface.
\subsection{Direct manipulation of terms}
pattern n at 2 in H
\end{grafite}
would have resulted in the sequent:
-\sequent{n: nat\\m : nat\\H: (fun n0: nat => m + n = n0) n}{m = 0}
+\sequent{n: nat\\m : nat\\H: (fun~n0: nat => m + n = n0)~n}{m = 0}
where \texttt{H} is $\beta$-expanded over the second \texttt{n}
occurrence.
x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
\texttt{(fun n0: nat => m + n = n0)}.
-Since \TAC{rewrite}, \TAC{replace} and several other tactics boils down to
+Since \TAC{rewrite}, \TAC{replace} and several other tactics boil down to
the application of the equality elimination principle, the previous
trick implements the expected behavior.
The idea behind this way of identifying subterms in not really far
from the idea behind patterns, but fails in extending to
complex notation, since it relies on a mono-dimensional sequent representation.
-Real math notation places arguments upside-down (like in indexed sums or
+Real mathematical notation places arguments upside-down (like in indexed sums or
integrations) or even puts them inside a bidimensional matrix.
In these cases using the mouse to select the wanted term is probably the
more effective way to tell the system what to do.
-
-One of the goals of \MATITA{} is to use modern publishing techniques, and
-adopting a method for restricting tactics application domain that discourages
-using heavy math notation would have definitively been a bad choice.
+One of the goals of \MATITA{} is to use modern publishing techniques,
+so we prefer our method that does not discourage the use of complex layout schemata.
In \MATITA{}, tactics accepting pattern arguments can be more expressive than
the equivalent tactics in \COQ{} since variables bound in the pattern context,
change in H: \forall _. (? ? % ?) with (S m) * n.
\end{grafite}
to change $n+m*n$ with $(S~m)*n$. To achieve the same effect in \COQ, the
-user is obliged to change the whole hypothesis rewriting its right hand side
+user is forced to change the whole hypothesis rewriting its right hand side
as well.
\subsection{Tacticals}
projects / helm.git / blobdiff