From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 6 Dec 2005 11:36:15 +0000 (+0000)
Subject: Naming convention.
X-Git-Tag: make_still_working~8042
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a28be581787d98b13ffae6d3042261cde919d4f;p=helm.git

Naming convention.
---

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index c994cbc12..2cc1dc8a0 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1223,10 +1223,8 @@ 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. The most complex result proved
-so far in Matita (that however, at our knoweledge, has never been proved
-before in any other system) is the multiplicative property for Eulers'
-totient function $\phi$.
+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).
@@ -1253,6 +1251,73 @@ developing wiki-technologies to support a collaborative
 development of the library, encouraging people to expand, 
 modify and elaborate previous contributions.
 
+\subsection{Matita's naming convention}
+A minor but not entirely negligeable 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 fo such a theorem. 
+So, somehow unexpectedly, the introduction of semi-rigid naming convention
+also had benefical effects 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 $_to_Prop$. In the above example, 
+$eqb_to_Prop$ is accepted. 
+
+
+
 
 \acknowledgements
 We would like to thank all the students that during the past