cleaning up vstte10 queens example

examples/programs/vstte10_queens.mlw

@@ -6,8 +6,6 @@ module M
   use import int.Int
   use import module stdlib.Array
 
-  type map 'a = t int 'a
-
   logic consistent_row (board : map int) (pos : int) (q : int) = 
     board[q] <> board[pos] and
     board[q] - board[pos] <> pos - q and
@@ -50,7 +48,14 @@ let check_is_consistent (board : array int) pos =
     forall q:int. 0 <= q < pos -> is_consistent board q
 
   logic eq_board (b1 b2 : map int) (pos : int) =
-    forall q:int. 0 <= q < pos -> b2[q] = b1[q]
+    forall q:int. 0 <= q < pos -> b1[q] = b2[q]
+
+  lemma eq_board_extension :
+    forall b1 b2 : map int, pos : int.
+    eq_board b1 b2 pos -> b1[pos] = b2[pos] -> eq_board b1 b2 (pos+1)
+
+  lemma arith1 : forall x y : int. x < y+1 -> x <= y
+  lemma arith2 : forall x y : int. x < y -> x+1 <= y
 
   lemma Is_consistent_eq :
     forall b1 b2 : map int, pos : int.
@@ -58,7 +63,7 @@ let check_is_consistent (board : array int) pos =
 
   lemma Solution_eq_board :
     forall b1 b2 : map int, pos : int. length b1 = length b2 ->
-    eq_board b2 b1 pos -> solution b1 pos -> solution b2 pos
+    eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos
 
   lemma Eq_board_set :
     forall b : map int, pos q i : int.

