1. Coq development example: proof of correctness of a simple algorithm

The proof of correctness of a simple functional program allows us to present some essential aspects of the Coq software: mathematical statements and formal specification of programs, tools for interactive proof, etc. The proposed example consists of the definition of a sorting function on lists, accompanied by a formal proof of its correctness. The proposed example consists of the definition of a sorting function on lists, accompanied by a formal proof of its correctness.

• Typographical conventions

  We adopt the following conventions so that the reader can easily recognize which text a user should submit to Coq and what the system's responses are.

  • The text submitted to Coq is written in light blue inserts.

  • Coq's answers are presented in...