If I was courageous enough, I would finish packaging these proofs and
make sure they are distributed in the user's contributions of the Coq system,
but some of them really are only small examples.
- Tactics to prove that a multi-variate polynomial is positive
inside a box given by rational constants. The following file gives a few illustrating examples.
Proving the convergence of a sequence based
on algebraic-geometric means to PI. This example relies on
library developed by colleagues in Saclay. It contains
examples of improper integrals, properties of uniformly convergent
sequences of functions, arcsinh, variable changes in integrals,
etc. The latest version is compatible
with version 2 of coquelicot. The tar archive also contains files to really compute one million decimals
of PI, together with the proof of correctness (tested with coq-8.4pl6 and
This little file shows how to solve
a problem of quickly finding approximants for functions only know
through a few properties, like sqrt
Computing close approximations
of Pi These examples rely on an alternated series provided in
the standard library (only in the trunk version for now -- June
A proof of a theorem by Mertens about the product
of infinite sums . In general, it is not guaranteed that such a
product converges if each of the factors does. But if one of the
factors converges absolutely, then the product does. This theorem
is a useful lemma to prove trigonometric formulas.
A few proofs of unicity of proofs. In
particular, there is a proof of unicity of proofs of "n <= m" for
the standard Coq notion of comparison. I
use them as examples for my own training.
- An algorithm to compute
determinants of matrices and its proof with respect to a complete
theory of matrices, where determinants and their properties have
already been proved. The algorithm description relies marginally
on ssreflect syntax and The verification is done using the
library and relies marginally on its data structures (it relies on
the datatype seq instead of list).
- Canonical structures for
reification. This is a very small example showing how canonical
structures can help solve the reification problem for proofs by reflection.
This example runs only in versions of Coq that are more recent than
Coq-8.2-1. It is inspired from more ambitious code presented in the ssreflect, but this specific code can run in Coq without extension.
very short proof that the square root of 2 is not
rational. The size of the formalized proof is what matters here. This
proof is actually inspired by the representation of rational numbers
used in this work with Milad Niqui, which is in the
user contributions to Coq.
Proof of safety for Peterson's Mutual exclusion algorithm. this study
takes the point of view of programming language semantics, with a small
concurrent programming language defined by simply adding a "parallel" operator
to an imperative language, the semantics is expressed using a small-step
structural operational semantics. The mutual exclusion property is expressed
by defining predicates on parallel programs, which indentify syntactically
when each branch is inside its critical section. The statement is that
not both parallel programs can be in their critical section at the same time.
The proof is parametric in the code inside and outside the crtical section
and in the variables used for the algorithm. A future study would be to explore the nesting of solutions to accomodate more than two concurrent programs.
- Proof of strong normalization for simply typed combinatory logic. This proof was inspired
by Randy Pollack's proof of weak normalization for simply typed combinatory
logic. Of course, strong normalization is slightly more difficult. I
mostly relied on the proof plan given by Girard, Lafont, and Taylor's
types, transposing it from lambda-calculus (with pairs and projectors)
to combinatory logic. This compressed tar archive also contains Randy
- algorithms to compute integer square, cubic and nth roots.
and, of course, their proof of correctness.
A reflexive tactic to prove inclusions of lists. This was developed
as a side-product for the concert project. The documentation of the tactic
is in the comments.
A co-inductive implementation of exact real arithmetics for the interval
[0,1] , containing addition, representation of rational numbers, affine
combinations of real numbers with rational coefficients, series, and
multiplication. In particular, the fractional part of e is described as the
limit of the infinite sum of inverse of factorials and can be computed inside
Coq because it only relies on functions that are structural recursive or
- Filters in co-recursion
data associated to the paper
Filters on Co-Inductive streams: an application to Eratosthenes'
Experiments with Tarski's least fix-point theorem to define potentially
non-terminating recursive functions.
A survey of programming language semantics styles.
This is a survey of programming language semantics styles for a
miniature example of a programming language, with their encoding in Coq,
of equivalence of different styles, and the proof of soundess of tools obtained from
axiomatic semantics or abstract interpretation. The tools can be run inside Coq, thus
making them available for proof by reflection, and the code can also be extracted and
connected to a yacc-based parser, thanks to a precise use of modularity around the
type of strings.
- The product of p successive integers is divisible by p!.
The solution uses binomial coefficients, we look for the definitions and
properties of these coefficients in Coq's standard library and then we
deduce the result.
- Proofs in 'Coq in a Hurry' style.
Coq in a Hurry is a Coq tutorial where I attempt to teach
minimal rudiments of Coq without entering in the full power of the system.
Programs only use simply typed programming (but with a little polymorphism),
only a restricted subset of the tactics is used, but the subset being used
is already strong enough to address a wide variety of formalization problems.
This development gives a collection of examples: sorting, computing prime
numbers, verifying that the square root of 2 is not rational.