Documentation

Complexity.Algorithms.WordRAM.Dijkstra.Invariant

Dijkstra's algorithm: the invariant #

This file proves the graph theory behind Dijkstra's algorithm Dijkstra Cormen et al., Section 24.3, independently of the machine. The algorithm keeps a set S of visited vertices and a tentative distance D v for every vertex, and Cslib.Algorithms.WordRAM.Dijkstra.Instance.Inv states what it maintains: D bounds the distance from above, is exact on S, and is already relaxed along every edge out of S.

The key step (Cslib.Algorithms.WordRAM.Dijkstra.Instance.Inv.step) is the classical cut argument: on every path from the source to an unvisited vertex, either the source is unvisited, with tentative distance 0, or the path has an edge from S to an unvisited vertex. Either way its weight is at least the least tentative distance outside S. Hence an unvisited vertex of least finite tentative distance has the exact distance, and relaxing its edges keeps the invariant with that vertex visited.

Main definitions #

Main results #

References #

source
def Cslib.Algorithms.WordRAM.Dijkstra.decodeDist (x : ℕ) :
ℕ∞

The distance a word encodes: ⊤ for 0 and d for d + 1.

Instances For
    source
    @[simp]
    theorem Cslib.Algorithms.WordRAM.Dijkstra.encodeDist_decodeDist (x : ℕ) :
    encodeDist (decodeDist x) = x
    source
    @[simp]
    theorem Cslib.Algorithms.WordRAM.Dijkstra.decodeDist_encodeDist (d : ℕ∞) :
    decodeDist (encodeDist d) = d

    Decoding inverts the encoding of distances: a distance word decodes to its distance.

    source
    theorem Cslib.Algorithms.WordRAM.Dijkstra.decodeDist_ne_top {b : ℕ} (hb : b ≠ 0) :
    decodeDist b ≠ ⊤

    A nonzero distance word decodes to a finite distance.

    source
    theorem Cslib.Algorithms.WordRAM.Dijkstra.decodeDist_le {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a ≤ b) :
    decodeDist a ≤ decodeDist b

    Decoding preserves order between nonzero distance words.

    source
    theorem Cslib.Algorithms.WordRAM.Dijkstra.Instance.le_maxWeight (I : Instance) {u v : Fin I.n} {c : ℕ} (h : I.weight u v = some c) :
    c ≤ I.maxWeight

    Every edge weight is at most the largest one.

    source
    noncomputable def Cslib.Algorithms.WordRAM.Dijkstra.Instance.relax (I : Instance) (D : Fin I.n → ℕ∞) (u v : Fin I.n) :
    ℕ∞

    Relaxation of the edges out of u: the tentative distance of v becomes at most that of u plus the weight of the edge from u to v, if there is one.

    Instances For
      source
      structure Cslib.Algorithms.WordRAM.Dijkstra.Instance.Inv (I : Instance) (S : Finset (Fin I.n)) (D : Fin I.n → ℕ∞) :
      Prop

      The invariant of Dijkstra's algorithm, for the visited set S and the tentative distances D.

      • source : D I.source = 0

        The source has tentative distance 0.

      • dist_le (v : Fin I.n) : I.dist I.source v ≤ D v

        Tentative distances bound the distances from above.

      • eq_of_mem (v : Fin I.n) : v ∈ S → D v = I.dist I.source v

        Tentative distances are exact on visited vertices.

      • relaxed (a : Fin I.n) : a ∈ S → ∀ b ∉ S, ∀ (c : ℕ), I.weight a b = some c → D b ≤ D a + ↑c

        Every edge from a visited vertex to an unvisited one is relaxed.

      • bound (v : Fin I.n) : D v ≠ ⊤ → D v ≤ ↑(S.card * I.maxWeight)

        Finite tentative distances are at most |S| times the largest weight.

      Instances For
        source
        theorem Cslib.Algorithms.WordRAM.Dijkstra.Instance.dist_le_edge (I : Instance) {a b : Fin I.n} {c : ℕ} (he : I.weight a b = some c) :
        I.dist I.source b ≤ I.dist I.source a + ↑c

        Extending a path by an edge bounds the distance to the new endpoint.

        source
        theorem Cslib.Algorithms.WordRAM.Dijkstra.Instance.Inv.init (I : Instance) :
        I.Inv ∅ (Function.update (fun (x : Fin I.n) => ⊤) I.source 0)

        The invariant holds with no vertex visited, the source at tentative distance 0 and every other vertex at ⊤.

        source
        theorem Cslib.Algorithms.WordRAM.Dijkstra.Instance.Inv.step (I : Instance) {S : Finset (Fin I.n)} {D : Fin I.n → ℕ∞} (h : I.Inv S D) {u : Fin I.n} (hu : u ∉ S) (hmin : ∀ v ∉ S, D u ≤ D v) (hfin : D u ≠ ⊤) :
        I.Inv (insert u S) (I.relax D u)

        Dijkstra's step. Visiting an unvisited vertex u of least finite tentative distance and relaxing its edges keeps the invariant.

        source
        theorem Cslib.Algorithms.WordRAM.Dijkstra.Instance.Inv.eq_dist (I : Instance) {S : Finset (Fin I.n)} {D : Fin I.n → ℕ∞} (h : I.Inv S D) (hdone : ∀ v ∉ S, D v = ⊤) (v : Fin I.n) :
        D v = I.dist I.source v

        Termination. Once every unvisited vertex has infinite tentative distance, the tentative distances are the distances.