summaryrefslogtreecommitdiff
path: root/theories/Arith/intro.tex
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Arith/intro.tex
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Arith/intro.tex')
-rwxr-xr-xtheories/Arith/intro.tex55
1 files changed, 55 insertions, 0 deletions
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
new file mode 100755
index 00000000..655de34c
--- /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.v} proves 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}