bf_WP_BellmanFord_WP_parameter_relax_7.v 17.4 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
Require Import BuiltIn.
Require BuiltIn.
5 6 7 8 9
Require int.Int.

(* Why3 assumption *)
Definition unit  := unit.

Andrei Paskevich's avatar
Andrei Paskevich committed
10 11 12 13
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.
14

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
21 22 23
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).
24

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

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

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

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
36
Inductive list (a:Type) {a_WT:WhyType a} :=
37 38
  | Nil : list a
  | Cons : a -> (list a) -> list a.
Andrei Paskevich's avatar
Andrei Paskevich committed
39 40 41 42
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
43 44

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
45
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
46 47 48 49 50
  match l with
  | Nil => 0%Z
  | (Cons _ r) => (1%Z + (length r))%Z
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
51 52
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
  a)), (0%Z <= (length l))%Z.
53

Andrei Paskevich's avatar
Andrei Paskevich committed
54
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
55 56
  ((length l) = 0%Z) <-> (l = (Nil :(list a))).

Andrei Paskevich's avatar
Andrei Paskevich committed
57 58 59
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
60

Andrei Paskevich's avatar
Andrei Paskevich committed
61
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
62 63

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
64 65
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
  a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
66

Andrei Paskevich's avatar
Andrei Paskevich committed
67 68
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
  (s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
69 70

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
71 72
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
  a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
73

Andrei Paskevich's avatar
Andrei Paskevich committed
74 75
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
  (subset s s).
76

Andrei Paskevich's avatar
Andrei Paskevich committed
77 78 79
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
  (s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
  (subset s1 s3)).
80

Andrei Paskevich's avatar
Andrei Paskevich committed
81
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
82

Andrei Paskevich's avatar
Andrei Paskevich committed
83 84 85
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
  forall (x:a), ~ (mem x s).
86

Andrei Paskevich's avatar
Andrei Paskevich committed
87 88
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
  a))).
89

Andrei Paskevich's avatar
Andrei Paskevich committed
90
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
91

