dijkstra: proof completed

examples/programs/dijkstra.mlw

@@ -123,7 +123,9 @@ module DijkstraShortestPath
 
   lemma Main_lemma:
     forall src v: vertex. forall d: int.
-    path src v d -> not shortest_path src v d ->
+    path src v d -> not (shortest_path src v d) ->
+    v = src /\ d > 0
+    \/
     exists v': vertex. exists d': int.
       shortest_path src v' d' /\ S.mem v (g_succ v') /\ d' + weight v' v < d
 
@@ -152,24 +154,22 @@ module DijkstraShortestPath
     (* we already found the shortest paths for vertices in S *)
     (forall v: vertex. S.mem v s -> shortest_path src v d[v]) /\
     (* there are paths for vertices in Q *)
-    (forall v: vertex. S.mem v q -> path src v d[v]) /\
-    (* vertices at distance < min(Q) are already in S *)
-    (forall m: vertex. min m q d ->
-       forall x: vertex. forall dx: int. (*shortest_*)path src x dx ->
-         dx < d[m] -> S.mem x s)
+    (forall v: vertex. S.mem v q -> path src v d[v])
 
-  predicate inv_succ (src: vertex) (s q: S.set vertex) =
+  predicate inv_succ (src: vertex) (s q: S.set vertex) (d: M.map vertex int) =
     (* successors of vertices in S are either in S or in Q *)
-    (forall x: vertex. S.mem x s ->
-       forall y: vertex. S.mem y (g_succ x) -> S.mem y s \/ S.mem y q)
+    forall x: vertex. S.mem x s ->
+    forall y: vertex. S.mem y (g_succ x) ->
+    (S.mem y s \/ S.mem y q) /\ d[y] <= d[x] + weight x y
 
-  predicate inv_succ2 (src: vertex) (s q: S.set vertex)
+  predicate inv_succ2 (src: vertex) (s q: S.set vertex) (d: M.map vertex int)
                       (u: vertex) (su: S.set vertex) =
     (* successors of vertices in S are either in S or in Q,
        unless they are successors of u still in su *)
-    (forall x: vertex. S.mem x s ->
-       forall y: vertex. S.mem y (g_succ x) ->
-         (x<>u \/ (x=u /\ not S.mem y su)) -> S.mem y s \/ S.mem y q)
+    forall x: vertex. S.mem x s ->
+    forall y: vertex. S.mem y (g_succ x) ->
+    (x<>u \/ (x=u /\ not (S.mem y su))) ->
+    (S.mem y s \/ S.mem y q) /\ d[y] <= d[x] + weight x y
 
   (* Iteration on a set *)
 
@@ -192,7 +192,11 @@ module DijkstraShortestPath
   = init src;
     while not (q_is_empty ()) do
       invariant { inv src !visited !q !d }
-      invariant { inv_succ src !visited !q }
+      invariant { inv_succ src !visited !q !d }
+      invariant { (* vertices at distance < min(Q) are already in S *)
+                  forall m: vertex. min m !q !d ->
+                  forall x: vertex. forall dx: int. path src x dx ->
+                  dx < !d[m] -> S.mem x !visited }
       variant   { S.cardinal v - S.cardinal !visited }
       let u = q_extract_min () in
       assert { shortest_path src u !d[u] };
@@ -201,10 +205,11 @@ module DijkstraShortestPath
       while set_has_next su do
         invariant { S.subset !su (g_succ u) }
         invariant { inv src !visited !q !d  }
-        invariant { inv_succ2 src !visited !q u !su }
+        invariant { inv_succ2 src !visited !q !d u !su }
         variant   { S.cardinal !su }
         let v = set_next su in
-        relax u v
+        relax u v;
+        assert { !d[v] <= !d[u] + weight u v }
       done
     done
 

examples/programs/dijkstra/dijkstra_DijkstraShortestPath_Completeness_lemma_1.v

+(* 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.
+
+(* 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 set : forall (a:Type) {a_WT:WhyType a}, Type.
+Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
+Existing Instance set_WhyType.
+
+Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
+
+(* Why3 assumption *)
+Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
+  a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
+
+Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
+
+(* Why3 assumption *)
+Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
+  forall (x:a), (mem x s1) -> (mem x s2).
+
+Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  (subset s s).
+
+Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
+  s3)).
+
+Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
+
+(* Why3 assumption *)
+Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
+  forall (x:a), ~ (mem x s).
+
+Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set
+  a))).
+
+Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
+  (empty :(set a))).
+
+Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
+
+Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
+  forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
+
+Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
+
+Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
+  (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
+
+Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
+  a)), (subset (remove x s) s).
+
+Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+  a).
+
+Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
+
+Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+  a).
+
+Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
+
+Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+  a).
+
+Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
+
+Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)), (subset (diff s1 s2) s1).
+
+Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
+
+Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  (~ (is_empty s)) -> (mem (choose s) s).
+
+Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
+
+Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  (0%Z <= (cardinal s))%Z.
+
+Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  ((cardinal s) = 0%Z) <-> (is_empty s).
+
+Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
+  forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
+  s)) = (1%Z + (cardinal s))%Z).
+
+Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
+  forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
+  s)))%Z).
+
+Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
+
+Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  ((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
+
+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 set1: 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 (set1 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 (set1 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).
+
+Axiom vertex : Type.
+Parameter vertex_WhyType : WhyType vertex.
+Existing Instance vertex_WhyType.
+
+Parameter v: (set vertex).
+
+Parameter g_succ: vertex -> (set vertex).
+
+Axiom G_succ_sound : forall (x:vertex), (subset (g_succ x) v).
+
+Parameter weight: vertex -> vertex -> Z.
+
+Axiom Weight_nonneg : forall (x:vertex) (y:vertex), (0%Z <= (weight x y))%Z.
+
+(* Why3 assumption *)
+Definition min(m:vertex) (q:(set vertex)) (d:(map vertex Z)): Prop := (mem m
+  q) /\ forall (x:vertex), (mem x q) -> ((get d m) <= (get d x))%Z.
+
+(* Why3 assumption *)
+Inductive path : vertex -> vertex -> Z -> Prop :=
+  | Path_nil : forall (x:vertex), (path x x 0%Z)
+  | Path_cons : forall (x:vertex) (y:vertex) (z:vertex), forall (d:Z),
+      (path x y d) -> ((mem z (g_succ y)) -> (path x z (d + (weight y z))%Z)).
+
+Axiom Length_nonneg : forall (x:vertex) (y:vertex), forall (d:Z), (path x y
+  d) -> (0%Z <= d)%Z.
+
+(* Why3 assumption *)
+Definition shortest_path(x:vertex) (y:vertex) (d:Z): Prop := (path x y d) /\
+  forall (d':Z), (path x y d') -> (d <= d')%Z.
+
+Axiom Path_inversion : forall (src:vertex) (v1:vertex), forall (d:Z),
+  (path src v1 d) -> (((v1 = src) /\ (d = 0%Z)) \/ exists v':vertex,
+  (path src v' (d - (weight v' v1))%Z) /\ (mem v1 (g_succ v'))).
+
+Axiom Path_shortest_path : forall (src:vertex) (v1:vertex), forall (d:Z),
+  (path src v1 d) -> exists d':Z, (shortest_path src v1 d') /\ (d' <= d)%Z.
+
+Axiom Main_lemma : forall (src:vertex) (v1:vertex), forall (d:Z), (path src
+  v1 d) -> ((~ (shortest_path src v1 d)) -> exists v':vertex, exists d':Z,
+  (shortest_path src v' d') /\ ((mem v1 (g_succ v')) /\ ((d' + (weight v'
+  v1))%Z < d)%Z)).
+
+Require Import Why3. Ltac ae := why3 "alt-ergo".
+
+(* Why3 goal *)
+Theorem Completeness_lemma : forall (s:(set vertex)), (forall (v1:vertex),
+  (mem v1 s) -> forall (w:vertex), (mem w (g_succ v1)) -> (mem w s)) ->
+  forall (src:vertex), (mem src s) -> forall (dst:vertex), forall (d:Z),
+  (path src dst d) -> (mem dst s).
+intros s h1 src h2 dst d h3.
+induction h3; trivial.
+ae.
+Qed.
+
+

examples/programs/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_1.v

@@ -181,9 +181,9 @@ Axiom Path_shortest_path : forall (src:vertex) (v1:vertex), forall (d:Z),
   (path src v1 d) -> exists d':Z, (shortest_path src v1 d') /\ (d' <= d)%Z.
 
 Axiom Main_lemma : forall (src:vertex) (v1:vertex), forall (d:Z), (path src
-  v1 d) -> ((~ (shortest_path src v1 d)) -> exists v':vertex, exists d':Z,
-  (shortest_path src v' d') /\ ((mem v1 (g_succ v')) /\ ((d' + (weight v'
-  v1))%Z < d)%Z)).
+  v1 d) -> ((~ (shortest_path src v1 d)) -> (((v1 = src) /\ (0%Z < d)%Z) \/
+  exists v':vertex, exists d':Z, (shortest_path src v' d') /\ ((mem v1
+  (g_succ v')) /\ ((d' + (weight v' v1))%Z < d)%Z))).
 
 Axiom Completeness_lemma : forall (s:(set vertex)), (forall (v1:vertex),
   (mem v1 s) -> forall (w:vertex), (mem w (g_succ v1)) -> (mem w s)) ->
@@ -252,7 +252,6 @@ intros dx IH x pathx hdx.
 destruct (Path_inversion _ _ _ pathx).
 ae.
 
-ae.
 
 Qed.
 

examples/programs/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v

@@ -181,9 +181,9 @@ Axiom Path_shortest_path : forall (src:vertex) (v1:vertex), forall (d:Z),
   (path src v1 d) -> exists d':Z, (shortest_path src v1 d') /\ (d' <= d)%Z.
 
 Axiom Main_lemma : forall (src:vertex) (v1:vertex), forall (d:Z), (path src
-  v1 d) -> ((~ (shortest_path src v1 d)) -> exists v':vertex, exists d':Z,
-  (shortest_path src v' d') /\ ((mem v1 (g_succ v')) /\ ((d' + (weight v'
-  v1))%Z < d)%Z)).
+  v1 d) -> ((~ (shortest_path src v1 d)) -> (((v1 = src) /\ (0%Z < d)%Z) \/
+  exists v':vertex, exists d':Z, (shortest_path src v' d') /\ ((mem v1
+  (g_succ v')) /\ ((d' + (weight v' v1))%Z < d)%Z))).
 
 Axiom Completeness_lemma : forall (s:(set vertex)), (forall (v1:vertex),
   (mem v1 s) -> forall (w:vertex), (mem w (g_succ v1)) -> (mem w s)) ->
@@ -199,20 +199,20 @@ Definition inv(src:vertex) (s:(set vertex)) (q:(set vertex)) (d:(map vertex
   Z)): Prop := (inv_src src s q) /\ (((get d src) = 0%Z) /\ ((subset s v) /\
   ((subset q v) /\ ((forall (v1:vertex), (mem v1 q) -> ~ (mem v1 s)) /\
   ((forall (v1:vertex), (mem v1 s) -> (shortest_path src v1 (get d v1))) /\
-  ((forall (v1:vertex), (mem v1 q) -> (path src v1 (get d v1))) /\
-  forall (m:vertex), (min m q d) -> forall (x:vertex), forall (dx:Z),
-  (path src x dx) -> ((dx < (get d m))%Z -> (mem x s)))))))).
+  forall (v1:vertex), (mem v1 q) -> (path src v1 (get d v1))))))).
 
 (* Why3 assumption *)
-Definition inv_succ(src:vertex) (s:(set vertex)) (q:(set vertex)): Prop :=
-  forall (x:vertex), (mem x s) -> forall (y:vertex), (mem y (g_succ x)) ->
-  ((mem y s) \/ (mem y q)).
+Definition inv_succ(src:vertex) (s:(set vertex)) (q:(set vertex)) (d:(map
+  vertex Z)): Prop := forall (x:vertex), (mem x s) -> forall (y:vertex),
+  (mem y (g_succ x)) -> (((mem y s) \/ (mem y q)) /\ ((get d y) <= ((get d
+  x) + (weight x y))%Z)%Z).
 
 (* Why3 assumption *)
-Definition inv_succ2(src:vertex) (s:(set vertex)) (q:(set vertex)) (u:vertex)
-  (su:(set vertex)): Prop := forall (x:vertex), (mem x s) ->
-  forall (y:vertex), (mem y (g_succ x)) -> (((~ (x = u)) \/ ((x = u) /\
-  ~ (mem y su))) -> ((mem y s) \/ (mem y q))).
+Definition inv_succ2(src:vertex) (s:(set vertex)) (q:(set vertex)) (d:(map
+  vertex Z)) (u:vertex) (su:(set vertex)): Prop := forall (x:vertex), (mem x
+  s) -> forall (y:vertex), (mem y (g_succ x)) -> (((~ (x = u)) \/ ((x = u) /\
+  ~ (mem y su))) -> (((mem y s) \/ (mem y q)) /\ ((get d y) <= ((get d
+  x) + (weight x y))%Z)%Z)).
 
 Require Import Why3. Ltac ae := why3 "alt-ergo".
 
@@ -222,16 +222,18 @@ Theorem WP_parameter_shortest_path_code : forall (src:vertex) (dst:vertex),
   vertex)) (d1:(map vertex Z)) (visited:(set vertex)), (((forall (x:vertex),
   ~ (mem x visited)) /\ (q = (add src (empty :(set vertex))))) /\
   (d1 = (set1 d src 0%Z))) -> forall (q1:(set vertex)) (d2:(map vertex Z))
-  (visited1:(set vertex)), (((inv_src src visited1 q1) /\ (((get d2
+  (visited1:(set vertex)), ((((inv_src src visited1 q1) /\ (((get d2
   src) = 0%Z) /\ ((subset visited1 v) /\ ((subset q1 v) /\
   ((forall (v1:vertex), (mem v1 q1) -> ~ (mem v1 visited1)) /\
   ((forall (v1:vertex), (mem v1 visited1) -> (shortest_path src v1 (get d2
-  v1))) /\ ((forall (v1:vertex), (mem v1 q1) -> (path src v1 (get d2 v1))) /\
-  forall (m:vertex), (min m q1 d2) -> forall (x:vertex), forall (dx:Z),
-  (path src x dx) -> ((dx < (get d2 m))%Z -> (mem x visited1))))))))) /\
-  forall (x:vertex), (mem x visited1) -> forall (y:vertex), (mem y
-  (g_succ x)) -> ((mem y visited1) \/ (mem y q1))) -> forall (o:bool),
-  ((o = true) <-> forall (x:vertex), ~ (mem x q1)) -> ((~ (o = true)) ->
+  v1))) /\ forall (v1:vertex), (mem v1 q1) -> (path src v1 (get d2
+  v1)))))))) /\ forall (x:vertex), (mem x visited1) -> forall (y:vertex),
+  (mem y (g_succ x)) -> (((mem y visited1) \/ (mem y q1)) /\ ((get d2
+  y) <= ((get d2 x) + (weight x y))%Z)%Z)) /\ forall (m:vertex), ((mem m
+  q1) /\ forall (x:vertex), (mem x q1) -> ((get d2 m) <= (get d2 x))%Z) ->
+  forall (x:vertex), forall (dx:Z), (path src x dx) -> ((dx < (get d2
+  m))%Z -> (mem x visited1))) -> forall (o:bool), ((o = true) <->
+  forall (x:vertex), ~ (mem x q1)) -> ((~ (o = true)) ->
   ((~ forall (x:vertex), ~ (mem x q1)) -> forall (q2:(set vertex)),
   forall (u:vertex), (((mem u q1) /\ forall (x:vertex), (mem x q1) ->
   ((get d2 u) <= (get d2 x))%Z) /\ (q2 = (remove u q1))) -> (((path src u
@@ -242,35 +244,33 @@ Theorem WP_parameter_shortest_path_code : forall (src:vertex) (dst:vertex),
   visited2 q3) /\ (((get d3 src) = 0%Z) /\ ((subset visited2 v) /\
   ((subset q3 v) /\ ((forall (v1:vertex), (mem v1 q3) -> ~ (mem v1
   visited2)) /\ ((forall (v1:vertex), (mem v1 visited2) -> (shortest_path src
-  v1 (get d3 v1))) /\ ((forall (v1:vertex), (mem v1 q3) -> (path src v1
-  (get d3 v1))) /\ forall (m:vertex), (min m q3 d3) -> forall (x:vertex),
-  forall (dx:Z), (path src x dx) -> ((dx < (get d3 m))%Z -> (mem x
-  visited2)))))))))) /\ forall (x:vertex), (mem x visited2) ->
-  forall (y:vertex), (mem y (g_succ x)) -> (((~ (x = u)) \/ ((x = u) /\
-  ~ (mem y su))) -> ((mem y visited2) \/ (mem y q3)))) ->
-  forall (result:bool), ((result = true) <-> ~ forall (x:vertex), ~ (mem x
-  su)) -> ((result = true) -> ((~ forall (x:vertex), ~ (mem x su)) ->
-  forall (su1:(set vertex)), forall (v1:vertex), ((mem v1 su) /\
-  (su1 = (remove v1 su))) -> forall (q4:(set vertex)) (d4:(map vertex Z)),
-  (((mem v1 visited2) /\ ((q4 = q3) /\ (d4 = d3))) \/ (((mem v1 q4) /\
-  (((get d4 v1) <= ((get d4 u) + (weight u v1))%Z)%Z /\ ((q4 = q3) /\
-  (d4 = d3)))) \/ (((mem v1 q4) /\ ((((get d3 u) + (weight u v1))%Z < (get d3
-  v1))%Z /\ ((q4 = q3) /\ (d4 = (set1 d3 v1 ((get d3 u) + (weight u
-  v1))%Z))))) \/ ((~ (mem v1 visited2)) /\ ((~ (mem v1 q3)) /\ ((q4 = (add v1
-  q3)) /\ (d4 = (set1 d3 v1 ((get d3 u) + (weight u v1))%Z)))))))) ->
-  forall (v2:vertex), (mem v2 q4) -> (path src v2 (get d4 v2))))))).
+  v1 (get d3 v1))) /\ forall (v1:vertex), (mem v1 q3) -> (path src v1 (get d3
+  v1))))))))) /\ forall (x:vertex), (mem x visited2) -> forall (y:vertex),
+  (mem y (g_succ x)) -> (((~ (x = u)) \/ ((x = u) /\ ~ (mem y su))) ->
+  (((mem y visited2) \/ (mem y q3)) /\ ((get d3 y) <= ((get d3 x) + (weight x
+  y))%Z)%Z))) -> forall (result:bool), ((result = true) <->
+  ~ forall (x:vertex), ~ (mem x su)) -> ((result = true) ->
+  ((~ forall (x:vertex), ~ (mem x su)) -> forall (su1:(set vertex)),
+  forall (v1:vertex), ((mem v1 su) /\ (su1 = (remove v1 su))) ->
+  forall (q4:(set vertex)) (d4:(map vertex Z)), (((mem v1 visited2) /\
+  ((q4 = q3) /\ (d4 = d3))) \/ (((mem v1 q4) /\ (((get d4 v1) <= ((get d4
+  u) + (weight u v1))%Z)%Z /\ ((q4 = q3) /\ (d4 = d3)))) \/ (((mem v1 q4) /\
+  ((((get d3 u) + (weight u v1))%Z < (get d3 v1))%Z /\ ((q4 = q3) /\
+  (d4 = (set1 d3 v1 ((get d3 u) + (weight u v1))%Z))))) \/ ((~ (mem v1
+  visited2)) /\ ((~ (mem v1 q3)) /\ ((q4 = (add v1 q3)) /\ (d4 = (set1 d3 v1
+  ((get d3 u) + (weight u v1))%Z)))))))) -> ((((get d4 v1) < ((get d4
+  u) + (weight u v1))%Z)%Z \/ ((get d4 v1) = ((get d4 u) + (weight u
+  v1))%Z)) -> forall (v2:vertex), (mem v2 q4) -> (path src v2 (get d4
+  v2)))))))).
+(*
 intros src dst d (h1,h2) q d1 visited ((h3,h4),h5) q1 d2 visited1
-((h6,(h7,(h8,(h9,(h10,(h11,(h12,h13))))))),h14) o h15 h16 h17 q2 u
+((h6,(h7,(h8,(h9,(h10,(h11,h12)))))),h14) o h15 h16 h17 q2 u
 ((h18,h19),h20) (h21,h22) visited2 h23 su q3 d3
 ((h24,(h25,(h26,(h27,(h28,(h29,(h30,(h31,h32)))))))),h33) result h34 h35 h36
 su1 v1 (h37,h38) q4 d4 h39 v2 h40.
+*)
+intuition; try ae.
 
