Commit fe725f26 authored by MARCHE Claude's avatar MARCHE Claude

LCP: restructured

parent 7fe1e115
......@@ -83,7 +83,7 @@ that it does so correctly.
module LCP
use import int.Int
use export int.Int
use import array.Array
(** [is_common_prefix a x y l] is true when the prefixes of length [l]
......@@ -101,7 +101,7 @@ predicate is_longest_common_prefix (a:array int) (x y:int) (l:int) =
is_common_prefix a x y l /\
forall m:int. l < m -> not (is_common_prefix a x y m)
use import ref.Refint
use export ref.Refint
(** the first function, that compute the longest common prefix *)
let lcp (a:array int) (x y:int) : int
......@@ -147,6 +147,15 @@ let test1 () =
check {x = 1}
end
(** {2 Second module: sorting with respect to prefixes } *)
module PrefixSort
use import array.Array
use import LCP
(** order by prefix *)
predicate lt (a : array int) (x y:int) =
let n = a.length in
0 <= x <= n /\ 0 <= y <= n /\
......@@ -184,7 +193,7 @@ lemma longest_common_prefix_succ:
0 <= x <= a.length /\ 0 <= y <= a.length /\
0 <= z <= a.length /\ le a x y /\ le a y z -> le a x z
(** comparison function, that decides the order of prefixes *)
let compare (a:array int) (x y:int) : int
requires { 0 <= x <= a.length }
requires { 0 <= y <= a.length }
......@@ -251,37 +260,6 @@ use map.MapInjection
assert { !j > 0 -> le a data[!j-1] data[!j] }
done
(* additional properties relating le and longest_common_prefix, needed
for SuffixArray and LRS
*)
(* needed for LRS function, last before last assert *)
lemma lcp_sym :
forall a:array int, x y l:int.
0 <= x <= a.length /\ 0 <= y <= a.length ->
is_longest_common_prefix a x y l -> is_longest_common_prefix a y x l
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
lemma le_le_common_prefix:
forall a:array int, x y z l:int.
le a x y /\ le a y z ->
is_common_prefix a x z l -> is_common_prefix a y z l
lemma le_le_longest_common_prefix:
forall a:array int, x y z l m :int.
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
end
......@@ -289,11 +267,12 @@ end
module SuffixArray
use import int.Int
use import array.Array
use import LCP
use import PrefixSort
type suffixArray = {
values : array int;
......@@ -312,6 +291,14 @@ let select (s:suffixArray) (i:int) : int
ensures { result = s.suffixes[i] }
= s.suffixes[i]
(* needed to establish invariant in function create *)
use import array.ArrayPermut
lemma permut_permutation :
forall a1 a2:array int.
permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length
let create (a:array int) : suffixArray
ensures { result.values = a /\ inv result }
=
......@@ -373,8 +360,37 @@ module LRS "longest repeated substring"
use import ref.Ref
use import array.Array
use map.MapInjection
use LCP
use SuffixArray
use import LCP
use import PrefixSort
use import SuffixArray
(* additional properties relating le and longest_common_prefix, needed
for SuffixArray and LRS
*)
(* needed for LRS function, last before last assert *)
lemma lcp_sym :
forall a:array int, x y l:int.
0 <= x <= a.length /\ 0 <= y <= a.length ->
is_longest_common_prefix a x y l -> is_longest_common_prefix a y x l
use import int.MinMax
lemma le_le_common_prefix:
forall a:array int, x y z l:int.
le a x y /\ le a y z ->
is_common_prefix a x z l -> is_common_prefix a y z l
lemma le_le_longest_common_prefix:
forall a:array int, x y z l m :int.
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
val solStart : ref int
val solLength : ref int
......@@ -392,7 +408,7 @@ module LRS "longest repeated substring"
!solLength >= l }
=
let sa = SuffixArray.create a in
assert { LCP.permutation sa.SuffixArray.suffixes.elts
assert { permutation sa.SuffixArray.suffixes.elts
sa.SuffixArray.suffixes.length };
solStart := 0;
solLength := 0;
......@@ -411,7 +427,7 @@ module LRS "longest repeated substring"
!solLength >= l }
let l = SuffixArray.lcp sa i in
assert { forall j:int. 0 <= j < i ->
LCP.le a sa.SuffixArray.suffixes[j]
le a sa.SuffixArray.suffixes[j]
sa.SuffixArray.suffixes[i] };
assert { forall j m:int. 0 <= j < i /\
LCP.is_longest_common_prefix a
......
(* 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 *)
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.
(* 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:(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)) /\ (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), (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_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)), (permut a1 a2) -> (permut a2 a1).
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)).
(* 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_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 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 *)
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)))).
(* 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 *)
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 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 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 *)
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
(elts (suffixes s)) (length (suffixes s))) /\ (sorted (values s)
(suffixes s))).
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)).
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) -> ((map.MapPermut.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),
map.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.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
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 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 (elts a1) (length a1)) -> (permutation (elts a2)
(length a2))).
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 *)
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 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)))).
(* 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 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.
(* Why3 assumption *)
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 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 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 *)
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)) /\ (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), (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_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)), (permut a1 a2) -> (permut a2 a1).
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