kmp_WP_KnuthMorrisPratt_WP_parameter_initnext_4.v 7.66 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Andrei Paskevich's avatar
Andrei Paskevich committed
3 4 5
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
6

Andrei Paskevich's avatar
Andrei Paskevich committed
7 8
(* Why3 assumption *)
Definition unit  := unit.
9

Andrei Paskevich's avatar
Andrei Paskevich committed
10 11
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
12
  | mk_ref : a -> ref a.
Andrei Paskevich's avatar
Andrei Paskevich committed
13 14 15 16 17 18 19 20
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
21 22
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
23 24 25 26
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.
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b.
30

Andrei Paskevich's avatar
Andrei Paskevich committed
31 32
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b -> (map a b).
33

Andrei Paskevich's avatar
Andrei Paskevich committed
34 35 36
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).
37

Andrei Paskevich's avatar
Andrei Paskevich committed
38 39 40
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)).
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42 43
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  b -> (map a b).
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45 46
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).
47

Andrei Paskevich's avatar
Andrei Paskevich committed
48 49
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
50
  | mk_array : Z -> (map Z a) -> array a.
Andrei Paskevich's avatar
Andrei Paskevich committed
51 52 53 54 55 56 57 58
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
59 60
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
61 62 63 64
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
  match v with
  | (mk_array x x1) => x
65 66
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
67 68 69
(* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
  (get (elts a1) i).
70

Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73 74 75 76 77
(* 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))).
78

Andrei Paskevich's avatar
Andrei Paskevich committed
79 80 81
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
82

