Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
31 lines (23 sloc) 905 Bytes
A Coq tutorial
--------------
Author: a semi-competent Coq user
Audience: people who invented all the things that I am going to talk about.
Resources:
* Coq web site: http://coq.inria.fr/
* these lecture files: http://andrej.com/coq/
* a cheat sheet: http://andrej.com/coq/cheatsheet.pdf
* video tutorials: http://www.youtube.com/view_play_list?p=DD40A96C2ED54E99
1. Coq is a proof assistant based on type theory (actually, Calculus
of Constructions + Inductive and Coinductive reasoning).
2. Things this tutorial does _not_ cover:
* how to install Coq
* how to use rewriting and hints
* how to define tactics
* setoids
* type universes
3. Outline:
* propositional reasoning: peirce.v
* first-order reasoning: frobenius.v
* inductive definitions: trees.v
* equality: equality.v
* how to read a more involved Coq file: univalence.v