Grace/Cumulus/GraphTheory/DijkstraVectors.g17

Open in Workbench Download source

Imports

DijkstraMinimum

Declarations

Source

1-- Indexed semantics of Dijkstra's recursive vector operations.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.DijkstraVectors8import DijkstraMinimum910namespace Dijkstra1112theorem list_cases (A : Set, values : List(A))13  shows values = List.nil ∨ ∃ head ∈ A, ∃ tail, List(A, tail) ∧ values = List.cons(head, tail)14proof15  induction values16  | List.nil =>17    left18    rfl19  | List.cons(head, tail) using ih =>20    right21    refine ⟨head, assumption, tail, assumption, rfl⟩2223theorem successor_less_iff (a b : Nat)24  shows Less(succ(a), succ(b)) ↔ Less(a, b)25proof26  have saNat := Naturals.constructor.succ at a27  have sbNat := Naturals.constructor.succ at b28  have outer := Dijkstra.less.true_iff with saNat, sbNat29  have inner := Dijkstra.less.true_iff at a, b with *30  have computed : Dijkstra.less(succ(a), succ(b)) = Dijkstra.less(a, b)31    settle with Dijkstra.less, isZero, predecessor, BoolOps.not, BoolOps.and32  rw computed at outer33  tauto3435theorem no_less_zero (a : Nat)36  shows ¬Less(a, 0)37proof38  intro impossible39  have member := membership.of_Less at a, 0 with Naturals.constructor.zero, impossible40  rw nat.zero at member41  exact set.empty with member4243def flagAt (flags : Set, index : Nat) → Set44  | flags, zero => Dijkstra.boolHead(flags)45  | flags, succ(index) => flagAt(Dijkstra.boolTail(flags), index)46  descends index4748theorem optionTail.closed (A : Set, values : List(A))49  shows List(A, Dijkstra.optionTail(values))50proof51  induction values52  | List.nil =>53    have computed : Dijkstra.optionTail(List.nil) = List.nil by simp [Dijkstra.optionTail]54    rw computed55    exact List.inductive.constructor.nil56  | List.cons(head, tail) using ih =>57    have computed : Dijkstra.optionTail(List.cons(head, tail)) = tail by simp [Dijkstra.optionTail]58    rwa computed5960theorem optionHead.valid (A : Set, values : List(A))61  requires cells : ∀ d ∈ A, Option(ℕ, d)62  shows Option(ℕ, Dijkstra.optionHead(values))63proof64  induction values65  | List.nil =>66    have computed : Dijkstra.optionHead(List.nil) = Option.none by simp [Dijkstra.optionHead]67    rw computed68    exact Option.inductive.constructor.none69  | List.cons(head, tail) using ih =>70    have computed : Dijkstra.optionHead(List.cons(head, tail)) = head by simp [Dijkstra.optionHead]71    rw computed72    exact cells with head, assumption7374theorem entry.valid (A : Set, index : Nat, values : List(A))75  requires cells : ∀ d ∈ A, Option(ℕ, d)76  shows Option(ℕ, Dijkstra.entry(values, index))77proof78  induction index generalizing values79  | zero =>80    intros values valuesType81    have computed : Dijkstra.entry(values, 0) = Dijkstra.optionHead(values) by settle with Dijkstra.entry82    rw computed83    exact optionHead.valid with valuesType, cells84  | succ(k) using ih =>85    intros values valuesType86    have tailType := optionTail.closed with valuesType87    have computed : Dijkstra.entry(values, succ(k)) = Dijkstra.entry(Dijkstra.optionTail(values), k)88      settle with Dijkstra.entry89    rw computed90    exact ih with Dijkstra.optionTail(values), tailType9192theorem flagAt.natural (index : Nat, flags : List(ℕ))93  shows Nat(flagAt(flags, index))94proof95  induction index generalizing flags96  | zero =>97    intros flags flagsType98    have computed : flagAt(flags, 0) = Dijkstra.boolHead(flags) by settle with flagAt99    rw computed100    exact Dijkstra.boolHead.natural with flagsType101  | succ(k) using ih =>102    intros flags flagsType103    have tailType := Dijkstra.boolTail.closed with flagsType104    have computed : flagAt(flags, succ(k)) = flagAt(Dijkstra.boolTail(flags), k) by settle with flagAt105    rw computed106    exact ih with Dijkstra.boolTail(flags), tailType107108theorem relax.entry (A : Set, index : Nat, values : List(A), weights flags sourceDistance : Set)109  requires bound : Less(index, ListOps.length{A := A}(values))110  shows Dijkstra.entry(Dijkstra.relax(weights, values, flags, sourceDistance), index) =111    Dijkstra.relaxValue(Dijkstra.entry(values, index), Dijkstra.entry(weights, index),112      equalNat(flagAt(flags, index), 1), sourceDistance)113proof114  induction index generalizing values weights flags sourceDistance115  | zero =>116    intros values weights flags sourceDistance valuesType bound117    have shape := list_cases with valuesType118    cases shape with empty | cons119    . rw empty at bound120      have lengthZero : ListOps.length{A := A}(List.nil) = 0 by settle with ListOps.length121      rw lengthZero at bound122      have impossible := no_less_zero with Naturals.constructor.zero123      exfalso124      exact impossible with bound125    . rcases cons with ⟨head, hhead, tail, tailType, equality⟩126      rw equality127      settle with Dijkstra.relax, Dijkstra.entry, Dijkstra.optionHead, flagAt128  | succ(k) using ih =>129    intros values weights flags sourceDistance valuesType bound130    have shape := list_cases with valuesType131    cases shape with empty | cons132    . rw empty at bound133      have lengthZero : ListOps.length{A := A}(List.nil) = 0 by settle with ListOps.length134      rw lengthZero at bound135      have kNat : Nat(k) by typecheck136      have skNat := Naturals.constructor.succ with kNat137      have impossible := no_less_zero with skNat138      exfalso139      exact impossible with bound140    . rcases cons with ⟨head, hhead, tail, tailType, equality⟩141      rw equality at bound142      have lengthStep : ListOps.length{A := A}(List.cons(head, tail)) = succ(ListOps.length{A := A}(tail))143        settle with ListOps.length144      rw lengthStep at bound145      have kNat : Nat(k) by typecheck146      have lengthNat := ListOps.length.closed with tailType147      have smaller := successor_less_iff.forward with kNat, lengthNat, bound148      have previous := ih with tail, Dijkstra.optionTail(weights), Dijkstra.boolTail(flags), sourceDistance, tailType, smaller149      rw equality150      simp [Dijkstra.relax, Dijkstra.entry, Dijkstra.optionTail, flagAt]151152-- A set carrier for optional natural distances.153def FiniteDistances : Set := { Option.some(d) | d ∈ ℕ }154def DistanceValues : Set := {Option.none} ∪ FiniteDistances155156theorem DistanceValues.membership (value : Set)157  shows value ∈ DistanceValues ↔ Option(ℕ, value)158proof159  have characterized : value ∈ DistanceValues ↔160    (value = Option.none ∨ ∃ d ∈ ℕ, Option.some(d) = value)161    simp [DistanceValues, union2.membership, singleton.membership, FiniteDistances]162  constructor163  . intro member164    have shape := characterized.forward with member165    cases shape with absent | finite166    . rw absent167      exact Option.inductive.constructor.none168    . rcases finite with ⟨d, hd, equality⟩169      rw ← equality170      exact Option.inductive.constructor.some with hd171  . intro valid172    have options := Dijkstra.option_cases with valid173    apply characterized.backward174    cases options with absent | finite175    . left176      exact absent177    . rcases finite with ⟨n, hn, equality⟩178      right179      refine ⟨n, hn, _⟩180      symm181      exact equality182183theorem DistanceValues.cells184  shows ∀ value ∈ DistanceValues, Option(ℕ, value)185proof186  simp187188theorem relaxValue.closed (old weight sourceDistance : Option(ℕ), flag : Bool)189  shows Option(ℕ, Dijkstra.relaxValue(old, weight, flag, sourceDistance))190proof191  induction flag192  | Bool.false =>193    have extended := Dijkstra.extension.closed at sourceDistance, weight with *194    have minimized := Dijkstra.minOption.closed at old, Dijkstra.extension(sourceDistance, weight) with assumption, extended195    simp [Dijkstra.relaxValue]196  | Bool.true =>197    simp [Dijkstra.relaxValue]198199theorem relax.closed (values weights : List(DistanceValues), flags : List(ℕ), sourceDistance : Option(ℕ))200  shows List(DistanceValues, Dijkstra.relax(weights, values, flags, sourceDistance))201proof202  induction values generalizing weights flags203  | List.nil =>204    intros weights flags weightsType flagsType205    have computed : Dijkstra.relax(weights, List.nil, flags, sourceDistance) = List.nil by simp [Dijkstra.relax]206    rw computed207    exact List.inductive.constructor.nil208  | List.cons(head, tail) using ih =>209    intros weights flags weightsType flagsType210    have headType := DistanceValues.membership.forward at head with assumption211    have weightType := entry.valid at DistanceValues, 0, weights with Naturals.constructor.zero, weightsType, DistanceValues.cells212    have headNat := Dijkstra.boolHead.natural with flagsType213    have condition := Dijkstra.equalNat.boolean with headNat, assumption214    have nextType := relaxValue.closed at head, Dijkstra.entry(weights, 0), sourceDistance, equalNat(Dijkstra.boolHead(flags), 1) with headType, weightType215    have nextMember := DistanceValues.membership.backward with nextType216    have weightsTail := optionTail.closed with weightsType217    have flagsTail := Dijkstra.boolTail.closed with flagsType218    have tailResult := ih with Dijkstra.optionTail(weights), Dijkstra.boolTail(flags), weightsTail, flagsTail219    have constructed := List.inductive.constructor.cons with nextMember, tailResult220    simp [Dijkstra.relax]221222def vectorLength (values : Set) : Set := ListOps.length{A := DistanceValues}(values)223224theorem relax.length (A : Set, values : List(A), weights flags sourceDistance : Set)225  shows vectorLength(Dijkstra.relax(weights, values, flags, sourceDistance)) = vectorLength(values)226proof227  induction values generalizing weights flags228  | List.nil =>229    intros weights flags230    simp [Dijkstra.relax, vectorLength, ListOps.length]231  | List.cons(head, tail) using ih =>232    intros weights flags233    have previous := ih with Dijkstra.optionTail(weights), Dijkstra.boolTail(flags)234    unfold vectorLength at previous235    simp [Dijkstra.relax, vectorLength, ListOps.length]236237end Dijkstra238