diff options
author | 2001-04-11 12:41:41 +0000 | |
---|---|---|
committer | 2001-04-11 12:41:41 +0000 | |
commit | 4ac0580306ea9e45da1863316936d700969465ad (patch) | |
tree | bf7595cd76895f3a349e7e75ca9d64231b01dcf8 /theories/Arith/intro.tex | |
parent | 8a7452976731275212f0c464385b380e2d590f5e (diff) |
documentation automatique de la bibliothèque standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/intro.tex')
-rwxr-xr-x | theories/Arith/intro.tex | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex new file mode 100755 index 000000000..7d922c5b6 --- /dev/null +++ b/theories/Arith/intro.tex @@ -0,0 +1,55 @@ +\section{Arith}\label{Arith} + +The {\tt Arith} library deals with various arithmetical notions and +their properties. + +\subsection*{Standard {\tt Arith} library} + +The following files are automatically loaded by {\tt Require Arith}. + +\begin{itemize} + +\item {\tt Le.v} states and proves properties of the large order {\tt le}. + +\item {\tt Lt.v} states and proves properties of the strict order {\tt +lt} (especially, the relationship with {\tt le}). + +\item {\tt Plus.v} states and proves properties on the addition. + +\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. + +\item {\tt Minus.v} defines the difference on +{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is +{\tt O} if {\tt n} $<$ {\tt p}. + +\item {\tt Mult.v} states and proves properties on the multiplication. + +\item {\tt Between.v} defines modalities on {\tt nat} and proves properties +of them. + +\end{itemize} + +\subsection*{Additional {\tt Arith} library} + +\begin{itemize} + +\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state +and prove various decidability results on {\tt nat}. + +\item {\tt Wf\_nat.v} states and proves various induction and recursion +principles on {\tt nat}. Especially, recursion for objects measurable by +a natural number and recursion on {\tt nat * nat} are provided. + +\item {\tt Min.v} defines the minimum of two natural numbers and proves +properties of it. + +\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows +the equivalence with Leibniz' equality. + +\item {\tt Euclid\_def.v} and {\tt Euclid\_prog.v} prove that the euclidean +division specification is realisable. Conversely, {\tt Div.v} exhibits +two different algorithms and semi-automatically reconstruct the proof of +their correctness. These files emphasize the extraction of program vs +reconstruction of proofs paradigm. + +\end{itemize} |