Sorry for a possibly off-topic question — there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar with.
I'm trying to obtain a working knowledge of the Coq programming language sufficient to be able to encode and (have it) verify constructive proofs in combinatorics and abstract algebra. The proofs, or at least a portion of them high enough to make me happy, are not really probing the boundaries of constructive mathematics; they require no univalence, no coinduction, and probably not even the full strength of inductive types other than $\mathbb N$ (think Peano arithmetic).
Obviously my first idea was to scour the internet for tutorials, but I found the kind of introduction that I want to be surprisingly scarce if not unavailable. So I'm wondering if someone knows such a source or one is currently being written (if so, how can one contribute?). Here is an outline of what I am looking for:
-
The focus should be on using Coq for verifying proofs in constructive mathematics, or in even more conservative subsets of it. It should not be on playing around with additional axioms (univalence, classical logic) or other systems (temporal logic etc.); nor should it be on practical software verification. It also shouldn't be a logics textbook with Coq used as illustration for the concepts. I'm abstractly interested in each of the things just mentioned, but what I really am looking for is a tutorial written for mathematicians in general rather than for logicians or HoTTists.
-
It should provide hands-on examples of proofs which aren't totally toylike or artificial. (I imagine things like "the conjugate of the conjugate of a partition is the old partition" or "if you sort each row of a matrix in increasing order and then do the same with each columns, then the rows are still increasing" or "$-1$ is a quadratic residue modulo the odd prime $p$ iff $p \equiv 1 \mod 4$".)
-
Ideally it should give some guidance on how to set up a Coq project (i. e., more than one .v file) and how to write literate Coq/TeX.
-
The text should provide the reader with a survival kit of syntax and basic tactics as early on as possible that theoretically allows formalizing any constructive proof in elementary combinatorics and number theory with enough patience. It should then go on with more advanced tactics that make this less of a pain, possibly even those from ssreflect (if that package is sufficiently stable).
The texts I'm currently trying to follow are Coq'Art and Software Foundations, but it seems they don't really fit the above description very much (and the only English version of Coq'Art is from 2004, which isn't very recent in computer science reckoning).
EDIT: Slightly off-topic, I'm also wondering what it would take to release Coq bundled with its most important user-made contributions like ssreflect, making the learning curve at least a little bit less steep by removing the PITA of compiling an ocaml ecosystem from source…
EDIT 2: Florent Hivert's Coq-Combi project seems to be the thing I was trying to build, and I suspect that reading its sources will be a good step towards learning Coq at least for me. On the other hand, Pierre-Yves Strub offers a bundle with Coq and SSReflect for Windows, which solves another problem I was having (the caveat being that the versions are not the newest). It looks like Coq is becoming usable 🙂
EDIT3: I feel that, with the progress done by now (particularly by Florent Hivert and others on Coq-Combi), I could learn Coq and get sufficiently experienced in it within half a year of not having to worry about publications, teaching and pretending to keep track of current developments. I am wondering if this is mainly me, or everyone in combinatorics is a half-year away from being able to teach their work to their computer. Meanwhile, I would like to share a talk by Neil Strickland I have just discovered, which is a far better rant about the current state of affairs than I could ever write.
Best Answer
My attempt to do something like this for Agda is here: http://neil-strickland.staff.shef.ac.uk/formal/. I would also like to see a Coq equivalent (also Isabelle, Mizar etc) but I do not currently have the knowledge to write one myself.