44

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use tactics to prove things like forall (n m : nat), n + n = m + m -> n = m.

Kaveh
  • 21,577
  • 8
  • 82
  • 183

4 Answers4

33

One place to start is the Coq reference manual (pdf). Chapter 4 describes the underlying logic of Coq, and ultimately everything is based on this. It's called the calculus of (co)inductive constructions, and many papers describe. Getting your hands on the Coq'Art book Interactive Theorem Proving and Program Development provides a more leisurely but not cheap introduction to Coq.

To learn about how tactics work, have a look at this earlier question: How do 'tactics' work in proof assistants?

To build up the required theory, you need to learn about Type Theory. Most closely related to the theory underlying a proof assistant is probably Per Martin-Löf's Intutionistic Type Theory notes (or book) or the book Programming in Martin-Löf Type Theory, which is really about writing and proving theorems in type theory. A programming language perspective on type theory can be obtained from Pierce's Types and Programming Languages. Girard et al's Proofs and Types, which also addresses the importance of the Curry-Howard Correspondence, is another excellent reference. Then you are probably well and truly ready to read Coquand and Huet's The Calculus of Constructions. Finally chase up some of the references in the back of the Coq manual.

There are other proof assistants, HOL, NuPRL, Mizar, Twelf, etc., and they have their theory too, so you can learn a lot too by reading in that direction.

Finally, for an overview of the history and future of proof assistants, check out the recent article by Herman Geuvers.

Archy Will He 何魏奇
  • 103
  • 5
Dave Clarke
  • 16,666
  • 3
  • 60
  • 106
  • 5
    Nice list. I'll add a reading order. Pierce's TAPL covers the background; most of the rest won't make sense until you get fluent with typing rules. Chapter 2 of ATTAPL introduces dependent types relatively gently. Then you can read chapter 4 of the Coq manual, which has the typing rules (you need to check the bibliography for some advanced stuff such as the exact rules for recursion). In parallel, the Coq'Art book has a more practical outlook. Bonus tip: Show Tree in coq. – Gilles 'SO- stop being evil' Apr 03 '11 at 13:34
  • 2
    I am someone in more or less the same position as the OP though a bit further along. After some experimenting, I finally found the order 1) Learn functional programming 2) read TAPL 3) Read about dependent types in ATTAPL to work better than other things. Glad to know I am on approximately the right path. – John Salvatier Apr 13 '11 at 19:08
  • 1
    I was here too, and got the Coq'Art book. It is absolutely perfect for understanding, they go into every tactic in detail and explain when and how to use it. The book also guides you quickly through every base rule in type theory, teaching you notation and how to use it in Coq. Loving this book. – Lance Jul 19 '15 at 16:39
14

As for typed lambda calculus, intuitionistic logic, various proof systems and Curry-Howard isomorphism, which are all parts of Coq mathematical background, I strongly recommend "Lectures on the Curry-Howard Isomorphism"(by P. Urzyczyn and M. Sørensen).

Marcin Kotowski
  • 2,806
  • 19
  • 25
6

Luo's book on the Extended Calculus of Constructions is also a good reference. ECC was quite influential in the design of Coq's type theory.

Dominic Mulligan
  • 837
  • 9
  • 15
4

The current Software Foundations book does explain all this later on: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html

So if you're following the book, just read on :)

Mario Galic
  • 103
  • 4
Catalin Hritcu
  • 141
  • 2