I am trying to prove the first assertion in the following code, taken from notes of Damon Wischik:
def dijkstra(g, s): for v in g.vertices: v.distance = ∞ s.distance = 0 toexplore = PriorityQueue([s], sortkey = lambda v: v.distance) while not toexplore.isempty(): v = toexplore.popmin() # Assert: v.distance is the true shortest path distance between s and v # Assert: v is never put back into toexplore for (w, edgecost) in v.neighbours: dist_w = v.distance + edgecost if dist_w < w.distance: w.distance = dist_w if w in toexplore: toexplore.decreasekey(w) else: toexplore.push(w)
Base case: The estimate of the source node is correct when it is popped.
Inductive step: Consider the shortest path from the source node $s$ to some destination node $d$,
$$ s \to v_1 \to v_2 \to \cdots \to v_k \to d. $$
Assume that the estimates for $s,v_1,v_2,\ldots,v_k$ are correct when they are popped.
When $d$ is popped, we can be sure that $s, v_1, v_2, \dots, v_k$ were popped prior to that as their true shortest distances from the source $s$ are lower than that of $d$. In particular, when $v_k$ is popped, we are sure that the edge $(v_k, d)$ will be relaxed since relaxing the edge $(v_k, d)$ gives us the true shortest distance from the source to the destination, which is definitely an improvement on any prior estimate of D. Hence D's estimate is the true shortest distance from the source when it is popped.
Hence the assertion is true.
Is there a flaw in my proof?