# 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.
## Errata

Page 7, in the paragraph
if l is empty, then n::nil
if l has the form p::l' then
- if n <= p then n::p::l'
- if p < n then p::(aux n l).

Please read:
if l is empty, then n::nil
if l has the form p::l' then
- if n <= p then n::p::l'
- if p < n then p::(aux n l').

Going home

Pierre Castéran