Standard library of the future?

Developing the Coq system
1

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. 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. 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? Unfortunately the word «rational» does not appear anywhere on page r.

Maybe I should look elsewhere? This module looks like it might be related. 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.

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?
2

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.

3

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. 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 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.

4

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.

5

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.

1 Like
6

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.

7

Maybe we need a better CoqdocJS that integrates functionalities of Hoogle.

4 Likes