FiniteDirectedBFS.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Deterministic directed breadth-first search

Each round retains every discovered path and scans the vertex list for one predecessor of each undiscovered vertex. There is one stored path per vertex; the search does not enumerate candidate paths.

inductive OAI.ContingencyTables.FiniteDirectedBFS.Route line 20

Source documentation

A directed walk, including its two endpoints.

inductive Route (E : Fin n → Fin n → Bool) (s : Fin n) :
    Fin n → List (Fin n) → Prop
  | start : Route E s s [s]
  | extend {u v xs} : Route E s u xs → E u v=true → Route E s v (xs++[v])

namespace Route

variable {E : Fin n → Fin n → Bool} {s v : Fin n} {xs : List (Fin n)}

theorem OAI.ContingencyTables.FiniteDirectedBFS.Route.nonempty line 29
theorem OAI.ContingencyTables.FiniteDirectedBFS.Route.length_pos line 32
theorem OAI.ContingencyTables.FiniteDirectedBFS.Route.head line 35
theorem OAI.ContingencyTables.FiniteDirectedBFS.Route.last line 42
theorem OAI.ContingencyTables.FiniteDirectedBFS.Route.chain line 45
theorem OAI.ContingencyTables.FiniteDirectedBFS.Route.routePrefix line 53
Source documentation
Every visited vertex has a prefix walk no longer than the whole walk.
```
theorem routePrefix (h : Route E s v xs) {w : Fin n} (hw : w∈xs) :
    ∃ ys, Route E s w ys ∧ ys.length≤xs.length := by
…
```
Mentions: OAI.ContingencyTables.FiniteDirectedBFS.Route
abbrev OAI.ContingencyTables.FiniteDirectedBFS.Paths line 70
def OAI.ContingencyTables.FiniteDirectedBFS.discovered line 72
def OAI.ContingencyTables.FiniteDirectedBFS.predecessor line 74
def OAI.ContingencyTables.FiniteDirectedBFS.round line 78
def OAI.ContingencyTables.FiniteDirectedBFS.paths line 84
lemma OAI.ContingencyTables.FiniteDirectedBFS.predecessor_some line 88
lemma OAI.ContingencyTables.FiniteDirectedBFS.predecessor_none line 95
lemma OAI.ContingencyTables.FiniteDirectedBFS.round_retains line 104
lemma OAI.ContingencyTables.FiniteDirectedBFS.round_discovered line 108
theorem OAI.ContingencyTables.FiniteDirectedBFS.paths_sound line 132
theorem OAI.ContingencyTables.FiniteDirectedBFS.route_discovered line 163
theorem OAI.ContingencyTables.FiniteDirectedBFS.paths_shortest line 182
theorem OAI.ContingencyTables.FiniteDirectedBFS.paths_nodup line 204
theorem OAI.ContingencyTables.FiniteDirectedBFS.paths_length_le line 241
theorem OAI.ContingencyTables.FiniteDirectedBFS.route_found line 247
Source documentation
Every directed walk is found within n rounds. The proof uses the short simple path stored by the search, rather than enumerating walks.
```
theorem route_found {E : Fin n → Fin n → Bool} {s v : Fin n}
    {xs : List (Fin n)} (h : Route E s v xs) :
    discovered (paths E s n) v := by
…
```
Mentions: OAI.ContingencyTables.FiniteDirectedBFS.Route, OAI.ContingencyTables.FiniteDirectedBFS.discovered, OAI.ContingencyTables.FiniteDirectedBFS.paths
theorem OAI.ContingencyTables.FiniteDirectedBFS.paths_complete line 254
theorem OAI.ContingencyTables.FiniteDirectedBFS.source_found line 264
Source documentation
The computed reached set contains the source and is closed under every directed edge. This is the cut certificate used on failure.
```
theorem source_found (E : Fin n → Fin n → Bool) (s : Fin n) :
    discovered (paths E s n) s := route_found Route.start
```
Mentions: OAI.ContingencyTables.FiniteDirectedBFS.discovered, OAI.ContingencyTables.FiniteDirectedBFS.paths, OAI.ContingencyTables.FiniteDirectedBFS.route_found
theorem OAI.ContingencyTables.FiniteDirectedBFS.reached_closed line 267
theorem OAI.ContingencyTables.FiniteDirectedBFS.failure_no_route line 273