Formal proofs

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.

• An introductory example on how to use type classes for reification in tactics based on reflection.
• 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 the coquelicot 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 coquelicot 2.0.1).

  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 11, 2012).
• 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 math-components 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.
• A 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 Proofs and types, transposing it from lambda-calculus (with pairs and projectors) to combinatory logic. This compressed tar archive also contains Randy Pollack's proofs.
• 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 guarded co-recursive.
• Filters in co-recursion data associated to the paper Filters on Co-Inductive streams: an application to Eratosthenes' sieve (here is an old version of the files)
• 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, the proofs 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.