Grace/Cumulus/GraphTheory/DijkstraFlags.g17

Open in Workbench Download source

Imports

DijkstraVectors

Declarations

• flagAt.nil theorem derivation
• mark.nil theorem derivation
• mark.closed theorem derivation
• mark.length theorem derivation
• mark.at_same theorem derivation
• mark.at_other theorem derivation

Source

1-- Flag-vector semantics for Dijkstra's executable loop.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.DijkstraFlags8import DijkstraVectors910namespace Dijkstra111213theorem flagAt.nil (index : Nat)14  shows Dijkstra.flagAt(List.nil, index) = 115proof16  induction index17  | zero =>18    simp19  | succ(k) using ih =>20    simp [Dijkstra.flagAt, Dijkstra.boolTail]2122theorem mark.nil (index : Nat)23  shows Dijkstra.mark(List.nil, index) = List.nil24proof25  induction index26  | zero =>27    simp28  | succ(k) using ih =>29    simp [Dijkstra.mark, Dijkstra.keepHead]3031theorem mark.closed (index : Nat, flags : List(ℕ))32  shows List(ℕ, Dijkstra.mark(flags, index))33proof34  induction index generalizing flags35  | zero =>36    intros flags flagsType37    have shape := Dijkstra.list_cases with flagsType38    cases shape with empty | cons39    . rw empty40      have computed := mark.nil with Naturals.constructor.zero41      rw computed42      exact List.inductive.constructor.nil43    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩44      have oneIn := nat.omega.forward at 1 with assumption45      have constructed := List.inductive.constructor.cons with oneIn, tailType46      have computed : Dijkstra.mark(List.cons(head, tail), 0) = List.cons(1, tail)47        settle with Dijkstra.mark, Dijkstra.markHead48      rw equality49      rw computed50      exact constructed51  | succ(k) using ih =>52    intros flags flagsType53    have shape := Dijkstra.list_cases with flagsType54    cases shape with empty | cons55    . rw empty56      have skNat : Nat(succ(k)) by typecheck57      have computed := mark.nil with skNat58      rw computed59      exact List.inductive.constructor.nil60    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩61      have previous := ih with tail, tailType62      have constructed := List.inductive.constructor.cons with headIn, previous63      have computed : Dijkstra.mark(List.cons(head, tail), succ(k)) = List.cons(head, Dijkstra.mark(tail, k))64        settle with Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolTail65      rw equality66      rw computed67      exact constructed6869theorem mark.length (index : Nat, flags : List(ℕ))70  shows ListOps.length{A := ℕ}(Dijkstra.mark(flags, index)) = ListOps.length{A := ℕ}(flags)71proof72  induction index generalizing flags73  | zero =>74    intros flags flagsType75    have shape := Dijkstra.list_cases with flagsType76    cases shape with empty | cons77    . rw empty78      have computed := mark.nil with Naturals.constructor.zero79      rw computed80      rfl81    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩82      rw equality83      simp [Dijkstra.mark, Dijkstra.markHead, ListOps.length]84  | succ(k) using ih =>85    intros flags flagsType86    have shape := Dijkstra.list_cases with flagsType87    cases shape with empty | cons88    . rw empty89      have skNat : Nat(succ(k)) by typecheck90      have computed := mark.nil with skNat91      rw computed92      rfl93    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩94      have previous := ih with tail, tailType95      rw equality96      simp [Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolTail, ListOps.length]9798theorem mark.at_same (index : Nat, flags : List(ℕ))99  shows Dijkstra.flagAt(Dijkstra.mark(flags, index), index) = 1100proof101  induction index generalizing flags102  | zero =>103    intros flags flagsType104    have shape := Dijkstra.list_cases with flagsType105    cases shape with empty | cons106    . rw empty107      simp108    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩109      rw equality110      simp [Dijkstra.mark, Dijkstra.markHead, Dijkstra.flagAt, Dijkstra.boolHead]111  | succ(k) using ih =>112    intros flags flagsType113    have shape := Dijkstra.list_cases with flagsType114    cases shape with empty | cons115    . rw empty116      have skNat : Nat(succ(k)) by typecheck117      have computed := mark.nil with skNat118      rw computed119      exact flagAt.nil with skNat120    . rcases cons with ⟨head, headIn, tail, tailType, equality⟩121      have previous := ih with tail, tailType122      rw equality123      simp [Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolTail, Dijkstra.flagAt]124125theorem mark.at_other (index target : Nat, flags : List(ℕ))126  requires distinct : target ≠ index127  shows Dijkstra.flagAt(Dijkstra.mark(flags, index), target) = Dijkstra.flagAt(flags, target)128proof129  induction index generalizing target flags130  | zero =>131    intros target flags targetNat flagsType distinct132    have targetShape := natural.zero_or_successor with targetNat133    cases targetShape with targetZero | targetNext134    . exfalso135      exact distinct with targetZero136    . rcases targetNext with ⟨j, jNat, targetEquality⟩137      have flagsShape := Dijkstra.list_cases with flagsType138      cases flagsShape with empty | cons139      . rw empty140        have computed := mark.nil with Naturals.constructor.zero141        rw computed142        rfl143      . rcases cons with ⟨head, headIn, tail, tailType, flagsEquality⟩144        rw flagsEquality145        rw targetEquality146        settle with Dijkstra.mark, Dijkstra.markHead, Dijkstra.flagAt, Dijkstra.boolTail147  | succ(k) using ih =>148    intros target flags targetNat flagsType distinct149    have skNat : Nat(succ(k)) by typecheck150    have flagsShape := Dijkstra.list_cases with flagsType151    cases flagsShape with empty | cons152    . rw empty153      have computed := mark.nil with skNat154      rw computed155      rfl156    . rcases cons with ⟨head, headIn, tail, tailType, flagsEquality⟩157      have targetShape := natural.zero_or_successor with targetNat158      cases targetShape with targetZero | targetNext159      . rw flagsEquality160        rw targetZero161        settle with Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolHead, Dijkstra.flagAt162      . rcases targetNext with ⟨j, jNat, targetEquality⟩163        have smallerDistinct : j ≠ k164          intro same165          apply distinct166          rw targetEquality167          rw same168          rfl169        have previous := ih with j, tail, jNat, tailType, smallerDistinct170        rw flagsEquality171        rw targetEquality172        simp [Dijkstra.mark, Dijkstra.keepHead, Dijkstra.boolTail, Dijkstra.flagAt]173174end Dijkstra175