aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
Commit message (Collapse)AuthorAge
* Add empty compat file for Coq 8.8Gravatar Jason Gross2018-03-07
| | | | This closes #6598
* Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
|
* Doc: add Decimal-related files to index-list.html.templateGravatar Jason Gross2018-02-20
|
* Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
|
* Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
|
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
|
* Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
| | | | Also integrating suggestions from Théo.
* Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
| | | | | | | | | | choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo).
* Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | | | We also add a Coq86.v compat file.
* Fix build of documentation (broken for four months).Gravatar Guillaume Melquiond2016-06-03
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * MMaps: remove it from final 8.5 release, since this new library isn't mature ↵Gravatar Pierre Letouzey2016-01-13
| | | | | | | | | | | | | | | | enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
| |
* | Adding an amazing property of Prop.Gravatar Hugo Herbelin2015-11-07
|/
* Mark the Coq.Compat files for documentation. (Fix bug #4353)Gravatar Guillaume Melquiond2015-10-02
|
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* Fix compilation of documentation broken by the addition of MMapAVL.Gravatar Guillaume Melquiond2015-04-02
|
* Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)Gravatar Guillaume Melquiond2015-03-21
|
* doc/stdlib: fix the xhtml validity of the index-list templateGravatar Pierre Letouzey2014-12-09
|
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵Gravatar notin2014-12-09
| | | | | | documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
|
* Added a (constructive) proof of Weak Konig's lemma for decidable trees.Gravatar Hugo Herbelin2014-07-15
| | | | | Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem after all.
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The earlier proof-of-concept file NPeano (which instantiates the "Numbers" framework for nat) becomes now the entry point in the Arith lib, and gets renamed PeanoNat. It still provides an inner module "Nat" which sums up everything about type nat (functions, predicates and properties of them). This inner module Nat is usable as soon as you Require Import Arith, or just Arith_base, or simply PeanoNat. - Definitions of operations over type nat are now grouped in a new file Init/Nat.v. This file is meant to be used without "Import", hence providing for instance Nat.add or Nat.sqrt as soon as coqtop starts (but no proofs about them). - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult) are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul where here Nat is Init/Nat.v). - This Coq.Init.Nat module (with only pure definitions) is Include'd in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat sometimes instead of just Nat (for instance when doing "Print plus"). Normally it should be ok to just ignore these "Init" since Init.Nat is included in the full PeanoNat.Nat. I'm investigating if it's possible to get rid of these "Init" prefixes. - Concerning predicates, orders le and lt are still defined in Init/Peano.v, with their notations "<=" and "<". Properties in PeanoNat.Nat directly refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le", we cannot yet include an Inductive to implement a Parameter), but these aliased predicates won't probably be very convenient to use. - Technical remark: I've split the previous property functor NProp in two parts (NBasicProp and NExtraProp), it helps a lot for building PeanoNat.Nat incrementally. Roughly speaking, we have the following schema: Module Nat. Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *) ... (** proofs of specifications for basic ops such as + * - *) Include NBasicProp. (** generic properties of these basic ops *) ... (** proofs of specifications for advanced ops (pow sqrt log2...) that may rely on proofs for + * - *) Include NExtraProp. (** all remaining properties *) End Nat. - All other files in directory Arith are now taking advantage of PeanoNat : they are now filled with compatibility notations (when earlier lemmas have exact counterpart in the Nat module) or lemmas with one-line proofs based on the Nat module. All hints for database "arith" remain declared in these old-style file (such as Plus.v, Lt.v, etc). All the old-style files are still Require'd (or not) by Arith.v, just as before. - Compatibility should be almost complete. For instance in the stdlib, the only adaptations were due to .ml code referring to some Coq constant name such as Coq.Init.Peano.pred, which doesn't live well with the new compatibility notations.
* Avoid scanning .coq-native directories when building the library index.Gravatar Guillaume Melquiond2014-06-26
|
* Fix documentation.Gravatar Guillaume Melquiond2014-06-26
|
* - Fix index-list to show computational relations for rewriting files.Gravatar Matthieu Sozeau2014-05-06
| | | | | | | | | - Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower. Conflicts: kernel/constr.ml kernel/univ.ml proofs/proof_global.ml
* fixup complement FinGravatar Pierre Boutillier2014-02-24
|
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix failure to compile doc/stdlib/Library.tex.Gravatar gmelquio2012-09-15
| | | | | | | | | | | | | | | | Coqdoc converts the utf8 symbol lambda (that appears in Utf8_core.v) to itself when outputting utf8. Since Library.tex uses utf8x as the input encoding, it gets translated to \textlambda. This command is defined by both the LGR font encoding and the tipa package, and only by them. So the build fails. There are several solutions: 1. \usepackage[mathletters]{ucs} 2. \usepackage[T1,LGR]{fontenc} 3. \usepackage{tipa} 4. modify coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove a script unused since 2006 (cf commit r8626)Gravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector equalities first stuffGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
| | | | | | | | | | | | After discovering a rewrite in Ergo that takes a loooong time due to a bad interaction with the instances of Permutation and PermutationA : - PermutationA is now in a separate file SetoidPermutation - File Permutation.v isn't Require'd by SetoidList anymore nor MergeSort.v, just the definitions in Sorted.v - Attempt to put a priority on these instances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
| | | | | | | | | One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
* make sure that documentation compilation works after adding files forGravatar bertot2012-06-12
| | | | | | arc tangent and computations of PI approximations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15436 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
| | | | | | | | | | | | | | | | | | | Initial contribution by Andrew Appel, many ulterior modifications by myself. Interest: red-black trees maintain logarithmic depths as AVL, but they do not rely on integer height annotations as AVL, allowing interesting performance when computing in Coq or after standard extraction. More on this topic in the article by A. Appel. The common parts of MSetAVL and MSetRBT are shared in a new file MSetGenTree which include the definition of tree and functions such as mem fold elements compare subset. Note that the height of AVL trees is now the first arg of the Node constructor instead of the last one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved synchronisation of stdlib index page with current library state.Gravatar herbelin2012-02-01
| | | | | | | | | | - Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
* index-list.html.template: add missing filesGravatar pboutill2012-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc/stdlib: Update the list of ZArith filesGravatar letouzey2011-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
* update of the file list in doc/stdlibGravatar letouzey2011-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore documentation of library String which was removed in 2007 (r10049)Gravatar herbelin2011-03-05
| | | | | | | probably inadvertantly since it is not reported in the commit log. (Thanks to Cédric who noticed it.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove obsolete TheoryListGravatar glondu2011-02-10
| | | | | | | | This library is no longer used anywhere, and its contents is very... let's say historical... More seriously, many (and presumably the most useful) stuff that used to be there are in List, now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
| | | | | | | | | | | | | | | | | | | | | | | See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (floor convention). We follow Haskell naming convention: quot and rem are for Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf. the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom (a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷ for quot, and infix rem for rem (which is actually remainder in full). This way, both conventions can be used at the same time. Definitions (and proofs of specifications) for div mod quot rem are migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With this new organisation, no need for functor application in Zdiv and Zquot. On the abstract side, ZAxiomsSig now provides div mod quot rem. Zproperties now contains properties of them. In NZDiv, we stop splitting specifications in Common vs. Specific parts. Instead, the NZ specification is be extended later, even if this leads to a useless mod_bound_pos, subsumed by more precise axioms. A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff). A few proofs in Nnat, Znat, Zabs are reworked (no more dependency to Zmin, Zmax). A lcm (least common multiple) is derived abstractly from gcd and division (and hence available for nat N BigN Z BigZ :-). In these new files NLcm and ZLcm, we also provide some combined properties of div mod quot rem gcd. We also provide a new file Zeuclid implementing a third division convention, where the remainder is always positive. This file instanciate the abstract one ZDivEucl. Operation names are ZEuclid.div and ZEuclid.modulo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
| | | | | | | | | | | | | | | | | | | - For nat, we create a brand-new gcd function, structural in the sense of Coq, even if it's Euclid algorithm. Cool... - We re-organize the Zgcd that was in Znumtheory, create out of it files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised in order to be much simpler (no omega, no advanced lemmas of Znumtheory, etc). - Abstract Properties NZGcd / ZGcd / NGcd could still be completed, for the moment they contain up to Gauss thm. We could add stuff about (relative) primality, relationship between gcd and div,mod, or stuff about parity, etc etc. - Znumtheory remains as it was, apart for Zgcd and correctness proofs gone elsewhere. We could later take advantage of ZGcd in it. Someday, we'll have to switch from the current Zdivide inductive, to Zdivide' via exists. To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
| | | | | | | | | | Btw, we finally declare the original Zpower as the power on Z. We should switch to a more efficient one someday, but in the meantime BigN is proved with respect to the old one. TODO: reform Zlogarithm with respect to Zlog_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
| | | | | | | Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
| | | | | | | | | | Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 03:55:37 +0000