:: Dijkstra's Shortest Path Algorithm :: by Jing-Chao Chen :: :: Received March 17, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FINSEQ_1, INT_1, RELAT_1, FUNCT_1, ORDINAL4, XBOOLE_0, XXREAL_0, PARTFUN1, GRAPH_1, STRUCT_0, TREES_2, GLIB_000, GRAPH_5, CARD_3, GRAPH_4, NAT_1, ARYTM_3, TARSKI, CARD_1, FINSET_1, FUNCT_4, REAL_1, FUNCT_2, ARYTM_1, GRAPHSP, XREAL_0; notations XCMPLX_0, XXREAL_0, REAL_1, INT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, ORDINAL1, XREAL_0, STRUCT_0, GRAPH_1, PARTFUN1, FUNCT_2, CQC_SIM1, GRAPH_4, GRAPH_5, NAT_D, DOMAIN_1, RVSUM_1, NUMBERS, FUNCT_7, NAT_1; constructors DOMAIN_1, REAL_1, FINSEQ_4, FINSOP_1, NAT_D, FUNCT_7, CQC_SIM1, GRAPH_4, GRAPH_5, BINOP_2, RVSUM_1, RELSET_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, GRAPH_1, GRAPH_4, GRAPH_5, VALUED_0, CARD_1, FUNCT_1, XCMPLX_0; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries reserve x,y,X for set, i,j,k,m,n for Nat, p for FinSequence of X, ii for Integer; theorem :: GRAPHSP:1 for p being FinSequence,x being set holds not x in rng p & p is one-to-one iff p^<*x*> is one-to-one; theorem :: GRAPHSP:2 1 <= ii & ii <= len p implies p.ii in X; theorem :: GRAPHSP:3 1 <= ii & ii <= len p implies p/.ii = p.ii; reserve G for Graph, pe,qe for FinSequence of the carrier' of G, p,q for oriented Chain of G, W for Function, U,V,e,ee for set, v1,v2,v3,v4 for Vertex of G; theorem :: GRAPHSP:4 W is_weight_of G & len pe = 1 implies cost(pe,W) = W.(pe.1); theorem :: GRAPHSP:5 e in the carrier' of G implies <*e*> is Simple oriented Chain of G; theorem :: GRAPHSP:6 for p being Simple oriented Chain of G st p=pe^qe & len pe >= 1 & len qe >= 1 holds (the Target of G).(p.len p) <> (the Target of G).(pe.len pe ) & (the Source of G).(p.1) <> (the Source of G).(qe.1); begin :: The fundamental properties of directed paths and shortest paths theorem :: GRAPHSP:7 p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2}; theorem :: GRAPHSP:8 p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/{v2},W; theorem :: GRAPHSP:9 p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W implies cost(p,W)=cost(q,W); theorem :: GRAPHSP:10 for G being oriented Graph,v1,v2 be Vertex of G,e1,e2 be set st e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds e1=e2; theorem :: GRAPHSP:11 the carrier of G= U \/ V & v1 in U & v2 in V & (for v3,v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins v3,v4)) implies not ex p st p is_orientedpath_of v1,v2; theorem :: GRAPHSP:12 the carrier of G= U \/ V & v1 in U & (for v3,v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins v3,v4)) & p is_orientedpath_of v1,v2 implies p is_orientedpath_of v1,v2,U; begin :: The basic theorems for Dijkstra's shortest path algorithm (continue) reserve G for finite Graph, P,Q for oriented Chain of G, v1,v2,v3 for Vertex of G; theorem :: GRAPHSP:13 W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & not (ex e st e in the carrier' of G & e orientedly_joins v2,v3) & P islongestInShortestpath V,v1,W implies Q is_shortestpath_of v1,v3,V \/{v2},W; reserve G for finite oriented Graph, P,Q for oriented Chain of G, W for Function of (the carrier' of G), Real>=0, v1,v2,v3,v4 for Vertex of G; theorem :: GRAPHSP:14 e in the carrier' of G & P=<*e*> & e orientedly_joins v1,v2 implies P is_shortestpath_of v1,v2,{v1},W; theorem :: GRAPHSP:15 e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q=P^<*e*> & e orientedly_joins v2,v3 & v1 in V & (for v4 st v4 in V holds not (ex ee st ee in the carrier' of G & ee orientedly_joins v4,v3)) implies Q is_shortestpath_of v1,v3,V \/{v2},W; theorem :: GRAPHSP:16 the carrier of G= U \/ V & v1 in U & (for v3,v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins v3,v4)) implies (P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W); begin :: The definition of assignment statement notation let f be Function, i, x be object; synonym (f,i):=x for f+*(i,x); end; definition let f be FinSequence of REAL, x be object, r be Real; redefine func (f, x):=r -> FinSequence of REAL; end; definition let i,k be Nat,f be FinSequence of REAL,r be Real; func (f,i):=(k,r) -> FinSequence of REAL equals :: GRAPHSP:def 1 ((f,i):=k,k):=r; end; reserve f,g,h for Element of REAL*, r for Real; theorem :: GRAPHSP:17 i <> k & i in dom f implies ((f,i):=(k,r)).i = k; theorem :: GRAPHSP:18 m <> i & m <> k implies ((f,i):=(k,r)).m = f.m; theorem :: GRAPHSP:19 k in dom f implies ((f,i):=(k,r)).k = r; theorem :: GRAPHSP:20 dom ((f,i):=(k,r)) = dom f; begin :: The definition of Pascal-like while-do statement definition let X be set,f,g be Element of Funcs(X,X); redefine func g*f -> Element of Funcs(X,X); end; definition let X be set,f be Element of Funcs(X,X),g be Element of X; redefine func f.g -> Element of X; end; definition let X be set, f be Element of Funcs(X,X); func repeat(f) -> sequence of Funcs(X,X) means :: GRAPHSP:def 2 it.0 = id X & for i being Nat holds it.(i+1)=f*(it.i); end; theorem :: GRAPHSP:21 for F being Element of Funcs(REAL*,REAL*), f being Element of REAL*,n,i be Element of NAT holds (repeat F).0 .f = f; theorem :: GRAPHSP:22 for F,G being Element of Funcs(REAL*,REAL*),f being Element of REAL*, i be Nat holds (repeat (F*G)).(i+1).f = F.(G.((repeat (F*G)). i.f)); definition let g be Element of Funcs(REAL*,REAL*),f be Element of REAL*; redefine func g.f -> Element of REAL*; end; definition let f be Element of REAL*, n be Nat; func OuterVx(f,n) -> Subset of NAT equals :: GRAPHSP:def 3 {i: i in dom f & 1 <= i & i <= n & f.i <> -1 & f.(n+i) <> -1}; end; definition let f be Element of Funcs(REAL*,REAL*),g be Element of REAL*, n be Nat; assume ex i st OuterVx((repeat f).i.g,n) = {}; func LifeSpan(f,g,n) -> Element of NAT means :: GRAPHSP:def 4 OuterVx((repeat f).it.g, n) = {} & for k being Nat st OuterVx((repeat f).k.g,n) = {} holds it <= k; end; definition let f be Element of Funcs(REAL*,REAL*), n be Nat; func while_do(f,n) -> Element of Funcs(REAL*,REAL*) means :: GRAPHSP:def 5 dom it=REAL * & for h being Element of REAL* holds it.h=(repeat f).LifeSpan(f,h,n).h; end; begin :: Defining a weight function for an oriented graph definition let G be oriented Graph,v1,v2 be Vertex of G; assume ex e be set st e in the carrier' of G & e orientedly_joins v1,v2; func XEdge(v1,v2) -> set means :: GRAPHSP:def 6 ex e be set st it = e & e in the carrier' of G & e orientedly_joins v1,v2; end; definition let G be oriented Graph,v1,v2 be Vertex of G, W be Function; func Weight(v1,v2,W) -> set equals :: GRAPHSP:def 7 W.XEdge(v1,v2) if ex e be set st e in the carrier' of G & e orientedly_joins v1,v2 otherwise -1; end; registration let G be oriented Graph,v1,v2 be Vertex of G, W be Function of (the carrier' of G), Real>=0; cluster Weight(v1,v2,W) -> real; end; reserve G for oriented Graph, v1,v2 for Vertex of G, W for Function of (the carrier' of G), Real>=0; theorem :: GRAPHSP:23 Weight(v1,v2,W) >= 0 iff ex e be set st e in the carrier' of G & e orientedly_joins v1,v2; theorem :: GRAPHSP:24 Weight(v1,v2,W) = -1 iff not ex e be set st e in the carrier' of G & e orientedly_joins v1,v2; theorem :: GRAPHSP:25 e in the carrier' of G & e orientedly_joins v1,v2 implies Weight (v1,v2,W)=W.e; begin :: Basic operations for Dijkstra's shortest path algorithm definition let f be Element of REAL*, n be Nat; func UnusedVx(f,n) -> Subset of NAT equals :: GRAPHSP:def 8 {i: i in dom f & 1 <= i & i <= n & f.i <> -1}; end; definition let f be Element of REAL*, n be Nat; func UsedVx(f,n) -> Subset of NAT equals :: GRAPHSP:def 9 {i: i in dom f & 1 <= i & i <= n & f.i = -1}; end; theorem :: GRAPHSP:26 UnusedVx(f,n) c= Seg n; registration let f be Element of REAL*, n be Nat; cluster UnusedVx(f,n) -> finite; end; theorem :: GRAPHSP:27 OuterVx(f,n) c= UnusedVx(f,n); theorem :: GRAPHSP:28 OuterVx(f,n) c= Seg n; registration let f be Element of REAL*, n be Nat; cluster OuterVx(f,n) -> finite; end; definition let X be finite Subset of NAT,f be Element of REAL*,n; func Argmin(X,f,n) -> Nat means :: GRAPHSP:def 10 (X<>{} implies ex i st i= it & i in X & (for k st k in X holds f/.(2*n+i) <= f/.(2*n+k)) & for k st k in X & f/.(2*n+i) = f/.(2*n+k) holds i <= k ) & (X={} implies it=0); end; theorem :: GRAPHSP:29 OuterVx(f,n) <> {} & j=Argmin(OuterVx(f,n),f,n) implies j in dom f & 1<=j & j<=n & f.j <> -1 & f.(n+j) <> -1; theorem :: GRAPHSP:30 Argmin(OuterVx(f,n),f,n) <= n; definition let n be Nat; func findmin(n) -> Element of Funcs(REAL*,REAL*) means :: GRAPHSP:def 11 dom it = REAL* & for f be Element of REAL* holds it.f= (f,n*n+3*n+1) := (Argmin(OuterVx(f,n),f,n),-1); end; theorem :: GRAPHSP:31 i > n & i <> n*n+3*n+1 implies (findmin n).f.i=f.i; theorem :: GRAPHSP:32 i in dom f & f.i=-1 & i <> n*n+3*n+1 implies (findmin n).f.i=-1; theorem :: GRAPHSP:33 dom ((findmin n).f) = dom f; theorem :: GRAPHSP:34 OuterVx(f,n) <> {} implies ex j st j in OuterVx(f,n) & 1 <= j & j <= n & (findmin n).f.j=-1; definition let f be Element of REAL*,n,k be Nat; func newpathcost(f,n,k) -> Real equals :: GRAPHSP:def 12 f/.(2*n+f/.(n*n+3*n+1))+ f/.(2*n+n*(f /.(n*n+3*n+1))+k); end; definition let n,k be Nat,f be Element of REAL*; pred f hasBetterPathAt n,k means :: GRAPHSP:def 13 (f.(n+k)=-1 or f/.(2*n+k) > newpathcost(f,n,k)) & f/.(2*n+n*(f/.(n*n+3*n+1))+k) >= 0 & f.k <> -1; end; definition let f be Element of REAL*,n be Nat; func Relax(f,n) -> Element of REAL* means :: GRAPHSP:def 14 dom it = dom f & for k be Nat st k in dom f holds (n 3*n implies it.k=f.k); end; definition let n be Nat; func Relax(n) -> Element of Funcs(REAL*,REAL*) means :: GRAPHSP:def 15 dom it = REAL* & for f be Element of REAL* holds it.f=Relax(f,n); end; theorem :: GRAPHSP:35 dom ((Relax n).f) = dom f; theorem :: GRAPHSP:36 (i <= n or i > 3*n) & i in dom f implies (Relax n).f.i=f.i; theorem :: GRAPHSP:37 dom ((repeat(Relax(n)*findmin(n))).i.f) = dom ((repeat(Relax(n)* findmin(n))).(i+1).f); theorem :: GRAPHSP:38 OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) <> {} implies UnusedVx((repeat(Relax(n)*findmin(n))).(i+1).f,n) c< UnusedVx((repeat(Relax(n)* findmin(n))).i.f,n); theorem :: GRAPHSP:39 g=(repeat(Relax(n)*findmin(n))).i.f & h=(repeat(Relax(n)*findmin (n))).(i+1).f & k=Argmin(OuterVx(g,n),g,n) & OuterVx(g,n) <> {} implies UsedVx( h,n)=UsedVx(g,n) \/ {k} & not k in UsedVx(g,n); theorem :: GRAPHSP:40 ex i st i<=n & OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) = {}; theorem :: GRAPHSP:41 dom f = dom ((repeat(Relax(n)*findmin(n))).i.f); definition let f,g be Element of REAL*,m,n be Nat; pred f,g equal_at m,n means :: GRAPHSP:def 16 dom f = dom g & for k st k in dom f & m <=k & k <= n holds f.k=g.k; end; theorem :: GRAPHSP:42 f,f equal_at m,n; theorem :: GRAPHSP:43 f,g equal_at m,n & g,h equal_at m,n implies f,h equal_at m,n; theorem :: GRAPHSP:44 (repeat(Relax(n)*findmin(n))).i.f, (repeat(Relax(n)*findmin(n))) .(i+1).f equal_at 3*n+1,n*n+3*n; theorem :: GRAPHSP:45 for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*, n, i be Element of NAT st i < LifeSpan(F,f,n) holds OuterVx((repeat F).i.f,n) <> {}; theorem :: GRAPHSP:46 f, (repeat(Relax(n)*findmin(n))).i.f equal_at 3*n+1,n*n+3*n; theorem :: GRAPHSP:47 1<=n & 1 in dom f & f.(n+1) <> -1 & (for i st 1<=i & i<=n holds f.i=1) & (for i st 2<=i & i<=n holds f.(n+i)=-1) implies 1 = Argmin(OuterVx(f,n ),f,n) & UsedVx(f,n)={} & {1} = UsedVx((repeat(Relax(n)*findmin(n))).1.f,n); theorem :: GRAPHSP:48 g=(repeat(Relax(n)*findmin(n))).1.f & h=(repeat(Relax(n)*findmin (n))).i.f & 1<=i & i <= LifeSpan(Relax(n)*findmin(n),f,n) & m in UsedVx(g,n) implies m in UsedVx(h,n); definition let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat; pred p is_vertex_seq_at f,i,n means :: GRAPHSP:def 17 p.(len p)=i & for k st 1<=k & k < len p holds p.(len p-k)=f.(n+p/.(len p-k+1)); end; definition let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat; pred p is_simple_vertex_seq_at f,i,n means :: GRAPHSP:def 18 p.1=1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one; end; theorem :: GRAPHSP:49 for p,q being FinSequence of NAT,f be Element of REAL*,i,n be Element of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds p = q; definition let G be Graph,p be FinSequence of the carrier' of G,vs be FinSequence; pred p is_oriented_edge_seq_of vs means :: GRAPHSP:def 19 len vs = len p + 1 & for n be Nat st 1<=n & n<=len p holds (the Source of G).(p.n) = vs.n & (the Target of G).(p.n) = vs.(n+1); end; theorem :: GRAPHSP:50 for G being oriented Graph,vs be FinSequence,p,q being oriented Chain of G st p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds p=q ; theorem :: GRAPHSP:51 for G being Graph,vs1,vs2 be FinSequence,p being oriented Chain of G st p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1 holds vs1=vs2; begin :: Data structure for Dijkstra's shortest path algorithm :: address possible value init. value comment :: 1 1 or -1 1 -1 if node v1 is used :: 2 1 or -1 1 -1 if node v2 is used :: : : : : :: n 1 or -1 1 -1 if node vn is used :: n+1 0 0 preceding-node of v1 toward v1 :: n+2 -1 or Node No. -1 preceding-node of v2 toward v1 :: : : : : :: 2*n -1 or Node No. -1 preceding-node of vn toward v1 :: 2*n+1 0 0 cost from v1 to v1 :: 2*n+2 >=0 0 minimum cost from v2 to v1 :: : : : : :: 3*n >=0 0 minimum cost from vn to v1 :: 3*n+1 weight(v1,v1) the weight of edge(v1,v1) :: 3*n+2 weight(v1,v2) the weight of edge(v1,v2) :: : : : :: 4*n weight(v1,vn) the weight of edge(v1,vn) :: : : : :: n*n+3*n weight(vn,vn) the weight of edge(vn,vn) :: n*n+3n+1 Node No. current node with the shortest path definition let f be Element of REAL*,G be oriented Graph,n be Nat, W be Function of (the carrier' of G), Real>=0; pred f is_Input_of_Dijkstra_Alg G,n,W means :: GRAPHSP:def 20 len f=n*n+3*n+1 & Seg n= the carrier of G & (for i st 1 <= i & i <= n holds f.i=1 & f.(2*n+i)=0) & f.(n+ 1)=0 & (for i st 2 <= i & i <= n holds f.(n+i)=-1) & for i,j being Vertex of G, k,m st k=i & m=j holds f.(2*n+n*k+m)=Weight(i,j,W); end; begin :: The definition of Dijkstra's shortest path algorithm definition let n be Nat; func DijkstraAlgorithm n -> Element of Funcs(REAL*,REAL*) equals :: GRAPHSP:def 21 while_do( Relax(n)*findmin(n),n); end; begin :: Justifying the correctness of Dijkstra's shortest path algorithm reserve p,q for FinSequence of NAT, G for finite oriented Graph, P,Q,R for oriented Chain of G, W for Function of (the carrier' of G), Real>=0, v1,v2,v3, v4 for Vertex of G; theorem :: GRAPHSP:52 f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & 1 <> v2 & v2=i & n >= 1 & g= (DijkstraAlgorithm(n)).f implies the carrier of G = UsedVx(g,n) \/ UnusedVx(g,n ) & (v2 in UsedVx(g,n) implies ex p,P st p is_simple_vertex_seq_at g,i,n & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v2,W & cost(P,W)=g.(2*n+i)) & (v2 in UnusedVx(g,n) implies not ex Q st Q is_orientedpath_of v1,v2);