diff --git a/examples/programs/verifythis_fm2012_lcp.mlw b/examples/programs/verifythis_fm2012_lcp.mlw index e37a97251fc77d57547f66d75c6418ada9566734..5f231b7e430059dd28d5406bb1e9dd44f306a5e2 100644 --- a/examples/programs/verifythis_fm2012_lcp.mlw +++ b/examples/programs/verifythis_fm2012_lcp.mlw @@ -90,7 +90,7 @@ use import array.ArrayPermut lemma permut_permutation : forall a1 a2:array int. - permut a1 a2 /\ permutation a1 -> permutation a2 + permut a1 a2 -> permutation a1 -> permutation a2 @@ -138,7 +138,7 @@ lemma lcp_refl : lemma lcp_sym : forall a:array int, x y:int. - 0 <= x <= a.length /\ 0 <= y <= a.length -> + 0 <= x <= a.length /\ 0 <= y <= a.length -> longest_common_prefix a x y = longest_common_prefix a y x @@ -184,6 +184,7 @@ let test1 () = assert { is_common_prefix drr 2 3 1}; check {x = 1} + predicate le (a : array int) (x y:int) = let n = a.length in 0 <= x <= n /\ 0 <= y <= n /\ @@ -313,6 +314,14 @@ let compare (a:array int) (x y:int) : int *) + use import int.MinMax + + lemma lcp_le_le_min: + forall a:array int, x y z:int [le a x y, le a y z]. + le a x y /\ le a y z -> + longest_common_prefix a x z = + min (longest_common_prefix a x y) (longest_common_prefix a y z) + lemma lcp_le_le: forall a:array int, x y z:int. le a x y /\ le a y z -> @@ -339,7 +348,9 @@ type suffixArray = { use map.MapInjection predicate inv(s:suffixArray) = - s.values.length = s.suffixes.length /\ permutation s.suffixes + s.values.length = s.suffixes.length /\ + permutation s.suffixes /\ + sorted s.values s.suffixes let select (s:suffixArray) (i:int) : int requires { inv s /\ 0 <= i < s.values.length } @@ -362,11 +373,11 @@ let lcp (s:suffixArray) (i:int) : int requires { inv s } requires { 0 < i < s.values.length } ensures { result = - longest_common_prefix s.values s.suffixes[i] s.suffixes[i-1] } + longest_common_prefix s.values s.suffixes[i-1] s.suffixes[i] } = LCP.lcp s.values s.suffixes[i] s.suffixes[i-1] - +(* let test2 () = let arr = Array.make 4 0 in arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5; @@ -395,6 +406,7 @@ let test2 () = let sa = create drr in let x = lcp sa 2 in check {x = 0 (* TODO *)} +*) end @@ -446,7 +458,7 @@ module LRS "longest repeated substring" assert { forall j:int. 0 <= j < i -> LCP.longest_common_prefix a sa.SuffixArray.suffixes[j] - sa.SuffixArray.suffixes[i] + sa.SuffixArray.suffixes[i] <= l }; assert { forall j k:int. 0 <= j < k < i-1 -> !solLength >= LCP.longest_common_prefix a @@ -470,11 +482,13 @@ module LRS "longest repeated substring" x = sa.SuffixArray.suffixes[j] /\ y = sa.SuffixArray.suffixes[k] } +(* 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 diff --git a/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_lcp_le_le_1.v b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_lcp_le_le_1.v new file mode 100644 index 0000000000000000000000000000000000000000..6a493375f890d1077a7a82df67769ec885459044 --- /dev/null +++ b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_lcp_le_le_1.v @@ -0,0 +1,299 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. +Require int.MinMax. + +(* Why3 assumption *) +Definition unit := unit. + +Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. +Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} + (b:Type) {b_WT:WhyType b}, WhyType (map a b). +Existing Instance map_WhyType. + +Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + (map a b) -> a -> b. + +Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + (map a b) -> a -> b -> (map a b). + +Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> + ((get (set m a1 b1) a2) = b1). + +Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} + {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), + forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). + +Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + b -> (map a b). + +Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). + +(* Why3 assumption *) +Definition injective(a:(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)) -> ~ ((get a i) = (get a j)))). + +(* Why3 assumption *) +Definition surjective(a:(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) /\ + ((get a j) = i). + +(* Why3 assumption *) +Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ + (i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z). + +Axiom injective_surjective : forall (a:(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 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 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 get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := + (get (elts a1) i). + +(* Why3 assumption *) +Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array + a) := (mk_array (length a1) (set (elts a1) i v)). + +(* Why3 assumption *) +Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := + (mk_array n (const v:(map Z a))). + +(* Why3 assumption *) +Definition permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\ + (injective (elts a) (length a)). + +(* Why3 assumption *) +Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) + (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). + +(* Why3 assumption *) +Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) + (i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 + j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 + k))). + +Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)), + forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i + j). + +(* Why3 assumption *) +Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map Z a) -> (map Z a) -> Z + -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(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 Z a)) (a2:(map Z a)) (a3:(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 Z a)) (a2:(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 Z + a)) (a2:(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 Z a)) + (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), + ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)). + +Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)) + (a2:(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) /\ + ((get a2 i) = (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 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). + +Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), ((permut a1 + a2) /\ (permutation a1)) -> (permutation 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) -> ((get1 a (x + i)%Z) = (get1 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 /\ ~ ((get1 a (x + (l - 1%Z)%Z)%Z) = (get1 a + (y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l). + +Parameter longest_common_prefix: (array Z) -> Z -> 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))). + +Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y: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)). + +Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y: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) -> + ((get1 a (x + i)%Z) = (get1 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). + +Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y: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)). + +(* 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 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 /\ ((get1 a (x + l)%Z) <= (get1 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). + +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). + +Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x + y))) -> (le a y x). + +(* Why3 assumption *) +Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop := + forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> + (le a (get1 data i1) (get1 data i2)). + +Axiom sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) + (x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x + (get1 data l)))) -> (le a x (get1 data i)). + +Axiom sorted_ge : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) + (x:Z), ((sorted_sub a data l u) /\ ((le a (get1 data (u - 1%Z)%Z) x) /\ + ((l <= i)%Z /\ (i < u)%Z))) -> (le a (get1 data i) x). + +Axiom sorted_sub_sub : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (l':Z) (u':Z), ((l <= l')%Z /\ (u' <= u)%Z) -> ((sorted_sub a data l u) -> + (sorted_sub a data l' u')). + +Axiom sorted_sub_add : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z), + ((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get1 data l) (get1 data + (l + 1%Z)%Z))) -> (sorted_sub a data l u). + +Axiom sorted_sub_concat : forall (a:(array Z)) (data:(array Z)) (l:Z) (m:Z) + (u:Z), (((l <= m)%Z /\ (m <= u)%Z) /\ ((sorted_sub a data l m) /\ + ((sorted_sub a data m u) /\ (le a (get1 data (m - 1%Z)%Z) (get1 data + m))))) -> (sorted_sub a data l u). + +Axiom sorted_sub_set : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a + (set1 data i v) l u). + +Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a + (mk_array (length a) (set (elts data) i v)) l u). + +(* Why3 assumption *) +Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data + 0%Z (length data)). + +Axiom lcp_le_le_min : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\ + (le a y z)) -> ((longest_common_prefix a x + z) = (Zmin (longest_common_prefix a x y) (longest_common_prefix a y z))). + +(* Why3 goal *) +Theorem lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\ + (le a y z)) -> ((longest_common_prefix a x z) <= (longest_common_prefix a y + z))%Z. +intros a x y z (h1,h2). +rewrite lcp_le_le_min with (y:=y); auto. +apply Zle_min_r. +Qed. + + diff --git a/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_lcp_le_le_min_1.v b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_lcp_le_le_min_1.v new file mode 100644 index 0000000000000000000000000000000000000000..e370cae818f2274542dab7fb04a8c06d63c19698 --- /dev/null +++ b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_lcp_le_le_min_1.v @@ -0,0 +1,281 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. +Require int.MinMax. +Require map.Map. + +(* 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 permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\ + (injective (elts a) (length 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). + +Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 + a2) -> ((permutation a1) -> (permutation 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 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. + +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))). + +Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y: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)). + +Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y: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)). + +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). + +Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y: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)). + +(* 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 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))))). + +Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ + (x <= (length a))%Z) -> (le a x x). + +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). + +Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x + y))) -> (le a y x). + +(* Why3 assumption *) +Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop := + forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> + (le a (get data i1) (get data i2)). + +Axiom sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) + (x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x + (get data l)))) -> (le a x (get data i)). + +Axiom sorted_ge : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) + (x:Z), ((sorted_sub a data l u) /\ ((le a (get data (u - 1%Z)%Z) x) /\ + ((l <= i)%Z /\ (i < u)%Z))) -> (le a (get data i) x). + +Axiom sorted_sub_sub : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (l':Z) (u':Z), ((l <= l')%Z /\ (u' <= u)%Z) -> ((sorted_sub a data l u) -> + (sorted_sub a data l' u')). + +Axiom sorted_sub_add : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z), + ((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get data l) (get data + (l + 1%Z)%Z))) -> (sorted_sub a data l u). + +Axiom sorted_sub_concat : forall (a:(array Z)) (data:(array Z)) (l:Z) (m:Z) + (u:Z), (((l <= m)%Z /\ (m <= u)%Z) /\ ((sorted_sub a data l m) /\ + ((sorted_sub a data m u) /\ (le a (get data (m - 1%Z)%Z) (get data + m))))) -> (sorted_sub a data l u). + +Axiom sorted_sub_set : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a + (set data i v) l u). + +Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a + (mk_array (length a) (map.Map.set (elts data) i v)) l u). + +(* Why3 assumption *) +Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data + 0%Z (length data)). + +Require Import Why3. +Ltac ae := why3 "alt-ergo" timelimit 3. + +(* Why3 goal *) +Theorem lcp_le_le_min : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x + y) /\ (le a y z)) -> ((longest_common_prefix a x + z) = (Zmin (longest_common_prefix a x y) (longest_common_prefix a y z))). +intros a x y z (h1,h2). +unfold le in *. +intuition. +ae. +Qed. + + diff --git a/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_permut_permutation_1.v b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_permut_permutation_1.v new file mode 100644 index 0000000000000000000000000000000000000000..f250cdd49a066c86dd91e3e4ee8d43480cff372c --- /dev/null +++ b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_permut_permutation_1.v @@ -0,0 +1,193 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. + +(* Why3 assumption *) +Definition unit := unit. + +Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. +Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} + (b:Type) {b_WT:WhyType b}, WhyType (map a b). +Existing Instance map_WhyType. + +Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + (map a b) -> a -> b. + +Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + (map a b) -> a -> b -> (map a b). + +Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> + ((get (set m a1 b1) a2) = b1). + +Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} + {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), + forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). + +Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + b -> (map a b). + +Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). + +(* Why3 assumption *) +Definition injective(a:(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)) -> ~ ((get a i) = (get a j)))). + +(* Why3 assumption *) +Definition surjective(a:(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) /\ + ((get a j) = i). + +(* Why3 assumption *) +Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ + (i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z). + +Axiom injective_surjective : forall (a:(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 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 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 get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := + (get (elts a1) i). + +(* Why3 assumption *) +Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array + a) := (mk_array (length a1) (set (elts a1) i v)). + +(* Why3 assumption *) +Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := + (mk_array n (const v:(map Z a))). + +(* Why3 assumption *) +Definition permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\ + (injective (elts a) (length a)). + +(* Why3 assumption *) +Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) + (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). + +(* Why3 assumption *) +Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) + (i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 + j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 + k))). + +Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)), + forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i + j). + +(* Why3 assumption *) +Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map Z a) -> (map Z a) -> Z + -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(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 Z a)) (a2:(map Z a)) (a3:(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 Z a)) (a2:(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 Z + a)) (a2:(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 Z a)) + (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), + ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)). + +Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)) + (a2:(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) /\ + ((get a2 i) = (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 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). + +Require Import Why3. +Ltac ae := why3 "alt-ergo" timelimit 3. + +(* Why3 goal *) +Theorem permut_permutation : forall (a1:(array Z)) (a2:(array Z)), + ((((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z + (length a1))) /\ ((range (elts a1) (length a1)) /\ (injective (elts a1) + (length a1)))) -> (injective (elts a2) (length a2)). +intros a1 a2 ((h1,h2),(h3,h4)). +induction h2. +ae. +ae. +apply IHh2_2; auto. +ae. +red; intros. +destruct (permut_exists _ _ _ _ h2 i) as (i0 & gi & hi); auto with *. +destruct (permut_exists _ _ _ _ h2 j) as (j0 & gj & hj); auto with *. +rewrite hi. +rewrite hj. +apply h4; auto with zarith. +Qed. + + diff --git a/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_permut_permutation_2.v b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_permut_permutation_2.v new file mode 100644 index 0000000000000000000000000000000000000000..5dd0ab05c807ecebb9149f14f4ba82e8672e8b9e --- /dev/null +++ b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LCP_permut_permutation_2.v @@ -0,0 +1,169 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. +Require map.Map. + +(* 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 permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\ + (injective (elts a) (length 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). + +Require Import Why3. +Ltac ae := why3 "alt-ergo" timelimit 3. + +(* Why3 goal *) +Theorem permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 + a2) -> ((permutation a1) -> (permutation a2)). +intros (l1,a1) (l2,a2) (h1,h2) h. +simpl in *. +subst l2. +induction h2. +ae. +ae. +apply IHh2_2; auto. +ae. +Qed. + + diff --git a/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_7.v b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_7.v new file mode 100644 index 0000000000000000000000000000000000000000..7ee80f04455bd288eca3df45cb820989bc52c31e --- /dev/null +++ b/examples/programs/verifythis_fm2012_lcp/verifythis_fm2012_lcp_LRS_WP_parameter_lrs_7.v @@ -0,0 +1,344 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. + +(* 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. + +Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. +Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} + (b:Type) {b_WT:WhyType b}, WhyType (map a b). +Existing Instance map_WhyType. + +Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + (map a b) -> a -> b. + +Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + (map a b) -> a -> b -> (map a b). + +Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> + ((get (set m a1 b1) a2) = b1). + +Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} + {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), + forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). + +Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + b -> (map a b). + +Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). + +(* Why3 assumption *) +Inductive array (a:Type) {a_WT:WhyType a} := + | mk_array : Z -> (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 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 get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := + (get (elts a1) i). + +(* Why3 assumption *) +Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array + a) := (mk_array (length a1) (set (elts a1) i v)). + +(* Why3 assumption *) +Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := + (mk_array n (const v:(map Z a))). + +(* Why3 assumption *) +Definition injective(a:(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)) -> ~ ((get a i) = (get a j)))). + +(* Why3 assumption *) +Definition surjective(a:(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) /\ + ((get a j) = i). + +(* Why3 assumption *) +Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ + (i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z). + +Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) -> + ((range a n) -> (surjective a n)). + +(* Why3 assumption *) +Definition permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\ + (injective (elts a) (length a)). + +(* Why3 assumption *) +Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) + (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). + +(* Why3 assumption *) +Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) + (i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 + j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 + k))). + +Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)), + forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i + j). + +(* Why3 assumption *) +Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map Z a) -> (map Z a) -> Z + -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(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 Z a)) (a2:(map Z a)) (a3:(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 Z a)) (a2:(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 Z + a)) (a2:(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 Z a)) + (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), + ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)). + +Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)) + (a2:(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) /\ + ((get a2 i) = (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 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). + +Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), ((permut a1 + a2) /\ (permutation a1)) -> (permutation 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) -> ((get1 a (x + i)%Z) = (get1 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 /\ ~ ((get1 a (x + (l - 1%Z)%Z)%Z) = (get1 a + (y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l). + +Parameter longest_common_prefix: (array Z) -> Z -> 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))). + +Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y: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)). + +Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y: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) -> + ((get1 a (x + i)%Z) = (get1 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). + +Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y: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)). + +(* 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 /\ ((get1 a (x + l)%Z) <= (get1 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). + +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). + +Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ + (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x + y))) -> (le a y x). + +(* Why3 assumption *) +Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop := + forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> + (le a (get1 data i1) (get1 data i2)). + +Axiom sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) + (x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x + (get1 data l)))) -> (le a x (get1 data i)). + +Axiom sorted_ge : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) + (x:Z), ((sorted_sub a data l u) /\ ((le a (get1 data (u - 1%Z)%Z) x) /\ + ((l <= i)%Z /\ (i < u)%Z))) -> (le a (get1 data i) x). + +Axiom sorted_sub_sub : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (l':Z) (u':Z), ((l <= l')%Z /\ (u' <= u)%Z) -> ((sorted_sub a data l u) -> + (sorted_sub a data l' u')). + +Axiom sorted_sub_add : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z), + ((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get1 data l) (get1 data + (l + 1%Z)%Z))) -> (sorted_sub a data l u). + +Axiom sorted_sub_concat : forall (a:(array Z)) (data:(array Z)) (l:Z) (m:Z) + (u:Z), (((l <= m)%Z /\ (m <= u)%Z) /\ ((sorted_sub a data l m) /\ + ((sorted_sub a data m u) /\ (le a (get1 data (m - 1%Z)%Z) (get1 data + m))))) -> (sorted_sub a data l u). + +Axiom sorted_sub_set : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a + (set1 data i v) l u). + +Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) + (i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a + (mk_array (length a) (set (elts data) i v)) l u). + +(* Why3 assumption *) +Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data + 0%Z (length data)). + +Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\ + (le a y z)) -> ((longest_common_prefix a x z) <= (longest_common_prefix a y + z))%Z. + +(* 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 (suffixes s)). + +Require Import Why3. +Ltac ae := why3 "alt-ergo" timelimit 3. + +(* Why3 goal *) +Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map Z Z)), let a2 := + (mk_array a a1) in ((0%Z < a)%Z -> ((0%Z <= a)%Z -> forall (sa:Z) (sa1:(map + Z Z)) (sa2:Z) (sa3:(map Z Z)), let sa4 := (mk_suffixArray (mk_array sa sa1) + (mk_array sa2 sa3)) in ((((sa = a) /\ (sa1 = a1)) /\ (inv sa4)) -> + ((permutation (mk_array sa2 sa3)) -> forall (solStart:Z), + (solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) -> + ((1%Z <= (a - 1%Z)%Z)%Z -> forall (solLength1:Z) (solStart1:Z), + forall (i:Z), ((1%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) -> + ((((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\ + ((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ exists y:Z, + ((0%Z <= y)%Z /\ (y <= a)%Z) /\ ((~ (solStart1 = y)) /\ + (solLength1 = (longest_common_prefix a2 solStart1 y)))) /\ forall (j:Z) + (k:Z), (((0%Z <= j)%Z /\ (j < k)%Z) /\ (k < i)%Z) -> + ((longest_common_prefix a2 (get sa3 j) (get sa3 k)) <= solLength1)%Z) -> + (((inv sa4) /\ ((0%Z < i)%Z /\ (i < sa)%Z)) -> ((forall (j:Z), + ((0%Z <= j)%Z /\ (j < i)%Z) -> (le a2 (get sa3 j) (get sa3 i))) -> + forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ((longest_common_prefix a2 + (get sa3 j) (get sa3 i)) <= (longest_common_prefix (mk_array sa sa1) + (get sa3 (i - 1%Z)%Z) (get sa3 i)))%Z)))))))). +intros a a1 a2 h1 h2 sa sa1 sa2 sa3 sa4 ((h3,h4),h5) h6 solStart h7 solLength +h8 h9 solLength1 solStart1 i (h10,h11) +((((h12,h13),(h14,h15)),(y,((h16,h17),(h18,h19)))),h20) (h21,(h22,h23)) h24 j +(h25,h26). +replace (mk_array sa sa1) with a2 by ae. +apply lcp_le_le. +red in h5. +Qed. + + diff --git a/examples/programs/verifythis_fm2012_lcp/why3session.xml b/examples/programs/verifythis_fm2012_lcp/why3session.xml index 7c3c3f718f5c86617f78aa3ca0bb0ba4705d4f5d..67b1f18c4a6174abe7fb583afca7390b72e88ce5 100644 --- a/examples/programs/verifythis_fm2012_lcp/why3session.xml +++ b/examples/programs/verifythis_fm2012_lcp/why3session.xml @@ -11,26 +11,34 @@ version="0.95"/> + + version="8.3pl3"/> + + expanded="true">