  The k-d tree is a classic binary space-partitioning tree used to organize
points in k-dimensional space. While used in computational geometry and
graphics, the data structure has a long history of application in nearest
neighbor search. The objective of the nearest neighbor search problem is to
efficiently find the closest point(s) to a given query point, and is the basis,
in turn, of common machine learning techniques. We present in this paper a case
study in the certified implementation, using the Coq proof assistant, of k-d
tree construction from a set of data and the accompanying K-nearest neighbors
search algorithm. Our experience demonstrates an intuitive method for
specifying properties of these algorithms using the notion of list
permutations.
