81

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.

darij grinberg
  • 33,095
  • My spidey sense tells me that you'll find it either a) in the references (formal and informal) to the HoTT book or b) not at all – Steve Huntsman Jan 28 '14 at 04:22
  • 1
    I presume you aware of the coq-club list? And there is https://groups.google.com/forum/#!forum/hott-amateurs as well as https://groups.google.com/forum/#!forum/homotopytypetheory – David Roberts Jan 28 '14 at 05:42
  • 14
    Apologies for self-advertisment. To get you off the ground there are my Coq video tutorials at http://math.andrej.com/2011/02/22/video-tutorials-for-the-coq-proof-assistant/ 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 https://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. – Andrej Bauer Jan 28 '14 at 06:15
  • 15
    I wonder what a non-mathematician would make of the title of this question... – shane.orourke Jan 28 '14 at 10:22
  • How do you pronounce "Coq"? – Włodzimierz Holsztyński Jan 28 '14 at 10:26
  • 5
    @WlodzimierzHolsztynski I would assume it's pronounced just like `cock'. – shane.orourke Jan 28 '14 at 10:52
  • 15
    In France the non-mathematician would assume that after a hard day's work the mathematician wishes for a tasty coq au vin. – Andrej Bauer Jan 28 '14 at 13:04
  • @SteveHuntsman: This is something I thought first, but it seems to me now that HoTT really has a rather orthogonal objective to what I want (vanilla constructivism, in as far as such a thing exists, and practice rather than theory, in as far as mathematics can be practical). – darij grinberg Jan 28 '14 at 13:08
  • 1
    @AndrejBauer: This is interesting! Youtube wasn't on my list of places I was searching for tutorials. (That said, a PDF transcript would still be very nice -- it is much easier to switch between CoqIDE and a PDF window than to switch between CoqIDE and Youtube and play/pause the video all the time). – darij grinberg Jan 28 '14 at 13:10
  • 2
    That is not a book but still a good and recent introduction to Coq and SSReflect : http://www-sop.inria.fr/manifestations/MapSpringSchool/ It is the website of a spring school on Coq, it contains slides, exercises and solutions. – Lierre Jan 28 '14 at 14:28
  • Nice, thank you -- I haven't seen any kind of ssreflect tutorials so far. – darij grinberg Jan 28 '14 at 15:05
  • Ouch. Am I seeing it right that ssreflect can only be used if Coq has been compiled from source? – darij grinberg Jan 28 '14 at 15:15
  • @darijgrinberg: About a year ago I tried to install ssreflect and could not get anywhere, but today I saw this page, which seems promising: http://mhtsai208.blogspot.co.uk/2010/10/install-coq-and-ssreflect-in-cygwin.html I haven't tried it yet, though. – Neil Strickland Jan 28 '14 at 15:20
  • Thanks, but will this allow me to use CoqIDE in Windows? I've been trying to install it on a virtualized Ubuntu so far, but the dependencies don't play well... – darij grinberg Jan 28 '14 at 16:01
  • 1
    "I'm abstractly interested in [...]". LoL, only a mathematician could have used that adverb in a positive sense :) – Qfwfq Jan 28 '14 at 16:16
  • 1
    You should start with plain Coq. – Andrej Bauer Jan 28 '14 at 17:25
  • How do you start? Do you install Coq on your computer? How? (On MacBook Pro?). What computer environment do you need? – Włodzimierz Holsztyński Jan 05 '15 at 09:34
  • @WłodzimierzHolsztyński: If you have MacPorts, a sudo port install coq is all you need. If you're an Emacs user, you might also want to do sudo port install ProofGeneral, though the version there is a bit old, and I ended up downloading and installing the most recent ProofGeneral source. – Mark Dickinson Jul 08 '15 at 18:24
  • @MarkDickinson -- thank you. Thus does "sudo port" is a special port in Mac? I'll have to read this whole thread anew. – Włodzimierz Holsztyński Jul 09 '15 at 09:39
  • Have a Coq and a smile... – Todd Trimble Oct 26 '16 at 02:39
  • by the way, there are 3 volumes there now (since Sept 2017?): https://softwarefoundations.cis.upenn.edu/ – Dima Pasechnik Dec 09 '17 at 13:55

4 Answers4

25

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.

Neil Strickland
  • 55,003
15

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.

user48801
  • 311
  • 2
    This looks very interesting and promising. – Dima Pasechnik Jul 25 '17 at 08:54
  • 1
    +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.) – darij grinberg Jul 25 '17 at 20:51
  • 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. – user48801 Jul 26 '17 at 03:52
7

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.

James Smith
  • 505
  • 7
    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. – Dima Pasechnik Jul 25 '17 at 08:57
7

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.

Dima Pasechnik
  • 13,634
  • 2
    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. – Asaf Karagila Feb 28 '21 at 11:30