N-queens: proof in progress

parent 04a3f115
......@@ -30,8 +30,24 @@ theory Bits "the bits of an integer, as a set of integers"
forall x: int. is_empty (bits x) <-> x = 0
axiom bits_remove_singleton:
forall x a b: int. bits b = singleton x -> mem x (bits a) ->
bits (a - b) = remove x (bits a)
forall i a b: int. bits b = singleton i -> mem i (bits a) ->
bits (a - b) = remove i (bits a)
axiom bits_add_singleton:
forall i a b: int. bits b = singleton i -> not (mem i (bits a)) ->
bits (a + b) = add i (bits a)
axiom bits_mul2_1:
forall a i: int. mem (i-1) (bits a) -> mem i (bits (a*2))
axiom bits_mul2_2:
forall a i: int. mem i (bits (a*2)) -> i >= 1 -> mem (i-1) (bits a)
use export int.ComputerDivision
axiom bits_div2_1:
forall a i: int. mem (i+1) (bits a) -> i >= 0 -> mem i (bits (div a 2))
axiom bits_div2_2:
forall a i: int. mem i (bits (div a 2)) -> mem (i+1) (bits a)
use export BitwiseArithmetic
......@@ -41,6 +57,46 @@ theory Bits "the bits of an integer, as a set of integers"
axiom rightmost_bit_trick:
forall x: int. x <> 0 -> bits (x & -x) = singleton (min_elt (bits x))
axiom bits_below: forall n: int. n >= 0 -> bits (~(~0<<n)) = below n
end
theory Solution
use import int.Int
use export map.Map
function n : int
type solution = map int int
(* solutions t and u have the same prefix [0..i[ *)
predicate eq_prefix (t u: solution) (i: int) =
forall k: int. 0 <= k < i -> t[k] = u[k]
(* s stores a partial solution, for the rows 0..k-1 *)
predicate partial_solution (k: int) (s: solution) =
forall i: int. 0 <= i < k ->
0 <= s[i] < n /\
(forall j: int. 0 <= j < i -> s[i] <> s[j] /\
s[i]-s[j] <> i-j /\
s[i]-s[j] <> j-i)
predicate solution (s: solution) = partial_solution n s
lemma partial_solution_eq_prefix:
forall u t: solution, k: int.
partial_solution k t -> eq_prefix t u k -> partial_solution k u
predicate lt_sol (s1 s2: solution) =
exists i: int. 0 <= i < n /\ eq_prefix s1 s2 i /\ s1[i] < s2[i]
type solutions = map int solution
(* s[a..b[ is sorted for lt_sol *)
predicate sorted (s: solutions) (a b: int) =
forall i j: int. a <= i < j < b -> lt_sol s[i] s[j]
end
module NQueens
......@@ -72,6 +128,7 @@ module NQueens
while !e <> 0 do invariant { subset (bits !e) (bits a) }
let d = !e & (- !e) in
assert { bits d = singleton (min_elt (bits !e)) };
assert { bits (a-d) = remove (min_elt (bits !e)) (bits a) };
f += t2 (a - d) ((b+d) * 2) ((c+d)/2);
e -= d
done;
......@@ -79,6 +136,83 @@ module NQueens
end else
1
val min_elt (x: int) : { x <> 0 } int { result = min_elt (bits x) }
use import Solution
val sol: ref solutions (* all solutions *)
val s : ref int (* next slot for a solution *)
val k : ref int (* current row in the current solution *)
(****
/*@ requires solution(col)
@ assigns s, sol[s][0..N()-1]
@ ensures s==\old(s)+1 && eq_sol(sol[\old(s)], col)
@*/
void store_solution();
/*@ requires
@ 0 <= k && k + card(iset(a)) == N() && 0 <= s &&
@ pre_a:: (\forall int i; in_(i,iset(a)) <=>
@ (0<=i<N() && \forall int j; 0<=j<k => i != col[j])) &&
@ pre_b:: (\forall int i; i>=0 => (in_(i,iset(b)) <=>
@ (\exists int j; 0<=j<k && col[j] == i+j-k))) &&
@ pre_c:: (\forall int i; i>=0 => (in_(i,iset(c)) <=>
@ (\exists int j; 0<=j<k && col[j] == i+k-j))) &&
@ partial_solution(k, col)
@ assigns
@ col[k..], s, k, sol[s..][..]
@ ensures
@ \result == s - \old(s) && \result >= 0 && k == \old(k) &&
@ sorted(sol, \old(s), s) &&
@ \forall int* t; ((solution(t) && eq_prefix(col,t,k)) <=>
@ (\exists int i; \old(s)<=i<s && eq_sol(t, sol[i])))
@*/
int t3(int a, int b, int c){
int d, e=a&~b&~c, f=1;
//@ label L
if (a)
/*@ invariant
@ included(iset(e),\at(iset(e),L)) &&
@ f == s - \at(s,L) && f >= 0 && k == \old(k) &&
@ partial_solution(k, col) &&
@ sorted(sol, \at(s,L), s) &&
@ \forall int *t;
@ (solution(t) &&
@ \exists int di; in_(di, diff(\at(iset(e),L), iset(e))) &&
@ eq_prefix(col,t,k) && t[k]==di) <=>
@ (\exists int i; \at(s,L)<=i<s && eq_sol(t, sol[i]))
@ loop_assigns
@ col[k..], s, k, sol[s..][..]
@*/
for (f=0; d=e&-e; e-=d) {
//@ assert \exists int x; iset(d) == singleton(x) && in_(x,iset(a))
//@ ghost col[k] = min_elt(d); // ghost code
//@ ghost k++; // ghost code
f += t3(a-d, (b+d)*2, (c+d)/2);
//@ ghost k--; // ghost code
}
//@ ghost else
//@ ghost store_solution(); // ghost code
return f;
}
/*@ requires
@ n == N() && s == 0 && k == 0
@ ensures
@ \result == s &&
@ sorted(sol, 0, s) &&
@ \forall int* t;
@ solution(t) <=> (\exists int i; 0<=i<\result && eq_sol(t,sol[i]))
@*/
int queens(int n) {
return t3(~(~0<<n),0,0);
}
*****)
end
(*
......
......@@ -135,24 +135,19 @@ Parameter bits: Z -> (set Z).
Axiom bits_0 : forall (x:Z), (is_empty (bits x)) <-> (x = 0%Z).
Axiom bits_remove_singleton : forall (x:Z) (a:Z) (b:Z), ((bits b) = (add x
(empty:(set Z)))) -> ((mem x (bits a)) -> ((bits (a - b)%Z) = (remove x
Axiom bits_remove_singleton : forall (i:Z) (a:Z) (b:Z), ((bits b) = (add i
(empty:(set Z)))) -> ((mem i (bits a)) -> ((bits (a - b)%Z) = (remove i
(bits a)))).
Parameter infix_et: Z -> Z -> Z.
Parameter infix_lsls: Z -> Z -> Z.
Parameter prefix_tl: Z -> Z.
Axiom bits_add_singleton : forall (i:Z) (a:Z) (b:Z), ((bits b) = (add i
(empty:(set Z)))) -> ((~ (mem i (bits a))) -> ((bits (a + b)%Z) = (add i
(bits a)))).
Axiom bits_diff : forall (a:Z) (b:Z), ((bits (infix_et a
(prefix_tl b))) = (diff (bits a) (bits b))).
Axiom bits_mul2_1 : forall (a:Z) (i:Z), (mem (i - 1%Z)%Z (bits a)) -> (mem i
(bits (a * 2%Z)%Z)).
Axiom rightmost_bit_trick : forall (x:Z), (~ (x = 0%Z)) -> ((bits (infix_et x
(-x)%Z)) = (add (min_elt (bits x)) (empty:(set Z)))).
Axiom bits_mul2_2 : forall (a:Z) (i:Z), (mem i (bits (a * 2%Z)%Z)) ->
((1%Z <= i)%Z -> (mem (i - 1%Z)%Z (bits a))).
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
......@@ -196,6 +191,30 @@ Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
Axiom bits_div2_1 : forall (a:Z) (i:Z), (mem (i + 1%Z)%Z (bits a)) ->
((0%Z <= i)%Z -> (mem i (bits (ZOdiv a 2%Z)))).
Axiom bits_div2_2 : forall (a:Z) (i:Z), (mem i (bits (ZOdiv a 2%Z))) ->
(mem (i + 1%Z)%Z (bits a)).
Parameter infix_et: Z -> Z -> Z.
Parameter infix_lsls: Z -> Z -> Z.
Parameter prefix_tl: Z -> Z.
Axiom bits_diff : forall (a:Z) (b:Z), ((bits (infix_et a
(prefix_tl b))) = (diff (bits a) (bits b))).
Axiom rightmost_bit_trick : forall (x:Z), (~ (x = 0%Z)) -> ((bits (infix_et x
(-x)%Z)) = (add (min_elt (bits x)) (empty:(set Z)))).
Axiom bits_below : forall (n:Z), (0%Z <= n)%Z ->
((bits (prefix_tl (infix_lsls (prefix_tl 0%Z) n))) = (below n)).
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
......@@ -265,11 +284,12 @@ Implicit Arguments set2.
Theorem WP_parameter_t2 : forall (a:Z), (~ (a = 0%Z)) -> forall (f:Z),
forall (e:Z), (subset (bits e) (bits a)) -> ((~ (e = 0%Z)) ->
(((bits (infix_et e (-e)%Z)) = (add (min_elt (bits e)) (empty:(set Z)))) ->
((~ (2%Z = 0%Z)) -> (((0%Z <= (cardinal (bits a)))%Z /\
(((bits (a - (infix_et e (-e)%Z))%Z) = (remove (min_elt (bits e))
(bits a))) -> ((~ (2%Z = 0%Z)) -> (((0%Z <= (cardinal (bits a)))%Z /\
((cardinal (bits (a - (infix_et e
(-e)%Z))%Z)) < (cardinal (bits a)))%Z) -> forall (result:Z),
forall (f1:Z), (f1 = (f + result)%Z) -> forall (e1:Z),
(e1 = (e - (infix_et e (-e)%Z))%Z) -> (subset (bits e1) (bits a)))))).
(e1 = (e - (infix_et e (-e)%Z))%Z) -> (subset (bits e1) (bits a))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
assert (bits e1 = remove (min_elt (bits e)) (bits e)).
......@@ -280,7 +300,7 @@ omega.
apply min_elt_def1.
generalize (bits_0 e); intuition.
apply subset_trans with (bits e); auto.
rewrite H8.
rewrite H9.
apply subset_remove; auto.
Qed.
(* DO NOT EDIT BELOW *)
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment