LCP: proof of LRS function in progress

examples/programs/verifythis_fm2012_lcp.mlw

@@ -89,7 +89,7 @@ predicate permutation (a:array int) =
 use import array.ArrayPermut
 
 lemma permut_permutation :
-  forall a1 a2:array int, n:int.
+  forall a1 a2:array int.
   permut a1 a2 /\ permutation a1 -> permutation a2
 
 
@@ -136,6 +136,11 @@ lemma lcp_refl :
   forall a:array int, x:int.
      0 <= x <= a.length -> longest_common_prefix a x x = a.length - x
 
+lemma lcp_sym :
+  forall a:array int, x y:int.
+     0 <= x <= a.length /\ 0 <= y <= a.length -> 
+       longest_common_prefix a x y = longest_common_prefix a y x
+
 
 use import ref.Refint
 
@@ -303,6 +308,16 @@ let compare (a:array int) (x y:int) : int
    done
 
 
+(* additional properties relating le and longest_common_prefix, needed
+   for LRS
+
+*)
+
+  lemma lcp_le_le:
+    forall a:array int, x y z:int.
+     le a x y /\ le a y z ->
+     longest_common_prefix a x z <= longest_common_prefix a y z
+
 end
 
 
@@ -392,6 +407,7 @@ module LRS "longest repeated substring"
   use import int.Int
   use import ref.Ref
   use import array.Array
+  use map.MapInjection
   use LCP
   use SuffixArray
 
@@ -402,14 +418,15 @@ module LRS "longest repeated substring"
       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 }
+      ensures { forall x y:int.
+                  0 <= x < y < a.length ->
+                  !solLength >= LCP.longest_common_prefix a x y }
     =
       let sa = SuffixArray.create a in
+      assert { LCP.permutation sa.SuffixArray.suffixes };
       solStart := 0;
       solLength := 0;
       for i=1 to a.length - 1 do
@@ -418,12 +435,40 @@ module LRS "longest repeated substring"
         invariant { exists y:int.
                   0 <= y <= a.length /\ !solStart <> y /\
                   !solLength = LCP.longest_common_prefix a !solStart y }
+        invariant { forall j k:int.
+                  0 <= j < k < i ->
+                  !solLength >= LCP.longest_common_prefix a
+                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] }
          let l = SuffixArray.lcp sa i in
+         assert { forall j:int. 0 <= j < i ->
+                    LCP.le a sa.SuffixArray.suffixes[j]
+                             sa.SuffixArray.suffixes[i] };
+         assert { forall j:int. 0 <= j < i ->
+                    LCP.longest_common_prefix a
+                             sa.SuffixArray.suffixes[j]
+                             sa.SuffixArray.suffixes[i] 
+                  <= l };
+         assert { forall j k:int. 0 <= j < k  < i-1 ->
+                    !solLength >= LCP.longest_common_prefix a
+                             sa.SuffixArray.suffixes[j]
+                             sa.SuffixArray.suffixes[k] };
          if l > !solLength then begin
             solStart := SuffixArray.select sa i;
             solLength := l
          end
-      done
+      done;
+      assert { let s = sa.SuffixArray.suffixes in
+               MapInjection.surjective s.elts s.length };
+      assert { forall j k:int.
+                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k ->
+                  !solLength >= LCP.longest_common_prefix a
+                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] };
+      assert { forall x y:int.
+                  0 <= x < y < a.length ->
+                  exists j k : int.
+                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
+                  x = sa.SuffixArray.suffixes[j] /\
+                  y = sa.SuffixArray.suffixes[k] }
 
   let test () =
     let arr = Array.make 4 0 in

examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_2.v

@@ -77,9 +77,25 @@ 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).
+Definition injective(a:(map 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 a i) = (get a j)))).
+
+(* Why3 assumption *)
+Definition surjective(a:(map 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 a j) = i).
+
+(* Why3 assumption *)
+Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
+  (i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z).
+
+Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) ->
+  ((range a n) -> (surjective a n)).
+
+(* Why3 assumption *)
+Definition permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\
+  (injective (elts a) (length a)).
 
 (* Why3 assumption *)
 Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
@@ -165,8 +181,8 @@ Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
 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).
+Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), ((permut a1
+  a2) /\ (permutation a1)) -> (permutation a2).
 
 (* Why3 assumption *)
 Definition is_common_prefix(a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
@@ -206,6 +222,10 @@ 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).
 
+Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
+  (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
+  ((longest_common_prefix a x y) = (longest_common_prefix a y x)).
+
 (* 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 :=
@@ -262,6 +282,10 @@ Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
 Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data
   0%Z (length data)).
 
+Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\
+  (le a y z)) -> ((longest_common_prefix a x z) <= (longest_common_prefix a y
+  z))%Z.
+
 (* Why3 assumption *)
 Inductive suffixArray  :=
   | mk_suffixArray : (array Z) -> (array Z) -> suffixArray .
@@ -283,19 +307,27 @@ Definition values(v:suffixArray): (array Z) :=
 (* Why3 assumption *)
 Definition inv(s:suffixArray): Prop :=
   ((length (values s)) = (length (suffixes s))) /\
-  (array_bounded (suffixes s) (length (values s))).
+  (permutation (suffixes 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) -> (((a - 1%Z)%Z < 1%Z)%Z ->
-  exists y:Z, ((0%Z <= y)%Z /\ (y <= a)%Z) /\ ((~ (solStart = y)) /\
-  (solLength = (longest_common_prefix (mk_array a a1) solStart y))))).
-intros a a1 h1 h2 sa sa1 sa2 sa3 (h3,h4) solStart h5 solLength h6 h7.
+Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map Z Z)), let a2 :=
+  (mk_array a a1) in ((0%Z < a)%Z -> ((0%Z <= a)%Z -> forall (sa:Z) (sa1:(map
+  Z Z)) (sa2:Z) (sa3:(map Z Z)), (((sa = a) /\ (sa1 = a1)) /\
+  (inv (mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3)))) ->
+  ((permutation (mk_array sa2 sa3)) -> forall (solStart:Z),
+  (solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) ->
+  (((a - 1%Z)%Z < 1%Z)%Z -> ((surjective sa3 sa2) -> ((forall (j:Z) (k:Z),
+  (((0%Z <= j)%Z /\ (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\
+  ~ (j = k))) -> ((longest_common_prefix a2 (get sa3 j) (get sa3
+  k)) <= solLength)%Z) -> ((forall (x:Z) (y:Z), (((0%Z <= x)%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 = (get sa3 j)) /\ (y = (get sa3 k)))))) -> exists y:Z, ((0%Z <= y)%Z /\
+  (y <= a)%Z) /\ ((~ (solStart = y)) /\
+  (solLength = (longest_common_prefix a2 solStart y)))))))))).
+intro a; intros.
 exists a.
 why3 "alt-ergo".
 Qed.

examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_4.v

+(* 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 injective(a:(map 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 a i) = (get a j)))).
+
+(* Why3 assumption *)
+Definition surjective(a:(map 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 a j) = i).
+
+(* Why3 assumption *)
+Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
+  (i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z).
+
+Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) ->
+  ((range a n) -> (surjective a n)).
+
+(* Why3 assumption *)
+Definition permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\
+  (injective (elts a) (length a)).
+
+(* 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_permutation : forall (a1:(array Z)) (a2:(array Z)), ((permut a1
+  a2) /\ (permutation a1)) -> (permutation 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) -> ((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).
+
+Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
+  (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
+  ((longest_common_prefix a x y) = (longest_common_prefix a y x)).
+
+(* 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)).
+
+Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\
+  (le a y z)) -> ((longest_common_prefix a x z) <= (longest_common_prefix a y
+  z))%Z.
+
+(* 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))) /\
+  (permutation (suffixes s)).
+
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 3.
+
+(* Why3 goal *)
+Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map Z Z)), let a2 :=
+  (mk_array a a1) in ((0%Z < a)%Z -> ((0%Z <= a)%Z -> forall (sa:Z) (sa1:(map
+  Z Z)) (sa2:Z) (sa3:(map Z Z)), (((sa = a) /\ (sa1 = a1)) /\
+  (inv (mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3)))) ->
+  ((permutation (mk_array sa2 sa3)) -> forall (solStart:Z),
+  (solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) ->
+  ((1%Z <= (a - 1%Z)%Z)%Z -> forall (solLength1:Z) (solStart1:Z),
+  (((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\
+  ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ exists y:Z,
+  ((0%Z <= y)%Z /\ (y <= a)%Z) /\ ((~ (solStart1 = y)) /\
+  (solLength1 = (longest_common_prefix a2 solStart1 y)))) /\ forall (j:Z)
+  (k:Z), (((0%Z <= j)%Z /\ (j < k)%Z) /\ (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) ->
+  ((longest_common_prefix a2 (get sa3 j) (get sa3 k)) <= solLength1)%Z) ->
+  ((surjective sa3 sa2) -> ((forall (j:Z) (k:Z), (((0%Z <= j)%Z /\
+  (j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ~ (j = k))) ->
+  ((longest_common_prefix a2 (get sa3 j) (get sa3 k)) <= solLength1)%Z) ->