Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 65086408 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

LCP: enhanced spec of permutation

parent dcac9198
......@@ -79,20 +79,20 @@ module LCP "longest common prefix"
use import int.Int
use map.Map
use map.MapInjection
use import array.Array
(* TODO: dire plus precisement que c'est une permutation de 0..b-1 *)
predicate array_bounded (a:array int) (b:int) =
forall i:int. 0 <= i < a.length -> 0 <= a[i] < b
predicate permutation (a:array int) =
MapInjection.range a.elts a.length /\
MapInjection.injective a.elts a.length
use import array.ArrayPermut
lemma permut_permutation :
forall a1 a2:array int, n:int.
permut a1 a2 /\ permutation a1 -> permutation a2
(*
use import array.ArraySorted
*)
use import array.ArrayPermut
lemma permut_bounded :
forall a1 a2:array int, n:int.
permut a1 a2 /\ array_bounded a1 n -> array_bounded a2 n
predicate is_common_prefix (a:array int) (x y:int) (l:int) =
......@@ -101,11 +101,11 @@ predicate is_common_prefix (a:array int) (x y:int) (l:int) =
lemma common_prefix_eq:
forall a:array int, x:int.
0 <= x < a.length -> is_common_prefix a x x (a.length - x)
0 <= x <= a.length -> is_common_prefix a x x (a.length - x)
lemma common_prefix_eq2:
forall a:array int, x:int.
0 <= x < a.length -> not (is_common_prefix a x x (a.length - x + 1))
0 <= x <= a.length -> not (is_common_prefix a x x (a.length - x + 1))
lemma not_common_prefix_if_last_different:
forall a:array int, x y:int, l:int.
......@@ -116,32 +116,32 @@ function longest_common_prefix (a:array int) (x y:int) :int
axiom lcp_spec:
forall a:array int, x y:int, l:int.
0 <= x < a.length /\ 0 <= y < a.length ->
0 <= x <= a.length /\ 0 <= y <= a.length ->
(l = longest_common_prefix a x y <->
is_common_prefix a x y l /\ not is_common_prefix a x y (l+1))
lemma lcp_is_cp :
forall a:array int, x y:int.
0 <= x < a.length /\ 0 <= y < a.length ->
0 <= x <= a.length /\ 0 <= y <= a.length ->
let l = longest_common_prefix a x y in
is_common_prefix a x y l
lemma lcp_eq :
forall a:array int, x y:int.
0 <= x < a.length /\ 0 <= y < a.length ->
0 <= x <= a.length /\ 0 <= y <= a.length ->
let l = longest_common_prefix a x y in
forall i:int. 0 <= i < l -> a[x+i] = a[y+i]
lemma lcp_refl :
forall a:array int, x:int.
0 <= x < a.length -> longest_common_prefix a x x = a.length - x
0 <= x <= a.length -> longest_common_prefix a x x = a.length - x
use import ref.Refint
let lcp (a:array int) (x y:int) : int
requires { 0 <= x < a.length }
requires { 0 <= y < a.length }
requires { 0 <= x <= a.length }
requires { 0 <= y <= a.length }
ensures { result = longest_common_prefix a x y }
= let n = a.length in
let l = ref 0 in
......@@ -181,27 +181,27 @@ let test1 () =
predicate le (a : array int) (x y:int) =
let n = a.length in
0 <= x < n /\ 0 <= y < n /\
0 <= x <= n /\ 0 <= y <= n /\
let l = longest_common_prefix a x y in
x+l = n \/
(x+l < n /\ y+l < n /\ a[x+l] <= a[y+l])
lemma le_refl :
forall a:array int, x :int.
0 <= x < a.length -> le a x x
lemma le_asym :
forall a:array int, x y:int.
0 <= x < a.length /\ 0 <= y < a.length /\ not (le a x y) -> le a y x
0 <= x <= a.length -> le a x x
lemma le_trans :
forall a:array int, x y z:int.
0 <= x < a.length /\ 0 <= y < a.length /\
0 <= z < a.length /\ le a x y /\ le a y z -> le a x z
0 <= x <= a.length /\ 0 <= y <= a.length /\
0 <= z <= a.length /\ le a x y /\ le a y z -> le a x z
lemma le_asym :
forall a:array int, x y:int.
0 <= x <= a.length /\ 0 <= y <= a.length /\ not (le a x y) -> le a y x
let compare (a:array int) (x y:int) : int
requires { 0 <= x < a.length }
requires { 0 <= y < a.length }
requires { 0 <= x <= a.length }
requires { 0 <= y <= a.length }
ensures { result = 0 -> x = y }
ensures { result < 0 -> le a x y }
ensures { result > 0 -> le a y x }
......@@ -219,10 +219,6 @@ let compare (a:array int) (x y:int) : int
predicate sorted_sub (a : array int) (data:array int) (l u:int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a data[i1] data[i2]
lemma sorted_bounded:
forall a data: array int, l u i:int.
l <= i < u /\ sorted_sub a data l u -> 0 <= data[i] < a.length
lemma sorted_le:
forall a data: array int, l u i x:int.
l <= i < u /\ sorted_sub a data l u /\ le a x data[l] ->
......@@ -264,8 +260,8 @@ let compare (a:array int) (x y:int) : int
sorted_sub a data 0 data.length
let sort (a:array int) (data : array int)
(* requires { data.length >= 0 } *)
requires { array_bounded data a.length }
requires { data.length = a.length }
requires { permutation data }
ensures { sorted a data }
ensures { permut (old data) data }
=
......@@ -273,11 +269,11 @@ let compare (a:array int) (x y:int) : int
for i = 0 to data.length - 1 do
invariant { permut (at data 'Init) data }
invariant { sorted_sub a data 0 i }
invariant { array_bounded data a.length }
invariant { permutation data }
let j = ref i in
while !j > 0 && compare a data[!j-1] data[!j] > 0 do
invariant { 0 <= !j <= i }
invariant { array_bounded data a.length }
invariant { permutation data }
invariant { permut (at data 'Init) data }
invariant { sorted_sub a data 0 !j }
invariant { sorted_sub a data !j (i+1) }
......@@ -325,9 +321,10 @@ type suffixArray = {
suffixes : array int;
}
use map.MapInjection
predicate inv(s:suffixArray) =
s.values.length = s.suffixes.length /\
array_bounded s.suffixes s.values.length
s.values.length = s.suffixes.length /\ permutation s.suffixes
let select (s:suffixArray) (i:int) : int
requires { inv s /\ 0 <= i < s.values.length }
......@@ -336,12 +333,12 @@ let select (s:suffixArray) (i:int) : int
let create (a:array int) : suffixArray
requires { a.length >= 0 }
ensures { result.values.length = a.length /\ inv result }
ensures { result.values = a /\ inv result }
=
let n = a.length in
let suf = Array.make n 0 in
for i = 0 to n-1 do
invariant { array_bounded suf n }
invariant { forall j:int. 0 <= j < i -> suf[j] = j }
suf[i] <- i done;
sort a suf;
{ values = a; suffixes = suf }
......@@ -349,6 +346,8 @@ let create (a:array int) : suffixArray
let lcp (s:suffixArray) (i:int) : int
requires { inv s }
requires { 0 < i < s.values.length }
ensures { result =
longest_common_prefix s.values s.suffixes[i] s.suffixes[i-1] }
=
LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
......@@ -357,26 +356,30 @@ let test2 () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let sa = create arr in
assert { sa.suffixes[0] = 0 };
assert { sa.suffixes[1] = 1 };
assert { sa.suffixes[2] = 2 };
assert { sa.suffixes[3] = 3 };
let x = lcp sa 1 in
check {x = -1 (* TODO *)};
check {x = 0};
(* int[] brr = {1,2,3,5}; *)
let brr = Array.make 4 0 in
brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
let sa = create brr in
let x = lcp sa 1 in
check {x = -1 (* TODO *)};
check {x = 0 (* TODO *)};
(* int[] crr = {1,2,3,5}; *)
let crr = Array.make 4 0 in
crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
let sa = create crr in
let x = lcp sa 2 in
check {x = -1 (* TODO *)};
check {x = 0 (* TODO *)};
(* int[] drr = {1,2,3,3}; *)
let drr = Array.make 4 0 in
drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
let sa = create drr in
let x = lcp sa 2 in
check {x = -1 (* TODO *)}
check {x = 0 (* TODO *)}
end
......@@ -389,18 +392,32 @@ module LRS "longest repeated substring"
use import int.Int
use import ref.Ref
use import array.Array
use LCP
use SuffixArray
val solStart : ref int
val solLength : ref int
let lrs (a:array int) : unit
requires { a.length >= 0 }
requires { a.length > 0 }
ensures { 0 <= !solLength <= a.length }
ensures { 0 <= !solStart <= a.length }
ensures { forall x y:int.
0 <= x < a.length /\ 0 <= y <= a.length /\ x <> y ->
!solLength >= LCP.longest_common_prefix a x y }
ensures { exists y:int.
0 <= y <= a.length /\ !solStart <> y /\
!solLength = LCP.longest_common_prefix a !solStart y }
=
let sa = SuffixArray.create a in
solStart := 0;
solLength := 0;
for i=1 to a.length - 1 do
invariant { 0 <= !solLength <= a.length }
invariant { 0 <= !solStart <= a.length }
invariant { exists y:int.
0 <= y <= a.length /\ !solStart <> y /\
!solLength = LCP.longest_common_prefix a !solStart y }
let l = SuffixArray.lcp sa i in
if l > !solLength then begin
solStart := SuffixArray.select sa i;
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
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} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, 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 {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
(get (elts a1) i).
(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
(mk_array n (const v:(map Z a))).
(* Why3 assumption *)
Definition array_bounded(a:(array Z)) (b:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a
i) < b)%Z).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
(l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
(i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1
j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2
k))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)),
forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i
j).
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map Z a) -> (map Z a) -> Z
-> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
(u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z
a)) (a2:(map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\
(l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) ->
(permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
(a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
(a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\
((get a2 i) = (get a1 j)).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j).
(* Why3 assumption *)
Definition permut_sub1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2)
0%Z (length a1)).
Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
(((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) ->
(((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))).
Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)), (permut a1 a2) -> (permut a2 a1).
Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) ->
(permut a1 a3)).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z
(length a1)).
Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l
u) -> (permut_sub1 a1 a2 l u).
Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2).
Axiom permut_bounded : forall (a1:(array Z)) (a2:(array Z)) (n:Z),
((permut a1 a2) /\ (array_bounded a1 n)) -> (array_bounded a2 n).
(* Why3 assumption *)
Definition is_common_prefix(a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\
(((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < l)%Z) -> ((get1 a (x + i)%Z) = (get1 a (y + i)%Z)))).
Axiom common_prefix_eq : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z).
Axiom common_prefix_eq2 : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> ~ (is_common_prefix a x x
(((length a) - x)%Z + 1%Z)%Z).
Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z)
(l:Z), ((0%Z < l)%Z /\ (((x + l)%Z < (length a))%Z /\
(((y + l)%Z < (length a))%Z /\ ~ ((get1 a (x + (l - 1%Z)%Z)%Z) = (get1 a
(y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l).
Parameter longest_common_prefix: (array Z) -> Z -> Z -> Z.
Axiom lcp_spec : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
((l = (longest_common_prefix a x y)) <-> ((is_common_prefix a x y l) /\
~ (is_common_prefix a x y (l + 1%Z)%Z))).
Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
(is_common_prefix a x y (longest_common_prefix a x y)).
Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
forall (i:Z), ((0%Z <= i)%Z /\ (i < (longest_common_prefix a x y))%Z) ->
((get1 a (x + i)%Z) = (get1 a (y + i)%Z)).
Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> ((longest_common_prefix a x
x) = ((length a) - x)%Z).
(* Why3 assumption *)
Definition le(a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in
(((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ let l :=
(longest_common_prefix a x y) in (((x + l)%Z = n) \/ (((x + l)%Z < n)%Z /\
(((y + l)%Z < n)%Z /\ ((get1 a (x + l)%Z) <= (get1 a (y + l)%Z))%Z))))).
Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (le a x x).
Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\
(((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) ->
(le a x z).
Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x
y))) -> (le a y x).
(* Why3 assumption *)
Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop :=
forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) ->
(le a (get1 data i1) (get1 data i2)).
Axiom sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z)
(x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x
(get1 data l)))) -> (le a x (get1 data i)).
Axiom sorted_ge : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z)
(x:Z), ((sorted_sub a data l u) /\ ((le a (get1 data (u - 1%Z)%Z) x) /\
((l <= i)%Z /\ (i < u)%Z))) -> (le a (get1 data i) x).
Axiom sorted_sub_sub : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
(l':Z) (u':Z), ((l <= l')%Z /\ (u' <= u)%Z) -> ((sorted_sub a data l u) ->
(sorted_sub a data l' u')).
Axiom sorted_sub_add : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z),
((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get1 data l) (get1 data
(l + 1%Z)%Z))) -> (sorted_sub a data l u).
Axiom sorted_sub_concat : forall (a:(array Z)) (data:(array Z)) (l:Z) (m:Z)
(u:Z), (((l <= m)%Z /\ (m <= u)%Z) /\ ((sorted_sub a data l m) /\
((sorted_sub a data m u) /\ (le a (get1 data (m - 1%Z)%Z) (get1 data
m))))) -> (sorted_sub a data l u).
Axiom sorted_sub_set : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
(i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a
(set1 data i v) l u).
Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
(i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a
(mk_array (length a) (set (elts data) i v)) l u).
(* Why3 assumption *)
Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data
0%Z (length data)).
(* Why3 assumption *)
Inductive suffixArray :=
| mk_suffixArray : (array Z) -> (array Z) -> suffixArray .
Axiom suffixArray_WhyType : WhyType suffixArray.
Existing Instance suffixArray_WhyType.
(* Why3 assumption *)
Definition suffixes(v:suffixArray): (array Z) :=
match v with
| (mk_suffixArray x x1) => x1
end.
(* Why3 assumption *)
Definition values(v:suffixArray): (array Z) :=
match v with
| (mk_suffixArray x x1) => x
end.
(* Why3 assumption *)
Definition inv(s:suffixArray): Prop :=
((length (values s)) = (length (suffixes s))) /\
(array_bounded (suffixes s) (length (values s))).
Require Import Why3.
(* Why3 goal *)
Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map Z Z)),
(0%Z <= a)%Z -> ((0%Z <= a)%Z -> forall (sa:Z) (sa1:(map Z Z)) (sa2:Z)
(sa3:(map Z Z)), ((sa = a) /\ (inv (mk_suffixArray (mk_array sa sa1)
(mk_array sa2 sa3)))) -> forall (solStart:Z), (solStart = 0%Z) ->
forall (solLength:Z), (solLength = 0%Z) -> ((1%Z <= (a - 1%Z)%Z)%Z ->
exists y:Z, ((0%Z <= y)%Z /\ (y <= a)%Z) /\ ((~ (solStart = y)) /\