diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /doc/stdlib | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'doc/stdlib')
-rwxr-xr-x | doc/stdlib/Library.tex | 10 | ||||
-rw-r--r-- | doc/stdlib/index-list.html.template | 387 | ||||
-rwxr-xr-x | doc/stdlib/make-library-files | 2 | ||||
-rwxr-xr-x | doc/stdlib/make-library-index | 42 |
4 files changed, 278 insertions, 163 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 598943a4..f9764bea 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,7 +3,7 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage{coqdoc} +\usepackage{../../coqdoc} \input{../common/version} \input{../common/title} @@ -43,8 +43,10 @@ The standard library is composed of the following subdirectories: \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). + \item[Program] Tactics to deal with dependently-typed programs and + their proofs. + \item[Classes] Standard type class instances on relations and + Coq part of the setoid rewriting tactic. \end{description} @@ -59,4 +61,4 @@ you can access from the \Coq\ home page at \end{document} -% $Id: Library.tex 9245 2006-10-17 12:53:34Z notin $ +% $Id: Library.tex 11091 2008-06-10 18:24:52Z notin $ diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 81ab034b..5e95a692 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -3,10 +3,9 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> - <head> <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/> -<link rel="stylesheet" href="css/context.css" type="text/css"> +<link rel="stylesheet" href="css/context.css" type="text/css"/> <title>The Coq Standard Library</title> </head> @@ -41,6 +40,7 @@ through the <tt>Require Import</tt> command.</p> Classical logic and dependent equality </dt> <dd> + theories/Logic/SetIsType.v theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.v @@ -66,12 +66,29 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/ProofIrrelevance.v theories/Logic/ProofIrrelevanceFacts.v theories/Logic/ConstructiveEpsilon.v + theories/Logic/Description.v + theories/Logic/Epsilon.v + theories/Logic/IndefiniteDescription.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>Arith</b>: Basic Peano arithmetic </dt> <dd> + theories/Arith/Arith_base.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Plus.v @@ -86,7 +103,6 @@ through the <tt>Require Import</tt> command.</p> 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 @@ -107,7 +123,7 @@ through the <tt>Require Import</tt> command.</p> theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndec.v -. </dd> + </dd> <dt> <b>ZArith</b>: Binary integers @@ -131,14 +147,19 @@ through the <tt>Require Import</tt> command.</p> (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v theories/ZArith/Zsqrt.v + theories/ZArith/Zpow_def.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) + theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v theories/ZArith/Zbinary.v theories/ZArith/Znumtheory.v theories/ZArith/Int.v + theories/ZArith/ZOdiv_def.v + theories/ZArith/ZOdiv.v + theories/ZArith/Zpow_facts.v </dd> <dt> <b>QArith</b>: @@ -146,72 +167,114 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/QArith/QArith_base.v + theories/QArith/Qabs.v + theories/QArith/Qpower.v theories/QArith/Qreduction.v theories/QArith/Qring.v + theories/QArith/Qfield.v (theories/QArith/QArith.v) theories/QArith/Qreals.v theories/QArith/Qcanon.v + theories/QArith/Qround.v </dd> - - <dt> <b>Reals</b>: - Formalization of real numbers + + <dt> <b>Numbers</b>: + A modular axiomatic construction for numbers + </dt> + <dd> + theories/Numbers/NumPrelude.v + theories/Numbers/BigNumPrelude.v + theories/Numbers/NaryFunctions.v + </dd> + + <dd> +theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +theories/Numbers/Cyclic/Abstract/NZCyclic.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v +theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +theories/Numbers/Cyclic/Int31/Cyclic31.v +theories/Numbers/Cyclic/Int31/Int31.v +theories/Numbers/Cyclic/ZModulo/ZModulo.v + </dd> + + <dd> + theories/Numbers/Integer/Abstract/ZAdd.v +theories/Numbers/Integer/Abstract/ZAddOrder.v +theories/Numbers/Integer/Abstract/ZAxioms.v +theories/Numbers/Integer/Abstract/ZBase.v +theories/Numbers/Integer/Abstract/ZDomain.v +theories/Numbers/Integer/Abstract/ZLt.v +theories/Numbers/Integer/Abstract/ZMul.v +theories/Numbers/Integer/Abstract/ZMulOrder.v +theories/Numbers/Integer/BigZ/BigZ.v +theories/Numbers/Integer/BigZ/ZMake.v +theories/Numbers/Integer/Binary/ZBinary.v +theories/Numbers/Integer/NatPairs/ZNatPairs.v +theories/Numbers/Integer/SpecViaZ/ZSig.v +theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v + </dd> + + <dd> +theories/Numbers/NatInt/NZAdd.v +theories/Numbers/NatInt/NZAddOrder.v +theories/Numbers/NatInt/NZAxioms.v +theories/Numbers/NatInt/NZBase.v +theories/Numbers/NatInt/NZMul.v +theories/Numbers/NatInt/NZMulOrder.v +theories/Numbers/NatInt/NZOrder.v + </dd> + + <dd> +theories/Numbers/Natural/Abstract/NAdd.v +theories/Numbers/Natural/Abstract/NAddOrder.v +theories/Numbers/Natural/Abstract/NAxioms.v +theories/Numbers/Natural/Abstract/NBase.v +theories/Numbers/Natural/Abstract/NDefOps.v +theories/Numbers/Natural/Abstract/NIso.v +theories/Numbers/Natural/Abstract/NMul.v +theories/Numbers/Natural/Abstract/NMulOrder.v +theories/Numbers/Natural/Abstract/NOrder.v +theories/Numbers/Natural/Abstract/NStrongRec.v +theories/Numbers/Natural/Abstract/NSub.v +theories/Numbers/Natural/BigN/BigN.v +theories/Numbers/Natural/BigN/Nbasic.v +theories/Numbers/Natural/BigN/NMake.v +theories/Numbers/Natural/Binary/NBinary.v +theories/Numbers/Natural/Binary/NBinDefs.v +theories/Numbers/Natural/Peano/NPeano.v +theories/Numbers/Natural/SpecViaZ/NSig.v +theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v + </dd> + + <dd> + theories/Numbers/Rational/BigQ/BigQ.v + theories/Numbers/Rational/BigQ/Q0Make.v + theories/Numbers/Rational/BigQ/QbiMake.v + theories/Numbers/Rational/BigQ/QifMake.v + theories/Numbers/Rational/BigQ/QMake_base.v + theories/Numbers/Rational/BigQ/QpMake.v + theories/Numbers/Rational/BigQ/QvMake.v + theories/Numbers/Rational/SpecViaQ/QSig.v + </dd> + + <dt> <b>Relations</b>: + Relations (definitions and basic results) </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/LegacyRfield.v - theories/Reals/Rpow_def.v - (theories/Reals/Reals.v) + 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>Sets</b>: @@ -242,51 +305,26 @@ through the <tt>Require Import</tt> command.</p> theories/Sets/Uniset.v </dd> - <dt> <b>Relations</b>: - Relations (definitions and basic results) - </dt> + <dt> <b>Classes</b>: <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 + theories/Classes/Init.v + theories/Classes/RelationClasses.v + theories/Classes/Morphisms.v + theories/Classes/Morphisms_Prop.v + theories/Classes/Morphisms_Relations.v + theories/Classes/Equivalence.v + theories/Classes/EquivDec.v + theories/Classes/SetoidTactics.v + theories/Classes/SetoidClass.v + theories/Classes/SetoidDec.v + theories/Classes/SetoidAxioms.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>Setoids</b>: <dd> theories/Setoids/Setoid.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> @@ -296,12 +334,40 @@ through the <tt>Require Import</tt> command.</p> theories/Lists/MonoList.v theories/Lists/SetoidList.v theories/Lists/Streams.v + theories/Lists/StreamMemo.v theories/Lists/TheoryList.v theories/Lists/ListTactics.v </dd> + <dt> <b>Sorting</b>: + Axiomatizations of sorts + </dt> + <dd> + theories/Sorting/Heap.v + theories/Sorting/Permutation.v + theories/Sorting/Sorting.v + theories/Sorting/PermutEq.v + theories/Sorting/PermutSetoid.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>FSets</b>: - Modular implementation of finite sets/maps using lists + Modular implementation of finite sets/maps using lists or + efficient trees </dt> <dd> theories/FSets/OrderedType.v @@ -309,67 +375,110 @@ through the <tt>Require Import</tt> command.</p> theories/FSets/OrderedTypeEx.v theories/FSets/FSetInterface.v theories/FSets/FSetBridge.v + theories/FSets/FSetFacts.v + theories/FSets/FSetDecide.v theories/FSets/FSetProperties.v theories/FSets/FSetEqProperties.v theories/FSets/FSetList.v + theories/FSets/FSetWeakList.v (theories/FSets/FSets.v) - theories/FSets/FSetFacts.v theories/FSets/FSetAVL.v theories/FSets/FSetToFiniteSet.v - theories/FSets/FSetWeakProperties.v - theories/FSets/FSetWeakInterface.v - theories/FSets/FSetWeakFacts.v - theories/FSets/FSetWeakList.v - theories/FSets/FSetWeak.v theories/FSets/FMapInterface.v + theories/FSets/FMapWeakList.v theories/FSets/FMapList.v theories/FSets/FMapPositive.v - theories/FSets/FMapIntMap.v theories/FSets/FMapFacts.v (theories/FSets/FMaps.v) theories/FSets/FMapAVL.v - theories/FSets/FMapWeakInterface.v - theories/FSets/FMapWeakList.v - theories/FSets/FMapWeak.v - theories/FSets/FMapWeakFacts.v + theories/FSets/FSetFullAVL.v + theories/FSets/FMapFullAVL.v </dd> - <dt> <b>IntMap</b>: - An implementation of finite sets/maps as trees indexed by addresses - </dt> - <dd> - 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>Strings</b> +<!-- <dt> <b>Strings</b> Implementation of string as list of ascii characters </dt> <dd> theories/Strings/Ascii.v theories/Strings/String.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/Rpow_def.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/Rlogic.v + theories/Reals/LegacyRfield.v + (theories/Reals/Reals.v) </dd> - <dt> <b>Sorting</b>: - Axiomatizations of sorts + <dt> <b>Program</b>: + Support for dependently-typed programming. </dt> <dd> - theories/Sorting/Heap.v - theories/Sorting/Permutation.v - theories/Sorting/Sorting.v - theories/Sorting/PermutEq.v - theories/Sorting/PermutSetoid.v + theories/Program/Basics.v + theories/Program/Wf.v + theories/Program/Subset.v + theories/Program/Equality.v + theories/Program/Tactics.v + theories/Program/Utils.v + theories/Program/Syntax.v + theories/Program/Program.v + theories/Program/FunctionalExtensionality.v + theories/Program/Combinators.v </dd> </dl> diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index 91e3cc3f..add14a13 100755 --- a/doc/stdlib/make-library-files +++ b/doc/stdlib/make-library-files @@ -10,7 +10,7 @@ # 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" +LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes" rm -f library.files.ls.tmp (cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index ddbcd09f..04bcff91 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -7,27 +7,31 @@ FILE=$1 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -for i in ../theories/*; do - echo $i +LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" - 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 +for k in $LIBDIRS; do + i=theories/$k + 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/$k/$b.v tmp + a=$? + if [ $a = 0 ]; then + p=`echo $k | sed 's:/:.:g'` + sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + mv -f tmp2 tmp + else + echo Warning: theories/$k/$b.v is missing in the template file + fi + done fi - done - fi - rm -f tmp2 - sed -e "s/#$d#//" tmp > tmp2 - mv -f tmp2 tmp + 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 |