Grace/Cumulus/GraphTheory/Dijkstra.g17

Open in Workbench Download source

Imports

Complement · Nat.Mod · Core.List

Declarations

Source

1-- Executable Dijkstra search on a finite nonnegative weighted digraph.2-- An absent matrix entry is no edge; an absent distance is infinity.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.GraphTheory.Dijkstra9import Complement10import Nat.Mod11import Core.List12-- Nested executable containers use Set until their carrier sets are constructed.13-- Constructor equations and mathematical correctness certificates remain checked.1415datatype Candidate(Index Weight : Set)16  | value(vertex : Index, distance : Weight)1718datatype State(Distances Flags : Set)19  | current(distances : Distances, settled : Flags)2021def less (a b : Nat) → Bool22  | zero, b => BoolOps.not(isZero(b))23  | succ(a), b => BoolOps.and(BoolOps.not(isZero(b)), less(a, predecessor(b)))24  descends a2526def boolTail (flags : List(ℕ)) → List(ℕ)27  | [] => List.nil28  | flag :: rest => rest2930def boolHead (flags : List(ℕ)) → Nat31  | [] => 132  | flag :: rest => flag3334def optionTail (row : Set) → Set35  | [] => List.nil36  | weight :: rest => rest3738def optionHead (row : Set) → Set39  | [] => Option.none40  | weight :: rest => weight4142def entry (row : Set, index : Nat) → Set43  | row, zero => optionHead(row)44  | row, succ(index) => entry(optionTail(row), index)45  descends index4647def rowsHead (rows : Set) → Set48  | [] => List.nil49  | row :: rest => row5051def rowsTail (rows : Set) → Set52  | [] => List.nil53  | row :: rest => rest5455def rowAt (rows : Set, index : Nat) → Set56  | rows, zero => rowsHead(rows)57  | rows, succ(index) => rowAt(rowsTail(rows), index)58  descends index5960def select (pickLeft : Bool, left right : Set) → Set61  | Bool.true, left, right => left62  | Bool.false, left, right => right6364def candidateDistance (candidate : Candidate(ℕ,ℕ)) → Nat65  | Candidate.value(i, d) => d6667def preferSome (left : Candidate(ℕ,ℕ), right : Set) → Set68  | left, Option.none => Option.some(left)69  | left, Option.some(candidate) =>70    select(less(candidateDistance(left), candidateDistance(candidate)),71      Option.some(left), Option.some(candidate))72  descends right7374def prefer (left right : Set) → Set75  | Option.none, right => right76  | Option.some(candidate), right => preferSome(candidate, right)77  descends left7879def availableOpen (distance : Option(ℕ), index : Nat) → Set80  | Option.none, index => Option.none81  | Option.some(d), index => Option.some(Candidate.value(index, d))8283def available (visited : Bool, distance : Option(ℕ), index : Nat) → Set84  | Bool.true, distance, index => Option.none85  | Bool.false, distance, index => availableOpen(distance, index)8687-- Linear priority search.  The index advances with the list spine.88def minimum (distances : Set, visited : List(ℕ), index : Nat) → Set89  | List.nil, visited, index => Option.none90  | List.cons(d, rest), visited, index =>91    prefer(available(equalNat(boolHead(visited), 1), d, index),92      minimum(rest, boolTail(visited), succ(index)))93  descends distances9495def markHead (visited : List(ℕ)) → List(ℕ)96  | [] => List.nil97  | flag :: rest => List.cons(1, rest)9899def keepHead (visited rest : List(ℕ)) → List(ℕ)100  | List.nil, rest => List.nil101  | List.cons(flag, oldRest), rest => List.cons(flag, rest)102103def mark (visited : List(ℕ), index : Nat) → List(ℕ)104  | visited, zero => markHead(visited)105  | visited, succ(index) => keepHead(visited, mark(boolTail(visited), index))106  descends index107108def chooseDistance (pickFirst : Bool, first second : Option(ℕ)) → Option(ℕ)109  | Bool.true, first, second => first110  | Bool.false, first, second => second111112def minSome (old : Nat, new : Option(ℕ)) → Option(ℕ)113  | old, Option.none => Option.some(old)114  | old, Option.some(e) =>115    chooseDistance(less(e, old), Option.some(e), Option.some(old))116  descends new117118def minOption (old new : Option(ℕ)) → Option(ℕ)119  | Option.none, new => new120  | Option.some(d), new => minSome(d, new)121  descends old122123def extendSome (d : Nat, weight : Option(ℕ)) → Option(ℕ)124  | d, Option.none => Option.none125  | d, Option.some(w) => Option.some(Grace.Core.Nat.Rec.add(d, w))126127def extension (distance weight : Option(ℕ)) → Option(ℕ)128  | Option.none, weight => Option.none129  | Option.some(d), weight => extendSome(d, weight)130  descends distance131132def relaxValue (old weight : Option(ℕ), settled : Bool, sourceDistance : Option(ℕ)) → Option(ℕ)133  | old, weight, Bool.true, sourceDistance => old134  | old, weight, Bool.false, sourceDistance => minOption(old, extension(sourceDistance, weight))135136def relax (weights distances : Set, visited : List(ℕ), sourceDistance : Option(ℕ)) → Set137  | weights, List.nil, visited, sourceDistance => List.nil138  | weights, List.cons(d, rest), visited, sourceDistance =>139    List.cons(relaxValue(d, entry(weights, 0), equalNat(boolHead(visited), 1), sourceDistance),140      relax(optionTail(weights), rest, boolTail(visited), sourceDistance))141  descends distances142143def advanceChosen (rows : Set, distances : Set, visited : List(ℕ), chosen : Set) → Set144  | rows, distances, visited, Option.none => State.current(distances, visited)145  | rows, distances, visited, Option.some(Candidate.value(index, d)) =>146    State.current(relax(rowAt(rows, index), distances, mark(visited, index), Option.some(d)),147      mark(visited, index))148149def advance (rows : Set, state : Set) → Set150  | rows, State.current(distances, visited) =>151    advanceChosen(rows, distances, visited, minimum(distances, visited, 0))152153def iterate (fuel : Nat, rows : Set, state : Set) → Set154  | zero, rows, state => state155  | succ(fuel), rows, state => iterate(fuel, rows, advance(rows, state))156157def initialCell (index source : Nat) : Option(ℕ) :=158  chooseDistance(equalNat(index, source), Option.some(0), Option.none)159160def initialDistances (count index source : Nat) → Set161  | zero, index, source => List.nil162  | succ(count), index, source =>163    List.cons(initialCell(index, source), initialDistances(count, succ(index), source))164165def initialFlags (count : Nat) → List(ℕ)166  | zero => List.nil167  | succ(count) => List.cons(0, initialFlags(count))168169def solve (count source : Nat, rows : Set) : Set :=170  iterate(count, rows, State.current(initialDistances(count, 0, source), initialFlags(count)))171172def distances (state : Set) → Set173  | State.current(ds, visited) => ds174175def settled (state : Set) → Set176  | State.current(ds, visited) => visited177178-- Local facts are valid for any input size, independently of a trace.179theorem minOption.none_right (d : Option(ℕ))180  shows minOption(d, Option.none) = d181proof182  induction d183  | Option.none => settle with minOption184  | Option.some(n) => settle with minOption, minSome185186theorem minOption.none_left (d : Option(ℕ))187  shows minOption(Option.none, d) = d188proof189  unfold minOption190  rfl191192theorem extension.absent_edge (d : Option(ℕ))193  shows extension(d, Option.none) = Option.none194proof195  induction d196  | Option.none => settle with extension197  | Option.some(n) => settle with extension, extendSome198199theorem available.settled (d : Option(ℕ), index : Nat)200  shows available(Bool.true, d, index) = Option.none201proof202  unfold available203  rfl204205theorem relaxValue.settled (d weight source : Option(ℕ))206  shows relaxValue(d, weight, Bool.true, source) = d207proof208  unfold relaxValue209  rfl210211namespace DijkstraExamples212213-- Six vertices, including vertex 5 which is disconnected from source 0.214def absent : Option(ℕ) := Option.none215def weight (n : Nat) : Option(ℕ) := Option.some(n)216217def rows : Set :=218  [[absent, weight(10), weight(3), absent, absent, absent],219   [absent, absent, absent, weight(2), weight(1), absent],220   [absent, weight(4), absent, weight(8), weight(2), absent],221   [absent, absent, absent, absent, weight(7), absent],222   [absent, absent, absent, weight(9), absent, absent],223   [absent, absent, absent, absent, absent, absent]]224225def result : Set := Dijkstra.solve(6, 0, rows)226227theorem six_vertices228  shows Dijkstra.distances(result) = [weight(0), weight(7), weight(3), weight(9), weight(5), absent]229proof230  compute231232theorem disconnected_is_unsettled233  shows Dijkstra.entry(Dijkstra.distances(result), 5) = Option.none234proof235  compute236237-- Zero is an edge weight, distinct from Option.none.238def zeroRows : Set :=239  [[absent, weight(0), weight(5), absent],240   [absent, absent, weight(0), absent],241   [absent, absent, absent, weight(1)],242   [absent, absent, absent, absent]]243244theorem zero_weight_route245  shows Dijkstra.distances(Dijkstra.solve(4, 0, zeroRows)) =246    [weight(0), weight(0), weight(0), weight(1)]247proof248  compute249250eval Dijkstra.distances(result)251252end DijkstraExamples253