Commit 66a8a56a authored by MARCHE Claude's avatar MARCHE Claude

LCP: more cleaning

parent 13ffc5b8
......@@ -165,23 +165,6 @@ module PrefixSort
exists l:int. is_common_prefix a x y l /\
(y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))
predicate le (a : array int) (x y:int) = x = y \/ lt a x y
lemma le_refl :
forall a:array int, x :int.
0 <= x <= a.length -> le a x x
(* needed for le_trans (why ?) *)
lemma lcp_refl :
forall a:array int, x:int.
0 <= x <= a.length -> is_longest_common_prefix a x x (a.length - x)
(* needed for le_trans *)
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] <> a[y+l] ->
not is_common_prefix a x y (l+1)
(* for proving lcp_sym and le_trans lemmas, and compare function in the absurd case *)
lemma longest_common_prefix_succ:
......@@ -190,12 +173,6 @@ lemma longest_common_prefix_succ:
is_longest_common_prefix a x y l
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
(** comparison function, that decides the order of prefixes *)
let compare (a:array int) (x y:int) : int
requires { 0 <= x <= a.length }
......@@ -215,13 +192,33 @@ let compare (a:array int) (x y:int) : int
absurd
use map.Map
use map.MapPermut
use map.MapInjection
predicate le (a : array int) (x y:int) = x = y \/ lt a x y
(* needed ?
lemma le_refl :
forall a:array int, x :int.
0 <= x <= a.length -> le a x x
*)
(* needed for le_trans (why ?) *)
lemma lcp_refl :
forall a:array int, x:int.
0 <= x <= a.length -> is_longest_common_prefix a x x (a.length - x)
predicate permutation (m:Map.map int int) (u : int) =
MapInjection.range m u /\ MapInjection.injective m u
(* needed for le_trans *)
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] <> a[y+l] ->
not is_common_prefix a x y (l+1)
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
use map.Map
predicate sorted_sub (a:array int) (data:Map.map int int) (l u:int) =
forall i1 i2 : int. l <= i1 <= i2 < u ->
......@@ -232,6 +229,8 @@ use map.MapInjection
use import array.ArrayPermut
use map.MapInjection (* for the range function used below *)
let sort (a:array int) (data : array int)
requires { data.length = a.length }
requires { MapInjection.range data.elts data.length }
......@@ -278,6 +277,10 @@ use import LCP
use import PrefixSort
use map.MapInjection
predicate permutation (m:Map.map int int) (u : int) =
MapInjection.range m u /\ MapInjection.injective m u
type suffixArray = {
values : array int;
suffixes : array int;
......
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment