A couple of weeks ago, I moved a project that I have been working on sporadically since 2021 under the wing of the Coq community: FDSA in SSReflect.
The idea is simple: rewrite the code from the publicly available book Nipkow et al, “Functional Data Structures and Algorithms” (at the beginning of the work, the book was called “Functional Algorithms, Verified”) from Isabelle/HOL into a fully type-theoretical language. For porting, I chose Coq + the Mathcomp/SSReflect framework + the Equations plugin for compact pattern matching and termination proofs.
Isabelle/HOL uses classical logic for reasoning, but for working with the correctness of computational data structures, the difference from constructive logic is small. This is because it is almost always assumed that the elements of these structures are at least discrete (i.e., equipped with a decidable equality check, which corresponds to the “local” excluded middle). The main difference is probably in only one place: instead of using equalities on multisets from Isabelle, I use lists and the permutation relation (perm_eq) on them. Additionally, functions in Isabelle do not have to be total, which requires slightly changing the definitions — expanding them to cover the entire domain of definition and providing proofs of termination in all cases (not just in selected ones, as in the book).
The book is structured as follows:
- An introductory chapter with basic concepts.
- A section devoted to sorting and selection algorithms: mergesort/quicksort/quickselect. In my opinion, the chapter on the selection algorithm makes a noticeable leap in complexity: for quickselect, the proofs of termination (due to the use of nested recursion) and complexity (a simplified version of the Akra-Bazzi theorem) are an order of magnitude (or even two) more complicated than those for sorting.
- A large section on tree algorithms - here you will find popular red-black trees/AVL trees, the lesser-known Braun trees, and specialized quadtrees.
- An ideological continuation of the previous section covering several ways to implement priority queues.
- A section on advanced algorithmic methods, including dynamic programming, amortized analysis, and splay trees. I haven’t reached this section yet; I stopped at adapting search trees from previous chapters into a search table for caching results in dynamic programming.
- A miscellaneous section, currently containing classical graph search algorithms, the Knuth-Morris-Pratt string algorithm, the Huffman compression algorithm, and the αβ-pruning search algorithm. So far, I have only implemented the Huffman algorithm.
Overall, the book explains classical immutable algorithms quite well (although it is sometimes too concise, especially in section 4). It serves as a kind of proof-engineering version of the well-known work, Okasaki, [1998] “Purely Functional Data Structures”. The book contains many exercises, most of which I have solved, but in the public repository I replaced the corresponding sections with skeletons of definitions and theorems to avoid spoiling the solutions for potential students.