81
$\begingroup$

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.

Improve this question
$\endgroup$
21
  • 14
    $\begingroup$ Apologies for self-advertisment. To get you off the ground there are my Coq video tutorials at math.andrej.com/2011/02/22/… In general, I am afraid, it will be hard to get what you're looking for. As a pedagogical project I set up a formalization of reals at github.com/andrejbauer/dedekind-reals, that will show you how to "unorganize" yourself. Those files purposely do not contain anything fancy, and if you play through some of the less scary proofs you might learn a few tricks. $\endgroup$
    – Andrej Bauer
    Jan 28, 2014 at 6:15
  • 15
    $\begingroup$ I wonder what a non-mathematician would make of the title of this question... $\endgroup$
    – shane.orourke
    Jan 28, 2014 at 10:22
  • 5
    $\begingroup$ @WlodzimierzHolsztynski I would assume it's pronounced just like `cock'. $\endgroup$
    – shane.orourke
    Jan 28, 2014 at 10:52
  • 15
    $\begingroup$ In France the non-mathematician would assume that after a hard day's work the mathematician wishes for a tasty coq au vin. $\endgroup$
    – Andrej Bauer
    Jan 28, 2014 at 13:04
  • 2
    $\begingroup$ That is not a book but still a good and recent introduction to Coq and SSReflect : www-sop.inria.fr/manifestations/MapSpringSchool It is the website of a spring school on Coq, it contains slides, exercises and solutions. $\endgroup$
    – Lierre
    Jan 28, 2014 at 14:28

4 Answers 4

Reset to default
25
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ very instructive. thank you for putting this out there, it fills more than a few gaps. $\endgroup$
    – nicolas
    Dec 28, 2014 at 14:59
15
$\begingroup$

I might suggest the book devised for the library on GitHub, Mathematical Components (the author of the question is acknowledged within actually). It makes no assumptions on the reader in terms of programming experience. There are of course I imagine an abundance of publications that developed these tools, so I was ecstatic myself to find no specialized background intended for the book's readers. It is written in English and is geared toward the project to formalize mathematics on GitHub, and you'll find in the introduction that in more ways than typical treatments of Coq that are for beginners a bent which is toward mathematical progress being achieved with Coq. Would love to hear reviews for the text in the comments to this answer. I myself just started.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ This looks very interesting and promising. $\endgroup$
    – Dima Pasechnik
    Jul 25, 2017 at 8:54
  • 1
    $\begingroup$ +1. I should have posted this one myself, as I've read the first 3-4 chapters of the book half a year ago! (That said, it is still an uphill battle; the book is much much better than what other sources I have seen before, but this is still one of the steepest learning curves I've seen in a programming language.) $\endgroup$
    – darij grinberg
    Jul 25, 2017 at 20:51
  • $\begingroup$ Note that some instances of code have notes on the side. The authors are refining it since some mistakes or shortcomings are identified in the draft. No doubt due to the complexity of this machinery! Note that the other suggestion, by Chlipala, is cited here so I imagine they had in mind making this a mathematics-oriented upgrade, but that's just speculation. $\endgroup$
    – user48801
    Jul 26, 2017 at 3:52
7
$\begingroup$

This online book by Adam Chlipala hasn't been mentioned:

Certified Programming with Dependent Types

The reason I suggest it is because of this claim by the author in the introduction:

"Most of the insights for Coq are barely even disseminated among the experts, let alone set down in a tutorial form. I hope to use this book to go a long way towards remedying that."

So not a book aimed at mathematicians but hopefully helpful for getting started nonetheless.

Improve this answer
$\endgroup$
1
  • 7
    $\begingroup$ It is way too CS-oriented; it uses examples that don't make much sense for someone not interested​ or not knowledgeable enough in programming languages theory, IMHO. $\endgroup$
    – Dima Pasechnik
    Jul 25, 2017 at 8:57
7
$\begingroup$

A relatively new project, Lean, has created a lot of activity lately, see Lean and Mathlib with its lots of learning material, driven in part by successful attempts by Kevin Buzzard to teach Lean to maths undergraduates.

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ You might say that it created a lot of Buzz...ard? No, there's a better joke in there. But I leave it as an exercise for the reader. $\endgroup$
    – Asaf Karagila ♦
    Feb 28, 2021 at 11:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.