]> matita.cs.unibo.it Git - helm.git/commitdiff
- towards completion of the disambiguation section
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 23 Jan 2006 07:54:21 +0000 (07:54 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 23 Jan 2006 07:54:21 +0000 (07:54 +0000)
- some \MATITA and \COQ here and there

helm/papers/matita/matita2.tex

index f1bc990c7d36c6799535bf47edd3e26e688fed4c..3f333440334aeed9c7fe542534e73c099f5692df 100644 (file)
@@ -1,4 +1,4 @@
-\documentclass[]{kluwer}
+\documentclass[draft]{kluwer}
 \usepackage{color}
 \usepackage{graphicx}
 % \usepackage{amssymb,amsmath}
@@ -18,6 +18,7 @@
 
 \newcommand{\AUTO}{\textsc{Auto}}
 \newcommand{\COQ}{Coq}
+\newcommand{\COQIDE}{CoqIde}
 \newcommand{\ELIM}{\textsc{Elim}}
 \newcommand{\GDOME}{Gdome}
 \newcommand{\HELM}{Helm}
 \institute{Department of Computer Science, University of Bologna\\
  Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
 
-\runningtitle{The Matita proof assistant}
+\runningtitle{The \MATITA{} proof assistant}
 \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
 
 % \date{data}
@@ -164,7 +165,7 @@ active in the MathML Working group since 1999.};
 \end{itemize}
 
 According to our content-centric commitment, the library exported from
-Coq was conceived as being distributed and most of the tools were developed
+\COQ{} was conceived as being distributed and most of the tools were developed
 as Web services. The user could interact with the library and the tools by
 means of a Web interface that orchestrates the Web services.
 
@@ -206,7 +207,7 @@ DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
 
 \begin{itemize}
  \item scelta del sistema fondazionale
- \item sistema indipendente (da Coq)
+ \item sistema indipendente (da \COQ)
  \item compatibilit\`a con sistemi legacy
 \end{itemize}
 
@@ -781,7 +782,7 @@ deletion of all the outputs of the compilation, metadata included, the
 library browsable trough the \WHELP{} technology is always up to date.
 
 \subsubsection{Interactive and batch (de)compilation}
-Matita includes an interactive graphical interface and a batch
+\MATITA{} includes an interactive graphical interface and a batch
 compiler. Only the former is intended to be used directly by the
 user, the latter is automatically invoked when a not yet compiled
 part of the user development is required.
@@ -830,8 +831,8 @@ symmetrically to undo single steps, thus removing single objects.
 
 \subsection{Automation}
 
-\subsection{Matita's naming convention}
-A minor but not entirely negligible aspect of Matita is that of
+\subsection{\MATITA's naming convention}
+A minor but not entirely negligible aspect of \MATITA{} is that of
 adopting a (semi)-rigid naming convention for identifiers, derived by 
 our studies about metadata for statements. 
 The convention is only applied to identifiers for theorems 
@@ -866,7 +867,7 @@ symmetric property for relations
 
 Then, you may state the symmetry of equality as
 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
-and \verb+symmetric_eq+ is valid Matita name for such a theorem. 
+and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem. 
 So, somehow unexpectedly, the introduction of semi-rigid naming convention
 has an important benefical effect on the global organization of the library, 
 forcing the user to define abstract notions and properties before 
@@ -1077,29 +1078,40 @@ twice that coercion on the left hand side of the implication. The obtained
 partially specified term however would not probably be the expected one, being a
 theorem which prove a trivial implication. For this reason we choose to always
 prefer fresh instances over implicit coercions, i.e. we always attempt
-disambiguation passes with fresh instances before attempting passes with
-implicit coercions.
+disambiguation passes with fresh instances and no implicit coercions before
+attempting passes with implicit coercions.
 
 \subsubsection{Disambiguation passes}
 
+Summarizing, we perform multiple disambiguation passes for each presentation
+level term and in each of them we have 3 degree of freedom: disambiguation
+aliases (mono/multi/library), operator instances (shared/fresh), and implicit
+coercions (enabled/disabled). This would lead to up to 12 different
+disambiguation passes with ordering to be decided upon. Our choice in \MATITA{}
+is depicted in Tab.~\ref{tab:disambpasses}.
+
 \TODO{spiegazione della tabella}
 
-\begin{center}
- \begin{tabular}{c|c|c|c}
-  \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
-  & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
-  & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
-  & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
-  \hline
-  \PASS & Normal & Mono & Disabled \\
-  \PASS & Normal & Multi & Disabled \\
-  \PASS & Fresh & Mono & Disabled \\
-  \PASS & Fresh & Multi & Disabled \\
-  \PASS & Fresh & Mono & Enabled \\
-  \PASS & Fresh & Multi & Enabled \\
-  \PASS & Fresh & Library & Enabled
- \end{tabular}
-\end{center}
+\begin{table}
+ \caption{\label{tab:disambpasses} Disambiguation passes.\strut}
+ \footnotesize
+ \begin{center}
+  \begin{tabular}{c|c|c|c}
+   \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+   & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+   & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+   & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+   \hline
+   \PASS & Mono aliases   & Shared         & Disabled \\
+   \PASS & Multi aliases  & Shared         & Disabled \\
+   \PASS & Mono aliases   & Fresh instances & Disabled \\
+   \PASS & Multi aliases  & Fresh instances & Disabled \\
+   \PASS & Mono        aliases   & Fresh instances & Enabled  \\
+   \PASS & Multi aliases  & Fresh instances & Enabled  \\
+   \PASS & Library aliases& Fresh instances & Enabled
+  \end{tabular}
+ \end{center}
+\end{table}
 
 \TODO{alias one shot}
 
@@ -1119,7 +1131,7 @@ tattichini.\\
 Patterns are the textual counterpart of the MathML widget graphical
 selection.
 
-Matita benefits of a graphical interface and a powerful MathML rendering
+\MATITA{} benefits of a graphical interface and a powerful MathML rendering
 widget that allows the user to select pieces of the sequent he is working
 on. While this is an extremely intuitive way for the user to
 restrict the application of tactics, for example, to some subterms of the
@@ -1272,8 +1284,8 @@ supportarlo bisogna far loro trasformare il pattern phase1+phase2
 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
 con una pattern\_of(select(pattern))}
 
-\subsubsection{Comparison with Coq}
-Coq has a two diffrent ways of restricting the application of tactis to
+\subsubsection{Comparison with \COQ{}}
+\COQ{} has a two diffrent ways of restricting the application of tactis to
 subterms of the sequent, both relaying on the same special syntax to identify
 a term occurrence.
 
@@ -1486,7 +1498,7 @@ even being a so simple idea:
 \item[Proof structuring] 
   is much easier. Consider for example a proof by induction, and imagine you
   are using classical tacticals in one of the state of the
-  art graphical interfaces for proof assistant like Proof General or Coq Ide.
+  art graphical interfaces for proof assistant like Proof General or \COQIDE.
   After applying the induction principle you have to choose: structure
   the proof or not. If you decide for the former you have to branch with
   ``\texttt{[}'' and write tactics for all the cases separated by 
@@ -1521,15 +1533,15 @@ even being a so simple idea:
   goal) gives you the feeling of what is going on.
 \end{description}
 
-\section{The Matita library}
+\section{The \MATITA{} library}
 
-Matita is Coq compatible, in the sense that every theorem of Coq
+\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
 can be read, checked and referenced in further developments. 
 However, in order to test the actual usability of the system, a
 new library of results has been started from scratch. In this case, 
 of course, we wrote (and offer) the source script files, 
-while, in the case of Coq, Matita may only rely on XML files of
-Coq objects. 
+while, in the case of \COQ, \MATITA{} may only rely on XML files of
+\COQ{} objects. 
 The current library just comprises about one thousand theorems in 
 elementary aspects of arithmetics up to the multiplicative property for 
 Eulers' totient function $\phi$.
@@ -1550,7 +1562,7 @@ count.ma  & relevant\_equations.ma & permutation.ma \\
 factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\     
 totient.ma& & \\
 \end{array}$
-\caption{\label{scripts}Matita scripts on natural numbers}
+\caption{\label{scripts}\MATITA{} scripts on natural numbers}
 \end{figure}
 
 We do not plan to maintain the library in a centralized way, 
@@ -1564,7 +1576,7 @@ modify and elaborate previous contributions.
 \acknowledgements
 We would like to thank all the students that during the past
 five years collaborated in the \HELM{} project and contributed to 
-the development of Matita, and in particular
+the development of \MATITA{}, and in particular
 M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
 and V.~Tamburrelli.