Commit e7949e64 authored by MARCHE Claude's avatar MARCHE Claude

LCP: removed useless asserts

parent 94154b89
......@@ -181,14 +181,16 @@ end
(** {2 Second module: sorting suffixes } *)
module SuffixSort
use import int.Int
use import ref.Refint
use import array.Array
use import LCP
use LCP
(** order by prefix *)
predicate lt (a : array int) (x y:int) =
let n = a.length in
0 <= x <= n /\ 0 <= y <= n /\
exists l:int. is_common_prefix a x y l /\
exists l:int. LCP.is_common_prefix a x y l /\
(y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))
......@@ -203,7 +205,7 @@ let compare (a:array int) (x y:int) : int
=
if x = y then 0 else
let n = a.length in
let l = lcp a x y in
let l = LCP.lcp a x y in
if x + l = n then -1 else
if y + l = n then 1 else
if a[x + l] < a[y + l] then -1 else
......@@ -216,7 +218,7 @@ let compare (a:array int) (x y:int) : int
(* needed for le_trans (for cases x = y /\ le y z and le x y /\ y = z) *)
lemma lcp_same_index :
forall a:array int, x:int.
0 <= x <= a.length -> is_longest_common_prefix a x x (a.length - x)
0 <= x <= a.length -> LCP.is_longest_common_prefix a x x (a.length - x)
lemma le_trans :
forall a:array int, x y z:int.
......@@ -280,9 +282,11 @@ end
module SuffixArray
use import int.Int
use import array.Array
use import LCP
use import SuffixSort
use LCP
use SuffixSort
use map.Map
use map.MapInjection
......@@ -295,7 +299,7 @@ type suffixArray = {
}
invariant { self.values.length = self.suffixes.length /\
permutation self.suffixes.elts self.suffixes.length /\
sorted self.values self.suffixes }
SuffixSort.sorted self.values self.suffixes }
let select (s:suffixArray) (i:int) : int
requires { 0 <= i < s.values.length }
......@@ -318,12 +322,13 @@ let create (a:array int) : suffixArray
for i = 0 to n-1 do
invariant { forall j:int. 0 <= j < i -> suf[j] = j }
suf[i] <- i done;
sort a suf;
SuffixSort.sort a suf;
{ values = a; suffixes = suf }
let lcp (s:suffixArray) (i:int) : int
requires { 0 < i < s.values.length }
ensures { is_longest_common_prefix s.values s.suffixes[i-1] s.suffixes[i] result }
ensures { LCP.is_longest_common_prefix s.values
s.suffixes[i-1] s.suffixes[i] result }
=
LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
......@@ -334,6 +339,7 @@ module SuffixArray_test
use import array.Array
use import SuffixArray
(*
let test () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
......@@ -362,6 +368,7 @@ let test () =
let sa = create drr in
let x = lcp sa 2 in
check {x = 0 (* TODO *)}
*)
end
......@@ -375,9 +382,9 @@ module LRS
use import ref.Ref
use import array.Array
use map.MapInjection
use import LCP
use import SuffixSort
use import SuffixArray
use LCP
use SuffixSort
use SuffixArray
(** additional properties relating [le] and [longest_common_prefix] *)
......@@ -386,7 +393,8 @@ module LRS
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
LCP.is_longest_common_prefix a x y l ->
LCP.is_longest_common_prefix a y x l
use import int.MinMax
......@@ -394,15 +402,16 @@ use import int.MinMax
(** allows CVC to prove the next lemma *)
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
SuffixSort.le a x y /\ SuffixSort.le a y z ->
LCP.is_common_prefix a x z l -> LCP.is_common_prefix a y z l
(** proved by Alt-Ergo and CVC. But only by Alt-Ergo if previous lemma is removed *)
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
SuffixSort.le a x y /\ SuffixSort.le a y z ->
LCP.is_longest_common_prefix a x z l /\
LCP.is_longest_common_prefix a y z m
-> l <= m
val solStart : ref int
......@@ -421,8 +430,6 @@ lemma le_le_common_prefix:
!solLength >= l }
=
let sa = SuffixArray.create a in
assert { permutation sa.SuffixArray.suffixes.elts
sa.SuffixArray.suffixes.length };
solStart := 0;
solLength := 0;
solStart2 := a.length;
......@@ -438,24 +445,13 @@ lemma le_le_common_prefix:
sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
!solLength >= l }
let l = SuffixArray.lcp sa i in
assert { forall j:int. 0 <= j < i ->
le a sa.SuffixArray.suffixes[j]
sa.SuffixArray.suffixes[i] };
assert { forall j m:int. 0 <= j < i /\
LCP.is_longest_common_prefix a
sa.SuffixArray.suffixes[j]
sa.SuffixArray.suffixes[i] m ->
m <= l };
assert { forall j k m:int. 0 <= j < k < i-1 /\
LCP.is_longest_common_prefix a
sa.SuffixArray.suffixes[j]
sa.SuffixArray.suffixes[k] m -> !solLength >= m};
if l > !solLength then begin
solStart := SuffixArray.select sa i;
solStart2 := SuffixArray.select sa (i-1);
solLength := l
end
done;
(* we state explicitly that sa.suffixes is surjective *)
assert { let s = sa.SuffixArray.suffixes in
MapInjection.surjective s.elts s.length };
(** the following assert needs [lcp_sym] lemma *)
......@@ -481,11 +477,13 @@ use import array.Array
use import ref.Ref
use import LRS
(*
let test () =
let arr = Array.make 4 0 in
arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
lrs arr;
check { !solStart = 1 /\ !solLength = 1 }
*)
end
......@@ -79,11 +79,20 @@ Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(((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_char_are_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) /\ forall (m:Z), (l < m)%Z ->
~ (is_common_prefix a x y m).
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).
(* 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) /\
......@@ -93,31 +102,15 @@ Definition lt (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in
(* 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 /\
Axiom lcp_same_index : 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) /\
......@@ -173,6 +166,10 @@ 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).
(* Why3 assumption *)
Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Inductive suffixArray :=
| mk_suffixArray : (array Z) -> (array Z) -> suffixArray.
......@@ -191,12 +188,6 @@ Definition values (v:suffixArray): (array Z) :=
| (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 permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1
a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2)
(length a2))).
......@@ -222,39 +213,37 @@ Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)),
forall (sa:Z) (sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)),
((((sa = sa2) /\ ((permutation sa3 sa2) /\ (sorted_sub (mk_array sa sa1)
sa3 0%Z sa2))) /\ ((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z)) /\ ((sa = a) /\
(sa1 = a1))) -> ((permutation sa3 sa2) -> forall (solStart:Z),
(solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) ->
forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z ->
forall (solStart21:Z) (solLength1:Z) (solStart1:Z),
(((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\
((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\
(solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\
(is_longest_common_prefix a2 solStart1 solStart21 solLength1)))) /\
forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\ (j < k)%Z) /\
(k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ (is_longest_common_prefix a2
(map.Map.get sa3 j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) ->
(sa1 = a1))) -> forall (solStart:Z), (solStart = 0%Z) ->
forall (solLength:Z), (solLength = 0%Z) -> forall (solStart2:Z),
(solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z -> forall (solStart21:Z)
(solLength1:Z) (solStart1:Z), (((((0%Z <= solLength1)%Z /\
(solLength1 <= a)%Z) /\ ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\
(((0%Z <= solStart21)%Z /\ (solStart21 <= a)%Z) /\
((~ (solStart1 = solStart21)) /\ (is_longest_common_prefix a2 solStart1
solStart21 solLength1)))) /\ forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\
(j < k)%Z) /\ (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ (is_longest_common_prefix
a2 (map.Map.get sa3 j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) ->
((surjective sa3 sa2) -> ((forall (j:Z) (k:Z) (l:Z), (((0%Z <= j)%Z /\
(j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\
(is_longest_common_prefix a2 (map.Map.get sa3 j) (map.Map.get sa3 k)
l)))) -> (l <= solLength1)%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 = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))))))).
(* intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10
solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1
solStart1 ((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 x y
((h26,h27),h28). *)
intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10
solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1
solStart1 ((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 x y
((h26,h27),h28).
((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k))))))))).
(* intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9))
solStart h10 solLength h11 solStart2 h12 h13 solStart21 solLength1
solStart1 ((((h14,h15),(h16,h17)),((h18,h19),(h20,h21))),h22) h23 h24 x y
((h25,h26),h27). *)
intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 h3 h10.
intros solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1.
intros solStart1 h18 h25 x y h26.
assert (h: sa2 = a) by ae.
subst sa2 sa.
red in h24.
subst sa2.
red in h18.
assert (ha : (0 <= x < a)%Z) by omega.
destruct (h24 _ ha) as (j & h30 & h31).
destruct (h18 _ ha) as (j & h30 & h31).
assert (hb : (0 <= y < a)%Z) by omega.
destruct (h24 _ hb) as (k & k32 & h33).
destruct (h18 _ hb) as (k & k32 & h33).
exists j.
exists k.
ae.
......
......@@ -79,11 +79,20 @@ Definition is_common_prefix (a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(((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_char_are_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) /\ forall (m:Z), (l < m)%Z ->
~ (is_common_prefix a x y m).
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).
(* 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) /\
......@@ -93,31 +102,15 @@ Definition lt (a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in
(* 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 /\
Axiom lcp_same_index : 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) /\
......@@ -173,6 +166,10 @@ 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).
(* Why3 assumption *)
Definition permutation (m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Inductive suffixArray :=
| mk_suffixArray : (array Z) -> (array Z) -> suffixArray.
......@@ -191,12 +188,6 @@ Definition values (v:suffixArray): (array Z) :=
| (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 permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1
a2) -> ((permutation (elts a1) (length a1)) -> (permutation (elts a2)
(length a2))).
......@@ -213,7 +204,6 @@ Axiom le_le_longest_common_prefix : forall (a:(array Z)) (x:Z) (y:Z) (z:Z)
(l:Z) (m:Z), ((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)%Z).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
......@@ -223,17 +213,16 @@ Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)),
forall (sa:Z) (sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)),
((((sa = sa2) /\ ((permutation sa3 sa2) /\ (sorted_sub (mk_array sa sa1)
sa3 0%Z sa2))) /\ ((0%Z <= sa)%Z /\ (0%Z <= sa2)%Z)) /\ ((sa = a) /\
(sa1 = a1))) -> ((permutation sa3 sa2) -> forall (solStart:Z),
(solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) ->
forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z ->
forall (solStart21:Z) (solLength1:Z) (solStart1:Z),
(((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\
((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\
(solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\
(is_longest_common_prefix a2 solStart1 solStart21 solLength1)))) /\
forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\ (j < k)%Z) /\
(k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ (is_longest_common_prefix a2
(map.Map.get sa3 j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) ->
(sa1 = a1))) -> forall (solStart:Z), (solStart = 0%Z) ->
forall (solLength:Z), (solLength = 0%Z) -> forall (solStart2:Z),
(solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z -> forall (solStart21:Z)
(solLength1:Z) (solStart1:Z), (((((0%Z <= solLength1)%Z /\
(solLength1 <= a)%Z) /\ ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\
(((0%Z <= solStart21)%Z /\ (solStart21 <= a)%Z) /\
((~ (solStart1 = solStart21)) /\ (is_longest_common_prefix a2 solStart1
solStart21 solLength1)))) /\ forall (j:Z) (k:Z) (l:Z), ((((0%Z <= j)%Z /\
(j < k)%Z) /\ (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ (is_longest_common_prefix
a2 (map.Map.get sa3 j) (map.Map.get sa3 k) l)) -> (l <= solLength1)%Z) ->
((surjective sa3 sa2) -> ((forall (j:Z) (k:Z) (l:Z), (((0%Z <= j)%Z /\
(j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\
(is_longest_common_prefix a2 (map.Map.get sa3 j) (map.Map.get sa3 k)
......@@ -242,12 +231,12 @@ Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)),
(j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\
((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))) -> forall (x:Z)
(y:Z) (l:Z), ((((0%Z <= x)%Z /\ (x < y)%Z) /\ (y < a)%Z) /\
(is_longest_common_prefix a2 x y l)) -> (l <= solLength1)%Z)))))).
intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9)) h10
solStart h11 solLength h12 solStart2 h13 h14 solStart21 solLength1 solStart1
((((h15,h16),(h17,h18)),((h19,h20),(h21,h22))),h23) h24 h25 h26 x y l
(h27,h30).
elim (h26 _ _ h27).
(is_longest_common_prefix a2 x y l)) -> (l <= solLength1)%Z))))).
intros a a1 a2 (h1,h2) sa sa1 sa2 sa3 (((h3,(h4,h5)),(h6,h7)),(h8,h9))
solStart h10 solLength h11 solStart2 h12 h13 solStart21 solLength1
solStart1 ((((h14,h15),(h16,h17)),((h18,h19),(h20,h21))),h22) h23 h24 h25
x y l (h26,h29).
elim (h25 _ _ h26).
ae.
Qed.
......
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