Commit 437ed722 by Jean-Christophe Filliatre

### N-queens: proof in progress

parent 18d45331
 (* Verification of the following 2-lines C program solving the N-queens puzzle: t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,( c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0< 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) 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)) end 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) = if a <> 0 then begin let e = ref (a & ~b & ~c) in let f = ref 0 in while !e <> 0 do variant { cardinal (bits !e) } let d = !e & (- !e) in f += t1 (a - d) ((b+d) * 2) ((c+d)/2); e -= d done; !f end else 1 (* warmup 2: termination of the recursive function *) let rec t2 (a b c : int) variant { cardinal (bits a) } = if a <> 0 then begin let e = ref (a & ~b & ~c) in let f = ref 0 in while !e <> 0 do invariant { subset (bits !e) (bits a) } let d = !e & (- !e) in assert { bits d = singleton (min_elt (bits !e)) }; f += t2 (a - d) ((b+d) * 2) ((c+d)/2); e -= d done; !f end else 1 end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/queens.gui" End: *)
 (* 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). 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 (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 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)). 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). Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Definition elts (a:Type)(u:(array a)): (map Z a) := match u with | mk_array _ elts1 => elts1 end. Implicit Arguments elts. Definition length (a:Type)(u:(array a)): Z := match u with | mk_array length1 _ => length1 end. Implicit Arguments length. Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. Definition set2 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := match a1 with | mk_array xcl0 _ => (mk_array xcl0 (set1 (elts a1) i v)) end. Implicit Arguments set2. (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) 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 /\ ((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)))))). (* 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 H8. apply subset_remove; auto. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -3,47 +3,70 @@ theory Set type set 'a (* membership *) predicate mem 'a (set 'a) (* equality *) predicate (==) (s1 s2: set 'a) = forall x : 'a. mem x s1 <-> mem x s2 axiom extensionality: forall s1 s2: set 'a. s1 == s2 -> s1 = s2 (* inclusion *) predicate subset (s1 s2: set 'a) = forall x : 'a. mem x s1 -> mem x s2 lemma subset_trans: forall s1 s2 s3: set 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3 (* empty set *) function empty : set 'a predicate is_empty (s : set 'a) = forall x : 'a. not mem x s predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s) axiom Empty_def1 : is_empty(empty : set 'a) axiom empty_def1: is_empty (empty : set 'a) (* addition *) function add 'a (set 'a) : set 'a axiom Add_def1 : forall x y : 'a. forall s : set 'a. axiom add_def1: forall x y: 'a. forall s: set 'a. mem x (add y s) <-> x = y \/ mem x s function singleton (x: 'a) : set 'a = add x empty (* removal *) function remove 'a (set 'a) : set 'a axiom Remove_def1 : forall x y : 'a. forall s : set 'a. axiom remove_def1: forall x y : 'a, s : set 'a. mem x (remove y s) <-> x <> y /\ mem x s lemma subset_remove: forall x: 'a, s: set 'a. subset (remove x s) s (* union *) function union (set 'a) (set 'a) : set 'a axiom Union_def1 : forall s1 s2 : set 'a. forall x : 'a. axiom union_def1: forall s1 s2: set 'a, x: 'a. mem x (union s1 s2) <-> mem x s1 \/ mem x s2 (* intersection *) function inter (set 'a) (set 'a) : set 'a axiom Inter_def1 : forall s1 s2 : set 'a. forall x : 'a. axiom inter_def1: forall s1 s2: set 'a, x: 'a. mem x (inter s1 s2) <-> mem x s1 /\ mem x s2 (* difference *) function diff (set 'a) (set 'a) : set 'a axiom Diff_def1 : forall s1 s2 : set 'a. forall x : 'a. mem x (diff s1 s2) <-> mem x s1 /\ not mem x s2 predicate equal(s1 s2 : set 'a) = forall x : 'a. mem x s1 <-> mem x s2 axiom diff_def1: forall s1 s2: set 'a, x: 'a. mem x (diff s1 s2) <-> mem x s1 /\ not (mem x s2) predicate subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2 lemma subset_diff: forall s1 s2: set 'a. subset (diff s1 s2) s1 end ... ... @@ -54,23 +77,53 @@ theory Fset function cardinal (set 'a) : int axiom Cardinal_nonneg : forall s : set 'a. cardinal s >= 0 axiom cardinal_nonneg: forall s: set 'a. cardinal s >= 0 axiom Cardinal_empty : cardinal(empty : set 'a) = 0 axiom cardinal_empty: forall s: set 'a. cardinal s = 0 <-> is_empty s axiom Cardinal_add : axiom cardinal_add: forall x : 'a. forall s : set 'a. not mem x s -> cardinal (add x s) = 1 + cardinal s not (mem x s) -> cardinal (add x s) = 1 + cardinal s axiom Cardinal_remove : axiom cardinal_remove: forall x : 'a. forall s : set 'a. mem x s -> cardinal s = 1 + cardinal (remove x s) axiom Cardinal_subset : axiom cardinal_subset: forall s1 s2 : set 'a. subset s1 s2 -> cardinal s1 <= cardinal s2 end (* finite sets of integers *) theory Fsetint use export int.Int use export Fset function min_elt (set int) : int axiom min_elt_def1: forall s: set int. not (is_empty s) -> mem (min_elt s) s axiom min_elt_def2: forall s: set int. not (is_empty s) -> forall x: int. mem x s -> min_elt s <= x function max_elt (set int) : int axiom max_elt_def1: forall s: set int. not (is_empty s) -> mem (max_elt s) s axiom max_elt_def2: forall s: set int. not (is_empty s) -> forall x: int. mem x s -> x <= max_elt s (* the set {0,1,...,n-1} *) function below int : set int axiom below_def: forall x n: int. mem x (below n) <-> 0 <= x < n end theory FsetExt use export Fset ... ... @@ -90,7 +143,7 @@ theory SetMap function empty : set 'a = const False predicate is_empty (s : set 'a) = forall x : 'a. not mem x s predicate is_empty (s : set 'a) = forall x : 'a. not (mem x s) goal Empty_def1 : is_empty(empty : set 'a) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!