From bdd8d14cd9014ebe2e4f10075831c2921078dfbe Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 1 Feb 2006 16:56:15 +0000 Subject: [PATCH] Snapshot --- helm/papers/matita/matita2.tex | 33 ++++++++++++++------------------- 1 file changed, 14 insertions(+), 19 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 86c7d4230..e8d55f5a1 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1337,22 +1337,19 @@ expression and the suffix \texttt{\_to\_Prop}. In the above example, 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 @@ -1367,7 +1364,7 @@ also fully supported so that mathematical glyphs can be input as such. \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} @@ -1574,7 +1571,7 @@ command: 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. @@ -1583,21 +1580,19 @@ the application of an elimination principle (of the form $\forall P.\forall 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, @@ -1608,7 +1603,7 @@ In \MATITA{} the user can issue the command: 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} -- 2.39.5