Commit 088a76ba authored by MARCHE Claude's avatar MARCHE Claude

LCP: lemma permut_permutation proved in Coq

parent 3fa88b32
......@@ -78,6 +78,13 @@ that it does so correctly.
module LCP "longest common prefix"
use import int.Int
use map.Map
use map.MapPermut
use map.MapInjection
use import array.Array
use import array.ArrayPermut
......@@ -98,9 +105,8 @@ lemma common_prefix_eq2:
lemma not_common_prefix_if_last_different:
forall a:array int, x y:int, l:int.
0 < l /\ x+l < a.length /\ y+l < a.length /\ a[x+(l-1)] <> a[y+(l-1)] ->
not is_common_prefix a x y l
0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] ->
not is_common_prefix a x y (l+1)
(*
function longest_common_prefix (a:array int) (x y:int) :int
......@@ -127,6 +133,9 @@ let lcp (a:array int) (x y:int) : int
invariant { is_common_prefix a x y !l }
incr l
done;
(* not needed, lemma not_common_prefix_if_last_different is enough
assert { not is_common_prefix a x y (!l+1) };
*)
!l
......@@ -156,24 +165,28 @@ let test1 () =
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let x = lcp arr 1 2 in
assert { is_common_prefix arr 1 2 1};
assert { not is_common_prefix arr 1 2 2};
check { x = 1 };
(* 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 x = lcp brr 1 2 in
assert { is_common_prefix brr 1 2 0};
assert { not is_common_prefix brr 1 2 1};
check { x = 0 };
(* 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 x = lcp crr 2 3 in
assert { is_common_prefix crr 2 3 0};
assert { not is_common_prefix crr 2 3 1};
check { x = 0 };
(* 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 x = lcp drr 2 3 in
assert { is_common_prefix drr 2 3 1};
assert { not is_common_prefix drr 2 3 2};
check {x = 1}
......@@ -214,9 +227,6 @@ let compare (a:array int) (x y:int) : int
if a[x + l] > a[y + l] then 1 else
absurd
use map.Map
use map.MapPermut
use map.MapInjection
predicate permutation (m:Map.map int int) (u : int) =
MapInjection.range m u /\ MapInjection.injective m u
......@@ -265,17 +275,11 @@ let compare (a:array int) (x y:int) : int
*)
(*
lemma map_permut_permutation :
forall m1 m2:Map.map int int, u:int [MapPermut.permut_sub m1 m2 0 u].
MapPermut.permut_sub m1 m2 0 u -> map_permutation m1 u -> map_permutation m2 u
*)
lemma permut_permutation :
forall a1 a2:array int.
permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length
use import int.MinMax
use import int.MinMax
(*
lemma lcp_le_le_min:
......
(* 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.
......@@ -7,41 +7,42 @@ Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.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.Map.map Z a) :=
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.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 :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
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
......@@ -84,15 +85,15 @@ Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
i) = (map.Map.get a1 j)).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
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).
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
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)).
......@@ -105,20 +106,20 @@ 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)).
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut
a1 a3)).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
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
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)).
......@@ -130,29 +131,19 @@ 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 :=
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).
Parameter longest_common_prefix: (array Z) -> Z -> Z -> 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 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))).
(* 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).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -162,33 +153,34 @@ 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 :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%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_common_prefix a x y (longest_common_prefix a x y)).
((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), (((0%Z <= x)%Z /\
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)) ->
forall (i:Z), ((0%Z <= i)%Z /\ (i < (longest_common_prefix a x y))%Z) ->
((get a (x + i)%Z) = (get a (y + i)%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) -> ((longest_common_prefix a x
x) = ((length a) - 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), (((0%Z <= 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)) ->
((longest_common_prefix a x y) = (longest_common_prefix a y x)).
((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) /\ let l :=
(longest_common_prefix a x y) in (((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))))).
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).
......@@ -203,17 +195,17 @@ Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
y))) -> (le a y x).
(* Why3 assumption *)
Definition injective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z),
Definition injective (a:(map.Map.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)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))).
(* Why3 assumption *)
Definition surjective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
Definition surjective (a:(map.Map.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) /\
((map.Map.get a j) = i).
(* Why3 assumption *)
Definition range(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
Definition range (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\
((map.Map.get a i) < n)%Z).
......@@ -221,27 +213,79 @@ Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
n) -> ((range a n) -> (surjective a n)).
(* Why3 assumption *)
Definition map_permutation(m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Definition permutation(a:(array Z)): Prop := (map_permutation (elts a)
(length a)).
(* Why3 assumption *)
Definition sorted_sub(a:(array Z)) (data:(map.Map.map Z Z)) (l:Z)
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
Definition sorted (a:(array Z)) (data:(array Z)): Prop := (sorted_sub a
(elts data) 0%Z (length data)).
Axiom permut_permutation_aux : forall (m1:(map.Map.map Z Z)) (m2:(map.Map.map
Z Z)) (u:Z), (map.MapPermut.permut_sub m1 m2 0%Z u) -> ((permutation m1
u) <-> (permutation m2 u)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Inductive permut2 {a:Type} {a_WT:WhyType a} (l u : Z) :
(map.Map.map Z a)-> (map.Map.map Z a) -> Prop :=
| permut2_refl : forall (a1:(map.Map.map Z a)), (permut2 l u a1 a1)
| permut2_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
(permut2 l u a1 a2) -> (permut2 l u a2 a1)
| permut2_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a))
(a3:(map.Map.map Z a)), (permut2 l u a1 a2) ->
((permut2 l u a2 a3) -> (permut2 l u a1 a3))
| permut2_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) ->
(((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut2 l u a1
a2))).
Lemma permut_permut2:
forall (a:Type) (a_WT:WhyType a) (a1 a2 :(map.Map.map Z a)) (l u:Z),
MapPermut.permut_sub a1 a2 l u -> permut2 l u a1 a2.
induction 1.
apply permut2_refl.
apply permut2_sym; auto.
eapply permut2_trans; eauto.
eapply permut2_exchange.
apply H.
apply H0.
auto.
Qed.
Lemma aux : forall (m1:(map.Map.map Z Z))
(m2:(map.Map.map Z Z)) (u:Z), (map.MapPermut.permut_sub m1 m2 0%Z u) ->
((permutation m1 u) <-> (permutation m2 u)).
(* intros m1 m2 u h1. *)
intros m1 m2 u H.
assert (permut2 0%Z u m1 m2).
apply permut_permut2; auto.
clear H.
induction H0; ae.
Qed.
(* Why3 goal *)
Theorem permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1
a2) -> ((permutation a1) -> (permutation a2)).
a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2)
(length a2))).
(* intros a1 a2 h1 h2. *)
intros a1 a2 h1 h2.
destruct h1 as (h3 & h4).
rewrite <- h3.
rewrite aux.
apply h2.
apply h2.
intros m1 m2 u H.
assert (permut2 0%Z u m1 m2).
apply permut_permut2; auto.
clear H.
induction H0; ae.
Qed.
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Definition injective (a:(map.Map.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)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))).
(* Why3 assumption *)
Definition surjective (a:(map.Map.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) /\
((map.Map.get a j) = i).
(* Why3 assumption *)
Definition range (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\
((map.Map.get a i) < n)%Z).
Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
n) -> ((range a n) -> (surjective a n)).
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.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.Map.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 get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
(* 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))).
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 *)
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)).
(* 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 map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* 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).
(* 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 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).
(* 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).
(* 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 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</