Commit 4e8f9fa3 authored by MARCHE Claude's avatar MARCHE Claude

LCP: all proved except tests

parent 47256f46
......@@ -107,19 +107,36 @@ let select (s:suffixArray) (i:int) : int
use import ref.Refint
predicate is_common_prefix (a:array int) (x y:int) (l:int) =
0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
(forall i:int. 0 <= i < l -> a[x+i] = a[y+i])
lemma not_common_prefix_if_last_different:
forall a:array int, x y:int, l:int.
0 < l /\ x+l < a.length /\ y+l < a.length /\ a[x+(l-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:
forall a:array int, x y:int, l:int.
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))
let lcp (a:array int) (x y:int) : int
requires { 0 <= x < a.length }
requires { 0 <= y < a.length }
ensures { 0 <= result /\ x+result <= a.length /\ y+result <= a.length }
ensures { forall i:int. 0 <= i < result -> a[x+i] = a[y+i] }
ensures { x+result = a.length \/ y+result = a.length \/ a[x+result] <> a[y+result] }
ensures { result = longest_common_prefix a x y }
= 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 { 0 <= !l /\ x + !l <= n /\ y + !l <= n }
invariant { forall i:int. 0 <= i < !l -> a[x+i] = a[y+i] }
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
let test1 () =
......@@ -143,21 +160,31 @@ let test1 () =
let x = lcp drr 2 3 in
check {x = 1}
(*
predicate le (a : array int) (x y:int) =
*)
let compare (a:array int) (x y:int) : int
requires { 0 <= x < a.length }
requires { 0 <= y < a.length }
(* ensures { result <= 0 <-> le a x y } *)
=
if x = y then 0 else
let n = a.length in
let l = lcp a x y in
assert { is_common_prefix a x y l };
if x + l = n then -1 else
if y + l = n then 1 else
if a[x + l] < a[y + l] then -1 else
if a[x + l] > a[y + l] then 1 else
absurd
(* predicate sorted_sub (a : array int) (data:array int) (l u:int) = *)
(* forall i1 i2 : int. l <= i1 <= i2 < u -> le a data[i1] data[i2] *)
let sort (a:array int) (data : array int)
requires { array_bounded data a.length }
(* ensures { sorted a data } *)
ensures { permut (old data) data }
=
'Init:
......
(* 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 *)
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 *)
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 array_bounded(a:(array Z)) (b:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a
i) < b)%Z).
(* 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_bounded : forall (a1:(array Z)) (a2:(array Z)) (n:Z),
((permut a1 a2) /\ (array_bounded a1 n)) -> (array_bounded a2 n).
(* Why3 assumption *)
Definition inv(s:suffixArray): Prop :=
((length (values s)) = (length (suffixes s))) /\
(array_bounded (suffixes s) (length (values s))).
(* 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 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)))).
(* Why3 goal *)
Theorem 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).
intros a x y l (h1,(h2,(h3,h4))).
red in h4.
red; intros (h5 & h6 & h7 & h8).
apply h4.
apply h8.
omega.
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