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.
The source file is here (V8) .
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.