-- Checked semantics of an executable Dijkstra advancement.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.GraphTheory.DijkstraStep
import DijkstraInitial
import DijkstraIndex

namespace Dijkstra


theorem relax.entry_no_increase (values weights : List(Dijkstra.DistanceValues), flags : List(ℕ), sourceDistance : Option(ℕ), index : Nat)
  requires bound : Less(index, ListOps.length{A := Dijkstra.DistanceValues}(values))
  shows Dijkstra.DistanceAtMost(Dijkstra.entry(Dijkstra.relax(weights, values, flags, sourceDistance), index), Dijkstra.entry(values, index))
proof
  have valueType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, values with Dijkstra.DistanceValues.cells
  have weightType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, weights with Dijkstra.DistanceValues.cells
  have flagNat := Dijkstra.flagAt.natural at index, flags with *
  have condition := Dijkstra.equalNat.boolean at Dijkstra.flagAt(flags, index), 1 with flagNat, assumption
  have monotone := Dijkstra.relaxValue.no_increase at Dijkstra.entry(values, index), Dijkstra.entry(weights, index), sourceDistance, equalNat(Dijkstra.flagAt(flags, index), 1) with valueType, weightType
  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, weights, flags, sourceDistance with *
  rwa pointwise

theorem relax.entry_witnessed (V E weights source u : Set, values row : List(Dijkstra.DistanceValues), flags : List(ℕ), sourceDistance : Option(ℕ), index : Nat)
  requires bound : Less(index, ListOps.length{A := Dijkstra.DistanceValues}(values))
  requires hu : u ∈ V
  requires hv : index ∈ V
  requires oldPaths : Dijkstra.WitnessedDistance(V, E, weights, source, index, Dijkstra.entry(values, index))
  requires sourcePaths : Dijkstra.WitnessedDistance(V, E, weights, source, u, sourceDistance)
  requires edges : ∀ k ∈ ℕ, Dijkstra.entry(row, index) = Option.some(k) → WeightedEdge(E, weights, u, index, k)
  shows Dijkstra.WitnessedDistance(V, E, weights, source, index, Dijkstra.entry(Dijkstra.relax(row, values, flags, sourceDistance), index))
proof
  have valueType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, values with Dijkstra.DistanceValues.cells
  have weightType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, row with Dijkstra.DistanceValues.cells
  have flagNat := Dijkstra.flagAt.natural at index, flags with *
  have condition := Dijkstra.equalNat.boolean at Dijkstra.flagAt(flags, index), 1 with flagNat, assumption
  have witnessed := Dijkstra.WitnessedDistance.relax with valueType, weightType, hu, hv, oldPaths, sourcePaths, edges
  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, row, flags, sourceDistance with *
  rwa pointwise

theorem advance.selected_distance (rows : Set, values : List(Dijkstra.DistanceValues), flags : List(ℕ), index distance : Nat)
  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))
  shows Dijkstra.entry(Dijkstra.distances(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))), index) = Option.some(distance)
proof
  have selected := Dijkstra.minimum.selected_entry at Dijkstra.DistanceValues, values, flags, index, distance with *{4}, Dijkstra.DistanceValues.cells, chosen
  rcases selected with ⟨bound, entryValue, open⟩
  have marked := Dijkstra.mark.at_same at index, flags with *
  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), Option.some(distance) with *
  have computed : Dijkstra.distances(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance))
    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.distances, chosen
  rw computed
  rw pointwise
  rw marked
  have same := Grace.Cumulus.Nat.Mod.equalNat.reflexive at 1 with assumption
  rw same
  have preserved : Dijkstra.relaxValue(Dijkstra.entry(values, index), Dijkstra.entry(Dijkstra.rowAt(rows, index), index), Bool.true, Option.some(distance)) = Dijkstra.entry(values, index)
    settle with Dijkstra.relaxValue
  rw preserved
  exact entryValue

theorem advance.selected_settled (rows values : Set, flags : List(ℕ), index distance : Nat)
  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))
  shows Dijkstra.flagAt(Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))), index) = 1
proof
  have computed : Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.mark(flags, index)
    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.settled, chosen
  rw computed
  exact Dijkstra.mark.at_same at index, flags with *

theorem advance.other_flag (rows values : Set, flags : List(ℕ), index distance target : Nat)
  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))
  requires distinct : target ≠ index
  shows Dijkstra.flagAt(Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))), target) = Dijkstra.flagAt(flags, target)
proof
  have computed : Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.mark(flags, index)
    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.settled, chosen
  rw computed
  exact Dijkstra.mark.at_other at index, target, flags with *

theorem advance.none (rows values flags : Set)
  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none
  shows Dijkstra.advance(rows, Dijkstra.State.current(values, flags)) = Dijkstra.State.current(values, flags)
proof
  unfold Dijkstra.advance
  simp [Dijkstra.advanceChosen]

theorem iterate.none (fuel : Nat, rows values flags : Set)
  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none
  shows Dijkstra.iterate(fuel, rows, Dijkstra.State.current(values, flags)) = Dijkstra.State.current(values, flags)
proof
  induction fuel
  | zero =>
    simp [Dijkstra.iterate]
  | succ(k) using ih =>
    have fixed := advance.none at rows, values, flags with absent
    simp [Dijkstra.iterate]

end Dijkstra