Warning: Please note that this version of the notes is out of date.
Currently, the authoritative, up-to-date version is located in the master branch of the
repository on GitHub.
This repository serves as a log of my endeavour to learn to use and understand the Coq proof assistant. It may contain proofs, attempts at proofs, links to related resources (blogs, articles, papers, books), notes on logic, type theory, formal verification, theorem proving, automated reasoning, and much more.
I will try to only include things that seem useful, informative, interesting or cool, things that I forget, and tips and warnings regarding the subtleties of Coq. Therefore, if you want to learn Coq from scratch, I suggest you try one of the resources listed below.
I do not claim completeness, correctness, consistency or usefulness of any information contained herein.
Coq is an interactive theorem prover and proof assistant based on an intensional intuitionistic type theory. The underlying formalism is called Calculus of Constructions (CoC) which is a dependently-typed λ-calculus and an intuitionistic higher-order logic. Its core is written in OCaml.
Tactics
Standard Coq contains many tactics for working with the proof state, some of which may be confused easily. The documentation on tactics may be the most informative and thorough part of the Coq reference manual, so it's worth a read if you're looking for a way to make your proofs more concise. See the Tactics Index and Chapter 8: Tactics in the reference manual.
The Ssreflect libary (see below) contains a more sensible and consistent set of tactics. Although its syntax is very different from the Coq standard, don't let this discourage you.
B. C. Pierce et al.: Software Foundations – probably the best introduction into Coq and theorem proving available
A. Chlipala: Certified Programming with Dependent Types – an awesome book to read after Software Foundations; a bit more advanced, slightly different topics; puts forth the idea of using automation whenever possible
Numerous journals, conferences and workshops, for instance, the Journal of Automated Reasoning, POPL, and CoqPL. For tools, see also page on the Coq website.
Idris – another new and hip "general purpose" language with dependent types, support for theorem proving and tactics; kind of like Coq-flavoured Haskell
Dedukti – proof checker based on the λΠ-calculus; tools for translation from other proof assistants available
IKOS – "library designed to facilitate the development of sound static analyzers based on Abstract Interpretation"
Crab – "language agnostic engine to perform static analysis based on abstract interpretation"
Seahorn – "fully automated verification framework for LLVM-based languages"
rise4fun – a collection of numerous tools, i.a. for program and algorithm analysis and verification, by Microsoft Research, CMU and others that you can try right on the web page
Profound – "an experiment in subformula linking as an interaction method"
Oregon Programming Languages Summer School – videos of awesome lectures on type theory, provers, logic, etc.; earlier editions only have lecture notes and slides published
Danny Gratzer's learn-tt is a fantastic resource for those interested in type and category theory. He presents all the terrific tools, textbooks, and papers that deal with both of these in a sensible and logical way, which is a quality that my repository will never have.
I'll only list here resources which he doesn't mention and which I personally find interesting.
mortberg/cubicaltt – a Haskell implementation of the type theory presented in this paper
Copyright
Written in 2015–2019 by Matěj Grabovský <matej at mgrabovsky dot net>
To the extent possible under law, the author has dedicated all copyright and related and neighboring rights to this software to the public domain worldwide. This software is distributed without any warranty.
