Grace/Cumulus/GraphTheory/DijkstraMinimum.g17

Open in Workbench Download source

Imports

DijkstraProofs

Declarations

Source

1-- Correctness of the complete executable priority scan.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.DijkstraMinimum8import DijkstraProofs910namespace Dijkstra1112predicate CandidateOption (result : Set) :=13  result = Option.none ∨ ∃ i ∈ ℕ, ∃ d ∈ ℕ,14    result = Option.some(Dijkstra.Candidate.value(i, d))1516predicate CandidateOrder (first second : Set) :=17  ∀ i ∈ ℕ, ∀ d ∈ ℕ, second = Option.some(Dijkstra.Candidate.value(i, d)) →18    ∃ j ∈ ℕ, ∃ c ∈ ℕ, first = Option.some(Dijkstra.Candidate.value(j, c)) ∧ c ≤ d1920theorem CandidateOrder.none (result : Set)21  shows CandidateOrder(result, Option.none)22proof23  intros i hi d hd equality24  have impossible := Option.inductive.disjoint.none.some at Dijkstra.Candidate.value(i, d)25  exfalso26  exact impossible with equality2728theorem CandidateOrder.reflexive (result : Set)29  shows CandidateOrder(result, result)30proof31  intros i hi d hd equality32  have dNat := nat.omega.backward with hd33  have same := LessEqual.reflexive with dNat34  refine ⟨i, hi, d, hd, equality, same⟩3536theorem CandidateOrder.transitive (a b c : Set)37  requires first : CandidateOrder(a, b)38  requires second : CandidateOrder(b, c)39  shows CandidateOrder(a, c)40proof41  intros i hi d hd equality42  obtain ⟨j, hj, e, he, bValue, ed⟩ := second with i, hi, d, hd, equality43  obtain ⟨k, hk, f, hf, aValue, fe⟩ := first with j, hj, e, he, bValue44  have dNat := nat.omega.backward with hd45  have eNat := nat.omega.backward with he46  have fNat := nat.omega.backward with hf47  have bound := LessEqual.transitive with fNat, eNat, dNat, fe, ed48  refine ⟨k, hk, f, hf, aValue, bound⟩4950theorem CandidateOrder.finite (i d j e : Nat)51  requires order : d ≤ e52  shows CandidateOrder(Option.some(Dijkstra.Candidate.value(i, d)), Option.some(Dijkstra.Candidate.value(j, e)))53proof54  intros k hk c hc equality55  have pair := Option.inductive.injective.some with equality56  have coordinates := Dijkstra.Candidate.inductive.injective.value with pair57  rcases coordinates with ⟨jk, ec⟩58  have iIn := nat.omega.forward at i with assumption59  have dIn := nat.omega.forward at d with assumption60  refine ⟨i, iIn, d, dIn, rfl, _⟩61  rw ← ec62  exact order6364theorem prefer.correct (left right : Set)65  requires leftValid : CandidateOption(left)66  requires rightValid : CandidateOption(right)67  shows CandidateOption(Dijkstra.prefer(left, right)) ∧68    (Dijkstra.prefer(left, right) = left ∨ Dijkstra.prefer(left, right) = right) ∧69    CandidateOrder(Dijkstra.prefer(left, right), left) ∧70    CandidateOrder(Dijkstra.prefer(left, right), right)71proof72  cases leftValid with noLeft | someLeft73  . have same := CandidateOrder.reflexive at right74    have computed : Dijkstra.prefer(left, right) = right75      rw noLeft76      settle with Dijkstra.prefer77    rw computed78    have noBound := CandidateOrder.none at right79    refine ⟨rightValid, _, _, same⟩80    . right81      rfl82    . rw noLeft83      exact noBound84  . rcases someLeft with ⟨i, hi, d, hd, leftValue⟩85    have rightCases := rightValid86    cases rightCases with noRight | someRight87    . have same := CandidateOrder.reflexive at left88      have computed : Dijkstra.prefer(left, right) = left89        rw leftValue90        rw noRight91        settle with Dijkstra.prefer, Dijkstra.preferSome92      rw computed93      have leftShape : CandidateOption(left)94        right95        refine ⟨i, hi, d, hd, leftValue⟩96      refine ⟨leftShape, _, same, _⟩97      . left98        rfl99      . rw noRight100        exact CandidateOrder.none101    . rcases someRight with ⟨j, hj, e, he, rightValue⟩102      have iNat := nat.omega.backward with hi103      have jNat := nat.omega.backward with hj104      have dNat := nat.omega.backward with hd105      have eNat := nat.omega.backward with he106      have typed := Dijkstra.less.boolean with dNat, eNat107      have choices := Dijkstra.boolean_cases with typed108      cases choices with no | yes109      . have order := Dijkstra.less.false_iff.forward at d, e with dNat, eNat, no110        have computed : Dijkstra.prefer(left, right) = right111          rw leftValue112          rw rightValue113          settle with Dijkstra.prefer, Dijkstra.preferSome, Dijkstra.candidateDistance, Dijkstra.select, no114        rw computed115        have rightShape : CandidateOption(right)116          right117          refine ⟨j, hj, e, he, rightValue⟩118        have same := CandidateOrder.reflexive at right119        refine ⟨rightShape, _, _, same⟩120        . right121          rfl122        . rw rightValue123          rw leftValue124          exact CandidateOrder.finite with jNat, eNat, iNat, dNat, order125      . have strict := Dijkstra.less.true_iff.forward at d, e with dNat, eNat, yes126        have order := Less.implies_LessEqual with dNat, eNat, strict127        have computed : Dijkstra.prefer(left, right) = left128          rw leftValue129          rw rightValue130          settle with Dijkstra.prefer, Dijkstra.preferSome, Dijkstra.candidateDistance, Dijkstra.select, yes131        rw computed132        have leftShape : CandidateOption(left)133          right134          refine ⟨i, hi, d, hd, leftValue⟩135        have same := CandidateOrder.reflexive at left136        refine ⟨leftShape, _, same, _⟩137        . left138          rfl139        . rw leftValue140          rw rightValue141          exact CandidateOrder.finite with iNat, dNat, jNat, eNat, order142143predicate MinimumOf (result offers : Set) :=144  CandidateOption(result) ∧ result ∈ offers ∧145  (∀ other ∈ offers, CandidateOrder(result, other))146147theorem MinimumOf.singleton (result : Set)148  requires valid : CandidateOption(result)149  shows MinimumOf(result, {result})150proof151  have member := singleton.self at result152  unfold MinimumOf153  refine ⟨valid, member, _⟩154  intros other inSet155  have equality := singleton.membership.forward with inSet156  rw equality157  exact CandidateOrder.reflexive158159theorem MinimumOf.union (left right A B : Set)160  requires first : MinimumOf(left, A)161  requires second : MinimumOf(right, B)162  shows MinimumOf(Dijkstra.prefer(left, right), A ∪ B)163proof164  rcases first with ⟨leftValid, leftIn, leftLeast⟩165  rcases second with ⟨rightValid, rightIn, rightLeast⟩166  obtain ⟨valid, selected, leLeft, leRight⟩ := prefer.correct with leftValid, rightValid167  unfold MinimumOf168  refine ⟨valid, _, _⟩169  . cases selected with chooseLeft | chooseRight170    . rw chooseLeft171      exact union2.left with leftIn172    . rw chooseRight173      exact union2.right with rightIn174  . intros other inUnion175    have alternatives := union2.membership.forward with inUnion176    cases alternatives with inA | inB177    . have bound := leftLeast with other, inA178      exact CandidateOrder.transitive with leLeft, bound179    . have bound := rightLeast with other, inB180      exact CandidateOrder.transitive with leRight, bound181182183theorem equalNat.boolean (a b : Nat)184  shows Bool(equalNat(a, b))185proof186  exact Grace.Cumulus.Nat.Mod.equalNat.boolean at a, b with *187188theorem boolHead.natural (flags : List(ℕ))189  shows Nat(Dijkstra.boolHead(flags))190proof191  induction flags192  | List.nil =>193    have computed : Dijkstra.boolHead(List.nil) = 1 by simp [Dijkstra.boolHead]194    rw computed195    typecheck196  | List.cons(flag, rest) using ih =>197    have computed : Dijkstra.boolHead(List.cons(flag, rest)) = flag by simp [Dijkstra.boolHead]198    rw computed199    typecheck200201theorem boolTail.closed (flags : List(ℕ))202  shows List(ℕ, Dijkstra.boolTail(flags))203proof204  induction flags205  | List.nil =>206    have computed : Dijkstra.boolTail(List.nil) = List.nil by simp [Dijkstra.boolTail]207    rw computed208    exact List.inductive.constructor.nil209  | List.cons(flag, rest) using ih =>210    have computed : Dijkstra.boolTail(List.cons(flag, rest)) = rest by simp [Dijkstra.boolTail]211    rwa computed212213theorem available.valid (distance : Option(ℕ), index : Nat, flag : Bool)214  shows CandidateOption(Dijkstra.available(flag, distance, index))215proof216  induction flag217  | Bool.true =>218    left219    settle with Dijkstra.available220  | Bool.false =>221    have shape := Dijkstra.option_cases at distance with assumption222    cases shape with absent | present223      left224      rw absent225      settle with Dijkstra.available, Dijkstra.availableOpen226    . rcases present with ⟨d, hd, equality⟩227      have indexIn := nat.omega.forward at index with assumption228      right229      refine ⟨index, indexIn, d, hd, _⟩230      rw equality231      settle with Dijkstra.available, Dijkstra.availableOpen232233-- A is a set of cells. The theorem below requires each of its234-- members to be an optional natural, without treating a class as a set.235def scanOffers {A : Set} (distances : List(A), flags : List(ℕ), index : Nat) → Set236  | List.nil, flags, index => {Option.none}237  | List.cons(d, rest), flags, index =>238    {Dijkstra.available(equalNat(Dijkstra.boolHead(flags), 1), d, index)} ∪239      scanOffers(rest, Dijkstra.boolTail(flags), succ(index))240  descends distances241242theorem minimum.correct (A : Set, distances : List(A), flags : List(ℕ), index : Nat)243  requires cells : ∀ d ∈ A, Option(ℕ, d)244  shows MinimumOf(Dijkstra.minimum(distances, flags, index), scanOffers{A := A}(distances, flags, index))245proof246  induction distances generalizing flags index247  | List.nil =>248    intros flags index flagsType indexNat249    have valid : CandidateOption(Option.none)250      left251      rfl252    have initial := MinimumOf.singleton with valid253    simp [Dijkstra.minimum, scanOffers]254  | List.cons(d, rest) using ih =>255    intros flags index flagsType indexNat256    have dType := cells with d, assumption257    have headNat := boolHead.natural with flagsType258    have tailType := boolTail.closed with flagsType259    have condition := equalNat.boolean at Dijkstra.boolHead(flags), 1 with headNat, assumption260    have nextNat := Naturals.constructor.succ with indexNat261    have valid := available.valid with dType, indexNat262    have first := MinimumOf.singleton with valid263    have second := ih with Dijkstra.boolTail(flags), succ(index), tailType, nextNat264    have merged := MinimumOf.union with first, second265    simp [Dijkstra.minimum, scanOffers]266267268theorem MinimumOf.none_iff (result offers : Set)269  requires minimum : MinimumOf(result, offers)270  shows result = Option.none ↔271    (∀ i ∈ ℕ, ∀ d ∈ ℕ, ¬(Option.some(Dijkstra.Candidate.value(i, d)) ∈ offers))272proof273  rcases minimum with ⟨valid, member, least⟩274  constructor275  . intros absent i hi d hd offered276    have order := least with Option.some(Dijkstra.Candidate.value(i, d)), offered277    have itself : Option.some(Dijkstra.Candidate.value(i, d)) = Option.some(Dijkstra.Candidate.value(i, d)) by rfl278    obtain ⟨j, hj, c, hc, equality, bound⟩ := order with i, hi, d, hd, itself279    rw absent at equality280    have impossible := Option.inductive.disjoint.none.some at Dijkstra.Candidate.value(j, c)281    exact impossible with equality282  . intro noFinite283    cases valid with absent | finite284    . exact absent285    . rcases finite with ⟨fi, hfi, fd, hfd, finiteEquality⟩286      have notOffered := noFinite with fi, hfi, fd, hfd287      rw finiteEquality at member288      exfalso289      exact notOffered with member290291theorem minimum.none_iff (A : Set, distances : List(A), flags : List(ℕ), index : Nat)292  requires cells : ∀ d ∈ A, Option(ℕ, d)293  shows Dijkstra.minimum(distances, flags, index) = Option.none ↔294    (∀ i ∈ ℕ, ∀ d ∈ ℕ, ¬(Option.some(Dijkstra.Candidate.value(i, d)) ∈ scanOffers{A := A}(distances, flags, index)))295proof296  have correct := minimum.correct with *297  exact MinimumOf.none_iff with correct298299theorem minimum.le_every_offer (A : Set, distances : List(A), flags : List(ℕ), index i d : Nat)300  requires cells : ∀ value ∈ A, Option(ℕ, value)301  requires offered : Option.some(Dijkstra.Candidate.value(i, d)) ∈ scanOffers{A := A}(distances, flags, index)302  shows ∃ j ∈ ℕ, ∃ c ∈ ℕ,303    Dijkstra.minimum(distances, flags, index) = Option.some(Dijkstra.Candidate.value(j, c)) ∧ c ≤ d304proof305  have correct := minimum.correct at A, distances, flags, index with *306  rcases correct with ⟨valid, member, least⟩307  have bound := least with Option.some(Dijkstra.Candidate.value(i, d)), offered308  have iIn := nat.omega.forward at i with assumption309  have dIn := nat.omega.forward at d with assumption310  have same : Option.some(Dijkstra.Candidate.value(i, d)) = Option.some(Dijkstra.Candidate.value(i, d)) by rfl311  exact bound with i, iIn, d, dIn, same312313end Dijkstra314