Grace/Cumulus/GraphTheory/DijkstraProgress.g17

Open in Workbench Download source

Imports

DijkstraStep

Declarations

Source

1-- A decreasing count of open flags for Dijkstra iterations.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.DijkstraProgress8import DijkstraStep910namespace Dijkstra111213def openCount (flags : List(ℕ)) → Nat14  | List.nil => 015  | List.cons(head, tail) => chooseNat(equalNat(head, 1), openCount(tail), succ(openCount(tail)))1617theorem openCount.closed (flags : List(ℕ))18  shows Nat(openCount(flags))19proof20  induction flags21  | List.nil =>22    have computed : openCount(List.nil) = 0 by settle with openCount23    rw computed24    exact Naturals.constructor.zero25  | List.cons(head, tail) using ih =>26    have headNat : Nat(head) by typecheck27    have condition := Dijkstra.equalNat.boolean at head, 1 with headNat, assumption28    have shape := Dijkstra.boolean_cases with condition29    have nextNat := Naturals.constructor.succ with ih30    cases shape with closed | open31    . have branch := closed32      have computed : openCount(List.cons(head, tail)) = succ(openCount(tail))33        settle with openCount, chooseNat, closed, Grace.Cumulus.Nat.Mod.equalNat.reflexive34      rw computed35      exact nextNat36    . have branch := open37      have computed : openCount(List.cons(head, tail)) = openCount(tail) by settle with openCount, chooseNat, open38      rw computed39      exact ih4041theorem openCount.initial (count : Nat)42  shows openCount(Dijkstra.initialFlags(count)) = count43proof44  induction count45  | zero =>46    simp47  | succ(k) using ih =>48    simp [Dijkstra.initialFlags, openCount, equalNat, isZero, chooseNat]4950theorem openCount.mark_decreases (index : Nat, flags : List(ℕ))51  requires open : Dijkstra.flagAt(flags, index) ≠ 152  shows openCount(flags) = succ(openCount(Dijkstra.mark(flags, index)))53proof54  induction index generalizing flags55  | zero =>56    intros flags flagsType open57    have shape := Dijkstra.list_cases with flagsType58    cases shape with empty | cons59    . rw empty at open60      have default := Dijkstra.flagAt.nil with Naturals.constructor.zero61      exfalso62      exact open with default63    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩64      have headNat := nat.omega.backward with headIn65      rw equality at open66      have position : Dijkstra.flagAt(List.cons(head, tail), 0) = head67        settle with Dijkstra.flagAt, Dijkstra.boolHead68      rw position at open69      have condition := Dijkstra.equalNat.false_iff.backward with headNat, assumption, open70      have same := Grace.Cumulus.Nat.Mod.equalNat.reflexive at 1 with assumption71      rw equality72      simp [Dijkstra.mark, Dijkstra.markHead, openCount, chooseNat]73  | succ(k) using ih =>74    intros flags flagsType open75    have shape := Dijkstra.list_cases with flagsType76    cases shape with empty | cons77    . rw empty at open78      have skNat : Nat(succ(k)) by typecheck79      have default := Dijkstra.flagAt.nil with skNat80      exfalso81      exact open with default82    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩83      have headNat := nat.omega.backward with headIn84      rw equality at open85      have position : Dijkstra.flagAt(List.cons(head, tail), succ(k)) = Dijkstra.flagAt(tail, k)86        settle with Dijkstra.flagAt, Dijkstra.boolTail87      rw position at open88      have previous := ih with tail, tailType, open89      have condition := Dijkstra.equalNat.boolean at head, 1 with headNat, assumption90      have alternatives := Dijkstra.boolean_cases with condition91      rw equality92      cases alternatives with closed | openHead93      . simp [Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolTail, openCount, chooseNat]94      . simp [Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolTail, openCount, chooseNat]9596theorem advance.openCount_decreases (rows : Set, values : List(Dijkstra.DistanceValues), flags : List(ℕ), index distance : Nat)97  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))98  shows openCount(flags) = succ(openCount(Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags)))))99proof100  have selected := Dijkstra.minimum.selected_entry at Dijkstra.DistanceValues, values, flags, index, distance with *{4}, Dijkstra.DistanceValues.cells, chosen101  rcases selected with ⟨bound, entryValue, open⟩102  have decreases := openCount.mark_decreases at index, flags with *103  have computed : Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.mark(flags, index)104    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.settled, chosen105  rw computed106  exact decreases107108theorem openCount.zero_all_closed (flags : List(ℕ), index : Nat)109  requires zeroCount : openCount(flags) = 0110  shows Dijkstra.flagAt(flags, index) = 1111proof112  induction flags generalizing index113  | List.nil =>114    intros index indexNat zeroCount115    exact Dijkstra.flagAt.nil with indexNat116  | List.cons(head, tail) using ih =>117    intros index indexNat zeroCount118    have headNat : Nat(head) by typecheck119    have condition := Dijkstra.equalNat.boolean at head, 1 with headNat, assumption120    have alternatives := Dijkstra.boolean_cases with condition121    cases alternatives with open | closed122    . have impossible := Naturals.disjoint.zero.succ at openCount(tail)123      have computed : openCount(List.cons(head, tail)) = succ(openCount(tail))124        settle with openCount, chooseNat, open125      rw computed at zeroCount126      exfalso127      apply impossible128      symm129      exact zeroCount130    . have headOne := Grace.Cumulus.Nat.Mod.equalNat.true_iff.forward at head, 1 with headNat, assumption, closed131      have computed : openCount(List.cons(head, tail)) = openCount(tail)132        settle with openCount, chooseNat, closed, Grace.Cumulus.Nat.Mod.equalNat.reflexive133      rw computed at zeroCount134      have indexShape := natural.zero_or_successor with indexNat135      cases indexShape with zeroIndex | nextIndex136      . rw zeroIndex137        simp [Dijkstra.flagAt, Dijkstra.boolHead]138      . rcases nextIndex with ⟨j, jNat, indexValue⟩139        have previous := ih with j, jNat, zeroCount140        rw indexValue141        simp [Dijkstra.flagAt, Dijkstra.boolTail]142143predicate TypedRows (rows : Set) :=144  ∀ index ∈ ℕ, List(Dijkstra.DistanceValues, Dijkstra.rowAt(rows, index))145146theorem iterate.exhausts_finite_frontier (fuel : Nat, rows : Set, values : List(Dijkstra.DistanceValues), flags : List(ℕ))147  requires rowsTyped : TypedRows(rows)148  requires budget : openCount(flags) ≤ fuel149  shows Dijkstra.minimum(Dijkstra.distances(Dijkstra.iterate(fuel, rows, Dijkstra.State.current(values, flags))),150    Dijkstra.settled(Dijkstra.iterate(fuel, rows, Dijkstra.State.current(values, flags))), 0) = Option.none151proof152  induction fuel generalizing values flags153  | zero =>154    intros values flags valuesType flagsType budget155    have countNat := openCount.closed with flagsType156    have nonnegative := Grace.Core.Nat.Order.LessEqual.zero with countNat157    have zeroCount := LessEqual.antisymmetric at openCount(flags), 0 with countNat, Naturals.constructor.zero, budget, nonnegative158    have noOpen : ∀ target ∈ ℕ, ∀ distance ∈ ℕ, Less(target, ListOps.length{A := Dijkstra.DistanceValues}(values)) → Dijkstra.entry(values, target) = Option.some(distance) → Dijkstra.flagAt(flags, target) = 1159      intros target targetIn distance distanceIn bound value160      have targetNat := nat.omega.backward with targetIn161      exact openCount.zero_all_closed with flagsType, targetNat, zeroCount162    have absent := Dijkstra.minimum.none_iff_no_open_finite.backward at Dijkstra.DistanceValues, values, flags with valuesType, flagsType, Dijkstra.DistanceValues.cells, noOpen163    simp [Dijkstra.iterate, Dijkstra.distances, Dijkstra.settled]164  | succ(k) using ih =>165    intros values flags valuesType flagsType budget166    have correct := Dijkstra.minimum.correct at Dijkstra.DistanceValues, values, flags, 0 with valuesType, flagsType, Naturals.constructor.zero, Dijkstra.DistanceValues.cells167    rcases correct with ⟨valid, member, least⟩168    have skNat : Nat(succ(k)) by typecheck169    cases valid with absent | finite170    . have fixed := Dijkstra.iterate.none at succ(k), rows, values, flags with skNat, absent171      rw fixed172      simp [Dijkstra.distances, Dijkstra.settled]173    . rcases finite with ⟨index, indexIn, distance, distanceIn, chosen⟩174      have indexNat := nat.omega.backward with indexIn175      have distanceNat := nat.omega.backward with distanceIn176      have selected := Dijkstra.minimum.selected_entry at Dijkstra.DistanceValues, values, flags, index, distance with valuesType, flagsType, indexNat, distanceNat, Dijkstra.DistanceValues.cells, chosen177      rcases selected with ⟨bound, value, open⟩178      have decreases := openCount.mark_decreases with indexNat, flagsType, open179      have markedType := Dijkstra.mark.closed with indexNat, flagsType180      have markedCountNat := openCount.closed with markedType181      have kNat : Nat(k) by typecheck182      rw decreases at budget183      have smaller : openCount(Dijkstra.mark(flags, index)) ≤ k184        apply LessEqual.add_right_cancel at openCount(Dijkstra.mark(flags, index)), k, 1185        . have leftStep := add.right_one at openCount(Dijkstra.mark(flags, index)) with markedCountNat186          have rightStep := add.right_one with kNat187          rw leftStep188          rw rightStep189          exact budget190      have rowType := rowsTyped with index, indexIn191      have sourceType := Option.inductive.constructor.some at ℕ, distance with distanceIn192      have relaxedType := Dijkstra.relax.closed with valuesType, rowType, markedType, sourceType193      have previous := ih with Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), Dijkstra.mark(flags, index), relaxedType, markedType, smaller194      have advanced : Dijkstra.advance(rows, Dijkstra.State.current(values, flags)) = Dijkstra.State.current(Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), Dijkstra.mark(flags, index))195        settle with Dijkstra.advance, Dijkstra.advanceChosen, chosen196      simp [Dijkstra.iterate]197198theorem solve.exhausts_finite_frontier (count source : Nat, rows : Set)199  requires rowsTyped : TypedRows(rows)200  shows Dijkstra.minimum(Dijkstra.distances(Dijkstra.solve(count, source, rows)), Dijkstra.settled(Dijkstra.solve(count, source, rows)), 0) = Option.none201proof202  have valuesType := Dijkstra.initialDistances.closed at count, 0, source with Naturals.constructor.zero203  have countValue := openCount.initial at count204  have budget : openCount(Dijkstra.initialFlags(count)) ≤ count205    rw countValue206    exact LessEqual.reflexive with assumption207  have terminated := iterate.exhausts_finite_frontier with rowsTyped, budget208  unfold Dijkstra.solve209  exact terminated210211end Dijkstra212