The Coq mailing list

[Laurent Thery <Laurent.Thery AT sophia.inria.fr>]

Hi,


just for fun I´ve implemented and proved the correctness
of  a naive Davis-Putnam procedure to solve Sodukos.

A soduko is represented as a mono-dimensional list of natural 
numbers. Zeros represent empty cells. For example,
for 3x3 sodukos:

  -------------------------------------
  |   |   | 8 | 1 | 6 |   | 9 |   |   |
  -------------------------------------
  |   |   | 4 |   | 5 |   | 2 |   |   |
  -------------------------------------
  | 9 | 7 |   |   |   | 8 |   | 4 | 5 |
  -------------------------------------
  |   |   | 5 |   |   |   |   |   | 6 |
  -------------------------------------
  | 8 | 9 |   |   |   |   |   | 3 | 7 | 
  -------------------------------------
  | 1 |   |   |   |   |   | 4 |   |   |
  -------------------------------------
  | 3 | 6 |   | 5 |   |   |   | 8 | 4 |
  -------------------------------------
  |   |   | 2 |   | 7 |   | 5 |   |   |
  -------------------------------------
  |   |   | 7 |   | 4 | 9 | 3 |   |   | 
  -------------------------------------

is represented as

  0 :: 0 :: 8 :: 1 :: 6 :: 0 :: 9 :: 0 :: 0 ::
  0 :: 0 :: 4 :: 0 :: 5 :: 0 :: 2 :: 0 :: 0 ::
  9 :: 7 :: 0 :: 0 :: 0 :: 8 :: 0 :: 4 :: 5 ::
  0 :: 0 :: 5 :: 0 :: 0 :: 0 :: 0 :: 0 :: 6 ::
  8 :: 9 :: 0 :: 0 :: 0 :: 0 :: 0 :: 3 :: 7 :: 
  1 :: 0 :: 0 :: 0 :: 0 :: 0 :: 4 :: 0 :: 0 ::
  3 :: 6 :: 0 :: 5 :: 0 :: 0 :: 0 :: 8 :: 4 ::
  0 :: 0 :: 2 :: 0 :: 7 :: 0 :: 5 :: 0 :: 0 ::
  0 :: 0 :: 7 :: 0 :: 4 :: 9 :: 3 :: 0 :: 0 :: nil.

All functions are parametrized by the height and width of
its subrectangles.

For example for 3x3,

  soduko 3 3: list nat -> Prop

   check 3 3: forall l, {soduko 3 3 l} + {~ soduko 3 3 l}

find_one 3 3: list nat -> option (list nat)

find_all 3 3: list nat -> list (list nat)

It can be downloaded at

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Soduko.zip

Have fun,

--
Laurent Théry