Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

The abstract of the Mizar article:

Dijkstra's Shortest Path Algorithm

by
Jing-Chao Chen

Received March 17, 2003

MML identifier: GRAPHSP
[ Mizar article, MML identifier index ]


environ

 vocabulary ARYTM_1, INT_1, RELAT_1, SCM_1, RLVECT_1, AMI_3, GRAPHSP, FUNCT_1,
      BOOLE, FINSET_1, ORDERS_1, FINSEQ_1, CARD_1, FUNCT_2, GRAPH_1, FINSEQ_4,
      GRAPH_5, GRAPH_4, MSAFREE2, FUNCT_4;
 notation XREAL_0, REAL_1, NAT_1, INT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1,
      FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, GRAPH_1,
      PARTFUN1, FUNCT_2, GRAPH_4, GRAPH_3, GRAPH_5, BINARITH, DOMAIN_1,
      RVSUM_1, GOBOARD1, NUMBERS, FUNCT_7;
 constructors REAL_1, INT_1, FINSEQ_4, GRAPH_5, GRAPH_4, DOMAIN_1, BINARITH,
      GOBOARD1, FUNCT_7, MEMBERED, RELAT_2;
 clusters FRAENKEL, INT_1, GRAPH_5, FINSEQ_1, FINSET_1, RELSET_1, GRAPH_1,
      FUNCT_2, GRAPH_4, XREAL_0, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2;
 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 Edges 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 Edges 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 Edges of G & e2 in the Edges of G &
e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds e1=e2;

theorem :: GRAPHSP:11
the Vertices 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 Edges of G & e orientedly_joins v3,v4))
 implies not ex p st p is_orientedpath_of v1,v2;

theorem :: GRAPHSP:12
the Vertices 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 Edges 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 Edges 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 Edges of G), Real>=0,
        v1,v2,v3,v4 for Vertex of G;

theorem :: GRAPHSP:14
e in the Edges of G & v1 <> v2 & P=<*e*> & e orientedly_joins v1,v2
implies P is_shortestpath_of v1,v2,{v1},W;

theorem :: GRAPHSP:15
e in the Edges 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 Edges of G & ee orientedly_joins v4,v3)) implies
Q is_shortestpath_of v1,v3,V \/{v2},W;

theorem :: GRAPHSP:16
the Vertices 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 Edges 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

definition let f be Function, i, x be set;
  redefine func f+*(i,x);
  synonym (f,i):=x;
end;

theorem :: GRAPHSP:17
  for x,y being set, f being Function holds rng (f,x):=y c= rng f \/ {y};

definition let f be FinSequence of REAL, x be set, 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:18
   i <> k & i in dom f implies ((f,i):=(k,r)).i = k;

theorem :: GRAPHSP:19
  m <> i & m <> k & m in dom f implies ((f,i):=(k,r)).m = f.m;

theorem :: GRAPHSP:20
  k in dom f implies ((f,i):=(k,r)).k = r;

theorem :: GRAPHSP:21
 dom ((f,i):=(k,r)) = dom f;

begin  :: The definition of Pascal-like while-do statement

definition let X be set;
  redefine func id X -> Element of Funcs(X,X);
end;

definition let X be set,f,g be Function of X,X;
  redefine func g*f -> Function of X,X;
end;

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) -> Function of NAT,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:22
for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*,n,i be Nat
holds (repeat F).0 .f = f;

theorem :: GRAPHSP:23
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) -> 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 Edges of G & e orientedly_joins v1,v2;
   func Edge(v1,v2) means
:: GRAPHSP:def 6
    ex e be set st it = e & e in the Edges 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) equals
:: GRAPHSP:def 7
      W.Edge(v1,v2) if ex e be set st e in the Edges of G &
      e orientedly_joins v1,v2 otherwise -1;
end;

definition
   let G be oriented Graph,v1,v2 be Vertex of G,
       W be Function of (the Edges of G), Real>=0;
   redefine func Weight(v1,v2,W) -> Real;
end;

reserve G for oriented Graph,
        v1,v2 for Vertex of G,
        W for Function of (the Edges of G), Real>=0;

theorem :: GRAPHSP:24
  Weight(v1,v2,W) >= 0 iff ex e be set st e in the Edges of G &
  e orientedly_joins v1,v2;

theorem :: GRAPHSP:25
   Weight(v1,v2,W) = -1 iff not ex e be set st e in the Edges of G &
    e orientedly_joins v1,v2;

theorem :: GRAPHSP:26
  e in the Edges 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:27
  UnusedVx(f,n) c= Seg n;

definition let f be Element of REAL*, n be Nat;
 cluster UnusedVx(f,n) -> finite;
end;

theorem :: GRAPHSP:28
  OuterVx(f,n) c= UnusedVx(f,n);

theorem :: GRAPHSP:29
  OuterVx(f,n) c= Seg n;

definition 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:30
 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:31
  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:32
  i in dom f & i > n & i <> n*n+3*n+1 implies (findmin n).f.i=f.i;

theorem :: GRAPHSP:33
  i in dom f & f.i=-1 & i <> n*n+3*n+1 implies (findmin n).f.i=-1;

theorem :: GRAPHSP:34
  dom ((findmin n).f) = dom f;

theorem :: GRAPHSP:35
  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<k & k <= 2*n implies (f hasBetterPathAt n,(k-'n)
    implies it.k=f/.(n*n+3*n+1)) & (not f hasBetterPathAt n,(k-'n)
    implies it.k=f.k)) &
    (2*n <k & k <=3*n implies (f hasBetterPathAt n,(k-'2*n)
    implies it.k=newpathcost(f,n,k-'2*n)) & (not f hasBetterPathAt n,(k-'2*n)
    implies it.k=f.k)) &
    (k<=n or k > 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:36
    dom ((Relax n).f) = dom f;

theorem :: GRAPHSP:37
 (i <= n or i > 3*n) & i in dom f implies (Relax n).f.i=f.i;

theorem :: GRAPHSP:38
   dom ((repeat(Relax(n)*findmin(n))).i.f) =
   dom ((repeat(Relax(n)*findmin(n))).(i+1).f);

theorem :: GRAPHSP:39
 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:40
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:41
 ex i st i<=n & OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) = {};

theorem :: GRAPHSP:42
   dom f = dom ((repeat(Relax(n)*findmin(n))).i.f);

definition
   let f,g be Element of REAL*,m,n;
   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:43
   f,f equal_at m,n;

theorem :: GRAPHSP:44
   f,g equal_at m,n & g,h equal_at m,n implies f,h equal_at m,n;

theorem :: GRAPHSP:45
 (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:46
 for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*,n,i be Nat
st i < LifeSpan(F,f,n) holds OuterVx((repeat F).i.f,n) <> {};

theorem :: GRAPHSP:47
  f, (repeat(Relax(n)*findmin(n))).i.f equal_at 3*n+1,n*n+3*n;

theorem :: GRAPHSP:48
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:49
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:50
  for p,q being FinSequence of NAT,f be Element of REAL*,i,n be 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 Edges of G,vs be FinSequence;
 pred p is_oriented_edge_seq_of vs means
:: GRAPHSP:def 19
    len vs = len p + 1 &
    for n 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:51
  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:52
  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 Edges 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 Vertices 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 Edges of G), Real>=0,
        v1,v2,v3,v4 for Vertex of G;

theorem :: GRAPHSP:53
  f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & 1 <> v2 & v2=i & n >= 1 &
g=(DijkstraAlgorithm(n)).f implies the Vertices 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);

Back to top