Commit 9ac18bf3 by Jean-Christophe Filliâtre

### updated proof for VSTTE'10 problem 4

parent be01c33b
 (* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 4: N-queens *) module M module NQueens use import int.Int use import module array.Array ... ... @@ -47,7 +47,7 @@ module M let check_is_consistent (board: array int) pos = { 0 <= pos < length board } try for q = 0 to pos-1 do 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 ... ...
 (* 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 label : Type. Parameter at1: forall (a:Type), a -> label -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Parameter map : forall (a:Type) (b:Type), Type. Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. Implicit Arguments get. Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). Implicit Arguments set. Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map 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:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set 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 set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := match a1 with | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v)) end. Implicit Arguments set1. Definition eq_board(b1:(array Z)) (b2:(array Z)) (pos:Z): Prop := forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> ((get1 b1 q) = (get1 b2 q)). Axiom eq_board_set : forall (b:(array Z)) (pos:Z) (q:Z) (i:Z), (pos <= q)%Z -> (eq_board b (set1 b q i) pos). Axiom eq_board_sym : forall (b1:(array Z)) (b2:(array Z)) (pos:Z), (eq_board b1 b2 pos) -> (eq_board b2 b1 pos). Axiom eq_board_trans : forall (b1:(array Z)) (b2:(array Z)) (b3:(array Z)) (pos:Z), (eq_board b1 b2 pos) -> ((eq_board b2 b3 pos) -> (eq_board b1 b3 pos)). Axiom eq_board_extension : forall (b1:(array Z)) (b2:(array Z)) (pos:Z), (eq_board b1 b2 pos) -> (((get1 b1 pos) = (get1 b2 pos)) -> (eq_board b1 b2 (pos + 1%Z)%Z)). Definition consistent_row(board:(array Z)) (pos:Z) (q:Z): Prop := (~ ((get1 board q) = (get1 board pos))) /\ ((~ (((get1 board q) - (get1 board pos))%Z = (pos - q)%Z)) /\ ~ (((get1 board pos) - (get1 board q))%Z = (pos - q)%Z)). Axiom consistent_row_eq : forall (b1:(array Z)) (b2:(array Z)) (pos:Z), (eq_board b1 b2 (pos + 1%Z)%Z) -> forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> ((consistent_row b1 pos q) -> (consistent_row b2 pos q)). Definition is_consistent(board:(array Z)) (pos:Z): Prop := forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> (consistent_row board pos q). Axiom is_consistent_eq : forall (b1:(array Z)) (b2:(array Z)) (pos:Z), (eq_board b1 b2 (pos + 1%Z)%Z) -> ((is_consistent b1 pos) -> (is_consistent b2 pos)). Definition is_board(board:(array Z)) (pos:Z): Prop := forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> ((0%Z <= (get1 board q))%Z /\ ((get1 board q) < (length board))%Z). Definition solution(board:(array Z)) (pos:Z): Prop := (is_board board pos) /\ forall (q:Z), ((0%Z <= q)%Z /\ (q < pos)%Z) -> (is_consistent board q). Theorem solution_eq_board : forall (b1:(array Z)) (b2:(array 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 solution, eq_board, is_board, is_consistent; intuition. rewrite <- H0; generalize (H2 q); auto with *. rewrite <- H0; generalize (H2 q); auto with *. unfold consistent_row in *. assert (hq: (0 <= q < pos)%Z) by omega. assert (hq0: (0 <= q0 < q)%Z) by omega. generalize (H3 q hq q0 hq0). do 2 (rewrite <- H0; try omega). Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -2,136 +2,56 @@ ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!