example Dijkstra: proof in progress

parent 205f6b86
......@@ -178,7 +178,6 @@ pvsbin/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/binary_search_c/
/examples/programs/dijkstra/
/examples/why3bench.html
/examples/why3regtests.err
/examples/why3regtests.out
......
(* Dijkstra's shortest path algorithm *)
module M
(* Dijkstra's shortest path algorithm.
This proof follows Cormen et al's "Algorithms".
Author: Jean-Christophe Filliâtre (CNRS) *)
module DijkstraShortestPath
use import int.Int
use import ref.Ref
use set.Fset as S
use import map.Map as M
(* iteration on a set *)
val set_has_next (s: ref (S.set 'a)) : bool reads {s}
ensures { result = True <-> not (S.is_empty !s) }
val set_next (s: ref (S.set 'a)) : 'a writes {s}
requires { not S.is_empty !s }
ensures { S.mem result (old !s) /\ !s = S.remove result (old !s) }
(* the graph *)
(** The graph is introduced as a set v of vertices and a function g_succ
returning the successors of a given vertex.
The weight of an edge is defined independently, using function weight.
The weight is an integer. *)
type vertex
constant v : S.set vertex
constant v: S.set vertex
function g_succ(vertex) : S.set vertex
function g_succ vertex : S.set vertex
axiom G_succ_sound :
forall x:vertex. S.subset (g_succ x) v
forall x: vertex. S.subset (g_succ x) v
function weight vertex vertex : int (* edge weight, if there is an edge *)
axiom Weight_nonneg : forall x y:vertex. weight x y >= 0
axiom Weight_nonneg: forall x y: vertex. weight x y >= 0
val eq_vertex (x:vertex) (y:vertex) : bool
ensures { result = True <-> x = y }
(** Data structures for the algorithm. *)
(* visited vertices *)
(* The set of already visited vertices. *)
val visited : ref (S.set vertex)
val visited: ref (S.set vertex)
val visited_add (x:vertex) : unit writes {visited}
val visited_add (x: vertex) : unit writes {visited}
ensures { !visited = S.add x (old !visited) }
(* current distances *)
(* Map d holds the current distances from the source.
There is no need to introduce infinite distances. *)
val d : ref (M.map vertex int)
val d: ref (M.map vertex int)
(* priority queue *)
(* The priority queue. *)
val q : ref (S.set vertex)
val q: ref (S.set vertex)
val q_is_empty () : bool reads {q}
ensures { result = True <-> S.is_empty !q }
val init (src:vertex) : unit writes { visited, q, d }
predicate min (m: vertex) (q: S.set vertex) (d: M.map vertex int) =
S.mem m q /\
forall x: vertex. S.mem x q -> d[m] <= d[x]
val q_extract_min () : vertex reads {d} writes {q}
requires { not S.is_empty !q }
ensures { min result (old !q) !d }
ensures { !q = S.remove result (old !q) }
(* Initialisation of visited, q, and d. *)
val init (src: vertex) : unit writes { visited, q, d }
ensures { S.is_empty !visited }
ensures { !q = S.add src S.empty }
ensures { !d = (old !d)[src <- 0] }
(* Relaxation of edge u->v. *)
let relax u v
ensures {
(S.mem v !visited /\ !q = old !q /\ !d = old !d)
......@@ -78,116 +90,119 @@ module M
d := !d[v <- x]
end
predicate min (m:vertex) (q:S.set vertex) (d:M.map vertex int) =
S.mem m q /\
forall x:vertex. S.mem x q -> d[m] <= d[x]
val q_extract_min () : vertex reads {d} writes {q}
requires { not S.is_empty !q }
ensures { min result (old !q) !d /\ !q = S.remove result (old !q) }
(* Paths and shortest paths.
(* paths and shortest paths
path x y d =
there is a path from x to y of length d
shortest_path x y d =
there is a path from x to y of length d, and no shorter path *)
inductive path vertex vertex int =
| Path_nil :
forall x:vertex. path x x 0
| Path_cons :
forall x y z:vertex. forall d:int.
path x y d -> S.mem z (g_succ y) -> path x z (d+weight y z)
| Path_nil :
forall x: vertex. path x x 0
| Path_cons:
forall x y z: vertex. forall d: int.
path x y d -> S.mem z (g_succ y) -> path x z (d + weight y z)
lemma Length_nonneg : forall x y:vertex. forall d:int. path x y d -> d >= 0
lemma Length_nonneg: forall x y: vertex. forall d: int. path x y d -> d >= 0
predicate shortest_path (x y:vertex) (d:int) =
path x y d /\ forall d':int. path x y d' -> d <= d'
predicate shortest_path (x y: vertex) (d: int) =
path x y d /\ forall d': int. path x y d' -> d <= d'
lemma Path_inversion :
lemma Path_inversion:
forall src v:vertex. forall d:int. path src v d ->
(v = src /\ d = 0) \/
(exists v':vertex. path src v' (d - weight v' v) /\ S.mem v (g_succ v'))
lemma Path_shortest_path :
forall src v:vertex. forall d:int. path src v d ->
exists d':int. shortest_path src v d' /\ d' <= d
lemma Path_shortest_path:
forall src v: vertex. forall d: int. path src v d ->
exists d': int. shortest_path src v d' /\ d' <= d
(* lemmas (those requiring induction) *)
(* Lemmas (requiring induction). *)
lemma Main_lemma :
forall src v:vertex. forall d:int.
lemma Main_lemma:
forall src v: vertex. forall d: int.
path src v d -> not shortest_path src v d ->
exists v':vertex. exists d':int.
exists v': vertex. exists d': int.
shortest_path src v' d' /\ S.mem v (g_succ v') /\ d' + weight v' v < d
lemma Completeness_lemma :
forall s:S.set vertex. forall src:vertex. forall dst:vertex. forall d:int.
lemma Completeness_lemma:
forall s: S.set vertex.
(* if s is closed under g_succ *)
(forall v:vertex.
S.mem v s -> forall w:vertex. S.mem w (g_succ v) -> S.mem w s) ->
(forall v: vertex.
S.mem v s -> forall w: vertex. S.mem w (g_succ v) -> S.mem w s) ->
(* and if s contains src *)
S.mem src s ->
forall src: vertex. S.mem src s ->
(* then any vertex reachable from s is also in s *)
forall dst: vertex. forall d: int.
path src dst d -> S.mem dst s
(* definitions used in loop invariants *)
(* Definitions used in loop invariants. *)
predicate inv_src (src:vertex) (s q:S.set vertex) =
predicate inv_src (src: vertex) (s q: S.set vertex) =
S.mem src s \/ S.mem src q
predicate inv (src:vertex) (s q:S.set vertex) (d:M.map vertex int) =
inv_src src s q
(* S,Q are contained in V *)
/\ S.subset s v /\ S.subset q v
(* S /\ Q are disjoint *)
/\
(forall v:vertex. S.mem v q -> S.mem v s -> false)
predicate inv (src: vertex) (s q: S.set vertex) (d: M.map vertex int) =
inv_src src s q /\ d[src] = 0 /\
(* S and Q are contained in V *)
S.subset s v /\ S.subset q v /\
(* S and Q are disjoint *)
(forall v: vertex. S.mem v q -> S.mem v s -> false) /\
(* we already found the shortest paths for vertices in S *)
/\
(forall v:vertex. S.mem v s -> shortest_path src v d[v])
(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])
(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 ->
(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)
predicate inv_succ (src:vertex) (s q : S.set vertex) =
predicate inv_succ (src: vertex) (s q: S.set vertex) =
(* 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)
predicate inv_succ2 (src:vertex) (s q : S.set vertex)
(u:vertex) (su:S.set vertex) =
predicate inv_succ2 (src: vertex) (s q: S.set vertex)
(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) ->
(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)
(* code *)
(* Iteration on a set *)
val set_has_next (s: ref (S.set 'a)) : bool reads {s}
ensures { result = True <-> not (S.is_empty !s) }
val set_next (s: ref (S.set 'a)) : 'a writes {s}
requires { not S.is_empty !s }
ensures { S.mem result (old !s) }
ensures { !s = S.remove result (old !s) }
(* Algorithm's code. *)
let shortest_path_code (src:vertex) (dst:vertex)
let shortest_path_code (src dst: vertex)
requires { S.mem src v /\ S.mem dst v }
ensures { (forall v:vertex.
S.mem v !visited -> shortest_path src v !d[v]) }
ensures { (forall v:vertex.
not S.mem v !visited -> forall dv:int. not path src v dv) }
ensures { forall v: vertex. S.mem v !visited ->
shortest_path src v !d[v] }
ensures { forall v: vertex. not S.mem v !visited ->
forall dv: int. not path src v dv }
= init src;
while not (q_is_empty ()) do
invariant { inv src !visited !q !d /\ inv_succ src !visited !q }
invariant { inv src !visited !q !d }
invariant { inv_succ src !visited !q }
variant { S.cardinal v - S.cardinal !visited }
let u = q_extract_min () in
assert { shortest_path src u !d[u] };
visited_add u;
let su = ref (g_succ u) in
while not (set_has_next su) do
invariant{ S.subset !su (g_succ u) /\
inv src !visited !q !d /\ inv_succ2 src !visited !q u !su }
variant { S.cardinal !su }
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 }
variant { S.cardinal !su }
let v = set_next su in
relax u v
done
......
(* 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)).
(* Why3 goal *)
Theorem Length_nonneg : forall (x:vertex) (y:vertex), forall (d:Z), (path x y
d) -> (0%Z <= d)%Z.
induction 1; try omega.
generalize (Weight_nonneg y z); omega.
Qed.
(* 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</