ReflectionOnStandardLibrary
See also StandardLibrary for older discussion (should these pages be merged?)
- Lack of overall design consistency due to not-always-coordinated multi-author development through different times of the history of Coq.
- Lack of human resources for a correct maintenance of many components of the library:
- many users propose to complete and extend some libraries but no availability from the development team to evaluate these additions and to check these extensions do not add design inconsistencies to the existing setting [Comment by HH: tentative guidelines are available here with the objective of making easier the work of evaluation and integration of user's contributions].
- many users developed libraries that could be considered of general purpose (UserContributions) but, again, the Coq developers do not have the time to referee and validate these libraries.
Possible solution: A more modular approach of libraries with a small core of standard library maintained by the Coq development team and a second distinct distributed archive of libraries with a coordinated maintenance so as, not to necessarily guarantee a strict overall consistent design, but to at least guarantee correct compilation dependencies (see the MathWiki project). The responsibility of the maintenance of the consistency of each individual component of this second archive would be distributed.
From the StandardLibrary page:
- Easy-to-contribute library is much better. Although we should keep library clean and strict we should allow user to contribute in even small part. Nobody will write thousands lines of code before contribution. If every ten lines can be submitted, then we'll have much more active and wide community. [Comment by HH: how to ensure design consistency? Official guidelines to follow? Who takes the responsability of the integration? Set up of a user-contributor group?]
- There should be clean list of common problems defined in both existing and to-be-written code. One should be able to easily find the problem and solve it. (See ProjectIdeas?)
- Compatibility issues hinder or at least complicate the improvement of some libraries, e.g.:
- definitions or lemmas got inconsistent names, e.g.:
-
_symm
vs_sym
,le_n
vsle_refl
, ...), -
plus
/mult
instead ofplus
/times
oradd
/mult
oradd
/mul
, - very basic lemmas such as
n = pred (S n)
were stated in an unnatural way (this historically was due to the use of elim for simulating rewriting before rewrite was implemented),
-
- bound variables sometimes got inconsistent names in the same library (e.g. lemmas on nat generally use n, m, p, q in this order, but sometimes, it is a,b or x, y or the differently ordered m, n),
- hints database cannot be improved without breaking auto in general.
- bad definition choices were sometimes made (e.g.
Zplus
of numbers of opposite signs which uselessly computes twice the difference, or the questioned design of <=, <, >= and >), - lemmas not always stated on their optimal generality (useless or arbitrarily weak side-conditions).
- definitions or lemmas got inconsistent names, e.g.:
- How to address the compatibility issues?
- Completely forget about too inconsistently built libraries? But they will still be needed anyway. And with what to replace them?
- Use mechanisms as in the V7 to V8 translator?
- Notations to provide only-parsing compatibility aliases to newly consistently-named lemmas?
- ML support for on the fly renaming of binders?
- Eventually arrive at a V9 generation and use a translator?
- Combine the cleaner parts with parts clearly flagged as obsolete?
- Dependency of the technical design of the libraries over the support (or absence of support!) of Coq for some features, e.g.:
- lack of support for freely reasoning with less-or-equal or greater-or-equal as one would do in a mathematical text: either one is a notation for the other and then the user cannot choose which one he wants to read, or there are two distinct definitions but then there are often not converted one to the other by Coq,
- lack of support for freely switching between a computational representation of decidable properties (as order in
ZArith
is defined) and a propositional representation of it (as order inArith
is defined), - automatic introduction of names and hypotheses in the context?
Coqdoc is a rather nice tool for documentation but there is a need for metadatas liable to ease the formal treatment of informations like title, author, table of contents, ...
- Naming policy:
-
_n_0
style vs_0_r
style? - Heterogenous pair
plus
/mult
(with adopted solution being the pairadd
/mul
)?
-
- Design choice for less vs greater:
- Have explicit constants for > and >= (better for displaying things as the user did but requires better support for such "notational" definitions)?
- Have only < and <= what is easier to manage and mathematically "cleaner" to think about?
- Notation policy:
- Adopt the nice
.+1
notation? - Use "_ = _ ?", "_ <= _ ?" for the computational operations?
- Adopt the nice
- What design choices for orders and decidable predicates?
- Design choice for decidable operations:
- Decidability to
bool
or decidability tosumbool
(but then requires better support for rewriting modulo proof-irrelevance)?
- Decidability to
- Modularity:
- Proceed further with the
Numbers
modular approach?
- Proceed further with the
- Organisation:
- One large file vs small files (as it is now)?
- What to put in
Init
? Just the operations or also the basic lemmas? - Make all non basic lemmas derived from
Numbers
?
- How to deal with partial functions: by returning a default element, by returning an option type, by guarding the definition with a precondition?
Coq provides a single file with a few results (with comments in French) in the Bool library. The CoLoR contribution provides much more.
- Add a function to interpret C-style strings (using for escaping).
- Add a primitive function
print : string -> unit
(or: forall A, string -> A -> A
natively interpreted at evaluation time as a side-effect on the standard output.
There should be a module for extensional equality for functions (see the axiom of functional extensionality declared in Coq.Program.FunctionalExtensionality
).
Is this worth to be a distinct library?
- The
Coq.Sets.Relations_
* modules duplicate the theory of relations provided byCoq.Relations.Relations
, with different theorems following from each. - Now that nested directories are being supported for theories/Numbers, the
Wellfounded
directory should probably be moved underRelations
for clarity, as it was in Coq 6.x.
Coq sparsely provides definitions of algebraic structures but to which extend is this usable as a standard library? Many approaches to algebra exist (see the various Algebra contributions in the user contribution server of Coq, including C-CoRN).
Libraries on these topics exist:
- Floating point numbers (IEEE754, fp2)
- Constructive real analysis (computing and mathematical aspects, see e.g. ExactRealArithmetic, CoinductiveReals, CoRN, interval arithmetic, ...)
- Finite sets (either InductiveFiniteTypes or FixpointFiniteTypes would be reasonable candidates for inclusion in the standard library, there is also a library by Jean-François Monin).
What about the licence issues?
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.