Library Nqueens
Require Import Arith.
Require Import Omega.
Require Import Dec.
Require Import List.
Require Import Sets.
Require Import Coq.Program.Program.
Section Nqueens.
The parametric number of queens on the board
A board is represented as a function from nat to nat
falist P k a0;..;an holds when
P k a0 a1;..an /\ P (k+1) a1 a2;..;an /\ P (k+n) an ☐
Inductive falist A (P:nat -> A -> Prop) (k : nat) : list A -> Prop :=
fanil : falist P k nil
| facons : forall a l, P k a -> falist P (S k) l -> falist P k (cons a l).
Hint Constructors falist.
Lemma falist_dec : forall A (P:nat -> A -> Prop),
(forall n a, {P n a}+{~ P n a}) ->
forall l k, {falist P k l}+{~ falist P k l}.
fanil : falist P k nil
| facons : forall a l, P k a -> falist P (S k) l -> falist P k (cons a l).
Hint Constructors falist.
Lemma falist_dec : forall A (P:nat -> A -> Prop),
(forall n a, {P n a}+{~ P n a}) ->
forall l k, {falist P k l}+{~ falist P k l}.
The condition for a new value in k to be compatible with the board after k
Definition ok (k qk:nat) : board -> Prop :=
falist (fun i qi => qk <> qi /\ k + qk <> i + qi /\ N - k + qk <> N - i + qi)
(S k).
falist (fun i qi => qk <> qi /\ k + qk <> i + qi /\ N - k + qk <> N - i + qi)
(S k).
This condition is decidable
Lemma ok_dec : forall (k qk:nat) (q: board), {ok k qk q} + {~ ok k qk q}.
Definition psol k (p : board) : Prop :=
length p = N - k /\
forall i, i < N - k -> let qi:= nth i p 0 in
(qi < N /\ ok (i+k) qi (skipn (S i) p)).
Hint Unfold ok psol.
Definition psol k (p : board) : Prop :=
length p = N - k /\
forall i, i < N - k -> let qi:= nth i p 0 in
(qi < N /\ ok (i+k) qi (skipn (S i) p)).
Hint Unfold ok psol.
Correctness when extending the board
Lemma psol_ext : forall (q: board) (k qk:nat),
k < N -> qk < N -> psol (S k) q -> ok k qk q -> psol k (qk::q).
Hint Resolve psol_ext.
Lemma psol_nil : psol N nil.
Hint Resolve psol_nil.
k < N -> qk < N -> psol (S k) q -> ok k qk q -> psol k (qk::q).
Hint Resolve psol_ext.
Lemma psol_nil : psol N nil.
Hint Resolve psol_nil.
Pure functional version, we start from a partial solution and search for an extension
Fixpoint sol k (q:board) {struct k}
: option board :=
match k with O => Some q
| S m =>
let fix search i {struct i}
: option board :=
match i with O => None
| S j => if ok_dec m j q then
match sol m (j::q) with
| None => search j
| Some b => Some b
end
else search j
end
in search N
end.
Notation "! P " := {_:unit | P } (at level 35) : type_scope.
Local Obligation Tactic := program_simpl; try omega.
: option board :=
match k with O => Some q
| S m =>
let fix search i {struct i}
: option board :=
match i with O => None
| S j => if ok_dec m j q then
match sol m (j::q) with
| None => search j
| Some b => Some b
end
else search j
end
in search N
end.
Notation "! P " := {_:unit | P } (at level 35) : type_scope.
Local Obligation Tactic := program_simpl; try omega.
Solution with dependent types
Program Fixpoint solr k (q:board) (_:!(psol k q /\ k <= N)) {struct k}
: option {p : board | psol 0 p} :=
match k with O => Some q
| S m =>
let fix search i (_:!(i <=N)) {struct i}
: option {b: board | psol 0 b} :=
match i with O => None
| S j => if ok_dec m j q then
match solr (k:=m) (q:=j::q) tt with
| None => search j tt
| Some b => Some b
end
else search j tt
end
in search N tt
end.
Program Definition one_sol : option {p : board | psol 0 p} := solr (k:=N) (q:=nil) tt.
: option {p : board | psol 0 p} :=
match k with O => Some q
| S m =>
let fix search i (_:!(i <=N)) {struct i}
: option {b: board | psol 0 b} :=
match i with O => None
| S j => if ok_dec m j q then
match solr (k:=m) (q:=j::q) tt with
| None => search j tt
| Some b => Some b
end
else search j tt
end
in search N tt
end.
Program Definition one_sol : option {p : board | psol 0 p} := solr (k:=N) (q:=nil) tt.
Computing all solutions
Fixpoint all_solr k (q:board) {struct k}
: list board :=
match k with O => q :: nil
| S m =>
let fix search i {struct i}
: list board :=
match i with O => nil
| S j => if ok_dec m j q then
all_solr m (j::q) ++ search j
else search j
end
in search N
end.
Definition all_sol := all_solr N nil.
: list board :=
match k with O => q :: nil
| S m =>
let fix search i {struct i}
: list board :=
match i with O => nil
| S j => if ok_dec m j q then
all_solr m (j::q) ++ search j
else search j
end
in search N
end.
Definition all_sol := all_solr N nil.
Computing the number of solutions
Fixpoint nb_solr k (q:board) {struct k}
: nat :=
match k with O => 1
| S m =>
let fix search i {struct i}
: nat :=
match i with O => 0
| S j => if ok_dec m j q then
nb_solr m (j::q) + search j
else search j
end
in search N
end.
Definition nb_sol := nb_solr N nil.
: nat :=
match k with O => 1
| S m =>
let fix search i {struct i}
: nat :=
match i with O => 0
| S j => if ok_dec m j q then
nb_solr m (j::q) + search j
else search j
end
in search N
end.
Definition nb_sol := nb_solr N nil.
Specifying the computation of the number of solutions
Definition ext_board (p q : board) k :=
forall i, i < length q -> nth i q 0 = nth (k + i) p 0.
Lemma ext_board_refl : forall p, ext_board p p 0.
Hint Resolve ext_board_refl.
Lemma ext_board_prev : forall a p q k, ext_board p (a::q) k -> ext_board p q (S k).
Lemma ext_board_nil : forall p, ext_board p nil N.
Hint Resolve ext_board_prev ext_board_nil.
Lemma psol_length : forall p q m, psol 0 p -> psol m q ->
m <= N -> length q = length p - m.
Hint Immediate psol_length.
Lemma psol0_eq : forall p q, length p = length q -> ext_board p q 0 -> p = q.
Hint Resolve psol0_eq.
Lemma psol_skip :
forall k p q, length p = k + length q -> ext_board p q k -> skipn k p = q.
Lemma psol_nth : forall p q m j,
ext_board p (j::q) m -> nth m p 0 = j.
Lemma ext_board_nth : forall p q m j,
ext_board p q (S m) -> nth m p 0 = j -> ext_board p (j::q) m.
Hint Resolve ext_board_nth.
Lemma nb_solp : {n : nat | card (fun p => psol 0 p) n}.
End Nqueens.
Extracting the functions
Extraction "nqueens" all_sol nb_sol nb_solp.
Tests for computing the solution