Fortune's algorithm described in coq

Fortune's algorithm is a sweep line algorithm to construct the Voronoi diagram of a set of points in the plane. In this task, we wish to develop a formal description of Voronoi diagrams and of the algorithm proposed by Steven Fortune in 1986, in the context of the Coq system and the mathematical components library. If time allows, we also wish to study how executable algorithms can be derived from the formal description.

• doc/
  • progress contains an overview of the small progress achieved over short periods.
  • resources a bibliography for learning Coq and Fortune's algorithm.
  • plan high levle goals and their deadlines
  • polynomial-equalities-experiment A basic demo of how to prove identities in a ring using the mathematical components library.
• python/ a python implementation of Fotune's algorithm.
• fortune.v The main file in coq. It requires installing coq-mathcomp-field, coq-mathcomp-ssreflect, coq-mathcomp-algebra.
  • The relevant codes are those above End ab1., codes below that are mainly for extraction and it may present some errors.