# Standard library of the future?

**URL:** <https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357>\
**Category:** Developing the Rocq Prover\
**Created:** [June 18, 2021, 8:20pm UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357 "2021-06-18T20:20:49Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![kindaro](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kindaro/32/146_2.png) [@kindaro](https://discourse.rocq-prover.org/u/kindaro)\
**Post date:** [June 18, 2021, 8:20pm UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/1 "2021-06-18T20:20:49Z")

</div>

## The problem.

I really want to do computer-assisted proofs. Actually I am looking forward to decades of computer assisted proof writing. But so far it has not been going well. One reason is that libraries are either not there or not accessible.

## Examples.

[This is the official reference for Mathematical Components, the Coq Mathematics standard.](https://math-comp.github.io/htmldoc_1_12_0/index.html) Yes, it is an alphabetical index of identifiers. Sounds great, right? _(Not really. A reference should have a structure — a tree of contents.)_ Suppose I am looking for [the Gauss’s lemma concerning polynomials](https://en.m.wikipedia.org/wiki/Gauss's_lemma_(polynomials)). Well, that would be on page _g_, right? So I am in luck!

> Gauss\_gcdl [lemma, in mathcomp.ssreflect.div]  
> Gauss\_gcdr [lemma, in mathcomp.ssreflect.div]  
> Gauss\_dvdl [lemma, in mathcomp.ssreflect.div]  
> Gauss\_dvdr [lemma, in mathcomp.ssreflect.div]  
> Gauss\_dvd [lemma, in mathcomp.ssreflect.div]  
> Gauss\_gcdzl [lemma, in mathcomp.algebra.intdiv]  
> Gauss\_gcdzr [lemma, in mathcomp.algebra.intdiv]  
> Gauss\_dvdzl [lemma, in mathcomp.algebra.intdiv]  
> Gauss\_dvdzr [lemma, in mathcomp.algebra.intdiv]  
> Gauss\_dvdz [lemma, in mathcomp.algebra.intdiv]

Oh… Well, Gauss has a lot of mathematics to his name. Maybe the one I need is one of these. But which?

How about [the Rational Root Theorem](https://en.m.wikipedia.org/wiki/Rational_root_theorem)? Unfortunately the word _«rational»_ does not appear anywhere on page _r_.

Maybe I should look elsewhere? [This module looks like it might be related.](https://github.com/math-comp/multinomials/blob/master/src/mpoly.v) Unfortunately the definitions herein do not appear in the index. The theorems are named like `nvar0_mpolyC_eq`, so it is hard to tell if the result I am looking for is there or not.

So:

1. There is no structured reference.
2. There are no comments to most definitions.
3. Naming is a disaster.

I do not mean to bash specifically this library. I mean, look at [the standard library that goes with the installation of Coq](https://coq.github.io/doc/v8.13/stdlib/).

> BinNatDef BinNat Nnat Ndigits Ndist Ndec Ndiv\_def Ngcd\_def Nsqrt\_def (NArith)

Oh… Well, at least sometimes it has readable names and comments.

## My explanation.

What is going on? Is the style of these works officially considered a good style for writing Coq? Or am I unlucky to stumble upon particularly thorny examples and to miss all the beautiful flowers?

I think this disaster is systematic and the reason for it is habit and the system of motivation that supports it.

- Software engineers are expected to maintain their work, so it must be made clear and accessible. I am a software engineer — I need proofs to help me and my team continuously deliver correct software.
- Research mathematicians are only expected to publish a result once and for a relatively local audience, so who cares if the devil himself would break a leg wading through their code. The code is an appendix № _n_ of an appendix № _m_. People that write the libraries mentioned above are research mathematicians.

## What next?

But, as I mentioned, I am looking forward to decades of computer assisted proof writing. And it looks like Coq will be the prime proof assistant in the foreseeable future. So I may as well re-write the works mentioned above if I feel like it.

- Should I?
- What should my plan be for getting a standard library that would make my efforts in proof writing more effective?
- How do I make sure it helps others too? How do I blaze a trail?
- Am I going to make more friends than enemies along the way?

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [June 19, 2021, 5:15pm UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/2 "2021-06-19T17:15:56Z")

</div>

Have a look at coq-platform, stdpp, stdlib2, all efforts for improving the stdlib in different ways.  
The coq opam packages also came out of this urge.

---

<div class="post-metadata">

**Author:** ![kindaro](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kindaro/32/146_2.png) [@kindaro](https://discourse.rocq-prover.org/u/kindaro)\
**Post date:** [June 22, 2021, 1:33am UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/3 "2021-06-22T01:33:45Z")

</div>

Thanks Bas. I only discovered `stdlib2`, and from it `stdpp`, after I opened this topic, when looking for a development of finite sets. I wish these libraries were mentioned more prominently on the official site of Coq. I have not yet looked at `coq-platform`.

My understanding is that `stdpp` is the more widely used and feature rich one, and `stdlib2` aims to be a more cleaner revision of the features provided by `stdlib`, is that right? I was glad to see `stdpp` actually has [a reference with a tree of contents](https://plv.mpi-sws.org/coqdoc/stdpp/). Encouraging! And finite sets do work!

However, it is my understanding that `stdpp` does not develop any mathematical theory to a length required for it to have anything like that lemma of Gauss I was looking for.

As for `mathcomp`, from [a long _(and not entirely pleasant)_ conversation elsewhere](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60false.3A.20bool.60.20.E2.86.92.20contradiction.20.E2.80.94.20how.3F) I found that it is purposefully written in such a way that makes it unfit for me. As was explained:

> math-comp is an amazing tool, and so far it has not been surpassed IMO, however it is optimized for one particular thing: ultra expert users writing a particular set of proofs in a particular style [for example, no automation]

So, I see a place for a library that would also develop the usual mathematical theories, even in the same way, but focused on being approachable and promoting automation.

---

<div class="post-metadata">

**Author:** ![mrhaandi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mrhaandi/32/379_2.png) [@mrhaandi](https://discourse.rocq-prover.org/u/mrhaandi)\
**Post date:** [June 22, 2021, 7:04am UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/4 "2021-06-22T07:04:54Z")

</div>

The existing, powerful `Search` command is very useful to discover lemmas in a large library. This approach is missing from the initial post and maybe could have considerably sped up lemma discovery.

---

<div class="post-metadata">

**Author:** ![kindaro](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kindaro/32/146_2.png) [@kindaro](https://discourse.rocq-prover.org/u/kindaro)\
**Post date:** [June 22, 2021, 9:54am UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/5 "2021-06-22T09:54:23Z")

</div>

I can `Search` for things when I know what type a definition I want might have. But how can I possibly know how, if at all, polynomials would be defined in an unfamiliar library? Surely `Search` is great when you need to do something about a goal you have before your eyes, but I do not find it to be a good tool for exploration. I do not know how `Search` would have helped me here.

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [June 22, 2021, 11:24am UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/6 "2021-06-22T11:24:03Z")

</div>

stdpp is more focused on CS applications/data structures.  
corn/math-classes are big libraries of mathematics that focus on the constructive and computational/numerical aspects.

People have different goals when they are developing mathematics, this is why some people believe that the package model (opam/platform) is more appropriate.

Your asking good questions, but these are discussions that have been taking place in the coq community for decades, so it not always easy to condense those discussions into a few words.  
Perhaps: mathematicians tend to be too optimistic about how coherent mathematics actually is.

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [July 4, 2021, 11:51pm UTC](https://discourse.rocq-prover.org/t/standard-library-of-the-future/1357/7 "2021-07-04T23:51:35Z")

</div>

Maybe we need a better [CoqdocJS](https://github.com/coq-community/coqdocjs) that integrates functionalities of [Hoogle](https://hoogle.haskell.org/).