New example : Alpha-Beta

examples/programs/alphaBeta.mlw

+
+theory TwoPlayerGame
+
+  use import int.Int
+  use import list.List
+
+
+  (** type describing a position in the game. It must include every
+     needed info, in particular in general it will include whose
+     turn it is. *)
+  type position
+
+  (** type describing a move *)
+  type move
+
+  (** the initial_position of the game *)
+  constant initial_position : position
+
+  (** gives the list of legal moves in the given position *)
+  function legal_moves position : list move
+
+  (** [do_move p m] returns the position obtained by doing the move [m]
+     on position [p]. 
+  *)
+  function do_move position move : position
+
+  (** [position_value p] returns an evaluation of position [p], an
+     integer [v] between [-infinity] and [+infinity] which is supposed
+     to be as higher as the position is good FOR THE PLAYER WHO HAS
+     THE TURN. [v] must be 0 for a position where nobody can win
+     anymore (draw game). For a position where the player who has the
+     turn wins, [v] must be between [winning_value] and [infinity],
+     and if the other player wins, [v] must be between [-infinity] and
+     [-winning_value].
+  *)
+  constant winning_value : int
+  constant infinity : int
+  function position_value position : int
+
+  (*
+
+    [minmax p d] returns the min-max evaluation of position [p] at depth [d].
+    As for [position_value], the value is for the player who has the turn.
+
+  *)
+  function minmax position int : int
+
+  axiom minmax_depth_0 :
+    forall p:position. minmax p 0 = position_value p
+
+  type param = (position,int)
+  function cost (p:param) (m:move) : int =
+    match p with (p,n) -> minmax (do_move p m) n
+    end
+
+  clone import set.Min as MinMaxRec with 
+    type param = param,
+    type elt = move,
+    function cost = cost
+
+  use list.Elements
+  use set.Fset
+
+  axiom minmax_depth_non_zero:
+    forall p:position, n:int. n >= 0 ->
+     minmax p (n+1) = 
+        let moves = Elements.elements (legal_moves p) in
+        if Fset.is_empty moves then position_value p else
+          - MinMaxRec.min (p,n) moves
+
+  use list.Mem
+
+  goal Test:
+    forall p:position, m:move.
+      let moves = legal_moves p in
+      Mem.mem m moves -> - (position_value (do_move p m)) <= minmax p 1
+
+end
+
+
+(*
+
+   alpha-beta
+
+*)
+
+module AlphaBeta
+
+  use import int.Int
+  use import int.MinMax
+
+  use TwoPlayerGame as G
+  use import list.List
+
+  let rec move_value_alpha_beta alpha beta pos max_prof prof move =
+    let pos' = G.do_move pos move in
+    let s =
+      if prof = max_prof
+      then G.position_value pos'
+      else
+	negabeta (-beta) (-alpha) pos' max_prof (prof+1)
+    in -s
+
+  with negabeta alpha beta pos max_prof prof =
+    { }
+    let l = G.legal_moves pos in
+    match l with
+      | Nil -> G.position_value pos
+      | Cons c l ->
+	  let best =
+	    move_value_alpha_beta alpha beta pos max_prof prof c
+	  in
+	  if best >= beta then best else
+	    negabeta_rec (max best alpha) beta pos max_prof prof best l
+    end
+    { result = G.minmax pos (max_prof - prof + 1) }
+
+  with negabeta_rec alpha beta pos max_prof prof best l =
+    match l with
+      |	Nil -> best
+      | Cons c l ->
+	  let s =
+            move_value_alpha_beta alpha beta pos max_prof prof c
+          in
+	  let new_best  = max s best in
+	  if new_best >= beta then new_best else
+   	    negabeta_rec (max new_best alpha) beta pos max_prof prof new_best l
+    end
+
+(* alpha-beta at a given depth *)
+
+let alpha_beta pos depth = 
+  { }
+  negabeta (-G.infinity) G.infinity pos depth 1
+  { result = G.minmax pos depth }
+
+(* iterative deepening *)
+
+(*
+  let best_move_alpha_beta pos =
+    let l =
+      List.map
+	(fun c ->
+	   (move_value_alpha_beta (-G.infinity) G.infinity pos 2 0 c,c))
+	(G.legal_moves pos)
+    in
+    if List.length l < 2 then l else
+      let current_best_moves =
+	ref
+	  (List.sort (fun (x,_) (y,_) -> compare y x) l)
+      in
+      try
+	for max_prof = 3 to 1000 do
+	  begin
+	    match !current_best_moves with
+	      | (v1,_)::(v2,_)::_ ->
+		  if v1 >= G.winning_value or v2 <= - G.winning_value
+		  then raise Timeout
+	      | _ -> assert false
+	  end;
+	  let l =
+	    List.map
+	      (fun c ->
+		 (move_value_alpha_beta (-G.infinity) G.infinity
+		    pos max_prof 0 c,c))
+	      (G.legal_moves pos)
+	  in
+	  current_best_moves :=
+	  (List.sort (fun (x,_) (y,_) -> compare y x) l)
+	done;
+	!current_best_moves
+      with
+	| Timeout -> !current_best_moves
+
+*)
+
+end
+

