DijkstraStarter

Computable exact shortest-path candidates through the public graph import

Open in Workbench View on GitHub

1-- Computable exact shortest-path candidates through the public graph import.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module DijkstraStarter7import Grace.Cumulus.GraphTheory89-- A directed graph with six vertices; vertex 5 is unreachable from 0.10theorem sample_distances11  shows Dijkstra.distances(DijkstraExamples.result) =12    List.cons(DijkstraExamples.weight(0), List.cons(DijkstraExamples.weight(7),13      List.cons(DijkstraExamples.weight(3), List.cons(DijkstraExamples.weight(9),14        List.cons(DijkstraExamples.weight(5),15          List.cons(DijkstraExamples.absent, List.nil))))))16proof17  simp1819-- Zero-weight edges are traversed; they are not confused with missing edges.20theorem zero_weight_edges21  shows Dijkstra.distances(Dijkstra.solve(4, 0, DijkstraExamples.zeroRows)) =22    List.cons(DijkstraExamples.weight(0), List.cons(DijkstraExamples.weight(0),23      List.cons(DijkstraExamples.weight(0),24        List.cons(DijkstraExamples.weight(1), List.nil))))25proof26  simp27