Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator

In this article we present the implementation and formal verification, using the Coq system, of a generalized version of the crossover operator applied to genetic algorithms (GA). The first part of this work defines the multiple crossover of two lists in any finite number of points, generalizing a previous definition by Uchibori. In the second part, we show that the definition does not depend on the order of the list of points. Then, a more efficient definition of the crossover operation is provided, and formally proved to be equivalent to the previous one, exploiting the notion of difference list.