Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

author: Samuel Mimram <smimram@debian.org> 2006-04-28 14:59:16 +0000
committer: Samuel Mimram <smimram@debian.org> 2006-04-28 14:59:16 +0000
commit: 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
tree: ad89c6bb57ceee608fcba2bb3435b74e0f57919e /doc/stdlib
parent: 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
5 files changed, 474 insertions, 0 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
new file mode 100755
index 00000000..97748af6
--- /dev/null
+++ b/doc/stdlib/Library.tex
@@ -0,0 +1,62 @@
+\documentclass[11pt]{article}
+
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+
+\input{../common/version}
+\input{../common/title}
+\input{../common/macros}
+
+\begin{document}
+ 
+\coverpage{The standard library}%
+{\ }
+{This material is distributed under the terms of the GNU Lesser
+General Public License Version 2.1.}
+
+\tableofcontents
+
+\newpage
+\section*{The \Coq\ standard library}
+
+This document is a short description of the \Coq\ standard library.
+This library comes with the system as a complement of the core library
+(the {\bf Init} library ; see the Reference Manual for a description
+of this library). It provides a set of modules directly available
+through the \verb!Require! command.
+
+The standard library is composed of the following subdirectories:
+\begin{description}
+  \item[Logic]  Classical logic and dependent equality
+  \item[Bool]   Booleans (basic functions and results)
+  \item[Arith]  Basic Peano arithmetic
+  \item[ZArith] Basic integer arithmetic
+  \item[Reals]  Classical Real Numbers and Analysis
+  \item[Lists]  Monomorphic and polymorphic lists (basic functions and
+                  results), Streams (infinite sequences defined 
+                  with co-inductive types)
+  \item[Sets]   Sets (classical, constructive, finite, infinite, power set,
+                  etc.)
+  \item[Relations] Relations (definitions and basic results).
+  \item[Sorting] Sorted list (basic definitions and heapsort
+                 correctness). 
+  \item[Wellfounded] Well-founded relations (basic results).
+  \item[IntMap]       Representation of finite sets by an efficient
+                     structure of map (trees indexed by binary integers).
+\end{description}
+
+
+Each of these subdirectories contains a set of modules, whose
+specifications (\gallina{} files) have
+been roughly, and automatically, pasted in the following pages. There
+is also a version of this document in HTML format on the WWW, which
+you can access from the \Coq\ home page at
+\texttt{http://coq.inria.fr/library}.
+
+\input{Library.coqdoc}
+
+\end{document}
+
+% $Id: Library.tex 8626 2006-03-14 15:01:00Z notin $ 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
new file mode 100644
index 00000000..cbb8580d
--- /dev/null
+++ b/doc/stdlib/index-list.html.template
@@ -0,0 +1,339 @@
+<html>
+
+<head>
+<link rel="stylesheet" href="coqdoc.css" type="text/css">
+<title>The Coq Standard Library
+</head>
+
+<body>
+
+<H1>The Coq Standard Library</H1>
+
+<p>Here is a short description of the Coq standard library, which is
+distributed with the system.
+It provides a set of modules directly available 
+through the <tt>Require Import</tt> command.</p>
+
+<p>The standard library is composed of the following subdirectories:</p>
+
+<dl>
+  <dt> <b>Init</b>:
+    The core library (automatically loaded when starting Coq)
+  </dt>
+  <dd> 
+    theories/Init/Notations.v
+    theories/Init/Datatypes.v
+    theories/Init/Logic.v
+    theories/Init/Logic_Type.v
+    theories/Init/Peano.v
+    theories/Init/Specif.v
+    theories/Init/Tactics.v
+    theories/Init/Wf.v
+    (theories/Init/Prelude.v)
+  </dd>
+  
+  <dt> <b>Logic</b>:
+      Classical logic and dependent equality
+  </dt>
+  <dd>
+    theories/Logic/Classical_Pred_Set.v
+    theories/Logic/Classical_Pred_Type.v
+    theories/Logic/Classical_Prop.v
+    theories/Logic/Classical_Type.v
+    (theories/Logic/Classical.v)
+    theories/Logic/Decidable.v
+    theories/Logic/Eqdep_dec.v
+    theories/Logic/EqdepFacts.v
+    theories/Logic/Eqdep.v
+    theories/Logic/JMeq.v
+    theories/Logic/RelationalChoice.v
+    theories/Logic/ClassicalChoice.v
+    theories/Logic/ChoiceFacts.v
+    theories/Logic/ClassicalDescription.v
+    theories/Logic/ClassicalFacts.v
+    theories/Logic/Berardi.v
+    theories/Logic/Diaconescu.v
+    theories/Logic/Hurkens.v
+    theories/Logic/ProofIrrelevance.v
+    theories/Logic/ProofIrrelevanceFacts.v
+  </dd>
+    
+  <dt> <b>Arith</b>:
+    Basic Peano arithmetic
+  </dt>
+  <dd> 
+    theories/Arith/Le.v
+    theories/Arith/Lt.v
+    theories/Arith/Plus.v
+    theories/Arith/Minus.v
+    theories/Arith/Mult.v
+    theories/Arith/Gt.v
+    theories/Arith/Between.v
+    theories/Arith/Peano_dec.v
+    theories/Arith/Compare_dec.v
+    (theories/Arith/Arith.v)
+    theories/Arith/Min.v
+    theories/Arith/Max.v
+    theories/Arith/Compare.v
+    theories/Arith/Div2.v
+    theories/Arith/Div.v
+    theories/Arith/EqNat.v
+    theories/Arith/Euclid.v
+    theories/Arith/Even.v
+    theories/Arith/Bool_nat.v
+    theories/Arith/Factorial.v
+    theories/Arith/Wf_nat.v
+  </dd>
+    
+  <dt> <b>NArith</b>:
+    Binary positive integers
+  </dt>
+  <dd> 
+    theories/NArith/BinPos.v
+    theories/NArith/BinNat.v
+    (theories/NArith/NArith.v)
+    theories/NArith/Pnat.v
+  </dd>
+
+  <dt> <b>ZArith</b>:
+       Binary integers
+  </dt>
+  <dd> 
+    theories/ZArith/BinInt.v
+    theories/ZArith/Zorder.v
+    theories/ZArith/Zcompare.v
+    theories/ZArith/Znat.v
+    theories/ZArith/Zmin.v
+    theories/ZArith/Zmax.v
+    theories/ZArith/Zminmax.v
+    theories/ZArith/Zabs.v
+    theories/ZArith/Zeven.v
+    theories/ZArith/auxiliary.v
+    theories/ZArith/ZArith_dec.v
+    theories/ZArith/Zbool.v
+    theories/ZArith/Zmisc.v
+    theories/ZArith/Wf_Z.v
+    theories/ZArith/Zhints.v
+    (theories/ZArith/ZArith_base.v)
+    theories/ZArith/Zcomplements.v
+    theories/ZArith/Zsqrt.v
+    theories/ZArith/Zpower.v
+    theories/ZArith/Zdiv.v
+    theories/ZArith/Zlogarithm.v
+    (theories/ZArith/ZArith.v)
+    theories/ZArith/Zwf.v
+    theories/ZArith/Zbinary.v
+    theories/ZArith/Znumtheory.v
+  </dd>
+    
+  <dt> <b>Reals</b>:
+    Formalization of real numbers
+  </dt>
+  <dd> 
+    theories/Reals/Rdefinitions.v
+    theories/Reals/Raxioms.v
+    theories/Reals/RIneq.v
+    theories/Reals/DiscrR.v
+    (theories/Reals/Rbase.v)
+    theories/Reals/RList.v
+    theories/Reals/Ranalysis.v
+    theories/Reals/Rbasic_fun.v
+    theories/Reals/Rderiv.v
+    theories/Reals/Rfunctions.v
+    theories/Reals/Rgeom.v
+    theories/Reals/R_Ifp.v
+    theories/Reals/Rlimit.v
+    theories/Reals/Rseries.v
+    theories/Reals/Rsigma.v
+    theories/Reals/R_sqr.v
+    theories/Reals/Rtrigo_fun.v
+    theories/Reals/Rtrigo.v
+    theories/Reals/SplitAbsolu.v
+    theories/Reals/SplitRmult.v
+    theories/Reals/Alembert.v
+    theories/Reals/AltSeries.v
+    theories/Reals/ArithProp.v
+    theories/Reals/Binomial.v
+    theories/Reals/Cauchy_prod.v
+    theories/Reals/Cos_plus.v
+    theories/Reals/Cos_rel.v
+    theories/Reals/Exp_prop.v
+    theories/Reals/Integration.v
+    theories/Reals/MVT.v
+    theories/Reals/NewtonInt.v
+    theories/Reals/PSeries_reg.v
+    theories/Reals/PartSum.v
+    theories/Reals/R_sqrt.v
+    theories/Reals/Ranalysis1.v
+    theories/Reals/Ranalysis2.v
+    theories/Reals/Ranalysis3.v
+    theories/Reals/Ranalysis4.v
+    theories/Reals/Rcomplete.v
+    theories/Reals/RiemannInt.v
+    theories/Reals/RiemannInt_SF.v
+    theories/Reals/Rpower.v
+    theories/Reals/Rprod.v
+    theories/Reals/Rsqrt_def.v
+    theories/Reals/Rtopology.v
+    theories/Reals/Rtrigo_alt.v
+    theories/Reals/Rtrigo_calc.v
+    theories/Reals/Rtrigo_def.v
+    theories/Reals/Rtrigo_reg.v
+    theories/Reals/SeqProp.v
+    theories/Reals/SeqSeries.v
+    theories/Reals/Sqrt_reg.v
+    (theories/Reals/Reals.v)
+  </dd>
+    
+  <dt> <b>Bool</b>:
+       Booleans (basic functions and results)
+  </dt>
+  <dd> 
+    theories/Bool/Bool.v
+    theories/Bool/BoolEq.v
+    theories/Bool/DecBool.v
+    theories/Bool/IfProp.v
+    theories/Bool/Sumbool.v
+    theories/Bool/Zerob.v
+    theories/Bool/Bvector.v
+  </dd>
+    
+  <dt> <b>Lists</b>:
+    Polymorphic lists, Streams (infinite sequences)
+  </dt>
+  <dd> 
+    theories/Lists/List.v
+    theories/Lists/ListSet.v
+    theories/Lists/MonoList.v
+    theories/Lists/MoreList.v
+    theories/Lists/SetoidList.v
+    theories/Lists/Streams.v
+    theories/Lists/TheoryList.v
+  </dd>
+  
+  <dt> <b>Sets</b>:
+       Sets (classical, constructive, finite, infinite, powerset, etc.)
+  </dt>
+  <dd> 
+    theories/Sets/Classical_sets.v
+    theories/Sets/Constructive_sets.v
+    theories/Sets/Cpo.v
+    theories/Sets/Ensembles.v
+    theories/Sets/Finite_sets_facts.v
+    theories/Sets/Finite_sets.v
+    theories/Sets/Image.v
+    theories/Sets/Infinite_sets.v
+    theories/Sets/Integers.v
+    theories/Sets/Multiset.v
+    theories/Sets/Partial_Order.v
+    theories/Sets/Permut.v
+    theories/Sets/Powerset_Classical_facts.v
+    theories/Sets/Powerset_facts.v
+    theories/Sets/Powerset.v
+    theories/Sets/Relations_1_facts.v
+    theories/Sets/Relations_1.v
+    theories/Sets/Relations_2_facts.v
+    theories/Sets/Relations_2.v
+    theories/Sets/Relations_3_facts.v
+    theories/Sets/Relations_3.v
+    theories/Sets/Uniset.v
+  </dd>
+    
+  <dt> <b>Relations</b>:
+       Relations (definitions and basic results)
+  </dt>
+  <dd> 
+    theories/Relations/Relation_Definitions.v
+    theories/Relations/Relation_Operators.v
+    theories/Relations/Relations.v
+    theories/Relations/Operators_Properties.v
+    theories/Relations/Rstar.v
+    theories/Relations/Newman.v
+  </dd>
+    
+  <dt> <b>Wellfounded</b>:
+       Well-founded Relations
+  </dt>
+  <dd> 
+    theories/Wellfounded/Disjoint_Union.v
+    theories/Wellfounded/Inclusion.v
+    theories/Wellfounded/Inverse_Image.v
+    theories/Wellfounded/Lexicographic_Exponentiation.v
+    theories/Wellfounded/Lexicographic_Product.v
+    theories/Wellfounded/Transitive_Closure.v
+    theories/Wellfounded/Union.v
+    theories/Wellfounded/Wellfounded.v
+    theories/Wellfounded/Well_Ordering.v
+  </dd>
+    
+  <dt> <b>Sorting</b>:
+    Axiomatizations of sorts
+  </dt>
+  <dd> 
+    theories/Sorting/Heap.v
+    theories/Sorting/Permutation.v
+    theories/Sorting/Sorting.v
+  </dd>
+  
+  <dt> <b>Setoids</b>:
+  <dd> 
+    theories/Setoids/Setoid.v
+  </dd>
+    
+  <dt> <b>IntMap</b>:
+    Finite sets/maps as trees indexed by addresses
+  </dt>
+  <dd> 
+    theories/IntMap/Addr.v
+    theories/IntMap/Adist.v
+    theories/IntMap/Addec.v
+    theories/IntMap/Adalloc.v
+    theories/IntMap/Map.v
+    theories/IntMap/Fset.v
+    theories/IntMap/Mapaxioms.v
+    theories/IntMap/Mapiter.v
+    theories/IntMap/Mapcanon.v
+    theories/IntMap/Mapsubset.v
+    theories/IntMap/Lsort.v
+    theories/IntMap/Mapfold.v
+    theories/IntMap/Mapcard.v
+    theories/IntMap/Mapc.v
+    theories/IntMap/Maplists.v
+    theories/IntMap/Allmaps.v
+  </dd>
+    
+  <dt> <b>FSets</b>:
+    Modular implementation of finite sets/maps using lists
+  </dt>
+  <dd>
+    theories/FSets/DecidableType.v
+    theories/FSets/OrderedType.v
+    theories/FSets/FSetInterface.v
+    theories/FSets/FSetBridge.v
+    theories/FSets/FSetProperties.v
+    theories/FSets/FSetEqProperties.v
+    theories/FSets/FSetFacts.v
+    theories/FSets/FSetList.v
+    theories/FSets/FSet.v
+    theories/FSets/FMapInterface.v
+    theories/FSets/FMapList.v
+    theories/FSets/FMap.v
+    theories/FSets/FSetWeakInterface.v
+    theories/FSets/FSetWeakFacts.v
+    theories/FSets/FSetWeakList.v
+    theories/FSets/FSetWeak.v
+    theories/FSets/FMapWeakInterface.v
+    theories/FSets/FMapWeakList.v
+    theories/FSets/FMapWeak.v
+  </dd>
+
+  <dt> <b>Strings</b>
+    Implementation of string as list of ascii characters
+  </dt>
+  <dd>
+    theories/Strings/Ascii.v
+    theories/Strings/String.v
+  </dd>
+    
+  </dd>
+</dl>
diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html
new file mode 100644
index 00000000..308b1d01
--- /dev/null
+++ b/doc/stdlib/index-trailer.html
@@ -0,0 +1,2 @@
+</body>
+</html>
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
new file mode 100755
index 00000000..91e3cc3f
--- /dev/null
+++ b/doc/stdlib/make-library-files
@@ -0,0 +1,36 @@
+#!/bin/sh
+
+# Needs COQTOP and GALLINA set
+
+# On garde la liste de tous les *.v avec dates dans library.files.ls
+# Si elle a change depuis la derniere fois ou library.files n'existe pas
+# on fabrique des .g (si besoin) et la liste library.files dans 
+# l'ordre de ls -tr des *.vo
+# Ce dernier trie les fichiers dans l'ordre inverse de leur date de cr�ation
+# En supposant que make fait son boulot, ca fait un tri topologique du
+# graphe des d�pendances
+
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids"
+
+rm -f library.files.ls.tmp
+(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
+if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then
+  mv -f library.files.ls.tmp library.files.ls
+  rm -f library.files; touch library.files
+  ABSOLUTE=`pwd`/library.files
+  cd $COQTOP/theories
+  echo $LIBDIRS
+  for rep in $LIBDIRS ; do
+    (cd $rep
+     echo $rep/intro.tex >> $ABSOLUTE
+     VOFILES=`ls -tr *.vo`
+     for file in $VOFILES ; do
+       VF=`basename $file \.vo`
+       if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then
+          $GALLINA $VF.v
+       fi
+       echo $rep/$VF.g >> $ABSOLUTE
+     done
+    )
+  done
+fi
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
new file mode 100755
index 00000000..ddbcd09f
--- /dev/null
+++ b/doc/stdlib/make-library-index
@@ -0,0 +1,35 @@
+#!/bin/sh
+
+# Instantiate links to library files in index template
+
+FILE=$1
+
+cp -f $FILE.template tmp
+echo -n Building file index-list.prehtml ...
+
+for i in ../theories/*; do
+    echo $i
+
+  d=`basename $i`
+  if [ "$d" != "Num" -a "$d" != "CVS" ]; then
+  for j in $i/*.v; do
+    b=`basename $j .v`
+    rm -f tmp2
+    grep -q theories/$d/$b.v tmp
+    a=$?
+    if [ $a = 0 ]; then
+      sed -e "s:theories/$d/$b.v:<a href=\"Coq.$d.$b.html\">$b</a>:g" tmp > tmp2
+      mv -f tmp2 tmp
+    else
+      echo Warning: theories/$d/$b.v is missing in the template file
+    fi
+  done
+  fi
+  rm -f tmp2
+  sed -e "s/#$d#//" tmp > tmp2
+  mv -f tmp2 tmp
+done
+a=`grep theories tmp`
+if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi
+mv tmp $FILE
+echo Done
author	Samuel Mimram <smimram@debian.org>	2006-04-28 14:59:16 +0000
committer	Samuel Mimram <smimram@debian.org>	2006-04-28 14:59:16 +0000
commit	3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
tree	ad89c6bb57ceee608fcba2bb3435b74e0f57919e /doc/stdlib
parent	018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)