examples/programs/alphaBeta/alphaBeta_TwoPlayerGame_Test_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 assumption *)
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Parameter position : Type.
+
+Parameter move : Type.
+
+Parameter initial_position: position.
+
+Parameter legal_moves: position -> (list move).
+
+Parameter do_move: position -> move -> position.
+
+Parameter winning_value: Z.
+
+Parameter infinity: Z.
+
+Parameter position_value: position -> Z.
+
+Parameter minmax: position -> Z -> Z.
+
+Axiom minmax_depth_0 : forall (p:position), ((minmax p
+  0%Z) = (position_value p)).
+
+(* Why3 assumption *)
+Definition param  := (position* Z)%type.
+
+(* Why3 assumption *)
+Definition cost(p:(position* Z)%type) (m:move): Z :=
+  match p with
+  | (p1, n) => (minmax (do_move p1 m) n)
+  end.
+
+Parameter set : forall (a:Type), Type.
+
+Parameter mem: forall (a:Type), a -> (set a) -> Prop.
+Implicit Arguments mem.
+
+(* Why3 assumption *)
+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).
+
+(* Why3 assumption *)
+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.
+
+(* Why3 assumption *)
+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 choose: forall (a:Type), (set a) -> a.
+Implicit Arguments choose.
+
+Axiom choose_def : forall (a:Type), forall (s:(set a)), (~ (is_empty s)) ->
+  (mem (choose s) s).
+
+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.
+
+Axiom cardinal1 : forall (a:Type), forall (s:(set a)),
+  ((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
+
+Parameter nth: forall (a:Type), Z -> (set a) -> a.
+Implicit Arguments nth.
+
+Axiom nth_injective : forall (a:Type), forall (s:(set a)) (i:Z) (j:Z),
+  ((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (((0%Z <= j)%Z /\
+  (j < (cardinal s))%Z) -> (((nth i s) = (nth j s)) -> (i = j))).
+
+Axiom nth_surjective : forall (a:Type), forall (s:(set a)) (x:a), (mem x
+  s) -> exists i:Z, ((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (x = (nth i
+  s)).
+
+Parameter min: (position* Z)%type -> (set move) -> Z.
+
+Axiom min_is_a_lower_bound : forall (p:(position* Z)%type) (s:(set move))
+  (x:move), (mem x s) -> ((min p s) <= (cost p x))%Z.
+
+Axiom min_appears_in_set : forall (p:(position* Z)%type) (s:(set move)),
+  (~ (is_empty s)) -> exists x:move, (mem x s) /\ ((cost p x) = (min p s)).
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint mem1 (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem1 x r)
+  end.
+Unset Implicit Arguments.
+
+Parameter elements: forall (a:Type), (list a) -> (set a).
+Implicit Arguments elements.
+
+Axiom elements_mem : forall (a:Type), forall (l:(list a)) (x:a), (mem1 x
+  l) <-> (mem x (elements l)).
+
+Axiom minmax_depth_non_zero : forall (p:position) (n:Z), (0%Z <= n)%Z ->
+  let moves := (elements (legal_moves p)) in (((is_empty moves) -> ((minmax p
+  (n + 1%Z)%Z) = (position_value p))) /\ ((~ (is_empty moves)) -> ((minmax p
+  (n + 1%Z)%Z) = (-(min (p, n) moves))%Z))).
+
+Open Scope Z_scope.
+
+(* Why3 goal *)
+Theorem Test : forall (p:position) (m:move), (mem1 m (legal_moves p)) ->
+  ((-(position_value (do_move p m)))%Z <= (minmax p 1%Z))%Z.
+intros p m h1.
+destruct (minmax_depth_non_zero p 0); auto with zarith.
+clear H.
+replace 1 with (0+1) by omega.
+assert (h: mem m (elements (legal_moves p))).
+  now rewrite <- elements_mem.
+rewrite H0. 
+generalize (min_is_a_lower_bound (p,0) _ _ h).
+simpl.
+rewrite minmax_depth_0.
+omega.
+clear H0.
+unfold is_empty.
+intro H.
+now apply (H m).
+Qed.
+
+

examples/programs/alphaBeta/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
+<why3session
+ name="alphaBeta/why3session.xml" shape_version="2">
+ <prover
+  id="0"
+  name="Alt-Ergo"
+  version="0.94"/>
+ <prover
+  id="1"
+  name="Coq"
+  version="8.3pl3"/>
+ <prover
+  id="2"
+  name="Z3"
+  version="2.19"/>
+ <prover
+  id="3"
+  name="Z3"
+  version="3.2"/>
+ <file
+  name="../alphaBeta.mlw"
+  verified="false"
+  expanded="true">
+  <theory
+   name="TwoPlayerGame"
+   locfile="alphaBeta/../alphaBeta.mlw"
+   loclnum="2" loccnumb="7" loccnume="20"
+   verified="true"
+   expanded="true">
+   <goal
+    name="Test"
+    locfile="alphaBeta/../alphaBeta.mlw"
+    loclnum="73" loccnumb="7" loccnume="11"
+    sum="67b40aee2368f16ea7d0587212ff4945"
+    proved="true"
+    expanded="true"
+    shape="ainfix &lt;=aprefix -aposition_valueado_moveV0V1aminmaxV0c1IamemV1V2Lalegal_movesV0F">
+    <proof
+     prover="2"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.05"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="10"
+     memlimit="1000"
+     edited="alphaBeta_TwoPlayerGame_Test_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.83"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.07"/>
+    </proof>
+   </goal>
+  </theory>
+  <theory
+   name="AlphaBeta"
+   locfile="alphaBeta/../alphaBeta.mlw"
+   loclnum="87" loccnumb="7" loccnume="16"
+   verified="false"
+   expanded="true">
+   <goal
+    name="WP_parameter move_value_alpha_beta"
+    locfile="alphaBeta/../alphaBeta.mlw"
+    loclnum="95" loccnumb="10" loccnume="31"
+    expl="normal postcondition"
+    sum="1166f011b7545b1ba75685a11ad22581"
+    proved="true"
+    expanded="true"
+    shape="t">
+    <label
+     name="expl:parameter move_value_alpha_beta"/>
+    <proof
+     prover="0"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="WP_parameter negabeta"
+    locfile="alphaBeta/../alphaBeta.mlw"
+    loclnum="104" loccnumb="7" loccnume="15"
+    expl="parameter negabeta"
+    sum="9e6b9bade21340c597985f94c1f3ee3f"
+    proved="false"
+    expanded="true"
+    shape="Calegal_movesV1aNilainfix =aposition_valueV1aminmaxV1ainfix +ainfix -V2V3c1aConsVViainfix &gt;=V6V0ainfix =V6aminmaxV1ainfix +ainfix -V2V3c1ainfix =V7aminmaxV1ainfix +ainfix -V2V3c1FFF">
+    <label
+     name="expl:parameter negabeta"/>
+    <proof
+     prover="0"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="WP_parameter negabeta_rec"
+    locfile="alphaBeta/../alphaBeta.mlw"
+    loclnum="118" loccnumb="7" loccnume="19"
+    expl="parameter negabeta_rec"
+    sum="3b961de9787633290d315ec737d261ef"
+    proved="true"
+    expanded="true"
+    shape="CV0aNiltaConsVVtF">
+    <label
+     name="expl:parameter negabeta_rec"/>
+    <proof
+     prover="0"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="WP_parameter alpha_beta"
+    locfile="alphaBeta/../alphaBeta.mlw"
+    loclnum="132" loccnumb="4" loccnume="14"
+    expl="normal postcondition"
+    sum="8ba0807b7798457a268d25f5c06f46d0"
+    proved="true"
+    expanded="true"
+    shape="ainfix =aminmaxV0ainfix +ainfix -V1c1c1aminmaxV0V1F">
+    <label
+     name="expl:parameter alpha_beta"/>
+    <proof
+     prover="0"
+     timelimit="10"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+  </theory>
+ </file>
+</why3session>

theories/list.why

@@ -40,6 +40,20 @@ theory Mem
 
 end
 
+theory Elements
+
+  use import List
+  use Mem
+  use set.Fset as FSet
+
+  function elements (list 'a) : FSet.set 'a
+
+  axiom elements_mem:
+    forall l:list 'a, x:'a.
+      Mem.mem x l <-> FSet.mem x (elements l)
+
+end
+
 (** {2 Nth element of a list} *)
 
 theory Nth
@@ -341,6 +355,7 @@ theory Induction
 
 end
 
+
 (** {2 Maps as lists of pairs} *)
 
 theory Map

theories/set.why

@@ -213,6 +213,30 @@ theory Fsetint
 
 end
 
+(** {2 Finite set iterators} *)
+
+theory Min
+
+  use import Fset
+  use import int.Int
+
+  type param
+
+  type elt
+
+  function cost param elt : int
+
+  function min param (set elt) : int
+
+  axiom min_is_a_lower_bound:
+    forall p:param, s:set elt, x:elt. mem x s -> cost p x >= min p s
+
+  axiom min_appears_in_set:
+    forall p:param, s:set elt. not (is_empty s) ->
+      exists x:elt. mem x s /\ cost p x = min p s
+
+end
+
 (** {2 Sets realized as maps} *)
 
 theory SetMap