A brief presentation of Coq

Some features of the Coq system are illustrated by the development of a certified program of insertion sort on lists of integers. It differs from the 2004 book by the use of the library RelationClasses.

The source file is here .

You should notice that this development uses many tactics which are defined in the rest of the book. This example aims to give a flavour of coq programming, and you should focus on the global structure more than on technical details.
Nevertheless, as for any example in this site, it is a good practice to replay it on your computer, and even try to modify it.

Errata

Page 6, section 1.5.1:
the last line of the section should contain "sorted(z::l)" instead of "sorted(n::l)".