Andrei Paskevich's avatar
Andrei Paskevich committed
92 93
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
  forall (s:(set1 a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95 96
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
  a).
97

Andrei Paskevich's avatar
Andrei Paskevich committed
98 99
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (s:(set1 a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
100

Andrei Paskevich's avatar
Andrei Paskevich committed
101 102
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
  a)), (subset (remove x s) s).
103

Andrei Paskevich's avatar
Andrei Paskevich committed
104 105
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
  (set1 a).
106

Andrei Paskevich's avatar
Andrei Paskevich committed
107 108
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
  (s2:(set1 a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
109

Andrei Paskevich's avatar
Andrei Paskevich committed
110 111
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
  (set1 a).
112

Andrei Paskevich's avatar
Andrei Paskevich committed
113 114
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
  (s2:(set1 a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
115

Andrei Paskevich's avatar
Andrei Paskevich committed
116 117
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
  (set1 a).
118

Andrei Paskevich's avatar
Andrei Paskevich committed
119 120
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
  (s2:(set1 a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
121

Andrei Paskevich's avatar
Andrei Paskevich committed
122 123
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
  (s2:(set1 a)), (subset (diff s1 s2) s1).
124

Andrei Paskevich's avatar
Andrei Paskevich committed
125
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
126

Andrei Paskevich's avatar
Andrei Paskevich committed
127 128
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
  (~ (is_empty s)) -> (mem (choose s) s).
129

Andrei Paskevich's avatar
Andrei Paskevich committed
130
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> Z.
131

Andrei Paskevich's avatar
Andrei Paskevich committed
132 133
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1
  a)), (0%Z <= (cardinal s))%Z.
134

Andrei Paskevich's avatar
Andrei Paskevich committed
135
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
136 137
  ((cardinal s) = 0%Z) <-> (is_empty s).

Andrei Paskevich's avatar
Andrei Paskevich committed
138 139 140
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
  forall (s:(set1 a)), (~ (mem x s)) -> ((cardinal (add x
  s)) = (1%Z + (cardinal s))%Z).
141

Andrei Paskevich's avatar
Andrei Paskevich committed
142 143 144
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
  forall (s:(set1 a)), (mem x s) ->
  ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
145

Andrei Paskevich's avatar
Andrei Paskevich committed
146 147
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1
  a)) (s2:(set1 a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
150 151
  ((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).

Andrei Paskevich's avatar
Andrei Paskevich committed
152
Parameter nth: forall {a:Type} {a_WT:WhyType a}, Z -> (set1 a) -> a.
153

Andrei Paskevich's avatar
Andrei Paskevich committed
154 155 156
Axiom nth_injective : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a))
  (i:Z) (j:Z), ((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (((0%Z <= j)%Z /\
  (j < (cardinal s))%Z) -> (((nth i s) = (nth j s)) -> (i = j))).
157

Andrei Paskevich's avatar
Andrei Paskevich committed
158 159 160
Axiom nth_surjective : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a))
  (x:a), (mem x s) -> exists i:Z, ((0%Z <= i)%Z /\ (i < (cardinal s))%Z) ->
  (x = (nth i s)).
161

Andrei Paskevich's avatar
Andrei Paskevich committed
162 163 164
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179

Parameter vertices: (set1 vertex).

Parameter edges: (set1 (vertex* vertex)%type).

(* Why3 assumption *)
Definition edge(x:vertex) (y:vertex): Prop := (mem (x, y) edges).

Axiom edges_def : forall (x:vertex) (y:vertex), (mem (x, y) edges) -> ((mem x
  vertices) /\ (mem y vertices)).

Parameter s: vertex.

Axiom s_in_graph : (mem s vertices).

Andrei Paskevich's avatar
Andrei Paskevich committed
180
Axiom vertices_cardinal_pos : (0%Z < (cardinal vertices))%Z.
181 182

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
183 184
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
  a)) {struct l1}: (list a) :=
185 186 187 188 189
  match l1 with
  | Nil => l2
  | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
190 191
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
  (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
192 193
  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).

Andrei Paskevich's avatar
Andrei Paskevich committed
194 195
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
  ((infix_plpl l (Nil :(list a))) = l).
196

Andrei Paskevich's avatar
Andrei Paskevich committed
197 198 199
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
  (l2:(list a)), ((length (infix_plpl l1
  l2)) = ((length l1) + (length l2))%Z).
200 201

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
202
Fixpoint mem1 {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
203 204 205 206 207
  match l with
  | Nil => False
  | (Cons y r) => (x = y) \/ (mem1 x r)
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
208 209 210
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
  a)) (l2:(list a)), (mem1 x (infix_plpl l1 l2)) <-> ((mem1 x l1) \/ (mem1 x
  l2)).
211

Andrei Paskevich's avatar
Andrei Paskevich committed
212 213 214
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
  a)), (mem1 x l) -> exists l1:(list a), exists l2:(list a),
  (l = (infix_plpl l1 (Cons x l2))).
215 216 217 218 219 220 221 222 223 224 225 226 227

(* Why3 assumption *)
Inductive path : vertex -> (list vertex) -> vertex -> Prop :=
  | Path_empty : forall (x:vertex), (path x (Nil :(list vertex)) x)
  | Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
      (edge x y) -> ((path y l z) -> (path x (Cons x l) z)).

Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex) (l:(list
  vertex)), (path x l y) -> ((edge y z) -> (path x (infix_plpl l (Cons y
  (Nil :(list vertex)))) z)).

Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
  (path x l z) -> (((x = z) /\ (l = (Nil :(list vertex)))) \/
Andrei Paskevich's avatar
Andrei Paskevich committed
228 229
  exists y:vertex, exists l':(list vertex), (path x l' y) /\ ((edge y z) /\
  (l = (infix_plpl l' (Cons y (Nil :(list vertex))))))).
230 231 232 233 234 235 236 237

Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
  (l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
  (infix_plpl l1 l2) z)).

Axiom empty_path : forall (x:vertex) (y:vertex), (path x (Nil :(list vertex))
  y) -> (x = y).

Andrei Paskevich's avatar
Andrei Paskevich committed
238 239 240 241
Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list
  vertex)) (l2:(list vertex)), (path x (infix_plpl l1 (Cons y l2)) z) ->
  ((path x l1 y) /\ (path y (Cons y l2) z)).

242 243 244 245 246 247 248 249 250 251 252 253 254 255
Parameter weight: vertex -> vertex -> Z.

(* Why3 assumption *)
Fixpoint path_weight(l:(list vertex)) (dst:vertex) {struct l}: Z :=
  match l with
  | Nil => 0%Z
  | (Cons x Nil) => (weight x dst)
  | (Cons x ((Cons y _) as r)) => ((weight x y) + (path_weight r dst))%Z
  end.