Andrei Paskevich's avatar
Andrei Paskevich committed
83
(* Why3 assumption *)
84 85 86
Definition matches(a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
  (n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
  (((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
Andrei Paskevich's avatar
Andrei Paskevich committed
87
  ((0%Z <= i)%Z /\ (i < n)%Z) -> ((get1 a1 (i1 + i)%Z) = (get1 a2
88 89 90 91 92 93 94 95 96 97 98 99 100 101
  (i2 + i)%Z))).

Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
  (i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
  (i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).

Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
  (i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
  ((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
  ((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get1 a1
  (i1 + n)%Z) = (get1 a2 (i2 + n)%Z)) -> (matches a1 i1 a2 i2
  (n + 1%Z)%Z)))).

Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
Andrei Paskevich's avatar
Andrei Paskevich committed
102
  char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get1 a1 i1) = (get1 a2
103 104 105
  i2))) -> ~ (matches a1 i1 a2 i2 n)).

Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
Andrei Paskevich's avatar
Andrei Paskevich committed
106
  (i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
107 108 109 110
  ((~ ((get1 a1 (i1 + i)%Z) = (get1 a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2
  i2 n))).

Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
Andrei Paskevich's avatar
Andrei Paskevich committed
111 112
  (i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 i1 a2 i2 n) -> ((n' < n)%Z ->
  (matches a1 i1 a2 i2 n')).
113 114

Axiom matches_left_weakening : forall (a1:(array char)) (a2:(array char))
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116
  (i1:Z) (i2:Z) (n:Z) (n':Z), (matches a1 (i1 - (n - n')%Z)%Z a2
  (i2 - (n - n')%Z)%Z n) -> ((n' < n)%Z -> (matches a1 i1 a2 i2 n')).
117 118 119 120 121 122 123 124

Axiom matches_sym : forall (a1:(array char)) (a2:(array char)) (i1:Z) (i2:Z)
  (n:Z), (matches a1 i1 a2 i2 n) -> (matches a2 i2 a1 i1 n).

Axiom matches_trans : forall (a1:(array char)) (a2:(array char)) (a3:(array
  char)) (i1:Z) (i2:Z) (i3:Z) (n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2
  i2 a3 i3 n) -> (matches a1 i1 a3 i3 n)).

Andrei Paskevich's avatar
Andrei Paskevich committed
125
(* Why3 assumption *)
126
Definition is_next(p:(array char)) (j:Z) (n:Z): Prop := ((0%Z <= n)%Z /\
Andrei Paskevich's avatar
Andrei Paskevich committed
127 128
  (n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\ forall (z:Z), ((n < z)%Z /\
  (z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
129 130

Axiom next_iteration : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
Andrei Paskevich's avatar
Andrei Paskevich committed
131
  (n:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
132 133 134 135
  (i <= (length a))%Z) -> ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j
  n) -> (matches a (i - n)%Z p 0%Z n)))).

Axiom next_is_maximal : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
Andrei Paskevich's avatar
Andrei Paskevich committed
136 137
  (n:Z) (k:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
  (i <= (length a))%Z) -> ((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) ->
138 139 140 141 142 143
  ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j n) -> ~ (matches a k p 0%Z
  (length p)))))).

Axiom next_1_0 : forall (p:(array char)), (1%Z <= (length p))%Z -> (is_next p
  1%Z 0%Z).

Andrei Paskevich's avatar
Andrei Paskevich committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
(* Why3 goal *)
Theorem WP_parameter_initnext : forall (p:Z), forall (p1:(map Z char)),
  let p2 := (mk_array p p1) in ((1%Z <= p)%Z -> ((0%Z <= p)%Z ->
  ((1%Z < p)%Z -> (((0%Z <= 1%Z)%Z /\ (1%Z < p)%Z) -> forall (next:(map Z
  Z)), (next = (set (const 0%Z:(map Z Z)) 1%Z 0%Z)) -> forall (j:Z) (i:Z)
  (next1:(map Z Z)), ((((((0%Z <= j)%Z /\ (j < i)%Z) /\ (i <= p)%Z) /\
  (matches p2 (i - j)%Z p2 0%Z j)) /\ forall (z:Z), (((j + 1%Z)%Z < z)%Z /\
  (z < (i + 1%Z)%Z)%Z) -> ~ (matches p2 ((i + 1%Z)%Z - z)%Z p2 0%Z z)) /\
  forall (k:Z), ((0%Z < k)%Z /\ (k <= i)%Z) -> (is_next p2 k (get next1
  k))) -> ((i < (p - 1%Z)%Z)%Z -> (((0%Z <= j)%Z /\ (j < p)%Z) ->
  (((0%Z <= i)%Z /\ (i < p)%Z) -> ((~ ((get p1 i) = (get p1 j))) ->
  ((~ (j = 0%Z)) -> (((0%Z <= j)%Z /\ (j < p)%Z) -> forall (j1:Z),
  (j1 = (get next1 j)) -> forall (z:Z), (((j1 + 1%Z)%Z < z)%Z /\
  (z < (i + 1%Z)%Z)%Z) -> ~ (matches p2 ((i + 1%Z)%Z - z)%Z p2 0%Z
  z))))))))))).
159
(* YOU MAY EDIT THE PROOF BELOW *)
Andrei Paskevich's avatar
Andrei Paskevich committed
160
intros n p1.
161
intro p3. unfold p3. clear p3.
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
intros _ _ hn _ _ _.
intros j i next4 ((((hj, hi), h0), h1), h2).
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
intros hi' _ _ neq j0 _.
intros j1 hji1; subst j1.

assert (hji: (0 < j <= i)%Z) by omega.
generalize (h2 j hji); clear h2.
unfold is_next. intros (hn1, (hn2, hn3)).

intros z hz.

assert (casez: (j+1 < z \/ z <= j+1)%Z) by omega. destruct casez.

(* j+1 < z *)
apply h1; omega. clear h1.
destruct hz as (hz,_).

assert (casez: (z = j+1 \/ z < j+1)%Z) by omega. destruct casez.

(* z = j+1 *)
subst z.
red; intro h. unfold matches, length , get1 in h. simpl in h.
destruct h as (hy1, (hy2, hy3)).
generalize (hy3 j%Z).
ring_simplify (i + 1 - (j + 1)+ j)%Z.
intro. absurd (get p1 i = get p1 j); intuition. 

(* z < j+1 *)
clear H. red; intro h.
absurd (matches (mk_array n p1)  (j - (z-1)) (mk_array n p1) 0 (z-1))%Z.
apply (hn3 (z-1)%Z); omega.
clear hn2 hn3.
apply matches_trans with (mk_array n p1) (i+1-z)%Z.

unfold matches, length, get1; simpl.
repeat split; try omega. intros.
unfold matches, length, get1 in h0. simpl in h0.
destruct h0 as (hy1, (hy2, hy3)).
assert (hi0: (0 <= j+1-z+i0 < j)%Z) by omega.
generalize (hy3 (j+1-z+i0) hi0)%Z.
ring_simplify (i - j + (j + 1 - z + i0))%Z.
ring_simplify (j - (z - 1) + i0)%Z.
ring_simplify (j + 1 - z + i0)%Z. ring_simplify (i + 1 - z + i0)%Z.
auto.
apply  matches_right_weakening with z; auto.
omega.
Qed.