Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq
Résumé
The firing squad synchronization is a cellular automata problem introduced by Moore; in 1987, J.Mazoyer gave a six state solution to this problem. The proof of correctness of this solution uses discrete geometrical considerations, but is quite hard to verify due to the multiplication of cases and indexes. To be more confident in this proof, a proof assistant developed by the Inria, Coq has been used. This report exposes the development in Coq of this proof. A large use of inductive structures, a natural way in Coq, offers a clearer vision of the Mazoyer's solution. The full development of the proof is avalaible in the contributions of the Coq software.
La synchronisation d’une ligne de fusiliers est un problème d’automates cellulaires posé par Moore, en 1987, J.Mazoyer donna une solution avec six états à ce problème. La preuve de correction de cette solution utilise des considérations de géométrie discrète, mais elle est assez difficile à vérifier à cause de la multiplication des cas et des indices. Pour être plus sûr de cette preuve, un assistant à la preuve développé par l’Inria, Coq, a été utilisé. Ce rapport expose le développement en Coq de la preuve. Un grand usage des structures inductives, une voie naturelle en Coq, offre une vision plus claire de la solution de J.Mazoyer. Le développement complet de la preuve est disponible dans les contributions du logiciel Coq
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...