Axiom path_weight_right_extension : forall (x:vertex) (y:vertex) (l:(list
  vertex)), ((path_weight (infix_plpl l (Cons x (Nil :(list vertex))))
  y) = ((path_weight l x) + (weight x y))%Z).

Andrei Paskevich's avatar
Andrei Paskevich committed
256 257 258 259
Axiom path_weight_decomposition : forall (y:vertex) (z:vertex) (l1:(list
  vertex)) (l2:(list vertex)), ((path_weight (infix_plpl l1 (Cons y l2))
  z) = ((path_weight l1 y) + (path_weight (Cons y l2) z))%Z).

260 261 262
Axiom path_in_vertices : forall (v1:vertex) (v2:vertex) (l:(list vertex)),
  (mem v1 vertices) -> ((path v1 l v2) -> (mem v2 vertices)).

Andrei Paskevich's avatar
Andrei Paskevich committed
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320
(* Why3 assumption *)
Definition pigeon_set(s1:(set1 vertex)): Prop := forall (l:(list vertex)),
  (forall (e:vertex), (mem1 e l) -> (mem e s1)) ->
  (((cardinal s1) < (length l))%Z -> exists e:vertex, exists l1:(list
  vertex), exists l2:(list vertex), exists l3:(list vertex),
  (l = (infix_plpl l1 (Cons e (infix_plpl l2 (Cons e l3)))))).

Axiom Induction : (forall (s1:(set1 vertex)), (is_empty s1) ->
  (pigeon_set s1)) -> ((forall (s1:(set1 vertex)), (pigeon_set s1) ->
  forall (t:vertex), (~ (mem t s1)) -> (pigeon_set (add t s1))) ->
  forall (s1:(set1 vertex)), (pigeon_set s1)).

Axiom corner : forall (s1:(set1 vertex)) (l:(list vertex)),
  ((length l) = (cardinal s1)) -> ((forall (e:vertex), (mem1 e l) -> (mem e
  s1)) -> ((exists e:vertex, (exists l1:(list vertex), (exists l2:(list
  vertex), (exists l3:(list vertex), (l = (infix_plpl l1 (Cons e
  (infix_plpl l2 (Cons e l3))))))))) \/ forall (e:vertex), (mem e s1) ->
  (mem1 e l))).

Axiom pigeon_0 : (pigeon_set (empty :(set1 vertex))).

Axiom pigeon_1 : forall (s1:(set1 vertex)), (pigeon_set s1) ->
  forall (t:vertex), (pigeon_set (add t s1)).

Axiom pigeon_2 : forall (s1:(set1 vertex)), (pigeon_set s1).

Axiom pigeonhole : forall (s1:(set1 vertex)) (l:(list vertex)),
  (forall (e:vertex), (mem1 e l) -> (mem e s1)) ->
  (((cardinal s1) < (length l))%Z -> exists e:vertex, exists l1:(list
  vertex), exists l2:(list vertex), exists l3:(list vertex),
  (l = (infix_plpl l1 (Cons e (infix_plpl l2 (Cons e l3)))))).

Axiom long_path_decomposition_pigeon1 : forall (l:(list vertex)) (v:vertex),
  (path s l v) -> ((~ (l = (Nil :(list vertex)))) -> forall (v1:vertex),
  (mem1 v1 (Cons v l)) -> (mem v1 vertices)).

Axiom long_path_decomposition_pigeon2 : forall (l:(list vertex)) (v:vertex),
  (forall (v1:vertex), (mem1 v1 (Cons v l)) -> (mem v1 vertices)) ->
  (((cardinal vertices) < (length (Cons v l)))%Z -> exists e:vertex,
  exists l1:(list vertex), exists l2:(list vertex), exists l3:(list vertex),
  ((Cons v l) = (infix_plpl l1 (Cons e (infix_plpl l2 (Cons e l3)))))).

Axiom long_path_decomposition_pigeon3 : forall (l:(list vertex)) (v:vertex),
  (exists e:vertex, (exists l1:(list vertex), (exists l2:(list vertex),
  (exists l3:(list vertex), ((Cons v l) = (infix_plpl l1 (Cons e
  (infix_plpl l2 (Cons e l3))))))))) -> ((exists l1:(list vertex),
  (exists l2:(list vertex), (l = (infix_plpl l1 (Cons v l2))))) \/
  exists n:vertex, exists l1:(list vertex), exists l2:(list vertex),
  exists l3:(list vertex), (l = (infix_plpl l1 (Cons n (infix_plpl l2 (Cons n
  l3)))))).

