kmp_WP_KnuthMorrisPratt_WP_parameter_initnext_2.v 6.87 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 159
(* 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)) ->
  forall (i1:Z), (i1 = (i + 1%Z)%Z) -> forall (j1:Z), (j1 = (j + 1%Z)%Z) ->
  (((0%Z <= i1)%Z /\ (i1 < p)%Z) -> forall (next2:(map Z Z)),
  (next2 = (set next1 i1 j1)) -> forall (z:Z), (((j1 + 1%Z)%Z < z)%Z /\
  (z < (i1 + 1%Z)%Z)%Z) -> ~ (matches p2 ((i1 + 1%Z)%Z - z)%Z p2 0%Z
  z)))))))))).
160
(* YOU MAY EDIT THE PROOF BELOW *)
Andrei Paskevich's avatar
Andrei Paskevich committed
161
intros n p1.
162
intro p3. unfold p3. clear p3.
Andrei Paskevich's avatar
Andrei Paskevich committed
163 164
intros _ _ hn _ _ _.
intros j i next4 ((((hj, hi), h0), h1), h2).
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
intros hi' _ _ eq.
intros i1 hi1; subst i1.
intros j1 hji1; subst j1.
intros _ _ _ z hz.
red; intro h. unfold matches, length , get1 in h. simpl in h.
destruct h as (hy1, (hy2, hy3)).

apply h1 with (z-1)%Z.
omega.
red; unfold length, get1; simpl.
repeat split; try omega.
intros.
replace (i + 1 - (z - 1) + i0)%Z with (i + 1 + 1 - z + i0)%Z by omega.
apply hy3.
omega.
Qed.