DijkstraVerificationStarter

Using Dijkstra's scalar, greedy-step, and complete solver correctness theorems

Open in Workbench View on GitHub

1-- Using Dijkstra's scalar, greedy-step, and complete solver correctness theorems.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module User.DijkstraVerificationStarter8import Grace.Cumulus.GraphTheory910theorem executable_comparison (a b : Nat)11  shows Dijkstra.less(a, b) = Bool.true ↔ a < b12proof13  exact Dijkstra.less.true_iff with assumption, assumption1415theorem relaxation_improves (old weight distance : Option(ℕ), flag : Bool)16  shows Dijkstra.DistanceAtMost(Dijkstra.relaxValue(old, weight, flag, distance), old)17proof18  exact Dijkstra.relaxValue.no_increase with assumption, assumption, assumption, assumption1920-- The competing paths have arbitrary finite length.21theorem certified_greedy_step (V E weights source S labels bound target : Set)22  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)23  requires frontier : FrontierCutBound(V, E, weights, source, S, labels, bound)24  requires targetIn : target ∈ V25  requires outside : ¬(target ∈ S)26  requires path : HasPathCost(V, E, weights, source, target, bound)27  shows ShortestPathCost(V, E, weights, source, target, bound)28proof29  exact FrontierCutBound.certifies_next with settled, frontier, targetIn, outside, path3031theorem no_path_across_closed_boundary (V E weights source target cost S : Set)32  requires start : source ∈ S33  requires closed : EdgeClosed(V, E, S)34  requires targetIn : target ∈ V35  requires outside : ¬(target ∈ S)36  requires costNat : Nat(cost)37  shows ¬HasPathCost(V, E, weights, source, target, cost)38proof39  exact EdgeClosed.excludes_path with start, closed, targetIn, outside, costNat4041theorem finite_update42  shows Dijkstra.relaxValue(Option.some(20), Option.some(4), Bool.false, Option.some(7)) = Option.some(11)43proof44  compute4546theorem settled_update47  shows Dijkstra.relaxValue(Option.some(20), Option.some(4), Bool.true, Option.some(7)) = Option.some(20)48proof49  compute5051-- The public theorem applies to arbitrary represented matrices and sizes.52theorem computed_cost_is_shortest (count source target distance : Nat, E weights rows : Set)53  requires sourceIn : source ∈ Dijkstra.Vertices(count)54  requires targetIn : target ∈ Dijkstra.Vertices(count)55  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)56  requires value : Dijkstra.entry(Dijkstra.distances(Dijkstra.solve(count, source, rows)), target) = Option.some(distance)57  shows ShortestPathCost(Dijkstra.Vertices(count), E, weights, source, target, distance)58proof59  have correct := Dijkstra.solve.correct with assumption, assumption, assumption, sourceIn, targetIn, matrix60  rcases correct with ⟨finite, unreachable⟩61  have distanceIn := nat.omega.forward at distance with assumption62  have characterization := finite with distance, distanceIn63  exact characterization.forward with value6465theorem none_exactly_unreachable (count source target : Nat, E weights rows : Set)66  requires sourceIn : source ∈ Dijkstra.Vertices(count)67  requires targetIn : target ∈ Dijkstra.Vertices(count)68  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)69  shows Dijkstra.entry(Dijkstra.distances(Dijkstra.solve(count, source, rows)), target) = Option.none ↔70    (∀ cost ∈ ℕ, ¬HasPathCost(Dijkstra.Vertices(count), E, weights, source, target, cost))71proof72  have correct := Dijkstra.solve.correct with assumption, assumption, assumption, sourceIn, targetIn, matrix73  rcases correct with ⟨finite, unreachable⟩74  exact unreachable75