Axiom long_path_decomposition : forall (l:(list vertex)) (v:vertex), (path s
  l v) -> (((cardinal vertices) <= (length l))%Z -> ((exists l1:(list
  vertex), (exists l2:(list vertex), (l = (infix_plpl l1 (Cons v l2))))) \/
  exists n:vertex, exists l1:(list vertex), exists l2:(list vertex),
  exists l3:(list vertex), (l = (infix_plpl l1 (Cons n (infix_plpl l2 (Cons n
  l3))))))).

321
Axiom simple_path : forall (v:vertex) (l:(list vertex)), (path s l v) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
322 323
  exists l':(list vertex), (path s l' v) /\
  ((length l') < (cardinal vertices))%Z.
324 325 326 327

(* Why3 assumption *)
Definition negative_cycle(v:vertex): Prop := (mem v vertices) /\
  ((exists l1:(list vertex), (path s l1 v)) /\ exists l2:(list vertex),
Andrei Paskevich's avatar
Andrei Paskevich committed
328
  (path v l2 v) /\ ((path_weight l2 v) < 0%Z)%Z).
329 330

Axiom key_lemma_1 : forall (v:vertex) (n:Z), (forall (l:(list vertex)),
Andrei Paskevich's avatar
Andrei Paskevich committed
331
  (path s l v) -> (((length l) < (cardinal vertices))%Z ->
332
  (n <= (path_weight l v))%Z)) -> ((exists l:(list vertex), (path s l v) /\
Andrei Paskevich's avatar
Andrei Paskevich committed
333
  ((path_weight l v) < n)%Z) -> exists u:vertex, (negative_cycle u)).
334 335 336 337 338

(* Why3 assumption *)
Inductive t  :=
  | Finite : Z -> t 
  | Infinite : t .
Andrei Paskevich's avatar
Andrei Paskevich committed
339 340
Axiom t_WhyType : WhyType t.
Existing Instance t_WhyType.
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359

(* Why3 assumption *)
Definition add1(x:t) (y:t): t :=
  match x with
  | Infinite => Infinite
  | (Finite x1) =>
      match y with
      | Infinite => Infinite
      | (Finite y1) => (Finite (x1 + y1)%Z)
      end
  end.

(* Why3 assumption *)
Definition lt(x:t) (y:t): Prop :=
  match x with
  | Infinite => False
  | (Finite x1) =>
      match y with
      | Infinite => True
Andrei Paskevich's avatar
Andrei Paskevich committed
360
      | (Finite y1) => (x1 < y1)%Z
361 362 363 364 365 366 367 368 369 370 371 372 373 374 375
      end
  end.

(* Why3 assumption *)
Definition le(x:t) (y:t): Prop := (lt x y) \/ (x = y).

Axiom Refl : forall (x:t), (le x x).

Axiom Trans : forall (x:t) (y:t) (z:t), (le x y) -> ((le y z) -> (le x z)).

Axiom Antisymm : forall (x:t) (y:t), (le x y) -> ((le y x) -> (x = y)).

Axiom Total : forall (x:t) (y:t), (le x y) \/ (le y x).

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
376
Inductive ref (a:Type) {a_WT:WhyType a} :=
377
  | mk_ref : a -> ref a.
Andrei Paskevich's avatar
Andrei Paskevich committed
378 379 380
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
381 382

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
383
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
384 385 386 387 388
  match v with
  | (mk_ref x) => x
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
389
Definition t1 (a:Type) {a_WT:WhyType a} := (ref (set1 a)).
390 391 392 393 394 395 396 397 398 399

(* Why3 assumption *)
Definition distmap  := (map vertex t).

(* Why3 assumption *)
Definition inv1(m:(map vertex t)) (pass:Z) (via:(set1 (vertex*
  vertex)%type)): Prop := forall (v:vertex), (mem v vertices) -> match (get m
  v) with
  | (Finite n) => (exists l:(list vertex), (path s l v) /\ ((path_weight l
      v) = n)) /\ ((forall (l:(list vertex)), (path s l v) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
400
      (((length l) < pass)%Z -> (n <= (path_weight l v))%Z)) /\
401
      forall (u:vertex) (l:(list vertex)), (path s l u) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
402
      (((length l) < pass)%Z -> ((mem (u, v) via) -> (n <= ((path_weight l
403 404 405 406 407 408 409 410 411 412 413
      u) + (weight u v))%Z)%Z)))
  | Infinite => (forall (l:(list vertex)), (path s l v) ->
      (pass <= (length l))%Z) /\ forall (u:vertex), (mem (u, v) via) ->
      forall (lu:(list vertex)), (path s lu u) -> (pass <= (length lu))%Z
  end.

(* Why3 assumption *)
Definition inv2(m:(map vertex t)) (via:(set1 (vertex* vertex)%type)): Prop :=
  forall (u:vertex) (v:vertex), (mem (u, v) via) -> (le (get m v)
  (add1 (get m u) (Finite (weight u v)))).

Andrei Paskevich's avatar
Andrei Paskevich committed
414 415 416
Axiom key_lemma_2 : forall (m:(map vertex t)), (inv1 m (cardinal vertices)
  (empty :(set1 (vertex* vertex)%type))) -> ((inv2 m edges) ->
  forall (v:vertex), ~ (negative_cycle v)).
417 418 419 420 421 422

Require Import Why3.
Ltac ae := why3 "alt-ergo".
Require Import Classical.

(* Why3 goal *)
Andrei Paskevich's avatar
Andrei Paskevich committed
423 424 425 426
Theorem WP_parameter_relax : forall (u:vertex) (v:vertex) (pass:Z) (via:(set1
  (vertex* vertex)%type)), forall (m:(map vertex t)), ((((1%Z < pass)%Z \/
  (1%Z = pass)) /\ ((mem (u, v) edges) /\ ~ (mem (u, v) via))) /\
  forall (v1:vertex), (mem v1 vertices) -> match (get m
427 428 429
  v1) with
  | (Finite n) => (exists l:(list vertex), (path s l v1) /\ ((path_weight l
      v1) = n)) /\ ((forall (l:(list vertex)), (path s l v1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
430
      (((length l) < pass)%Z -> (n <= (path_weight l v1))%Z)) /\
431
      forall (u1:vertex) (l:(list vertex)), (path s l u1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
432
      (((length l) < pass)%Z -> ((mem (u1, v1) via) -> (n <= ((path_weight l
433 434 435 436
      u1) + (weight u1 v1))%Z)%Z)))
  | Infinite => (forall (l:(list vertex)), (path s l v1) ->
      (pass <= (length l))%Z) /\ forall (u1:vertex), (mem (u1, v1) via) ->
      forall (lu:(list vertex)), (path s lu u1) -> (pass <= (length lu))%Z
Andrei Paskevich's avatar
Andrei Paskevich committed
437
  end) -> (match (get m
438 439 440 441 442
  u) with
  | Infinite => False
  | (Finite x) => match (get m
      v) with
      | Infinite => True
Andrei Paskevich's avatar
Andrei Paskevich committed
443
      | (Finite y) => ((x + (weight u v))%Z < y)%Z
444 445 446 447 448 449 450 451 452 453 454
      end
  end -> forall (m1:(map vertex t)), (m1 = (set m v match (get m
  u) with
  | Infinite => Infinite
  | (Finite x) => (Finite (x + (weight u v))%Z)
  end)) -> forall (v1:vertex), (mem v1 vertices) -> match (get m1
  v1) with
  | (Finite n) => exists l:(list vertex), (path s l v1) /\ ((path_weight l
      v1) = n)
  | Infinite => True
  end).
Andrei Paskevich's avatar
Andrei Paskevich committed
455
intros u v pass via m ((hpass, (h1, h2)), h3).
456 457 458 459 460 461 462 463 464 465 466 467
destruct (get m u) as [] _eqn. 2:intuition.
intros hlt m1 eqm1 v1 hv1.
destruct (classic (v1 = v)) as [h|h].
subst m1 v1. rewrite Select_eq; auto.
assert (H : exists lu: list vertex, path s lu u /\ path_weight lu u = z) by ae.
destruct H as (lu, (hu1, hu2)).
exists (infix_plpl lu (Cons u Nil)); ae.
subst m1. rewrite Select_neq; auto.
ae.
Qed.