Grace/Cumulus/GraphTheory/DijkstraIndex.g17

Open in Workbench Download source

Imports

DijkstraVectors

Declarations

Source

1-- The executable priority scan selects an open vector entry.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.DijkstraIndex8import DijkstraVectors910namespace Dijkstra111213theorem equalNat.false_iff (a b : Nat)14  shows equalNat(a, b) = Bool.false ↔ a ≠ b15proof16  exact Grace.Cumulus.Nat.Mod.equalNat.false_iff at a, b with *1718theorem available.finite_iff (value : Option(ℕ), flag index target distance : Nat)19  shows Dijkstra.available(equalNat(flag, 1), value, index) = Option.some(Dijkstra.Candidate.value(target, distance)) ↔20    flag ≠ 1 ∧ value = Option.some(distance) ∧ index = target21proof22  have condition := Dijkstra.equalNat.boolean at flag, 1 with *23  have flagCases := Dijkstra.boolean_cases with condition24  cases flagCases with open | closed25  . have different := equalNat.false_iff.forward at flag, 1 with *{2}, open26    have valueCases := Dijkstra.option_cases at value with assumption27    cases valueCases with absent | finite28    . rw open29      rw absent30      have computed : Dijkstra.available(Bool.false, Option.none, index) = Option.none31        settle with Dijkstra.available, Dijkstra.availableOpen32      rw computed33      have noCandidate := Option.inductive.disjoint.none.some at Dijkstra.Candidate.value(target, distance)34      have noDistance := Option.inductive.disjoint.none.some at distance35      tauto36    . rcases finite with ⟨d, hd, valueEquality⟩37      rw open38      rw valueEquality39      have computed : Dijkstra.available(Bool.false, Option.some(d), index) = Option.some(Dijkstra.Candidate.value(index, d))40        settle with Dijkstra.available, Dijkstra.availableOpen41      rw computed42      constructor43      . intro same44        have pair := Option.inductive.injective.some with same45        have coordinates := Dijkstra.Candidate.inductive.injective.value with pair46        rcases coordinates with ⟨sameIndex, sameDistance⟩47        refine ⟨different, _, sameIndex⟩48        rw sameDistance49        rfl50      . intro facts51        rcases facts with ⟨notClosed, sameValue, sameIndex⟩52        have sameDistance := Option.inductive.injective.some with sameValue53        rw sameIndex54        rw sameDistance55        rfl56  . have sameFlag := Grace.Cumulus.Nat.Mod.equalNat.true_iff.forward at flag, 1 with *{2}, closed57    rw closed58    have computed : Dijkstra.available(Bool.true, value, index) = Option.none by settle with Dijkstra.available59    rw computed60    have noCandidate := Option.inductive.disjoint.none.some at Dijkstra.Candidate.value(target, distance)61    tauto6263predicate IndexedOffer (A values flags start target distance : Set) :=64  ∃ offset ∈ ℕ, Less(offset, ListOps.length{A := A}(values)) ∧65    target = add(start, offset) ∧ Dijkstra.entry(values, offset) = Option.some(distance) ∧66    Dijkstra.flagAt(flags, offset) ≠ 16768theorem scanOffers.sound (A : Set, values : List(A), flags : List(ℕ), start target distance : Nat)69  requires cells : ∀ value ∈ A, Option(ℕ, value)70  requires offered : Option.some(Dijkstra.Candidate.value(target, distance)) ∈ Dijkstra.scanOffers{A := A}(values, flags, start)71  shows IndexedOffer(A, values, flags, start, target, distance)72proof73  induction values generalizing flags start74  | List.nil =>75    intros flags start flagsType startNat offered76    have computed : Dijkstra.scanOffers{A := A}(List.nil, flags, start) = {Option.none}77      settle with Dijkstra.scanOffers78    rw computed at offered79    have impossible := singleton.membership.forward with offered80    have distinct := Option.inductive.disjoint.none.some at Dijkstra.Candidate.value(target, distance)81    exfalso82    apply distinct83    symm84    exact impossible85  | List.cons(head, tail) using ih =>86    intros flags start flagsType startNat offered87    have alternatives : Option.some(Dijkstra.Candidate.value(target, distance)) = Dijkstra.available(equalNat(Dijkstra.boolHead(flags), 1), head, start) ∨ Option.some(Dijkstra.Candidate.value(target, distance)) ∈ Dijkstra.scanOffers{A := A}(tail, Dijkstra.boolTail(flags), succ(start))88      settle with Dijkstra.scanOffers, union2.membership, singleton.membership, offered89    cases alternatives with first | rest90    . have headType := cells with head, assumption91      have flagNat := Dijkstra.boolHead.natural with flagsType92      have equality : Dijkstra.available(equalNat(Dijkstra.boolHead(flags), 1), head, start) = Option.some(Dijkstra.Candidate.value(target, distance))93        symm94        exact first95      have facts := available.finite_iff.forward with headType, flagNat, startNat, *{2}, equality96      rcases facts with ⟨open, value, index⟩97      have zeroIn := nat.omega.forward with Naturals.constructor.zero98      have tailNat := ListOps.length.closed at A, tail with assumption99      have positive : Less(0, succ(ListOps.length{A := A}(tail)))100        unfold Less101        unfold LessEqual102        refine ⟨ListOps.length{A := A}(tail), tailNat, _⟩103        simp [add]104      unfold IndexedOffer105      refine ⟨0, zeroIn, _, _, _, _⟩106      . simp [ListOps.length]107      . rw ← index108        symm109        exact add.right_unit with startNat110      . simp [Dijkstra.entry, Dijkstra.optionHead]111      . simp [Dijkstra.flagAt]112    . have flagsTail := Dijkstra.boolTail.closed at flags with flagsType113      have nextNat := Naturals.constructor.succ with startNat114      have previous := ih with Dijkstra.boolTail(flags), succ(start), flagsTail, nextNat, rest115      rcases previous with ⟨offset, offsetIn, bound, targetValue, distanceValue, open⟩116      have offsetNat := nat.omega.backward with offsetIn117      have nextOffsetNat := Naturals.constructor.succ with offsetNat118      have nextOffsetIn := nat.omega.forward with nextOffsetNat119      have tailNat := ListOps.length.closed at A, tail with assumption120      have larger := Dijkstra.successor_less_iff.backward with offsetNat, tailNat, bound121      have shifted := add.successor_shift with startNat, offsetNat122      unfold IndexedOffer123      refine ⟨succ(offset), nextOffsetIn, _, _, _, _⟩124      . simp [ListOps.length]125      . rw shifted126        exact targetValue127      . simp [Dijkstra.entry, Dijkstra.optionTail]128      . simp [Dijkstra.flagAt]129130theorem scanOffers.includes (A : Set, offset : Nat, values : List(A), flags : List(ℕ), start distance : Nat)131  requires cells : ∀ value ∈ A, Option(ℕ, value)132  requires bound : Less(offset, ListOps.length{A := A}(values))133  requires value : Dijkstra.entry(values, offset) = Option.some(distance)134  requires open : Dijkstra.flagAt(flags, offset) ≠ 1135  shows Option.some(Dijkstra.Candidate.value(add(start, offset), distance)) ∈ Dijkstra.scanOffers{A := A}(values, flags, start)136proof137  induction offset generalizing values flags start138  | zero =>139    intros values flags start valuesType flagsType startNat bound value open140    have shape := Dijkstra.list_cases with valuesType141    cases shape with empty | cons142    . rw empty at bound143      have lengthZero : ListOps.length{A := A}(List.nil) = 0 by settle with ListOps.length144      rw lengthZero at bound145      have impossible := Dijkstra.no_less_zero with Naturals.constructor.zero146      exfalso147      exact impossible with bound148    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩149      have headType := cells with head, headIn150      have flagNat := Dijkstra.boolHead.natural with flagsType151      rw equality at value152      have headValue : head = Option.some(distance)153        simp [Dijkstra.entry, Dijkstra.optionHead] at value154        exact value155      have headOpen : Dijkstra.boolHead(flags) ≠ 1156        simp [Dijkstra.flagAt] at open157        exact open158      have facts : Dijkstra.boolHead(flags) ≠ 1 ∧ head = Option.some(distance) ∧ start = start159        refine ⟨headOpen, headValue, rfl⟩160      have available := available.finite_iff.backward with headType, flagNat, startNat, startNat, assumption, facts161      have sameIndex := add.right_unit with startNat162      rw sameIndex163      rw equality164      have collected : Dijkstra.scanOffers{A := A}(List.cons(head, tail), flags, start) = {Dijkstra.available(equalNat(Dijkstra.boolHead(flags), 1), head, start)} ∪ Dijkstra.scanOffers{A := A}(tail, Dijkstra.boolTail(flags), succ(start))165        settle with Dijkstra.scanOffers166      rw collected167      rw available168      apply union2.left169      exact singleton.self170  | succ(k) using ih =>171    intros values flags start valuesType flagsType startNat bound value open172    have shape := Dijkstra.list_cases with valuesType173    cases shape with empty | cons174    . rw empty at bound175      have lengthZero : ListOps.length{A := A}(List.nil) = 0 by settle with ListOps.length176      rw lengthZero at bound177      have skNat : Nat(succ(k)) by typecheck178      have impossible := Dijkstra.no_less_zero with skNat179      exfalso180      exact impossible with bound181    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩182      have tailNat := ListOps.length.closed with tailType183      have kNat : Nat(k) by typecheck184      rw equality at bound185      have lengthStep : ListOps.length{A := A}(List.cons(head, tail)) = succ(ListOps.length{A := A}(tail))186        settle with ListOps.length187      rw lengthStep at bound188      have smaller := Dijkstra.successor_less_iff.forward with kNat, tailNat, bound189      rw equality at value190      have tailValue : Dijkstra.entry(tail, k) = Option.some(distance)191        simp [Dijkstra.entry, Dijkstra.optionTail] at value192        exact value193      have tailOpen : Dijkstra.flagAt(Dijkstra.boolTail(flags), k) ≠ 1194        simp [Dijkstra.flagAt] at open195        exact open196      have flagsTail := Dijkstra.boolTail.closed with flagsType197      have nextNat := Naturals.constructor.succ with startNat198      have previous := ih with tail, Dijkstra.boolTail(flags), succ(start), tailType, flagsTail, nextNat, smaller, tailValue, tailOpen199      have shift := add.successor_shift with startNat, kNat200      rw shift201      rw equality202      have collected : Dijkstra.scanOffers{A := A}(List.cons(head, tail), flags, start) = {Dijkstra.available(equalNat(Dijkstra.boolHead(flags), 1), head, start)} ∪ Dijkstra.scanOffers{A := A}(tail, Dijkstra.boolTail(flags), succ(start))203        settle with Dijkstra.scanOffers204      rw collected205      apply union2.right206      exact previous207208theorem minimum.selected_entry (A : Set, values : List(A), flags : List(ℕ), target distance : Nat)209  requires cells : ∀ value ∈ A, Option(ℕ, value)210  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(target, distance))211  shows Less(target, ListOps.length{A := A}(values)) ∧212    Dijkstra.entry(values, target) = Option.some(distance) ∧ Dijkstra.flagAt(flags, target) ≠ 1213proof214  obtain ⟨valid, member, least⟩ := Dijkstra.minimum.correct with Naturals.constructor.zero, cells215  rw chosen at member216  obtain ⟨offset, offsetIn, bound, targetValue, value, open⟩ := scanOffers.sound with Naturals.constructor.zero, cells, member217  have zeroAdd : add(0, offset) = offset by simp [add]218  rw zeroAdd at targetValue219  rw targetValue220  refine ⟨bound, value, open⟩221222theorem minimum.le_open_entry (A : Set, values : List(A), flags : List(ℕ), target distance other cost : Nat)223  requires cells : ∀ value ∈ A, Option(ℕ, value)224  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(target, distance))225  requires bound : Less(other, ListOps.length{A := A}(values))226  requires value : Dijkstra.entry(values, other) = Option.some(cost)227  requires open : Dijkstra.flagAt(flags, other) ≠ 1228  shows distance ≤ cost229proof230  have offered := scanOffers.includes at A, other, values, flags, 0, cost with Naturals.constructor.zero, cells, bound, value, open231  have zeroAdd : add(0, other) = other by simp [add]232  rw zeroAdd at offered233  obtain ⟨j, hj, c, hc, equality, order⟩ := Dijkstra.minimum.le_every_offer with Naturals.constructor.zero, cells, offered234  rw chosen at equality235  have pair := Option.inductive.injective.some with equality236  obtain ⟨indexEquality, distanceEquality⟩ := Dijkstra.Candidate.inductive.injective.value with pair237  rwa distanceEquality238239theorem minimum.none_no_open_finite (A : Set, values : List(A), flags : List(ℕ), target distance : Nat)240  requires cells : ∀ value ∈ A, Option(ℕ, value)241  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none242  requires bound : Less(target, ListOps.length{A := A}(values))243  requires value : Dijkstra.entry(values, target) = Option.some(distance)244  shows Dijkstra.flagAt(flags, target) = 1245proof246  by_contra open247  have offered := scanOffers.includes at A, target, values, flags, 0, distance with *{3}, Naturals.constructor.zero, assumption, cells, bound, value, open248  have zeroAdd : add(0, target) = target by settle with add249  rw zeroAdd at offered250  have characterization := Dijkstra.minimum.none_iff.forward with *{2}, Naturals.constructor.zero, cells, absent251  have targetIn := nat.omega.forward at target with assumption252  have distanceIn := nat.omega.forward at distance with assumption253  have impossible := characterization with target, targetIn, distance, distanceIn254  exact impossible with offered255256theorem minimum.none_iff_no_open_finite (A : Set, values : List(A), flags : List(ℕ))257  requires cells : ∀ value ∈ A, Option(ℕ, value)258  shows Dijkstra.minimum(values, flags, 0) = Option.none ↔259    (∀ target ∈ ℕ, ∀ distance ∈ ℕ,260      Less(target, ListOps.length{A := A}(values)) → Dijkstra.entry(values, target) = Option.some(distance) → Dijkstra.flagAt(flags, target) = 1)261proof262  constructor263  . intros absent target targetIn distance distanceIn bound value264    have targetNat := nat.omega.backward with targetIn265    have distanceNat := nat.omega.backward with distanceIn266    exact minimum.none_no_open_finite with *267  . intro noOpen268    obtain ⟨valid, member, least⟩ := Dijkstra.minimum.correct with Naturals.constructor.zero, cells269    cases valid with absent | finite270    . exact absent271    . rcases finite with ⟨candidateIndex, candidateIndexIn, candidateCost, candidateCostIn, equality⟩272      have candidateIndexNat := nat.omega.backward with candidateIndexIn273      have candidateCostNat := nat.omega.backward with candidateCostIn274      have actual := minimum.selected_entry at A, values, flags, candidateIndex, candidateCost with *275      rcases actual with ⟨candidateBound, candidateValue, candidateOpen⟩276      have closed := noOpen with candidateIndex, candidateIndexIn, candidateCost, candidateCostIn, candidateBound, candidateValue277      exfalso278      exact candidateOpen with closed279280end Dijkstra281