N-queens: proof in progress

parent bb11c2df
......@@ -20,7 +20,7 @@ theory BitwiseArithmetic
end
theory Bits "the bits of an integer, as a set of integers"
theory Bits "the 1-bits of an integer, as a set of integers"
use export set.Fsetint
......@@ -66,14 +66,17 @@ theory Solution
use import int.Int
use export map.Map
(* the number of queens *)
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) =
predicate eq_prefix (t u: map int 'a) (i: int) =
forall k: int. 0 <= k < i -> t[k] = u[k]
predicate eq_sol (t u: solution) = eq_prefix t u n
(* s stores a partial solution, for the rows 0..k-1 *)
predicate partial_solution (k: int) (s: solution) =
forall i: int. 0 <= i < k ->
......@@ -104,7 +107,6 @@ module NQueens
use import Bits
use import module arith.Int
use import module ref.Refint
use import module array.Array
(* warmup 1: termination of the loop *)
let rec t1 (a b c : int) =
......@@ -140,78 +142,77 @@ module NQueens
use import Solution
val sol: ref solutions (* all solutions *)
val s : ref int (* next slot for a solution *)
val col: ref solution (* solution under construction *)
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);
}
*****)
val sol: ref solutions (* all solutions *)
val s : ref int (* next slot for a solution = number of solutions *)
let store_solution () =
{ solution !col }
sol := !sol[!s <- !col];
incr s
{ !s = old !s + 1 /\
eq_prefix (old !sol) !sol (old !s) /\
!sol[old !s] = !col }
let rec t3 (a b c : int) =
{ 0 <= !k /\ !k + cardinal (bits a) = n /\ 0 <= !s /\
"pre_a" (forall i: int. mem i (bits a) <->
(0<=i< n /\ forall j: int. 0 <= j < !k -> i <> !col[j])) /\
"pre_b" (forall i: int. i>=0 -> mem i (bits b) <->
(exists j: int. 0 <= j < !k /\ !col[j] = i + j - !k)) /\
"pre_c" (forall i: int. i>=0 -> mem i (bits c) <->
(exists j: int. 0 <= j < !k /\ !col[j] = i + !k - j)) /\
partial_solution !k !col }
if a <> 0 then begin
let e = ref (a & ~b & ~c) in
'L:let f = ref 0 in
while !e <> 0 do
invariant {
!f = !s - at !s 'L >= 0 /\ !k = at !k 'L /\
subset (bits !e) (at (bits !e) 'L) /\
partial_solution !k !col /\
sorted !sol (at !s 'L) !s /\
(forall t: solution.
(solution t /\
exists di: int. mem di (diff (at (bits !e) 'L) (bits !e)) /\
eq_prefix !col t !k /\ t[!k] = di)
<->
(exists i: int. (at !s 'L) <= i < !s /\ eq_sol t !sol[i])) /\
(* assigns *)
eq_prefix (at !col 'L) !col (at !k 'L) /\
eq_prefix (at !sol 'L) !sol (at !s 'L) }
let d = !e & (- !e) in
(* assert \exists int x; iset(d) == singleton(x) && in_(x,iset(a)) *)
assert { bits d = singleton (min_elt (bits !e)) };
assert { bits (a-d) = remove (min_elt (bits !e)) (bits a) };
(* ghost *) col := !col[!k <- min_elt d];
(* ghost *) incr k;
f += t3 (a - d) ((b+d) * 2) ((c+d)/2);
(* ghost *) decr k;
e -= d
done;
!f
end else begin
(* ghost *) store_solution ();
1
end
{ result = !s - old !s >= 0 /\ !k = old !k /\
sorted !sol (old !s) !s /\
(forall t: solution.
((solution t /\ eq_prefix !col t !k) <->
(exists i: int. old !s <= i < !s /\ eq_sol t !sol[i]))) /\
(* assigns *)
eq_prefix (old !col) !col !k /\
eq_prefix (old !sol) !sol (old !s) }
let queens3 (q: int) =
{ 0 <= q = n /\ !s = 0 /\ !k = 0 }
t3 (~(~0 << q)) 0 0
{ result = !s /\ sorted !sol 0 !s /\
forall t: solution.
solution t <-> (exists i: int. 0 <= i < result /\ eq_sol t !sol[i]) }
end
......
......@@ -130,6 +130,10 @@ Parameter below: Z -> (set Z).
Axiom below_def : forall (x:Z) (n:Z), (mem x (below n)) <-> ((0%Z <= x)%Z /\
(x < n)%Z).
Axiom cardinal_below : forall (n:Z), ((0%Z <= n)%Z ->
((cardinal (below n)) = n)) /\ ((~ (0%Z <= n)%Z) ->
((cardinal (below n)) = 0%Z)).
Parameter bits: Z -> (set Z).
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter set : forall (a:Type), Type.
Parameter mem: forall (a:Type), a -> (set a) -> Prop.
Implicit Arguments mem.
Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.
Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(infix_eqeq s1 s2) -> (s1 = s2).
Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Implicit Arguments subset.
Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a))
(s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Parameter empty: forall (a:Type), (set a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.
Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.
Axiom empty_def1 : forall (a:Type), (is_empty (empty:(set a))).
Parameter add: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments add.
Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments remove.
Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)),
(subset (remove x s) s).
Parameter union: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments union.
Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments inter.
Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments diff.
Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset (diff s1 s2) s1).
Parameter cardinal: forall (a:Type), (set a) -> Z.
Implicit Arguments cardinal.
Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall (a:Type), forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall (a:Type), forall (x:a), forall (s:(set a)),
(~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall (a:Type), forall (x:a), forall (s:(set a)),
(mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
Axiom cardinal_subset : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Parameter min_elt: (set Z) -> Z.
Axiom min_elt_def1 : forall (s:(set Z)), (~ (is_empty s)) -> (mem (min_elt s)
s).
Axiom min_elt_def2 : forall (s:(set Z)), (~ (is_empty s)) -> forall (x:Z),
(mem x s) -> ((min_elt s) <= x)%Z.
Parameter max_elt: (set Z) -> Z.
Axiom max_elt_def1 : forall (s:(set Z)), (~ (is_empty s)) -> (mem (max_elt s)
s).
Axiom max_elt_def2 : forall (s:(set Z)), (~ (is_empty s)) -> forall (x:Z),
(mem x s) -> (x <= (max_elt s))%Z.
Parameter below: Z -> (set Z).
Axiom below_def : forall (x:Z) (n:Z), (mem x (below n)) <-> ((0%Z <= x)%Z /\
(x < n)%Z).
Axiom cardinal_below : forall (n:Z), ((0%Z <= n)%Z ->
((cardinal (below n)) = n)) /\ ((~ (0%Z <= n)%Z) ->
((cardinal (below n)) = 0%Z)).
Parameter bits: Z -> (set Z).
Axiom bits_0 : forall (x:Z), (is_empty (bits x)) <-> (x = 0%Z).
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)))).
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_mul2_1 : forall (a:Z) (i:Z), (mem (i - 1%Z)%Z (bits a)) -> (mem i
(bits (a * 2%Z)%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.
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z).
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z).
Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZOdiv x y))%Z.
Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZOdiv x y) <= 0%Z)%Z.
Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZOmod x y))%Z.
Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZOmod x y) <= 0%Z)%Z.
Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z.
Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x).
Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z).
Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOdiv x y) = 0%Z).
Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOmod x y) = x).
Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%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.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set1: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set1.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set1 m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set1 m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Parameter n: Z.
Definition solution := (map Z Z).
Definition eq_prefix(t:(map Z Z)) (u:(map Z Z)) (i:Z): Prop := forall (k:Z),
((0%Z <= k)%Z /\ (k < i)%Z) -> ((get t k) = (get u k)).
Definition partial_solution(k:Z) (s:(map Z Z)): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < k)%Z) -> (((0%Z <= (get s i))%Z /\ ((get s
i) < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ((~ ((get s
i) = (get s j))) /\ ((~ (((get s i) - (get s j))%Z = (i - j)%Z)) /\
~ (((get s i) - (get s j))%Z = (j - i)%Z)))).
Axiom partial_solution_eq_prefix : forall (u:(map Z Z)) (t:(map Z Z)) (k:Z),
(partial_solution k t) -> ((eq_prefix t u k) -> (partial_solution k u)).
Definition lt_sol(s1:(map Z Z)) (s2:(map Z Z)): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < (n ))%Z) /\ ((eq_prefix s1 s2 i) /\ ((get s1
i) < (get s2 i))%Z).
Definition solutions := (map Z (map Z Z)).
Definition sorted(s:(map Z (map Z Z))) (a:Z) (b:Z): Prop := forall (i:Z)
(j:Z), (((a <= i)%Z /\ (i < j)%Z) /\ (j < b)%Z) -> (lt_sol (get s i)
(get s j)).
Parameter sol: (ref (map Z (map Z Z))).
Parameter s: (ref Z).
Parameter k: (ref Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_t3 : forall (a:Z), forall (b:Z), forall (c:Z),
forall (k1:Z), forall (s1:Z), forall (sol1:(map Z (map Z Z))),
((0%Z <= k1)%Z /\ (((k1 + (cardinal (bits a)))%Z = (n )) /\
((0%Z <= s1)%Z /\ forall (i:Z), (mem i (bits a)) <-> (((0%Z <= i)%Z /\
(i < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < k1)%Z) ->
~ (i = (get (get sol1 s1) j)))))) -> ((~ (a = 0%Z)) -> forall (f:Z),
forall (e:Z), forall (k2:Z), forall (s2:Z), forall (sol2:(map Z (map Z
Z))), (((f = (s2 - s1)%Z) /\ (0%Z <= (s2 - s1)%Z)%Z) /\ ((k2 = k1) /\
(subset (bits e) (bits (infix_et (infix_et a (prefix_tl b))
(prefix_tl c)))))) -> ((~ (e = 0%Z)) -> (((bits (infix_et e
(-e)%Z)) = (add (min_elt (bits e)) (empty:(set Z)))) ->
(((bits (a - (infix_et e (-e)%Z))%Z) = (remove (min_elt (bits e))
(bits a))) -> ((~ ((infix_et e (-e)%Z) = 0%Z)) -> forall (sol3:(map Z (map
Z Z))), (sol3 = (set1 sol2 s2 (set1 (get sol2 s2) k2
(min_elt (bits (infix_et e (-e)%Z)))))) -> forall (k3:Z),
(k3 = (k2 + 1%Z)%Z) -> ((~ (2%Z = 0%Z)) -> (((0%Z <= k3)%Z /\
(((k3 + (cardinal (bits (a - (infix_et e (-e)%Z))%Z)))%Z = (n )) /\
((0%Z <= s2)%Z /\ forall (i:Z), (mem i (bits (a - (infix_et e
(-e)%Z))%Z)) <-> (((0%Z <= i)%Z /\ (i < (n ))%Z) /\ forall (j:Z),
((0%Z <= j)%Z /\ (j < k3)%Z) -> ~ (i = (get (get sol3 s2) j)))))) ->
forall (k4:Z), forall (s3:Z), forall (result:Z),
(((result = (s3 - s2)%Z) /\ (0%Z <= (s3 - s2)%Z)%Z) /\ (k4 = k3)) ->
forall (f1:Z), (f1 = (f + result)%Z) -> forall (k5:Z),
(k5 = (k4 - 1%Z)%Z) -> forall (e1:Z), (e1 = (e - (infix_et e (-e)%Z))%Z) ->
(subset (bits e1) (bits (infix_et (infix_et a (prefix_tl b))
(prefix_tl c))))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
assert (bits e1 = remove (min_elt (bits e)) (bits e)).
subst e1.
apply bits_remove_singleton.
apply rightmost_bit_trick.
omega.
apply min_elt_def1.
generalize (bits_0 e); intuition.
apply subset_trans with (bits e); auto.
rewrite H25.
apply subset_remove; auto.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
......@@ -122,6 +122,9 @@ theory Fsetint
axiom below_def: forall x n: int. mem x (below n) <-> 0 <= x < n
lemma cardinal_below:
forall n: int. cardinal (below n) = if n >= 0 then n else 0
end
theory FsetExt
......
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