Commit 3fa88b32 authored by MARCHE Claude's avatar MARCHE Claude

LCP: remove useless lemmas

parent f91cc634
...@@ -86,6 +86,7 @@ predicate is_common_prefix (a:array int) (x y:int) (l:int) = ...@@ -86,6 +86,7 @@ predicate is_common_prefix (a:array int) (x y:int) (l:int) =
0 <= l /\ x+l <= a.length /\ y+l <= a.length /\ 0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
(forall i:int. 0 <= i < l -> a[x+i] = a[y+i]) (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])
(*
lemma common_prefix_eq: lemma common_prefix_eq:
forall a:array int, x:int. forall a:array int, x:int.
0 <= x <= a.length -> is_common_prefix a x x (a.length - x) 0 <= x <= a.length -> is_common_prefix a x x (a.length - x)
...@@ -93,12 +94,14 @@ lemma common_prefix_eq: ...@@ -93,12 +94,14 @@ lemma common_prefix_eq:
lemma common_prefix_eq2: lemma common_prefix_eq2:
forall a:array int, x:int. forall a:array int, x:int.
0 <= x <= a.length -> not (is_common_prefix a x x (a.length - x + 1)) 0 <= x <= a.length -> not (is_common_prefix a x x (a.length - x + 1))
*)
lemma not_common_prefix_if_last_different: lemma not_common_prefix_if_last_different:
forall a:array int, x y:int, l:int. 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)] -> 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 not is_common_prefix a x y l
(* (*
function longest_common_prefix (a:array int) (x y:int) :int function longest_common_prefix (a:array int) (x y:int) :int
...@@ -124,11 +127,6 @@ let lcp (a:array int) (x y:int) : int ...@@ -124,11 +127,6 @@ let lcp (a:array int) (x y:int) : int
invariant { is_common_prefix a x y !l } invariant { is_common_prefix a x y !l }
incr l incr l
done; done;
(*
assert { is_common_prefix a x y !l };
assert { x + !l < n /\ y + !l < n -> a[x + !l] <> a[y + !l] };
assert { not is_common_prefix a x y (!l+1) };
*)
!l !l
......
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