Commit 13ffc5b8 authored by MARCHE Claude's avatar MARCHE Claude

LCP: use a type invariant

parent ee8e9fa5
......@@ -71,6 +71,9 @@ comparison on arrays, a sorting routine, and LCP.
The client code (LRS.java) uses these to solve the LRS problem. Verify
that it does so correctly.
(Based on code by Robert Sedgewick and Kevin Wayne.)
*)
......@@ -117,7 +120,7 @@ let lcp (a:array int) (x y:int) : int
!l
(** test harness for lcp *)
let test1 () =
let test () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let x = lcp arr 1 2 in
......@@ -273,13 +276,15 @@ module SuffixArray
use import array.Array
use import LCP
use import PrefixSort
use map.MapInjection
type suffixArray = {
values : array int;
suffixes : array int;
}
use map.MapInjection
invariant { self.values.length = self.suffixes.length /\
permutation self.suffixes.elts self.suffixes.length /\
sorted self.values self.suffixes }
predicate inv(s:suffixArray) =
s.values.length = s.suffixes.length /\
......@@ -287,20 +292,20 @@ predicate inv(s:suffixArray) =
sorted s.values s.suffixes
let select (s:suffixArray) (i:int) : int
requires { inv s /\ 0 <= i < s.values.length }
requires { 0 <= i < s.values.length }
ensures { result = s.suffixes[i] }
= s.suffixes[i]
(* needed to establish invariant in function create *)
use import array.ArrayPermut
use import array.ArrayPermut
(** needed to establish invariant in function create *)
lemma permut_permutation :
forall a1 a2:array int.
permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length
(** constructor of suffixArray structure *)
let create (a:array int) : suffixArray
ensures { result.values = a /\ inv result }
ensures { result.values = a }
=
let n = a.length in
let suf = Array.make n 0 in
......@@ -318,7 +323,7 @@ let lcp (s:suffixArray) (i:int) : int
LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
(*
let test2 () =
let test () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let sa = create arr in
......@@ -470,5 +475,3 @@ use import int.MinMax
end
(* Based on code by Robert Sedgewick and Kevin Wayne. *)
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -74,70 +74,81 @@ Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
n) -> ((range a n) -> (surjective a n)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1
k) = (map.Map.get a2 k))).
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) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i
j).
(* Why3 assumption *)
Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(is_common_prefix a x y l) /\ forall (m:Z), (l < m)%Z ->
~ (is_common_prefix a x y m).
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a)
-> (map.Map.map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a1 l u)
| permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.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.Map.map Z a)) (a2:(map.Map.map Z a))
(a3:(map.Map.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.Map.map Z a)) (a2:(map.Map.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.Map.map Z a)) (a2:(map.Map.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.Map.map Z
a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2
i) = (map.Map.get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.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) /\ ((map.Map.get a2
i) = (map.Map.get a1 j)).
Definition lt (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) /\
exists l:Z, (is_common_prefix a x y l) /\ (((y + l)%Z < n)%Z /\
(((x + l)%Z = n) \/ ((get a (x + l)%Z) < (get a (y + l)%Z))%Z)))).
(* 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).
Definition le (a:(array Z)) (x:Z) (y:Z): Prop := (x = y) \/ (lt a x y).
Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (le a x x).
Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (is_longest_common_prefix a x x
((length a) - x)%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 /\ ~ ((get a (x + l)%Z) = (get a
(y + l)%Z))))) -> ~ (is_common_prefix a x y (l + 1%Z)%Z).
Axiom longest_common_prefix_succ : forall (a:(array Z)) (x:Z) (y:Z) (l:Z),
((is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z)) ->
(is_longest_common_prefix a x y l).
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).
(* 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).
Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z)
(u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\
(i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)).
(* Why3 assumption *)
Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a
(elts data) 0%Z (length data)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j).
(* Why3 assumption *)
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (map.MapPermut.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)).
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.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) ->
a)) (a2:(array a)) (i:Z) (j:Z), (exchange 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))
Axiom permut_sym : 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))
Axiom permut_trans : 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)).
......@@ -157,94 +168,11 @@ Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
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).
u) -> (permut_sub 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).
(* 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) -> ((get a (x + i)%Z) = (get 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 /\ ~ ((get a (x + (l - 1%Z)%Z)%Z) = (get a
(y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l).
(* Why3 assumption *)
Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(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) (l:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
((is_longest_common_prefix a x y l) -> (is_common_prefix a x y l)).
Axiom lcp_eq : 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)) ->
((is_longest_common_prefix a x y l) -> forall (i:Z), ((0%Z <= i)%Z /\
(i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z))).
Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (is_longest_common_prefix a x x
((length a) - x)%Z).
Axiom lcp_sym : 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)) ->
((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)).
(* 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) /\
exists l:Z, (is_common_prefix a x y l) /\ (((x + l)%Z = n) \/
(((x + l)%Z < n)%Z /\ (((y + l)%Z < n)%Z /\ ((get a (x + l)%Z) <= (get 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 permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z)
(u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\
(i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)).
(* Why3 assumption *)
Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a
(elts data) 0%Z (length data)).
Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1
a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2)
(length a2))).
Axiom lcp_le_le_aux : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z), ((le a x
y) /\ (le a y z)) -> ((is_common_prefix a x z l) -> (is_common_prefix a y z
l)).
Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z) (m:Z), ((le a
x y) /\ (le a y z)) -> (((is_longest_common_prefix a x z l) /\
(is_longest_common_prefix a y z m)) -> (l <= m)%Z).
(* Why3 assumption *)
Inductive suffixArray :=
| mk_suffixArray : (array Z) -> (array Z) -> suffixArray.
......@@ -269,6 +197,21 @@ Definition inv (s:suffixArray): Prop :=
(elts (suffixes s)) (length (suffixes s))) /\ (sorted (values s)
(suffixes s))).
Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1
a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2)
(length a2))).
Axiom lcp_sym : 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)) ->
((is_longest_common_prefix a x y l) -> (is_longest_common_prefix a y x l)).
Axiom le_le_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z) (l:Z),
((le a x y) /\ (le a y z)) -> ((is_common_prefix a x z l) ->
(is_common_prefix a y z l)).
Axiom le_le_longest_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z)
(l:Z) (m:Z), ((le a x y) /\ (le a y z)) -> (((is_longest_common_prefix a x
z l) /\ (is_longest_common_prefix a y z m)) -> (l <= m)%Z).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
......@@ -277,12 +220,13 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)),
let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (0%Z < a)%Z) ->
forall (sa:Z) (sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)),
(((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z) /\ (((sa = a) /\ (sa1 = a1)) /\ (inv
(mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3))))) -> ((permutation
sa3 sa2) -> forall (solStart:Z), (solStart = 0%Z) -> forall (solLength:Z),
(solLength = 0%Z) -> forall (solStart2:Z), (solStart2 = a) ->
((1%Z <= (a - 1%Z)%Z)%Z -> forall (solStart21:Z) (solLength1:Z)
(solStart1:Z), (((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\
((((sa = sa2) /\ ((permutation sa3 sa2) /\ (sorted_sub (mk_array sa sa1)
sa3 0%Z sa2))) /\ ((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z)) /\ ((sa = a) /\
(sa1 = a1))) -> ((permutation sa3 sa2) -> forall (solStart:Z),
(solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) ->
forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z ->
forall (solStart21:Z) (solLength1:Z) (solStart1:Z),
(((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\
((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\
(solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\
(is_longest_common_prefix a2 solStart1 solStart21 solLength1)))) /\
......@@ -296,17 +240,21 @@ Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)),
(x < y)%Z) /\ (y < a)%Z) -> exists j:Z, exists k:Z, ((0%Z <= j)%Z /\
(j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\
((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))))))).
intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 ((h3,h4),((h5,h6),h7)) h8 solStart h9
solLength h10 solStart2 h11 h12 solStart21 solLength1 solStart1
((((h13,h14),(h15,h16)),((h17,h18),(h19,h20))),h21) h22 h23 x y
((h24,h25),h26).
(* intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10
solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1
solStart1 ((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 x y
((h26,h27),h28). *)
intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10
solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1
solStart1 ((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 x y
((h26,h27),h28).
assert (h: sa2 = a) by ae.
subst sa2.
red in h22.
subst sa2 sa.
red in h24.
assert (ha : (0 <= x < a)%Z) by omega.
destruct (h22 _ ha) as (j & h30 & h31).
destruct (h24 _ ha) as (j & h30 & h31).
assert (hb : (0 <= y < a)%Z) by omega.
destruct (h22 _ hb) as (k & k32 & h33).
destruct (h24 _ hb) as (k & k32 & h33).
exists j.
exists k.
ae.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -74,70 +74,81 @@ Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
n) -> ((range a n) -> (surjective a n)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1
k) = (map.Map.get a2 k))).
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) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i
j).
(* Why3 assumption *)
Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(is_common_prefix a x y l) /\ forall (m:Z), (l < m)%Z ->
~ (is_common_prefix a x y m).
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a)
-> (map.Map.map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a1 l u)
| permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.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.Map.map Z a)) (a2:(map.Map.map Z a))
(a3:(map.Map.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.Map.map Z a)) (a2:(map.Map.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.Map.map Z a)) (a2:(map.Map.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.Map.map Z
a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2
i) = (map.Map.get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.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) /\ ((map.Map.get a2
i) = (map.Map.get a1 j)).
Definition lt (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) /\
exists l:Z, (is_common_prefix a x y l) /\ (((y + l)%Z < n)%Z /\
(((x + l)%Z = n) \/ ((get a (x + l)%Z) < (get a (y + l)%Z))%Z)))).
(* 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).
Definition le (a:(array Z)) (x:Z) (y:Z): Prop := (x = y) \/ (lt a x y).
Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (le a x x).
Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (is_longest_common_prefix a x x
((length a) - x)%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 /\ ~ ((get a (x + l)%Z) = (get a
(y + l)%Z))))) -> ~ (is_common_prefix a x y (l + 1%Z)%Z).
Axiom longest_common_prefix_succ : forall (a:(array Z)) (x:Z) (y:Z) (l:Z),
((is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z)) ->
(is_longest_common_prefix a x y l).
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).
(* 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).
Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Definition sorted_sub (a:(array Z)) (data:(map.Map.map Z Z)) (l:Z)
(u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\
(i2 < u)%Z) -> (le a (map.Map.get data i1) (map.Map.get data i2)).
(* Why3 assumption *)
Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a
(elts data) 0%Z (length data)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j).
(* Why3 assumption *)
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (map.MapPermut.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)).
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.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) ->
a)) (a2:(array a)) (i:Z) (j:Z), (exchange 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))
Axiom permut_sym : 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))
Axiom permut_trans : 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)).
......@@ -157,94 +168,11 @@ Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
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).
u) -> (permut_sub 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).
(* 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) -> ((get a (x + i)%Z) = (get 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 /\ ~ ((get a (x + (l - 1%Z)%Z)%Z) = (get a
(y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l).
(* Why3 assumption *)
Definition is_longest_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(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) (l:Z), (((0%Z <= x)%Z /\