Commit 63c6f2c6 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

cleaning up vstte'10 queens example

parent e5d3e35e
......@@ -6,39 +6,62 @@ module M
use import int.Int
use import module stdlib.Array
logic eq_board (b1 b2 : map int) (pos : int) =
forall q:int. 0 <= q < pos -> b1[q] = b2[q]
lemma eq_board_set :
forall b : map int, pos q i : int.
pos <= q -> eq_board b b[q <- i] pos
lemma eq_board_sym :
forall b1 b2 : map int, pos : int.
eq_board b1 b2 pos -> eq_board b2 b1 pos
lemma eq_board_trans :
forall b1 b2 b3 : map int, pos : int.
eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos
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)
logic consistent_row (board : map int) (pos : int) (q : int) =
board[q] <> board[pos] and
board[q] - board[pos] <> pos - q and
board[pos] - board[q] <> pos - q
lemma consistent_row_eq :
forall b1 b2 : map int, pos q : int. 0 <= q < pos ->
eq_board b1 b2 (pos+1) -> consistent_row b1 pos q -> consistent_row b2 pos q
logic is_consistent (board : map int) (pos : int) =
forall q:int. 0 <= q < pos -> consistent_row board pos q
lemma Is_consistent_set :
forall board : map int, pos q i : int.
is_consistent board pos -> pos < q -> is_consistent board[q <- i] pos
exception Inconsistent
let check_is_consistent (board : array int) pos =
{ 0 <= pos < length board }
try
for q = 0 to pos-1 do
invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
let bq = board[q] in
let bpos = board[pos] in
if bq = bpos then begin
assert { not (consistent_row board pos q) }; (* to help the provers *)
raise Inconsistent
end;
if bq - bpos = pos - q then raise Inconsistent;
if bpos - bq = pos - q then raise Inconsistent
done;
True
with Inconsistent ->
False
end
{ result=True <-> is_consistent board pos }
lemma is_consistent_eq :
forall b1 b2 : map int, pos : int.
eq_board b1 b2 (pos+1) -> is_consistent b1 pos -> is_consistent b2 pos
exception Inconsistent
let check_is_consistent (board : array int) pos =
{ 0 <= pos < length board }
try
for q = 0 to pos-1 do
invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
let bq = board[q] in
let bpos = board[pos] in
if bq = bpos then begin
assert { not (consistent_row board pos q) }; (* to help the provers *)
raise Inconsistent
end;
if bq - bpos = pos - q then raise Inconsistent;
if bpos - bq = pos - q then raise Inconsistent
done;
True
with Inconsistent ->
False
end
{ result=True <-> is_consistent board pos }
logic is_board (board : map int) (pos : int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
......@@ -47,64 +70,38 @@ let check_is_consistent (board : array int) pos =
is_board board pos and
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 -> 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.
eq_board b1 b2 (pos+1) -> is_consistent b1 pos -> is_consistent b2 pos
lemma Solution_eq_board :
lemma solution_eq_board :
forall b1 b2 : map int, pos : int. length b1 = length b2 ->
eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos
lemma Eq_board_set :
forall b : map int, pos q i : int.
pos <= q -> eq_board b b[q <- i] pos
lemma Eq_board_sym :
forall b1 b2 : map int, pos : int.
eq_board b1 b2 pos -> eq_board b2 b1 pos
lemma Eq_board_trans :
forall b1 b2 b3 : map int, pos : int.
eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos
exception Solution
let rec bt_queens (board : array int) n pos variant { n - pos } =
{ length board = n and 0 <= pos <= n and solution board pos }
label Init:( (* FIXME *)
if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
length board = n and eq_board board (at board Init) pos and
exception Solution
let rec bt_queens (board : array int) n pos variant { n - pos } =
{ length board = n and 0 <= pos <= n and solution board pos }
label Init:
if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
length board = n and eq_board board (at board Init) pos and
forall b:map int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
board[pos <- i];
assert { eq_board board (at board Init) pos };
if check_is_consistent board pos then bt_queens board n (pos+1)
done
{ (* no solution *)
length board = n and eq_board board (old board) pos and
forall b:map int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
board[pos <- i];
assert { eq_board board (at board Init) pos };
if check_is_consistent board pos then bt_queens board n (pos+1)
done)
{ (* no solution *)
length board = n and eq_board board (old board) pos and
forall b:map int. length b = n -> is_board b n ->
eq_board board b pos -> not (solution b n) }
| Solution ->
{ (* a solution *)
solution board n }
let queens (board : array int) n =
{ length board = n }
bt_queens board n 0
{ forall b:map int. length b = n -> is_board b n -> not (solution b n) }
| Solution -> { solution board n }
eq_board board b pos -> not (solution b n) }
| Solution ->
{ (* a solution *)
solution board n }
let queens (board : array int) n =
{ length board = n }
bt_queens board n 0
{ forall b:map int. length b = n -> is_board b n -> not (solution b n) }
| Solution -> { solution board n }
end
......
......@@ -79,48 +79,41 @@ Axiom Create_length_length : forall (a:Type), forall (n:Z), (0%Z <= n)%Z ->
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).
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 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)).
Axiom eq_board_set : forall (b:(t Z Z)) (pos:Z) (q:Z) (i:Z), (pos <= q)%Z ->
(eq_board b (set b 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).
Axiom eq_board_sym : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z), (eq_board b1
b2 pos) -> (eq_board b2 b1 pos).
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_trans : forall (b1:(t Z Z)) (b2:(t Z Z)) (b3:(t Z Z)) (pos:Z),
(eq_board b1 b2 pos) -> ((eq_board b2 b3 pos) -> (eq_board b1 b3 pos)).
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),
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)).
Axiom consistent_row_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z) (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((eq_board b1 b2 (pos + 1%Z)%Z) ->
((consistent_row b1 pos q) -> (consistent_row b2 pos q))).
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).
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.
unfold is_consistent, eq_board.
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.
apply consistent_row_eq with b1; auto.
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -79,17 +79,37 @@ Axiom Create_length_length : forall (a:Type), forall (n:Z), (0%Z <= n)%Z ->
Parameter array : forall (a:Type), Type.
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_set : forall (b:(t Z Z)) (pos:Z) (q:Z) (i:Z), (pos <= q)%Z ->
(eq_board b (set b q i) pos).
Axiom eq_board_sym : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z), (eq_board b1
b2 pos) -> (eq_board b2 b1 pos).
Axiom eq_board_trans : forall (b1:(t Z Z)) (b2:(t Z Z)) (b3:(t Z Z)) (pos:Z),
(eq_board b1 b2 pos) -> ((eq_board b2 b3 pos) -> (eq_board b1 b3 pos)).
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)).
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)).
Axiom consistent_row_eq : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z) (q:Z),
((0%Z <= q)%Z /\ (q < pos)%Z) -> ((eq_board b1 b2 (pos + 1%Z)%Z) ->
((consistent_row b1 pos q) -> (consistent_row b2 pos q))).
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)).
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)).
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
......@@ -98,18 +118,7 @@ Definition is_board(board:(t Z Z)) (pos:Z): Prop := forall (q: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),
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 *)
......@@ -119,7 +128,7 @@ rewrite <- H0; intuition.
destruct (H2 q); intuition.
rewrite <- H0; intuition.
destruct (H2 q); intuition.
apply Is_consistent_eq with b1; intuition.
apply is_consistent_eq with b1; intuition.
red; intros.
intuition.
Qed.
......
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