Commit 82b3fb69 by MARCHE Claude

### LCP: removed the axiom, but some proofs need to be completed

parent ff035059
 ... ... @@ -99,6 +99,7 @@ lemma not_common_prefix_if_last_different: 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 (* function longest_common_prefix (a:array int) (x y:int) :int axiom lcp_spec: ... ... @@ -106,45 +107,51 @@ axiom lcp_spec: 0 <= x <= a.length /\ 0 <= y <= a.length -> (l = longest_common_prefix a x y <-> is_common_prefix a x y l /\ not is_common_prefix a x y (l+1)) *) predicate is_longest_common_prefix (a:array int) (x y:int) (l:int) = is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) use import ref.Refint let lcp (a:array int) (x y:int) : int requires { 0 <= x <= a.length } requires { 0 <= y <= a.length } ensures { result = longest_common_prefix a x y } ensures { is_longest_common_prefix a x y result } = let n = a.length in let l = ref 0 in while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do invariant { is_common_prefix a x y !l } incr l 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 lemma lcp_is_cp : forall a:array int, x y:int. forall a:array int, x y l:int. 0 <= x <= a.length /\ 0 <= y <= a.length -> let l = longest_common_prefix a x y in is_longest_common_prefix a x y l -> is_common_prefix a x y l lemma lcp_eq : forall a:array int, x y:int. forall a:array int, x y l:int. 0 <= x <= a.length /\ 0 <= y <= a.length -> let l = longest_common_prefix a x y in is_longest_common_prefix a x y l -> forall i:int. 0 <= i < l -> a[x+i] = a[y+i] lemma lcp_refl : forall a:array int, x:int. 0 <= x <= a.length -> longest_common_prefix a x x = a.length - x 0 <= x <= a.length -> is_longest_common_prefix a x x (a.length - x) lemma lcp_sym : forall a:array int, x y:int. forall a:array int, x y l:int. 0 <= x <= a.length /\ 0 <= y <= a.length -> longest_common_prefix a x y = longest_common_prefix a y x is_longest_common_prefix a x y l -> is_longest_common_prefix a y x l let test1 () = let arr = Array.make 4 0 in ... ... @@ -175,9 +182,9 @@ let test1 () = predicate le (a : array int) (x y:int) = let n = a.length in 0 <= x <= n /\ 0 <= y <= n /\ let l = longest_common_prefix a x y in x+l = n \/ (x+l < n /\ y+l < n /\ a[x+l] <= a[y+l]) exists l:int. is_common_prefix a x y l /\ (x+l = n \/ (x+l < n /\ y+l < n /\ a[x+l] <= a[y+l])) lemma le_refl : forall a:array int, x :int. ... ... @@ -213,13 +220,9 @@ let compare (a:array int) (x y:int) : int use map.MapPermut use map.MapInjection predicate map_permutation (m:Map.map int int) (u : int) = predicate permutation (m:Map.map int int) (u : int) = MapInjection.range m u /\ MapInjection.injective m u predicate permutation (a:array int) = map_permutation a.elts a.length predicate sorted_sub (a:array int) (data:Map.map int int) (l u:int) = forall i1 i2 : int. l <= i1 <= i2 < u -> le a (Map.get data i1) (Map.get data i2) ... ... @@ -272,20 +275,27 @@ lemma map_permut_permutation : lemma permut_permutation : forall a1 a2:array int. permut a1 a2 -> permutation a1 -> permutation a2 permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length 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_aux: 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 lcp_le_le: forall a:array int, x y z:int. forall a:array int, x y z l m :int. le a x y /\ le a y z -> longest_common_prefix a x z <= longest_common_prefix a y z is_longest_common_prefix a x z l /\ is_longest_common_prefix a y z m -> l <= m end ... ... @@ -309,7 +319,7 @@ use map.MapInjection predicate inv(s:suffixArray) = s.values.length = s.suffixes.length /\ permutation s.suffixes /\ permutation s.suffixes.elts s.suffixes.length /\ sorted s.values s.suffixes let select (s:suffixArray) (i:int) : int ... ... @@ -332,8 +342,7 @@ let create (a:array int) : suffixArray 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-1] s.suffixes[i] } ensures { 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] ... ... @@ -392,13 +401,15 @@ module LRS "longest repeated substring" ensures { 0 <= !solLength <= a.length } ensures { 0 <= !solStart <= a.length } ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\ !solLength = LCP.longest_common_prefix a !solStart !solStart2 } ensures { forall x y:int. 0 <= x < y < a.length -> !solLength >= LCP.longest_common_prefix a x y } LCP.is_longest_common_prefix a !solStart !solStart2 !solLength } ensures { forall x y l:int. 0 <= x < y < a.length /\ LCP.is_longest_common_prefix a x y l -> !solLength >= l } = let sa = SuffixArray.create a in assert { LCP.permutation sa.SuffixArray.suffixes }; assert { LCP.permutation sa.SuffixArray.suffixes.elts sa.SuffixArray.suffixes.length }; solStart := 0; solLength := 0; solStart2 := a.length; ... ... @@ -406,25 +417,27 @@ module LRS "longest repeated substring" invariant { 0 <= !solLength <= a.length } invariant { 0 <= !solStart <= a.length } invariant { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\ !solLength = LCP.longest_common_prefix a !solStart !solStart2 } invariant { forall j k:int. 0 <= j < k < i -> !solLength >= LCP.longest_common_prefix a sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] } 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\ LCP.is_longest_common_prefix a !solStart !solStart2 !solLength } invariant { forall j k l:int. 0 <= j < k < i /\ LCP.is_longest_common_prefix a 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 -> LCP.le a sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[i] }; assert { forall j:int. 0 <= j < i -> LCP.longest_common_prefix a sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[i] <= l }; assert { forall j k:int. 0 <= j < k < i-1 -> !solLength >= LCP.longest_common_prefix a assert { forall j m:int. 0 <= j < i /\ LCP.is_longest_common_prefix a sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] }; 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); ... ... @@ -433,16 +446,18 @@ module LRS "longest repeated substring" done; assert { let s = sa.SuffixArray.suffixes in MapInjection.surjective s.elts s.length }; assert { forall j k:int. 0 <= j < a.length /\ 0 <= k < a.length /\ j <> k -> !solLength >= LCP.longest_common_prefix a sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] }; assert { forall j k l:int. 0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\ LCP.is_longest_common_prefix a sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l -> !solLength >= l}; assert { forall x y:int. 0 <= x < y < a.length -> exists j k : int. 0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\ x = sa.SuffixArray.suffixes[j] /\ y = sa.SuffixArray.suffixes[k] } y = sa.SuffixArray.suffixes[k] }; () (* let test () = ... ...
 (* 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. 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 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). (* 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))). (* 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 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 *) 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 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 map_permutation(m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ (injective m u). (* Why3 assumption *) Definition permutation(a:(array Z)): Prop := (map_permutation (elts a) (length a)). (* 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 goal *) Theorem permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 a2) -> ((permutation a1) -> (permutation a2)). intros a1 a2 h1 h2. 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