Grace/Cumulus/GraphTheory/DijkstraProofs.g17

Open in Workbench Download source

Imports

Dijkstra · WeightedPaths

Declarations

Source

1-- Arbitrary-size invariants for the executable Dijkstra 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.DijkstraProofs8import Dijkstra9import WeightedPaths1011namespace Dijkstra1213theorem less.true_iff (a b : Nat)14  shows Dijkstra.less(a, b) = Bool.true ↔ a < b15proof16  induction a generalizing b17  | zero =>18    intros b bNat19    have shape := natural.zero_or_successor with bNat20    cases shape with equal | successor21    . rw equal22      have computed : Dijkstra.less(0, 0) = Bool.false by simp [Dijkstra.less, isZero, BoolOps.not]23      rw computed24      have distinct := Bool.inductive.disjoint.false.true25      have noLess := Less.irreflexive with Naturals.constructor.zero26      tauto27    . rcases successor with ⟨k, kNat, bShape⟩28      rw bShape29      have computed : Dijkstra.less(0, succ(k)) = Bool.true by simp [Dijkstra.less, isZero, BoolOps.not]30      rw computed31      constructor32      . intro truth33        unfold Less34        unfold LessEqual35        refine ⟨k, kNat, _⟩36        simp [add]37      . intro order38        rfl39  | succ(k) using ih =>40    intros b bNat41    have shape := natural.zero_or_successor with bNat42    cases shape with equal | successor43    . rw equal44      have computed : Dijkstra.less(succ(k), 0) = Bool.false45        settle with Dijkstra.less, isZero, predecessor, BoolOps.not, BoolOps.and46      rw computed47      have distinct := Bool.inductive.disjoint.false.true48      have noLess : ¬Less(succ(k), 0)49        intro impossible50        have skNat : Nat(succ(k)) by typecheck51        have member := membership.of_Less with skNat, Naturals.constructor.zero, impossible52        rw nat.zero at member53        exact set.empty with member54      tauto55    . rcases successor with ⟨j, jNat, bShape⟩56      rw bShape57      have reduced : Dijkstra.less(succ(k), succ(j)) = Dijkstra.less(k, j)58        settle with Dijkstra.less, isZero, predecessor, BoolOps.not, BoolOps.and59      rw reduced60      have inner := ih with j, jNat61      constructor62      . intro truth63        have order := inner.forward with truth64        have lifted := Less.add_LessEqual at k, j, 1, 1 with assumption, jNat, *{2}, order, LessEqual.reflexive at 1 with assumption65        simp [add.right_one] at lifted66        exact lifted67      . intro order68        have smaller : k < j69          apply Less.add_right_cancel at k, j, 170          . simp [add.right_one]71        exact inner.backward with smaller727374theorem boolean_cases (b : Bool)75  shows b = Bool.false ∨ b = Bool.true76proof77  induction b78  | Bool.false =>79    left80    rfl81  | Bool.true =>82    right83    rfl8485theorem option_cases (o : Option(ℕ))86  shows o = Option.none ∨ ∃ d ∈ ℕ, o = Option.some(d)87proof88  induction o89  | Option.none =>90    left91    rfl92  | Option.some(d) =>93    right94    refine ⟨d, assumption, rfl⟩9596theorem candidate_cases (c : Dijkstra.Candidate(ℕ,ℕ))97  shows ∃ i ∈ ℕ, ∃ d ∈ ℕ, c = Dijkstra.Candidate.value(i, d)98proof99  induction c100  | Dijkstra.Candidate.value(i, d) =>101    refine ⟨i, assumption, d, assumption, rfl⟩102103theorem less.boolean (a b : Nat)104  shows Bool(Dijkstra.less(a, b))105proof106  induction a generalizing b107  | zero =>108    intros b bNat109    have shape := natural.zero_or_successor with bNat110    cases shape with equal | successor111    . rw equal112      have computed : Dijkstra.less(0, 0) = Bool.false by simp [Dijkstra.less, isZero, BoolOps.not]113      rw computed114      exact Bool.inductive.constructor.false115    . rcases successor with ⟨k, kNat, equal⟩116      rw equal117      have computed : Dijkstra.less(0, succ(k)) = Bool.true by simp [Dijkstra.less, isZero, BoolOps.not]118      rw computed119      exact Bool.inductive.constructor.true120  | succ(k) using ih =>121    intros b bNat122    have shape := natural.zero_or_successor with bNat123    cases shape with equal | successor124    . rw equal125      have computed : Dijkstra.less(succ(k), 0) = Bool.false126        settle with Dijkstra.less, isZero, BoolOps.not, BoolOps.and127      rw computed128      exact Bool.inductive.constructor.false129    . rcases successor with ⟨j, jNat, equal⟩130      rw equal131      have computed : Dijkstra.less(succ(k), succ(j)) = Dijkstra.less(k, j)132        settle with Dijkstra.less, isZero, predecessor, BoolOps.not, BoolOps.and133      rw computed134      exact ih with j, jNat135136theorem less.false_iff (a b : Nat)137  shows Dijkstra.less(a, b) = Bool.false ↔ b ≤ a138proof139  have typed := less.boolean at a, b with *140  have shape := boolean_cases with typed141  have meaning := less.true_iff at a, b with *142  have distinct := Bool.inductive.disjoint.false.true143  constructor144  . intro no145    have notLess : ¬(a < b)146      intro order147      have yes := meaning.backward with order148      rw no at yes149      exact distinct with yes150    exact LessEqual.of_not_Less with *151  . intro order152    cases shape with no | yes153    . exact no154    . have strict := meaning.forward with yes155      have cycle : a < a by arith156      have noCycle := Less.irreflexive at a157      exfalso158      exact noCycle with cycle159160161theorem chooseDistance.selects (first second : Set, condition : Bool)162  shows Dijkstra.chooseDistance(condition, first, second) = first ∨163    Dijkstra.chooseDistance(condition, first, second) = second164proof165  induction condition166  | Bool.false =>167    right168    simp [Dijkstra.chooseDistance]169  | Bool.true =>170    left171    simp [Dijkstra.chooseDistance]172173theorem minOption.selects (old new : Option(ℕ))174  shows Dijkstra.minOption(old, new) = old ∨ Dijkstra.minOption(old, new) = new175proof176  induction old generalizing new177  | Option.none =>178    intros new newType179    right180    settle with Dijkstra.minOption181  | Option.some(d) =>182    intros new newType183    have shape := option_cases with newType184    cases shape with absent | present185    . rw absent186      left187      settle with Dijkstra.minOption, Dijkstra.minSome188    . rcases present with ⟨e, he, equality⟩189      rw equality190      have dNat : Nat(d) by typecheck191      have eNat := nat.omega.backward with he192      have condition := less.boolean with eNat, dNat193      have selected := chooseDistance.selects at Option.some(e), Option.some(d), Dijkstra.less(e, d) with condition194      simp [Dijkstra.minOption, Dijkstra.minSome]195196theorem minOption.finite (a b : Nat)197  shows ∃ d ∈ ℕ, Dijkstra.minOption(Option.some(a), Option.some(b)) = Option.some(d) ∧198    (d = a ∨ d = b) ∧ d ≤ a ∧ d ≤ b199proof200  have condition := less.boolean at b, a with *201  have shape := boolean_cases with condition202  cases shape with no | yes203  . have order := less.false_iff.forward at b, a with *{2}, no204    have aIn := nat.omega.forward at a with assumption205    have same := LessEqual.reflexive at a with assumption206    have computed : Dijkstra.minOption(Option.some(a), Option.some(b)) = Option.some(a)207      settle with Dijkstra.minOption, Dijkstra.minSome, Dijkstra.chooseDistance, no208    refine ⟨a, aIn, computed, _, same, order⟩209    left210    rfl211  . have strict := less.true_iff.forward at b, a with *{2}, yes212    have order := Less.implies_LessEqual at b, a with *213    have bIn := nat.omega.forward at b with assumption214    have same := LessEqual.reflexive at b with assumption215    have computed : Dijkstra.minOption(Option.some(a), Option.some(b)) = Option.some(b)216      settle with Dijkstra.minOption, Dijkstra.minSome, Dijkstra.chooseDistance, yes217    refine ⟨b, bIn, computed, _, order, same⟩218    right219    rfl220221-- A finite distance is justified by a real path; none makes no claim.222predicate WitnessedDistance (V E weights source target distance : Set) :=223  ∀ d ∈ ℕ, distance = Option.some(d) → HasPathCost(V, E, weights, source, target, d)224225theorem WitnessedDistance.minimum (V E weights source target : Set, old new : Option(ℕ))226  requires oldPath : WitnessedDistance(V, E, weights, source, target, old)227  requires newPath : WitnessedDistance(V, E, weights, source, target, new)228  shows WitnessedDistance(V, E, weights, source, target, Dijkstra.minOption(old, new))229proof230  have selected := minOption.selects at old, new with *231  cases selected with first | second232  . rw first233    exact oldPath234  . rw second235    exact newPath236237theorem WitnessedDistance.some (V E weights source target : Set, cost : Nat)238  requires path : HasPathCost(V, E, weights, source, target, cost)239  shows WitnessedDistance(V, E, weights, source, target, Option.some(cost))240proof241  intros d hd equality242  have same := Option.inductive.injective.some with equality243  rwa ← same244245theorem WitnessedDistance.none (V E weights source target : Set)246  shows WitnessedDistance(V, E, weights, source, target, Option.none)247proof248  intros d hd equality249  have impossible := Option.inductive.disjoint.none.some at d250  exfalso251  exact impossible with equality252253theorem WitnessedDistance.extension (V E weights source u v : Set, c k : Nat)254  requires hu : u ∈ V255  requires hv : v ∈ V256  requires prefix : HasPathCost(V, E, weights, source, u, c)257  requires edge : WeightedEdge(E, weights, u, v, k)258  shows WitnessedDistance(V, E, weights, source, v,259    Dijkstra.extension(Option.some(c), Option.some(k)))260proof261  have path := HasPathCost.extend with hu, hv, prefix, edge262  have result := WitnessedDistance.some with path263  simp [Dijkstra.extension, Dijkstra.extendSome]264265266theorem minOption.closed (old new : Option(ℕ))267  shows Option(ℕ, Dijkstra.minOption(old, new))268proof269  have selected := minOption.selects at old, new with *270  cases selected with first | second271  . rw first272    assumption273  . rw second274    assumption275276theorem extension.closed (distance weight : Option(ℕ))277  shows Option(ℕ, Dijkstra.extension(distance, weight))278proof279  induction distance generalizing weight280  | Option.none =>281    intros weight weightType282    have computed : Dijkstra.extension(Option.none, weight) = Option.none283      settle with Dijkstra.extension284    rw computed285    exact Option.inductive.constructor.none at ℕ286  | Option.some(c) =>287    intros weight weightType288    have shape := option_cases at weight with weightType289    cases shape with absent | present290    . rw absent291      have computed : Dijkstra.extension(Option.some(c), Option.none) = Option.none292        settle with Dijkstra.extension, Dijkstra.extendSome293      rw computed294      exact Option.inductive.constructor.none at ℕ295    . rcases present with ⟨k, hk, equality⟩296      rw equality297      have computed : Dijkstra.extension(Option.some(c), Option.some(k)) = Option.some(add(c, k))298        settle with Dijkstra.extension, Dijkstra.extendSome299      rw computed300      have kNat := nat.omega.backward at k with hk301      have sumNat := add.closed at k, c with kNat302      have sumIn := nat.omega.forward at add(c, k) with sumNat303      exact Option.inductive.constructor.some at ℕ, add(c, k) with sumIn304305theorem WitnessedDistance.extend_option (V E weights source u v : Set, distance weight : Option(ℕ))306  requires hu : u ∈ V307  requires hv : v ∈ V308  requires sourcePaths : WitnessedDistance(V, E, weights, source, u, distance)309  requires edges : ∀ k ∈ ℕ, weight = Option.some(k) → WeightedEdge(E, weights, u, v, k)310  shows WitnessedDistance(V, E, weights, source, v, Dijkstra.extension(distance, weight))311proof312  have distanceShape := option_cases at distance with assumption313  have weightShape := option_cases at weight with assumption314  cases distanceShape with noDistance | finiteDistance315  . rw noDistance316    have computed : Dijkstra.extension(Option.none, weight) = Option.none by simp [Dijkstra.extension]317    rw computed318    exact WitnessedDistance.none319  . rcases finiteDistance with ⟨c, hc, distanceValue⟩320    cases weightShape with noEdge | finiteEdge321    . rw noEdge322      have computed := Dijkstra.extension.absent_edge at distance with assumption323      rw computed324      exact WitnessedDistance.none325    . rcases finiteEdge with ⟨k, hk, weightValue⟩326      have prefix := sourcePaths with c, hc, distanceValue327      have edge := edges with k, hk, weightValue328      have cNat := nat.omega.backward with hc329      have kNat := nat.omega.backward with hk330      rw [distanceValue, weightValue]331      exact WitnessedDistance.extension with cNat, kNat, hu, hv, prefix, edge332333theorem WitnessedDistance.relax (V E weights source u v : Set, old weight distance : Option(ℕ), flag : Bool)334  requires hu : u ∈ V335  requires hv : v ∈ V336  requires oldPaths : WitnessedDistance(V, E, weights, source, v, old)337  requires sourcePaths : WitnessedDistance(V, E, weights, source, u, distance)338  requires edges : ∀ k ∈ ℕ, weight = Option.some(k) → WeightedEdge(E, weights, u, v, k)339  shows WitnessedDistance(V, E, weights, source, v, Dijkstra.relaxValue(old, weight, flag, distance))340proof341  induction flag342  | Bool.false =>343    have extended := WitnessedDistance.extend_option with *344    have selected := WitnessedDistance.minimum with oldPaths, extended345    simp [Dijkstra.relaxValue]346  | Bool.true =>347    have computed := Dijkstra.relaxValue.settled at old, weight, distance with *348    rwa computed349350predicate DistanceAtMost (first second : Set) :=351  ∀ e ∈ ℕ, second = Option.some(e) →352    ∃ d ∈ ℕ, first = Option.some(d) ∧ d ≤ e353354theorem DistanceAtMost.reflexive (distance : Set)355  shows DistanceAtMost(distance, distance)356proof357  intros e he equality358  have eNat := nat.omega.backward with he359  have same := LessEqual.reflexive with eNat360  refine ⟨e, he, equality, same⟩361362theorem minOption.no_increase (old new : Option(ℕ))363  shows DistanceAtMost(Dijkstra.minOption(old, new), old)364proof365  intros e he oldValue366  have eNat := nat.omega.backward with he367  have newShape := option_cases at new with assumption368  cases newShape with absent | present369  . have same := LessEqual.reflexive at e with eNat370    refine ⟨e, he, _, same⟩371    rw absent372    have computed := Dijkstra.minOption.none_right at old with assumption373    rwa computed374  . rcases present with ⟨b, hb, newValue⟩375    have bNat := nat.omega.backward with hb376    obtain ⟨d, hd, computed, selected, leOld, leNew⟩ := minOption.finite with eNat, bNat377    refine ⟨d, hd, _, leOld⟩378    rwa [oldValue, newValue]379380theorem relaxValue.no_increase (old weight distance : Option(ℕ), flag : Bool)381  shows DistanceAtMost(Dijkstra.relaxValue(old, weight, flag, distance), old)382proof383  induction flag384  | Bool.false =>385    have extensionType := extension.closed at distance, weight with *386    have bound := minOption.no_increase at old, Dijkstra.extension(distance, weight) with assumption, extensionType387    simp [Dijkstra.relaxValue]388  | Bool.true =>389    have computed := Dijkstra.relaxValue.settled at old, weight, distance with *390    rw computed391    exact DistanceAtMost.reflexive392393end Dijkstra394