Commit 45a49413 by Jean-Christophe Filliâtre

### n-queens: proof in progress

parent 1cc8b330
 ... ... @@ -5,59 +5,23 @@ c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0< x = 0 axiom succ_def_1: forall s: set int, i: int. mem (i-1) s -> mem i (succ s) axiom succ_def_2: forall s: set int, i: int. mem i (succ s) -> i >= 1 -> mem (i-1) s axiom bits_remove_singleton: 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) function pred (set int) : set int use export BitwiseArithmetic axiom bits_diff: forall a b: int. bits (a & ~b) = diff (bits a) (bits b) 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< i >= 0 -> mem i (pred s) axiom pred_def__2: forall s: set int, i: int. mem i (pred s) -> mem (i+1) s end ... ... @@ -102,6 +66,138 @@ theory Solution end (* 1. Abstract version of the code using sets (not ints) *******************) module NQueensSets use import S use import module ref.Refint use import Solution val col: ref solution (* solution under construction *) val k : ref int (* current row in the current solution *) 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 : set int) variant { cardinal a } = { 0 <= !k /\ !k + cardinal a = n /\ "pre_a" (forall i: int. mem i a <-> (0<=i i <> !col[j])) /\ "pre_b" (forall i: int. i>=0 -> mem i b <-> (exists j: int. 0 <= j < !k /\ !col[j] = i + j - !k)) /\ "pre_c" (forall i: int. i>=0 -> mem i c <-> (exists j: int. 0 <= j < !k /\ !col[j] = i + !k - j)) /\ partial_solution !k !col } if not (is_empty a) then begin let e = ref (diff (diff a b) c) in 'L:let f = ref 0 in while not (is_empty !e) do invariant { !f = !s - at !s 'L >= 0 /\ !k = at !k 'L /\ subset !e (at !e 'L) /\ partial_solution !k !col /\ sorted !sol (at !s 'L) !s /\ (forall t: solution. (solution t /\ eq_prefix !col t !k /\ exists di: int. mem di (diff (at !e 'L) !e) /\ 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 = min_elt !e in (* ghost *) col := !col[!k <- d]; (* ghost *) incr k; f += t3 (remove d a) (succ (add d b)) (pred (add d c)); (* ghost *) decr k; e := remove d !e 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 (below q) empty empty { result = !s /\ sorted !sol 0 !s /\ forall t: solution. solution t <-> (exists i: int. 0 <= i < result /\ eq_sol t !sol[i]) } end (* 2. More realistic code with bitwise operations **************************) theory BitwiseArithmetic use export int.Int (* logical and *) function (&) int int : int (* logical shift left *) function (<<) int int : int (* logical negation *) function (~_) int : int end theory Bits "the 1-bits of an integer, as a set of integers" use export S function bits int : set int axiom bits_0: forall x: int. is_empty (bits x) <-> x = 0 axiom bits_remove_singleton: 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: forall a: int. bits (a*2) = succ (bits a) use export int.ComputerDivision axiom bits_div2: forall a: int. bits (div a 2) = pred (bits a) use export BitwiseArithmetic axiom bits_diff: forall a b: int. bits (a & ~b) = diff (bits a) (bits b) 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<
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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 succ: (set Z) -> (set Z). Axiom succ_def_1 : forall (s:(set Z)) (i:Z), (mem (i - 1%Z)%Z s) -> (mem i (succ s)). Axiom succ_def_2 : forall (s:(set Z)) (i:Z), (mem i (succ s)) -> ((1%Z <= i)%Z -> (mem (i - 1%Z)%Z s)). Parameter pred: (set Z) -> (set Z). Axiom pred_def_1 : forall (s:(set Z)) (i:Z), (mem (i + 1%Z)%Z s) -> ((0%Z <= i)%Z -> (mem i (pred s))). Axiom pred_def__2 : forall (s:(set Z)) (i:Z), (mem i (pred s)) -> (mem (i + 1%Z)%Z s). 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 (a:Type)(t:(map Z a)) (u:(map Z a)) (i:Z): Prop := forall (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) -> ((get t k) = (get u k)). Implicit Arguments eq_prefix. 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 col: (ref (map Z Z)). Parameter k: (ref Z). Parameter sol: (ref (map Z (map Z Z))). Parameter s: (ref Z). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_t3 : forall (a:(set Z)), forall (b:(set Z)), forall (c:(set Z)), forall (s1:Z), forall (sol1:(map Z (map Z Z))), forall (k1:Z), forall (col1:(map Z Z)), ((0%Z <= k1)%Z /\ (((k1 + (cardinal a))%Z = (n )) /\ ((forall (i:Z), (mem i a) <-> (((0%Z <= i)%Z /\ (i < (n ))%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < k1)%Z) -> ~ (i = (get col1 j)))) /\ ((forall (i:Z), (0%Z <= i)%Z -> ((mem i b) <-> exists j:Z, ((0%Z <= j)%Z /\ (j < k1)%Z) /\ ((get col1 j) = ((i + j)%Z - k1)%Z))) /\ ((forall (i:Z), (0%Z <= i)%Z -> ((mem i c) <-> exists j:Z, ((0%Z <= j)%Z /\ (j < k1)%Z) /\ ((get col1 j) = ((i + k1)%Z - j)%Z))) /\ (partial_solution k1 col1)))))) -> ((~ (is_empty a)) -> forall (f:Z), forall (e:(set Z)), forall (s2:Z), forall (sol2:(map Z (map Z Z))), forall (k2:Z), forall (col2:(map Z Z)), (((f = (s2 - s1)%Z) /\ (0%Z <= (s2 - s1)%Z)%Z) /\ ((k2 = k1) /\ ((subset e (diff (diff a b) c)) /\ ((partial_solution k2 col2) /\ ((sorted sol2 s1 s2) /\ ((forall (t:(map Z Z)), ((partial_solution (n ) t) /\ ((eq_prefix col2 t k2) /\ exists di:Z, (mem di (diff (diff (diff a b) c) e)) /\ ((get t k2) = di))) <-> exists i:Z, ((s1 <= i)%Z /\ (i < s2)%Z) /\ (eq_prefix t (get sol2 i) (n ))) /\ ((eq_prefix col1 col2 k1) /\ (eq_prefix sol1 sol2 s1)))))))) -> ((is_empty e) -> forall (t:(map Z Z)), ((partial_solution (n ) t) /\ (eq_prefix col2 t k2)) -> exists i:Z, ((s1 <= i)%Z /\ (i < s2)%Z) /\ (eq_prefix t (get sol2 i) (n )))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. subst k2. rename k1 into k. assert (k < n)%Z. generalize (cardinal_nonneg _ a). generalize (cardinal_empty _ a). intuition. assert (case: (cardinal a = 0 \/ cardinal a > 0)%Z) by omega. destruct case. absurd (is_empty a); auto. omega. destruct (H13 t) as (h1,_); clear H13. apply h1; intuition. exists (get t k); intuition. destruct (diff_def1 _ (diff (diff a b) c) e (get t k)) as (_, h); apply h; clear h; split. destruct (diff_def1 _ (diff a b) c (get t k)) as (_, h); apply h; clear h; split. destruct (diff_def1 _ a b (get t k)) as (_, h); apply h; clear h; split. (* mem .. a *) destruct (H2 (get t k)) as (_,h); apply h; clear h. split. destruct (H17 k) as (h,_). omega. assumption. intros j hj. rewrite H14. rewrite H18. destruct (H17 k) as (_,h). omega. destruct (h j); intuition. assumption. assumption. (* not (mem ... b) *) Qed. (* DO NOT EDIT BELOW *)
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!