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.
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.
- There is no structured reference.
- There are no comments to most definitions.
- 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.
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.
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?