Section: New Results

Formalisation work

Participants : Jean-Jacques Lévy, Daniel de Rauglaudre.

Proofs of algorithms on graphs

Jean-Jacques Lévy and Chen Ran (a PhD student of the Institute of Software, Beijing, visiting the Toccata team) pursue their work about formal proofs of algorithms. Their goal is to provide proofs of algorithms which ought to be both checked by computer and easily human readable. If these kinds of proofs exist for algorithms on inductive structures or recursive algorithms on arrays, they seem less easy to design for combinatorial structures such as graphs. In 2016, they completed proofs for algorithms computing the strongly connected components in graphs. There are mainly two algorithms: one by Kosaraju (1978) working in two phases (some formal proofs of it have already been achieved by Pottier with Coq-classic and by Théry and Gonthier with Coq-ssreflect), one by Tarjan (1972) working in a single pass.

Their proofs use a first-order logic with definitions of inductive predicates. This logic is the one defined in Why3 (research-team Toccata, Saclay). They widely use automatic provers interfaced by Why3. A very minor part of these proofs is also achieved in Coq. The difficulty of this approach is to combine automatic provers and intuitive design.

Part of this work (Tarjan 1972) is presented at JFLA 2017 in Gourette [30] A more comprehensive version is under submission to another conference [34]. Scripts of proofs can be found at http://jeanjacqueslevy.net/why3.

Formalization of theorems in Coq

This section reports on formalisation work by Daniel de Rauglaudre.

Puiseux' Theorem

Puiseux' theorem states that the set of Puiseux series (series with rational powers) is an algebraically closed field, i.e. every non-constant polynomial with Puiseux series coefficients admits a zero. This theorem was formalized in Coq a couple of years ago, but it depended on five ad hoc axioms. This year, all these axioms have been grouped together into the only axiom LPO (Limited Principle of Omniscience), stating that for each sequence of booleans, we can decide whether it is always false or if there is at least one true element. This formalized theorem now depends only on this axiom.

Banach-Tarski Paradox

Banach-Tarski Paradox states that, if we admit the axiom of choice, a sphere is equidecomposable into two spheres identical to the initial one. The equidecomposability is a property of geometric objects: two objects (sets) are equidecomposable if we can partition them into a same finite number of sets, and each set of the first object is mapped to a set of the second object by only rotations and translations. In other words, we break the first object into a finite number of pieces, and with them, we reconstitute the second object. Its pen and paper proof was done in 1924 by Banach and Tarski.

Its formal proof in Coq has been started this year. About 80% of the proof has been done. The already proved part includes a lemma which says that the sphere without some specific countable number of points is equidecomposable into twice itself. It also includes a formal proof that equidecomposability is an equivalence relation. This makes about 7000 lines of Coq. The remaining part is to formalize the proof that the sphere is equidecomposable into the sphere without this countable set of points.

The version of axiom of choice used for this proof is named TTCA (Type Theoretical Axiom of Choice, introduced by Benjamin Werner [88]), stating that for each equivalence relation, there exists a function mapping each relation class to one of its elements.