examples/programs/vstte10_queens/Is_consistent.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter ghost : forall (a:Type), Type.
+
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Parameter t : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (t a b) -> a  -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (t a b) -> a -> b  -> (t a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(t a b)), forall (a1:a)
+  (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(t a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter create_const: forall (b:Type) (a:Type), b  -> (t a b).
+
+Set Contextual Implicit.
+Implicit Arguments create_const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (create_const(b1):(t a b)) a1) = b1).
+
+Definition map (a:Type) := (t Z a).
+
+Parameter length: forall (a:Type), (t Z a)  -> Z.
+
+Implicit Arguments length.
+
+Axiom Length_non_negative : forall (a:Type), forall (a1:(t Z a)),
+  (0%Z <= (length a1))%Z.
+
+Axiom Length_set : forall (a:Type), forall (a1:(t Z a)), forall (k:Z),
+  forall (v:a), ((length (set a1 k v)) = (length a1)).
+
+Parameter create_const_length: forall (a:Type), a -> Z  -> (t Z a).
+
+Implicit Arguments create_const_length.
+
+Axiom Create_const_length_get : forall (a:Type), forall (b:a), forall (n:Z)
+  (i:Z), ((get (create_const_length b n) i) = b).
+
+Axiom Create_const_length_length : forall (a:Type), forall (a1:a),
+  forall (n:Z), (0%Z <= n)%Z -> ((length (create_const_length a1 n)) = n).
+
+Parameter create_length: forall (a:Type), Z  -> (t Z a).
+
+Set Contextual Implicit.
+Implicit Arguments create_length.
+Unset Contextual Implicit.
+
+Axiom Create_length_length : forall (a:Type), forall (n:Z), (0%Z <= n)%Z ->
+  ((length (create_length(n):(t Z a))) = n).
+
+Parameter array : forall (a:Type), Type.
+
+Definition consistent_row(board:(t Z Z)) (pos:Z) (q:Z): Prop :=
+  (~ ((get board q) = (get board pos))) /\ ((~ (((get board q) - (get board
+  pos))%Z = (pos - q)%Z)) /\ ~ (((get board pos) - (get board
+  q))%Z = (pos - q)%Z)).
+
+Definition is_consistent(board:(t Z Z)) (pos:Z): Prop := forall (q:Z),
+  ((0%Z <= q)%Z /\ (q <  pos)%Z) -> (consistent_row board pos q).
+
+Axiom Is_consistent_set : forall (board:(t Z Z)) (pos:Z) (q:Z) (i:Z),
+  (is_consistent board pos) -> ((pos <  q)%Z -> (is_consistent (set board q
+  i) pos)).
+
+Definition is_board(board:(t Z Z)) (pos:Z): Prop := forall (q:Z),
+  ((0%Z <= q)%Z /\ (q <  pos)%Z) -> ((0%Z <= (get board q))%Z /\ ((get board
+  q) <  (length board))%Z).
+
+Definition solution(board:(t Z Z)) (pos:Z): Prop := (is_board board pos) /\
+  forall (q:Z), ((0%Z <= q)%Z /\ (q <  pos)%Z) -> (is_consistent board q).
+
+Definition eq_board(b1:(t Z Z)) (b2:(t Z Z)) (pos:Z): Prop := forall (q:Z),
+  ((0%Z <= q)%Z /\ (q <  pos)%Z) -> ((get b1 q) = (get b2 q)).
+
+Axiom eq_board_extension : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
+  (eq_board b1 b2 pos) -> (((get b1 pos) = (get b2 pos)) -> (eq_board b1 b2
+  (pos + 1%Z)%Z)).
+
+Theorem Is_consistent_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
+  (eq_board b1 b2 (pos + 1%Z)%Z) -> ((is_consistent b1 pos) ->
+  (is_consistent b2 pos)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+unfold is_consistent, eq_board, consistent_row.
+intros.
+destruct (H0 q); intuition.
+apply H2.
+rewrite H; intuition.
+rewrite H; intuition.
+apply H1.
+rewrite H; intuition.
+rewrite H; intuition.
+apply H6.
+rewrite H; intuition.
+rewrite H; intuition.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/vstte10_queens/Solution_eq_board.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter ghost : forall (a:Type), Type.
+
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Parameter t : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (t a b) -> a  -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (t a b) -> a -> b  -> (t a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(t a b)), forall (a1:a)
+  (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(t a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter create_const: forall (b:Type) (a:Type), b  -> (t a b).
+
+Set Contextual Implicit.
+Implicit Arguments create_const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (create_const(b1):(t a b)) a1) = b1).
+
+Definition map (a:Type) := (t Z a).
+
+Parameter length: forall (a:Type), (t Z a)  -> Z.
+
+Implicit Arguments length.
+
+Axiom Length_non_negative : forall (a:Type), forall (a1:(t Z a)),
+  (0%Z <= (length a1))%Z.
+
+Axiom Length_set : forall (a:Type), forall (a1:(t Z a)), forall (k:Z),
+  forall (v:a), ((length (set a1 k v)) = (length a1)).
+
+Parameter create_const_length: forall (a:Type), a -> Z  -> (t Z a).
+
+Implicit Arguments create_const_length.
+
+Axiom Create_const_length_get : forall (a:Type), forall (b:a), forall (n:Z)
+  (i:Z), ((get (create_const_length b n) i) = b).
+
+Axiom Create_const_length_length : forall (a:Type), forall (a1:a),
+  forall (n:Z), (0%Z <= n)%Z -> ((length (create_const_length a1 n)) = n).
+
+Parameter create_length: forall (a:Type), Z  -> (t Z a).
+
+Set Contextual Implicit.
+Implicit Arguments create_length.
+Unset Contextual Implicit.
+
+Axiom Create_length_length : forall (a:Type), forall (n:Z), (0%Z <= n)%Z ->
+  ((length (create_length(n):(t Z a))) = n).
+
+Parameter array : forall (a:Type), Type.
+
+Definition consistent_row(board:(t Z Z)) (pos:Z) (q:Z): Prop :=
+  (~ ((get board q) = (get board pos))) /\ ((~ (((get board q) - (get board
+  pos))%Z = (pos - q)%Z)) /\ ~ (((get board pos) - (get board
+  q))%Z = (pos - q)%Z)).
+
+Definition is_consistent(board:(t Z Z)) (pos:Z): Prop := forall (q:Z),
+  ((0%Z <= q)%Z /\ (q <  pos)%Z) -> (consistent_row board pos q).
+
+Axiom Is_consistent_set : forall (board:(t Z Z)) (pos:Z) (q:Z) (i:Z),
+  (is_consistent board pos) -> ((pos <  q)%Z -> (is_consistent (set board q
+  i) pos)).
+
+Definition is_board(board:(t Z Z)) (pos:Z): Prop := forall (q:Z),
+  ((0%Z <= q)%Z /\ (q <  pos)%Z) -> ((0%Z <= (get board q))%Z /\ ((get board
+  q) <  (length board))%Z).
+
+Definition solution(board:(t Z Z)) (pos:Z): Prop := (is_board board pos) /\
+  forall (q:Z), ((0%Z <= q)%Z /\ (q <  pos)%Z) -> (is_consistent board q).
+
+Definition eq_board(b1:(t Z Z)) (b2:(t Z Z)) (pos:Z): Prop := forall (q:Z),
+  ((0%Z <= q)%Z /\ (q <  pos)%Z) -> ((get b1 q) = (get b2 q)).
+
+Axiom eq_board_extension : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
+  (eq_board b1 b2 pos) -> (((get b1 pos) = (get b2 pos)) -> (eq_board b1 b2
+  (pos + 1%Z)%Z)).
+
+Axiom Is_consistent_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
+  (eq_board b1 b2 (pos + 1%Z)%Z) -> ((is_consistent b1 pos) ->
+  (is_consistent b2 pos)).
+
+Theorem Solution_eq_board : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
+  ((length b1) = (length b2)) -> ((eq_board b1 b2 pos) -> ((solution b1
+  pos) -> (solution b2 pos))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+unfold eq_board, solution, is_board.
+intuition.
+rewrite <- H0; intuition.
+destruct (H2 q); intuition.
+rewrite <- H0; intuition.
+destruct (H2 q); intuition.
+apply Is_consistent_eq with b1; intuition.
+red; intros.
+intuition.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

theories/array.why

@@ -34,16 +34,18 @@ theory ArrayLength "Theory of arrays with length"
 
   use export Array
 
-  logic length (t int 'a) : int
+  type map 'a = t int 'a
+
+  logic length (map 'a) : int
 
   axiom Length_non_negative (* "Array length is always non negative" *):
-    forall a : t int 'a. length a >= 0
+    forall a : map 'a. length a >= 0
 
   axiom Length_set : 
-    forall a : t int 'a. forall k : int. forall v : 'a.
+    forall a : map 'a. forall k : int. forall v : 'a.
     length (set a k v) = length a
 
-  logic create_const_length 'a int : t int 'a
+  logic create_const_length 'a int : map 'a
     (* [create_const_length x n] is the array of length n
        with all cells initialized to x 
        (not specified if n is negative)
@@ -57,12 +59,12 @@ theory ArrayLength "Theory of arrays with length"
       (* premise needed to guaranty length >= 0 invariant *)
        n >= 0 -> length (create_const_length a n) = n
 
-  logic create_length int : t int 'a
+  logic create_length int : map 'a
 
   axiom Create_length_length : 
     forall n : int. 
       (* premise needed to guaranty length >= 0 invariant *)
-      n >=0 -> length (create_length n : t int 'a) = n
+      n >=0 -> length (create_length n : map 'a) = n
 
 end
 
@@ -75,10 +77,10 @@ theory ArraySorted
 
   logic le elt elt
 
-  logic sorted_sub (a : t int elt) (l u : int) =
+  logic sorted_sub (a : map elt) (l u : int) =
     forall i1 i2 : int. l <= i1 <= i2 <= u -> le a[i1] a[i2]
 
-  logic sorted (a : t int elt) =
+  logic sorted (a : map elt) =
     sorted_sub a 0 (length a - 1)
 
 end
@@ -88,10 +90,10 @@ theory ArrayEq
   use import int.Int
   use export ArrayLength
 
-  logic array_eq_sub (a1 a2 : t int 'a) (l u : int) = 
+  logic array_eq_sub (a1 a2 : map 'a) (l u : int) = 
     forall i:int. l <= i <= u -> a1[i] = a2[i]
 
-  logic array_eq (a1 a2 : t int 'a) =
+  logic array_eq (a1 a2 : map 'a) =
     length a1 = length a2 and
     forall i:int. 0 <= i < length a1 -> a1[i] = a2[i]
 
@@ -102,54 +104,54 @@ theory ArrayPermut
   use import int.Int
   use export ArrayLength
 
-  logic exchange (a1 a2 : t int 'a) (i j : int) = 
+  logic exchange (a1 a2 : map 'a) (i j : int) = 
     length a1 = length a2 and
     a1[i] = a2[j] and a2[i] = a1[j] and
     forall k:int. (k <> i and k <> j) -> a1[k] = a2[k]
 
   lemma exchange_set :
-    forall a : t int 'a. forall i j : int.
+    forall a : map 'a. forall i j : int.
     exchange a (set (set a i a[j]) j a[i]) i j
 
-  inductive permut (t int 'a) (t int 'a) int int =
+  inductive permut (map 'a) (map 'a) int int =
   | permut_refl :
-      forall a : t int 'a. forall l u : int. permut a a l u
+      forall a : map 'a. forall l u : int. permut a a l u
   | permut_sym :
-      forall a1 a2 : t int 'a. forall l u : int.
+      forall a1 a2 : map 'a. forall l u : int.
       permut a1 a2 l u -> permut a2 a1 l u
   | permut_trans :
-      forall a1 a2 a3 : t int 'a. forall l u : int.
+      forall a1 a2 a3 : map 'a. forall l u : int.
       permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u
   | permut_exchange :
-      forall a1 a2 : t int 'a. forall l u i j : int.
+      forall a1 a2 : map 'a. forall l u i j : int.
       l <= i <= u -> l <= j <= u -> exchange a1 a2 i j -> permut a1 a2 l u
 
   lemma permut_weakening :
-    forall a1 a2 : t int 'a. forall l1 r1 l2 r2 : int.
+    forall a1 a2 : map 'a. forall l1 r1 l2 r2 : int.
     l1 <= l2 <= r2 <= r1 -> permut a1 a2 l2 r2 -> permut a1 a2 l1 r1
 
   lemma permut_eq :
-    forall a1 a2 : t int 'a. forall l u : int.
+    forall a1 a2 : map 'a. forall l u : int.
     l <= u -> permut a1 a2 l u ->
     forall i:int. (i < l or u < i) -> a2[i] = a1[i]
 
   lemma permut_length :
-    forall a1 a2 : t int 'a. forall l u : int.
+    forall a1 a2 : map 'a. forall l u : int.
     permut a1 a2 l u -> length a1 = length a2
 
   lemma permut_exists :
-    forall a1 a2 : t int 'a. forall l u : int.
+    forall a1 a2 : map 'a. forall l u : int.
     permut a1 a2 l u -> 
     forall i : int. l <= i <= u ->
     exists j : int. l <= j <= u and a2[i] = a1[j]
 
-  logic permutation (a1 a2 : t int 'a) =
+  logic permutation (a1 a2 : map 'a) =
     permut a1 a2 0 (length a1 - 1)
 
   use export ArrayEq
 
   lemma array_eq_permut :
-    forall a1 a2 : t int 'a. forall l u : int.
+    forall a1 a2 : map 'a. forall l u : int.
     array_eq_sub a1 a2 l u -> permut a1 a2 l u
 
 end
@@ -160,22 +162,22 @@ theory ArrayRich
   
   use export ArrayLength
 
-  logic sub (t int 'a) int int : t int 'a
+  logic sub (map 'a) int int : map 'a
 
   axiom Sub_length : 
-    forall s : t int 'a, ofs len : int. length (sub s ofs len) = len
+    forall s : map 'a, ofs len : int. length (sub s ofs len) = len
 
   axiom Sub_get :
-    forall s : t int 'a, ofs len i : int. 
+    forall s : map 'a, ofs len i : int. 
     get (sub s ofs len) i = get s (ofs + i)
 
-  logic app (t int 'a) (t int 'a) : t int 'a
+  logic app (map 'a) (map 'a) : map 'a
 
   axiom App_length : 
-    forall s1 s2 : t int 'a. length (app s1 s2) = length s1 + length s2
+    forall s1 s2 : map 'a. length (app s1 s2) = length s1 + length s2
 
   axiom App_get :
-    forall s1 s2 : t int 'a, i : int. 
+    forall s1 s2 : map 'a, i : int. 
     get (app s1 s2) i = 
       if i < length s1 then get s1 i else get s2 (i - length s1)