Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 01831d42 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

vstte 10, aqueue: simplification

parent c52a5c26
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 636 deletions
examples/programs/vstte10_aqueue.mlw
+ 3
− 3
View file @ 01831d42
......@@ -6,6 +6,7 @@
use export list.Length
use export list.Append
use export list.Reverse
use export list.HdTl
type queue 'a = Q (front : list 'a) (lenf : int)
(rear : list 'a) (lenr : int)
......@@ -40,7 +41,7 @@ let head (q : queue 'a) =
| Nil -> absurd
| Cons x _ -> x
end
{ match model q with Nil -> false | Cons x _ -> result = x end }
{ hd (model q) = Some result }
let tail (q : queue 'a) =
{ inv q and model q <> Nil }
......@@ -48,8 +49,7 @@ let tail (q : queue 'a) =
| Nil -> absurd
| Cons _ r -> create r (lenf q - 1) (rear q) (lenr q)
end
{ inv result and
match model q with Nil -> false | Cons _ r -> model result = r end }
{ inv result and tl (model q) = Some (model result) }
let enqueue (x : 'a) (q : queue 'a) =
{ inv q }
......
examples/programs/vstte10_inverting/project.db
+ 0
− 0
View file @ 01831d42
No preview for this file type
examples/programs/vstte10_inverting/vstte10_inverting.mlw_Pgm_WP_inverting.v deleted 100644 → 0
+ 0
− 122
View file @ c52a5c26
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter arrow : forall (a:Type) (b:Type), Type.
Parameter ref : forall (a:Type), Type.
Parameter prefix_ex: forall (a:Type), (ref a) -> a.
Implicit Arguments prefix_ex.
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 exn : Type.
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
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).
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).
Definition array a := (t Z a).
Definition injective(a1:(t Z Z)) (n:Z): Prop := forall (i:Z) (j:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) ->
((~ (i = j)) -> ~ ((get a1 i) = (get a1 j)))).
Definition surjective(a2:(t Z Z)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\
((get a2 j) = i).
Definition range(a3:(t Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> ((0%Z <= (get a3 i))%Z /\ ((get a3 i) < n)%Z).
Axiom Injective_surjective : forall (a4:(t Z Z)) (n:Z), (injective a4 n) ->
((range a4 n) -> (surjective a4 n)).
Theorem WP_inverting : forall (n:Z), forall (b:(t Z Z)), forall (a5:(t Z Z)),
((**) (0%Z <= n)%Z /\ ((**) ((**) ((length a5) = n)) /\
((**) ((**) ((length b) = n)) /\ ((**) ((**) (injective a5 n)) /\
((**) (range a5 n)))))) -> ((0%Z <= (n - 1%Z)%Z)%Z -> forall (b1:(t Z Z)),
((**) ((**) ((length b1) = n)) /\ forall (j:Z),
((**) ((**) ((**) (0%Z <= j)%Z) /\
((**) (j < ((n - 1%Z)%Z + 1%Z)%Z)%Z)) -> ((**) ((get b1 (get a5
j)) = j)))) -> ((**) (injective b1 n))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
unfold injective; intros.
assert (Hs : surjective a5 n).
apply Injective_surjective; auto.
unfold surjective in Hs.
generalize (Hs i H4); intros (i0, (hi01, hi02)).
generalize (Hs j H8); intros (j0, (hj01, hj02)).
rewrite <- hi02.
rewrite <- hj02.
rewrite H7.
rewrite H7.
red; intro.
rewrite H10 in hi02.
omega.
omega.
omega.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/vstte10_queens/project.db
+ 0
− 0
View file @ 01831d42
No preview for this file type
examples/programs/vstte10_queens/vstte10_queens.mlw_Pgm_Is_consistent_eq.v deleted 100644 → 0
+ 0
− 122
View file @ c52a5c26
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter arrow : forall (a:Type) (b:Type), Type.
Parameter ref : forall (a:Type), Type.
Parameter prefix_ex: forall (a:Type), (ref a) -> a.
Implicit Arguments prefix_ex.
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 exn : Type.
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
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).
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).
Definition array a := (t Z a).
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 b2 q) = (get b1 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; intros.
destruct (H0 q H1).
split.
repeat (rewrite H); auto.
omega.
omega.
destruct H3. split.
repeat (rewrite H); auto.
omega.
omega.
repeat (rewrite H); auto.
omega.
omega.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/vstte10_queens/vstte10_queens.mlw_Pgm_Is_consistent_set.v deleted 100644 → 0
+ 0
− 99
View file @ c52a5c26
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter arrow : forall (a:Type) (b:Type), Type.
Parameter ref : forall (a:Type), Type.
Parameter prefix_ex: forall (a:Type), (ref a) -> a.
Implicit Arguments prefix_ex.
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 exn : Type.
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
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).
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).
Definition array a := (t Z a).
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).
Theorem 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)).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold is_consistent; unfold consistent_row; intros.
assert (q <> q0) by omega.
repeat (rewrite Select_neq); auto.
omega.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/vstte10_queens/vstte10_queens.mlw_Pgm_Solution_eq_board.v deleted 100644 → 0
+ 0
− 125
View file @ c52a5c26
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter arrow : forall (a:Type) (b:Type), Type.
Parameter ref : forall (a:Type), Type.
Parameter prefix_ex: forall (a:Type), (ref a) -> a.
Implicit Arguments prefix_ex.
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 exn : Type.
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
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).
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).
Definition array a := (t Z a).
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 b2 q) = (get b1 q)).
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 b2 b1 pos) -> ((solution b1
pos) -> (solution b2 pos))).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold solution; unfold eq_board.
unfold is_board; intros.
split; intros q Hq.
rewrite <- H.
rewrite <- H0; auto.
destruct H1.
auto.
apply Is_consistent_eq with b1; auto.
unfold eq_board.
intros; rewrite H0; auto.
omega.
intuition.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/vstte10_queens/vstte10_queens.mlw_Pgm_WP_bt_queens.v deleted 100644 → 0
+ 0
− 165
View file @ c52a5c26
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter arrow : forall (a:Type) (b:Type), Type.
Parameter ref : forall (a:Type), Type.
Parameter prefix_ex: forall (a:Type), (ref a) -> a.
Implicit Arguments prefix_ex.
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 exn : Type.
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
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).
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).
Definition array a := (t Z a).
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 b2 q) = (get b1 q)).
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)).
Axiom Solution_eq_board : forall (b1:(t Z Z)) (b2:(t Z Z)) (pos:Z),
((length b1) = (length b2)) -> ((eq_board b2 b1 pos) -> ((solution b1
pos) -> (solution b2 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).
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)).
Theorem WP_bt_queens : forall (n:Z), forall (pos:Z), forall (board:(t Z Z)),
((**) ((**) ((length board) = n)) /\ ((**) ((**) ((**) (0%Z <= pos)%Z) /\
((**) (pos <= n)%Z)) /\ ((**) (solution board pos)))) ->
((~ ((*WP*) (pos = n))) -> ((0%Z <= (n - 1%Z)%Z)%Z -> forall (board1:(t Z
Z)), forall (i:Z), ((*asym_split*) (0%Z <= i)%Z /\ (i <= (n - 1%Z)%Z)%Z) ->
(((**) ((**) ((length board1) = n)) /\ ((**) ((**) (eq_board board1 board
pos)) /\ forall (b:(t Z Z)), ((**) ((**) ((length b) = n)) ->
((**) ((**) (is_board b n)) -> ((**) ((**) (eq_board board1 b pos)) ->
((**) ((**) ((**) (0%Z <= (get b pos))%Z) /\ ((**) ((get b
pos) < i)%Z)) -> ((**) ~ ((**) (solution b n))))))))) -> (((*call pre*)
(**) ((**) (0%Z <= pos)%Z) /\ ((**) (pos < (length board1))%Z)) ->
(((**) (eq_board (set board1 pos i) board pos)) -> (((*call pre*)
(**) ((**) (0%Z <= pos)%Z) /\ ((**) (pos < (length (set board1 pos
i)))%Z)) -> forall (result:bool), ((**) ((**) (result = true)) <->
((**) (is_consistent (set board1 pos i) pos))) ->
((~ ((*WP*) (result = true))) -> forall (b:(t Z Z)),
((**) ((length b) = n)) -> (((**) (is_board b n)) ->
(((**) (eq_board (set board1 pos i) b pos)) -> (((**) ((**) (0%Z <= (get b
pos))%Z) /\ ((**) ((get b pos) < (i + 1%Z)%Z)%Z)) -> ~ ((**) (solution b
n)))))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
assert ((0 <= get b pos < i)%Z \/ get b pos = i) by omega.
destruct H21.
apply H15 with b; auto.
apply Eq_board_trans with (set board1 pos i); auto.
apply Eq_board_trans with board; auto.
apply Eq_board_sym; auto.
unfold solution in H22.
apply H16.
apply H18.
apply Is_consistent_eq with b.
unfold eq_board; intros.
assert (q = pos \/ (q < pos)%Z) by omega.
destruct H26.
rewrite H26; auto.
rewrite Select_eq; auto.
unfold eq_board in H20.
rewrite H20; auto.
omega.
destruct H22.
apply H25.
omega.
Qed.
(* DO NOT EDIT BELOW *)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment