Grace/Cumulus/GraphTheory/DijkstraInitial.g17

Open in Workbench Download source

Imports

DijkstraFlags

Declarations

Source

1-- Initialization of Dijkstra's executable distance and flag vectors.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.DijkstraInitial8import DijkstraFlags910namespace Dijkstra111213theorem initialCell.closed (index source : Nat)14  shows Option(ℕ, Dijkstra.initialCell(index, source))15proof16  have condition := Dijkstra.equalNat.boolean at index, source with *17  have choices := Dijkstra.chooseDistance.selects at Option.some(0), Option.none, equalNat(index, source) with condition18  have computed : Dijkstra.initialCell(index, source) = Dijkstra.chooseDistance(equalNat(index, source), Option.some(0), Option.none)19    settle with Dijkstra.initialCell20  rw computed21  cases choices with finite | absent22  . rw finite23    have zeroIn := nat.omega.forward with Naturals.constructor.zero24    exact Option.inductive.constructor.some with zeroIn25  . rw absent26    exact Option.inductive.constructor.none2728theorem initialDistances.closed (count index source : Nat)29  shows List(Dijkstra.DistanceValues, Dijkstra.initialDistances(count, index, source))30proof31  induction count generalizing index32  | zero =>33    intros index indexNat34    have computed : Dijkstra.initialDistances(0, index, source) = List.nil by settle with Dijkstra.initialDistances35    rw computed36    exact List.inductive.constructor.nil37  | succ(k) using ih =>38    intros index indexNat39    have cellType := initialCell.closed at index, source with indexNat, assumption40    have cellIn := Dijkstra.DistanceValues.membership.backward with cellType41    have nextNat := Naturals.constructor.succ with indexNat42    have tailType := ih with succ(index), nextNat43    have constructed := List.inductive.constructor.cons at Dijkstra.DistanceValues,44      Dijkstra.initialCell(index, source), Dijkstra.initialDistances(k, succ(index), source) with cellIn, tailType45    have computed : Dijkstra.initialDistances(succ(k), index, source) = List.cons(Dijkstra.initialCell(index, source), Dijkstra.initialDistances(k, succ(index), source))46      settle with Dijkstra.initialDistances47    rw computed48    exact constructed4950theorem initialDistances.length (count index source : Nat)51  shows Dijkstra.vectorLength(Dijkstra.initialDistances(count, index, source)) = count52proof53  induction count generalizing index54  | zero =>55    intros index indexNat56    simp [Dijkstra.initialDistances, Dijkstra.vectorLength, ListOps.length]57  | succ(k) using ih =>58    intros index indexNat59    have nextNat := Naturals.constructor.succ with indexNat60    have previous := ih with succ(index), nextNat61    unfold Dijkstra.vectorLength at previous62    simp [Dijkstra.initialDistances, Dijkstra.vectorLength, ListOps.length]6364theorem initialFlags.closed (count : Nat)65  shows List(ℕ, Dijkstra.initialFlags(count))66proof67  induction count68  | zero =>69    have computed : Dijkstra.initialFlags(0) = List.nil by simp [Dijkstra.initialFlags]70    rw computed71    exact List.inductive.constructor.nil72  | succ(k) using ih =>73    have zeroIn := nat.omega.forward with Naturals.constructor.zero74    have constructed := List.inductive.constructor.cons with zeroIn, ih75    have computed : Dijkstra.initialFlags(succ(k)) = List.cons(0, Dijkstra.initialFlags(k))76      settle with Dijkstra.initialFlags77    rwa computed7879theorem initialFlags.length (count : Nat)80  shows ListOps.length{A := ℕ}(Dijkstra.initialFlags(count)) = count81proof82  induction count83  | zero =>84    simp85  | succ(k) using ih =>86    simp [Dijkstra.initialFlags, ListOps.length]8788-- Indexed semantics of initialization, for arbitrary vector lengths.89theorem initialFlags.entry (count target : Nat)90  requires bound : Less(target, count)91  shows Dijkstra.flagAt(Dijkstra.initialFlags(count), target) = 092proof93  induction count generalizing target94  | zero =>95    intros target targetNat bound96    have impossible := Dijkstra.no_less_zero with targetNat97    exfalso98    exact impossible with bound99  | succ(k) using ih =>100    intros target targetNat bound101    have shape := natural.zero_or_successor with targetNat102    cases shape with atZero | atNext103    . rw atZero104      settle with Dijkstra.initialFlags, Dijkstra.flagAt, Dijkstra.boolHead105    . rcases atNext with ⟨j, jNat, position⟩106      rw position at bound107      have smaller := Dijkstra.successor_less_iff.forward with jNat, bound108      have previous := ih with j, jNat, smaller109      rw position110      simp [Dijkstra.initialFlags, Dijkstra.flagAt, Dijkstra.boolTail]111112theorem initialDistances.entry (count index source target : Nat)113  requires bound : Less(target, count)114  shows Dijkstra.entry(Dijkstra.initialDistances(count, index, source), target) = Dijkstra.initialCell(add(target, index), source)115proof116  induction count generalizing index target117  | zero =>118    intros index target indexNat targetNat bound119    have impossible := Dijkstra.no_less_zero with targetNat120    exfalso121    exact impossible with bound122  | succ(k) using ih =>123    intros index target indexNat targetNat bound124    have shape := natural.zero_or_successor with targetNat125    cases shape with atZero | atNext126    . rw atZero127      settle with Dijkstra.initialDistances, Dijkstra.entry, Dijkstra.optionHead, add128    . rcases atNext with ⟨j, jNat, position⟩129      rw position at bound130      have smaller := Dijkstra.successor_less_iff.forward with jNat, bound131      have previous := ih with succ(index), j, jNat, smaller132      have shifted : add(j, succ(index)) = add(succ(j), index) by simp [add, add.succ_right]133      rw shifted at previous134      rw position135      simp [Dijkstra.initialDistances, Dijkstra.entry, Dijkstra.optionTail]136137theorem initialCell.at_source (source : Nat)138  shows Dijkstra.initialCell(source, source) = Option.some(0)139proof140  have same := Grace.Cumulus.Nat.Mod.equalNat.reflexive at source141  simp [Dijkstra.initialCell, Dijkstra.chooseDistance]142143theorem initialCell.witnessed (V E weights : Set, source target : Nat)144  shows Dijkstra.WitnessedDistance(V, E, weights, source, target, Dijkstra.initialCell(target, source))145proof146  have condition := Dijkstra.equalNat.boolean at target, source with *147  have choices := Dijkstra.boolean_cases with condition148  cases choices with no | yes149  . have computed : Dijkstra.initialCell(target, source) = Option.none150      settle with Dijkstra.initialCell, Dijkstra.chooseDistance151    rw computed152    exact Dijkstra.WitnessedDistance.none153  . have same := Grace.Cumulus.Nat.Mod.equalNat.true_iff.forward at target, source with yes154    rw [same, initialCell.at_source]155    have path := HasPathCost.source at V, E, weights, source156    exact Dijkstra.WitnessedDistance.some with Naturals.constructor.zero, path157158theorem initialDistances.lookup (count source target : Nat)159  requires bound : Less(target, count)160  shows Dijkstra.entry(Dijkstra.initialDistances(count, 0, source), target) = Dijkstra.initialCell(target, source)161proof162  have indexed := initialDistances.entry at count, 0, source, target with Naturals.constructor.zero, bound163  simpa [add.right_unit] using indexed164165end Dijkstra166