X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=f2e411d4a6b097227b4a315698d3993d97caa0fb;hb=6db12650bceb071d9b5ea8f882613a98bd6df79b;hp=3cc2faf039f4826469b0f8e1a0e31ca8a50ac6a0;hpb=c2e705d92a743db375539b8face34e5ee114e909;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 3cc2faf03..f2e411d4a 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -123,6 +123,7 @@ Digital Libraries}
 
 \end{opening}
 
+
 \section{Introduction}
 \label{sec:intro}
 \MATITA{} is the Proof Assistant under development by the \HELM{} team
@@ -694,7 +695,73 @@ content selection and copy-paste.
 
 \subsection{Automation}
 
-\subsection{Naming}
+\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 
+(not definitions), and relates the name of a proof to its statement.
+The basic rules are the following:
+\begin{itemize}
+\item each identifier is composed by an ordered list of (short)
+names occurring in a left to right traversal of the statement; 
+\item all identifiers should (but this is not strictly compulsory) 
+separated by an underscore,
+\item identifiers in two different hypothesis, or in an hypothesis
+and in the conlcusion must be separated by the string ``\verb+_to_+'';
+\item the identifier may be followed by a numerical suffix, or a
+single or duoble apostrophe.
+
+\end{itemize}
+Take for instance the theorem
+\[\forall n:nat. n = plus \; n\; O\]
+Possible legal names are: \verb+plus_n_O+, \verb+plus_O+, 
+\verb+eq_n_plus_n_O+ and so on. 
+Similarly, consider the theorem 
+\[\forall n,m:nat. n<m \to n \leq m\]
+In this case \verb+lt_to_le+ is a legal name, 
+while \verb+lt_le+ is not.\\
+But what about, say, the symmetric law of equality? Probably you would like 
+to name such a theorem with something explicitly recalling symmetry.
+The correct approach, 
+in this case, is the following. You should start with defining the 
+symmetric property for relations
+
+\[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
+
+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. 
+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 
+using them (and formalizing such use).
+
+Two cases have a special treatment. The first one concerns theorems whose
+conclusion is a (universally quantified) predicate variable, i.e. 
+theorems of the shape
+$\forall P,\dots.P(t)$.
+In this case you may replace the conclusion with the word
+``elim'' or ``case''.
+For instance the name \verb+nat_elim2+ is a legal name for the double
+induction principle.
+
+The other special case is that of statements whose conclusion is a
+match expression. 
+A typical example is the following
+\begin{verbatim}
+  \forall n,m:nat. 
+      match (eqb n m) with
+        [ true  \Rightarrow n = m 
+        | false \Rightarrow n \neq m]
+\end{verbatim}
+where $eqb$ is boolean equality.
+In this cases, the name can be build starting from the matched
+expression and the suffix \verb+_to_Prop+. In the above example, 
+\verb+eqb_to_Prop+ is accepted. 
+
+\section{The \MATITA{} user interface}
+
 
 
 \subsection{Disambiguation}
@@ -906,111 +973,6 @@ implicit coercions.
 
 
 
-\subsection{The logical library}
-
-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. 
-The current library just comprises about one thousand theorems in 
-elementary aspects of arithmetics up to the multiplicative property for 
-Eulers' totient function $\phi$.
-The library is organized in five main directories: $logic$ (connectives,
-quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type 
-constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
-The most complex development is $nat$, organized in 25 scripts, listed
-in Figure\ref{scripts}
-\begin{figure}[htb]
-$\begin{array}{lll}
-nat.ma    & plus.ma & times.ma  \\
-minus.ma  & exp.ma  & compare.ma \\
-orders.ma & le\_arith.ma &  lt\_arith.ma \\   
-factorial.ma & sigma\_and\_pi.ma & minimization.ma  \\
-div\_and\_mod.ma & gcd.ma & congruence.ma \\
-primes.ma & nth\_prime.ma & ord.ma\\
-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}
-\end{figure}
-
-We do not plan to maintain the library in a centralized way, 
-as most of the systems do. On the contary we are currently
-developing wiki-technologies to support a collaborative 
-development of the library, encouraging people to expand, 
-modify and elaborate previous contributions.
-
-\subsubsection{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 
-(not definitions), and relates the name of a proof to its statement.
-The basic rules are the following:
-\begin{itemize}
-\item each identifier is composed by an ordered list of (short)
-names occurring in a left to right traversal of the statement; 
-\item all identifiers should (but this is not strictly compulsory) 
-separated by an underscore,
-\item identifiers in two different hypothesis, or in an hypothesis
-and in the conlcusion must be separated by the string ``\verb+_to_+'';
-\item the identifier may be followed by a numerical suffix, or a
-single or duoble apostrophe.
-
-\end{itemize}
-Take for instance the theorem
-\[\forall n:nat. n = plus \; n\; O\]
-Possible legal names are: \verb+plus_n_O+, \verb+plus_O+, 
-\verb+eq_n_plus_n_O+ and so on. 
-Similarly, consider the theorem 
-\[\forall n,m:nat. n<m \to n \leq m\]
-In this case \verb+lt_to_le+ is a legal name, 
-while \verb+lt_le+ is not.\\
-But what about, say, the symmetric law of equality? Probably you would like 
-to name such a theorem with something explicitly recalling symmetry.
-The correct approach, 
-in this case, is the following. You should start with defining the 
-symmetric property for relations
-
-\[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
-
-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. 
-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 
-using them (and formalizing such use).
-
-Two cases have a special treatment. The first one concerns theorems whose
-conclusion is a (universally quantified) predicate variable, i.e. 
-theorems of the shape
-$\forall P,\dots.P(t)$.
-In this case you may replace the conclusion with the word
-``elim'' or ``case''.
-For instance the name \verb+nat_elim2+ is a legal name for the double
-induction principle.
-
-The other special case is that of statements whose conclusion is a
-match expression. 
-A typical example is the following
-\begin{verbatim}
-  \forall n,m:nat. 
-      match (eqb n m) with
-        [ true  \Rightarrow n = m 
-        | false \Rightarrow n \neq m]
-\end{verbatim}
-where $eqb$ is boolean equality.
-In this cases, the name can be build starting from the matched
-expression and the suffix \verb+_to_Prop+. In the above example, 
-\verb+eqb_to_Prop+ is accepted. 
-
-\section{The \MATITA{} user interface}
-
 
 \subsection{Patterns}
 
@@ -1424,6 +1386,44 @@ even being a so simple idea:
   goal) gives you the feeling of what is going on.
 \end{description}
 
+\section{The Matita library}
+
+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. 
+The current library just comprises about one thousand theorems in 
+elementary aspects of arithmetics up to the multiplicative property for 
+Eulers' totient function $\phi$.
+The library is organized in five main directories: $logic$ (connectives,
+quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type 
+constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
+The most complex development is $nat$, organized in 25 scripts, listed
+in Figure\ref{scripts}
+\begin{figure}[htb]
+$\begin{array}{lll}
+nat.ma    & plus.ma & times.ma  \\
+minus.ma  & exp.ma  & compare.ma \\
+orders.ma & le\_arith.ma &  lt\_arith.ma \\   
+factorial.ma & sigma\_and\_pi.ma & minimization.ma  \\
+div\_and\_mod.ma & gcd.ma & congruence.ma \\
+primes.ma & nth\_prime.ma & ord.ma\\
+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}
+\end{figure}
+
+We do not plan to maintain the library in a centralized way, 
+as most of the systems do. On the contary we are currently
+developing wiki-technologies to support a collaborative 
+development of the library, encouraging people to expand, 
+modify and elaborate previous contributions.
+
 \section{Conclusions}
 
 \acknowledgements