-destruct h39.
-ae.
-destruct H.
-ae.
-destruct H.
-decompose [and] H; clear H.
 assert (case: (v2 = v1 \/ v2 <> v1)) by ae. destruct case.
 subst v2 d4; rewrite Select_eq.
 apply Path_cons.
@@ -280,11 +280,11 @@ trivial.
 subst d4; rewrite Select_neq.
 ae.
 ae.
-decompose [and] H; clear H.
+
 assert (case: (v2 = v1 \/ v2 <> v1)) by ae. destruct case.
 subst v2 d4; rewrite Select_eq.
 apply Path_cons.
-ae.
+why3 "z3".
 ae.
 trivial.
 ae.

examples/programs/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v

+(* 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.
+
+(* 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 set : forall (a:Type) {a_WT:WhyType a}, Type.
+Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
+Existing Instance set_WhyType.
+
+Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
+
+(* Why3 assumption *)
+Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
+  a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
+
+Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
+
+(* Why3 assumption *)
+Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
+  forall (x:a), (mem x s1) -> (mem x s2).
+
+Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  (subset s s).
+
+Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
+  s3)).
+
+Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
+
+(* Why3 assumption *)
+Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
+  forall (x:a), ~ (mem x s).
+
+Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set
+  a))).
+
+Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
+  (empty :(set a))).
+
+Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
+
+Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
+  forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
+
+Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
+
+Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
+  (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
+
+Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
+  a)), (subset (remove x s) s).
+
+Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+  a).
+
+Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
+
+Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+  a).
+
+Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
+
+Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+  a).
+
+Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
+
+Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+  (s2:(set a)), (subset (diff s1 s2) s1).
+
+Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
+
+Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+  (~ (is_empty s)) -> (mem (choose s) s).
+
+Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
+