Termination of BFS

Stream: new members

[Philipp]

I was doing some Advent of Code to learn Lean (horrible code here: https://github.com/klockeph/AdventOfCode2023; I definitely see improvement over the days, whenever I found better (syntax) features).

So one recurring pattern is a kind of BFS over a 2D map (List (List Char)). I was usually too lazy to parse that as a graph; instead I implemented a function getNext (Nat * Nat) -> List (Nat * Nat) that returned all valid neighbors.

I repeated myself quite often (https://github.com/klockeph/AdventOfCode2023/blob/main/AdventOfCode/Day10.lean#L64, https://github.com/klockeph/AdventOfCode2023/blob/main/AdventOfCode/Day16.lean#L74 to name two)... and while I could fix that by hardcoding less and making e.g. getNext an argument of bfs, the main thing that bothers me is the partial.

How would I prove termination of bfs over a finite graph? One idea I had is using Fin * Fin as positions; would that be enough?
Another idea would be having a HashSet of all nodes and removing visited ones, instead of adding; then that HashSet is always decreasing (or empty). But it would require a pass over the Graph beforehand.

So what is the standard way of implementing bfs and proving that it terminates?