Search code examples
coq

In Coq, what would be the steps to prove the correctness of a function that solves puzzles like Sudoku or Takuzu?

What would be the general steps to prove the correctness of a function that solves puzzles, for example Sudoku or Takuzu?

Solution

  • I'd expect a typical "sequential puzzle" formalization to be composed of:

    • To begin with, a definition of board configurations, invalid (i.e. without/before constraints) and valid (satisfying all constraints).

    • Two "solver" functions, which, given a valid board configuration:

      • step solver: makes one single move if possible (e.g. returns an option);
      • solver: finds a solution if possible by making several moves.

    • And, correspondingly, two "checker" functions:

      • step checker: checks that a board configuration (e.g the result of a single move) is valid;
      • solution checker: as the step checker plus checks that the board is full, i.e. that it is an end configuration.

    • Finally, for proving correctness:

      • step solver correct: prove that, given any valid non-end configuration, the step solver produces a valid new configuration if any is possible (i.e. produces a configuration that satisfies step checking);
      • solver correct: prove that, given any valid non-end configuration, the solver produces a solution if any.

    That scheme can become a bit more complicated by considering solvers that return the whole set of possible solutions, or, even better, solvers that "stream" solutions one by one, with some backtracking or other kind of continuation scheme.

    On the other hand, some simplification is possible: in particular, in a dependently-typed total language such as Coq's, the checkers might be dispensed with (though in practice these are useful anyway, to validate data), since the language lets us define board configurations (invalid and valid) strictly, and solvers (any functions) are guaranteed to return results that conform to (are instances of) the declared return types.

    For a concrete example, here is an implementation you might look at for comparison/reference, see the README up to "correctness theorems" in particular: coq-community / sudoku on GitHub