In Dijkstra’s algorithm, how do you prove that at any moment: distance[v] ≥ length(P) for shortest s → v path P where all vertices (except possibly v) are already processed (i.e., not in the priority queue Q)?
In the proof I'm reading this is used in the inductive proof of the invariant:
(a) If v ∉ Q, then distance[v] = d(v)
(b) If v ∈ Q, then distance[v] is the length of the shortest s → v path whose first and internal vertices are not in Q
But the claim itself is stated before the invariant is proved — can it be shown independently?
It feels intuitive, but I've been stuck on how to prove it for a while.
The invariant you're asking about doesn't seem to be particularly useful. It would probably be worthwhile to look up the original paper and see how Dijkstra proved his algorithm. It's probably brilliantly simple.
The way I do it, though, is like this...
Lemmas:
If distance[v] is only modified by relaxation, then distance[v] >= d(v) at all times. Easily proven by induction, since each relaxation preserves this property.
If distances are defined (no negative cycles), then some sequence of relaxations will assign all distances correctly (distance[v] == d(v)), because the first incorrect distance on any shortest path can be corrected by a relaxation.
Loop invariants:
distance[v] == d(v) for all processed vertices;
The minimum distance[v] across all unprocessed vertices cannot be further reduced by relaxation, and is therefore correct (== d(v)) by lemmas 1 and 2.
No further relaxations from processed vertices are possible, since their distances are fixed by lemma 1.
No relaxation from u -> v can set a distance less than distance[u], because edge weights are non-negative.
It is therefore valid to process the relaxations for any unprocessed vertex v if distance[v] is minimal, and and then remove it from the unprocessed set.