\end{opening}
+
\section{Introduction}
\label{sec:intro}
\MATITA{} is the Proof Assistant under development by the \HELM{} team
\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}
-\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}
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
projects / helm.git / blobdiff