I have taken the text from this link. First I will write the proof.
Skipping the pseudo-code I directly move to the Proof of correctness.
Let $\delta(u,v)$ be the cost of the least cost path from $u$ to $v$. Let $d[v]$ be the cost stored by Dijkstra.
Claim 1: $d[v] \geq \delta(u,v)$.
Informal proof of claim 1: initially, $d[v] = \infty$ and it's only reduced when we find a path to $v$. Clearly, the cost of the found path can never be less than the cost of the least cost path.
Claim2: the following invariant holds: in the while loop, when $v$ is removed from the priority queue, $d[v]\leq \delta(s,v)$.
If this claim is true then the two claims above imply that $d[v] =\delta(s,v)$
Proof of sketch of claim 2: This is a proof by contradiction. Suppose the claim is false there is some node for which Dijkstra's compute the wrong answer. In particular, let $u$ be the first node removed from the priority queue such that $d[u] > \delta(s,u)$.
There is some shortest path from $s$ to $u$. Let's call this path $P$. It's shown in figure above. Let's consider the moment in the execution of Dijkstra's algorithm when node $u$ is being removed from the priority queue.
Let $y$ be a node that lies on the least cost path and has already been removed. Let $z$ be also on the least cost path but not yet removed. (Note: it's fair to assume that such nodes exist. For instance, we can see $y=s$ and $z = u$)
We make the following observations
(a) $d[y] = \delta(s,y)$. This is true because $y$ is defined as the first node removed where $d[u] > \delta(s,u)$ and since $y$ has already been removed it must be the case that $d[y] \leq \delta(s,y)$, and we have claim 1 which says $d[y] \geq \delta(s,y)$.
(b) $d[z] \leq d[y] + w(y,z)$. This is true because when we removed $y$ from the queue, the for each loop ensures that we visited each neighbor of $y$, including $z$, and updated its cost. So if at that moment, $d[z] > d[y] + w(y,z)$, then $d[z]$ would have been updated to be $d[z] = d[y] +w(y,z)$. And notice that in algorithm, costs start at $\infty$ and can only decrease.
(c) $d[u] \leq d[z]$. This is true because $u$ is about to be removed and $z$ is defined as a node not yet removed from queue (so therefore its cost must be not less than $u$'s).
(d) $\delta(s,z) = \delta(s,y) + w(y,z)$ and $\delta(s,u) = \delta(s,z) + w(z,u)$. These claims are true because these nodes lie on $P$ which is define to be the shortest path.
Putting these claims together we have
$\quad \quad \quad \quad d[u]\leq d[z] \leq d[y]+w(y,z)=\delta(s,z) \leq \delta(s,z)+\delta (z,u)=\delta(s,u)$
This contradicts our supposition that $d[u] > \delta(s,u)$. Therefore, our supposition is false and there can be node such that $d[u] > \delta(s,u)$. $\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \square$
My question follows.
In part (c), how could node $z$ be not yet removed from priority queue while node $u$ is about to be removed. Unless there are same, this cannot be the case. If they is a path $P$ from $s$ to $u$ and $z$ is also on that path, then $z$ must be removed before the removal of $u$.
Could someone explain this part?
Best Answer
This is a proof by contradiction. We suppose that the algorithm wrongly computes some distance. Therefore such a vertex $z$ exists in the true shortest path. It could be either $u$ or some other vertex, but we definitely know that at least one such vertex exists. Otherwise the algorithm would compute the distance correctly. However, according to the proof, $z$ is supposed to be not any, but the first (i. e., the closest to $s$) vertex of the shortest $(s, u)$-path that is not removed from the queue, while $y$ is the last removed.