Proving: Decidable (g.Reachable v0 v1)

Stream: graph theory

[Owen Randall]

Hello!
Hoping to get some advice/guidance on how to prove that checking whether one vertex is reachable from another is Decidable.

instance decidable_reachable {V} [Fintype V] [DecidableEq V] {g : SimpleGraph V} {v0 v1 : V} : Decidable (g.Reachable v0 v1) := by
  sorry

Specifically how to do this without using Classical.dec which trivializes the problem, but makes it non-computable.
I.e. I would like to be able to get an answer from #eval g.Reachable v0 v1.
I have been able to rely on 'deriving' to get my Decidable instances so far, so apologies if there is an obvious answer but I don't have much experience with Decidable proofs.

[Kyle Miller]

Mathlib has this as docs#SimpleGraph.instDecidableRelReachable, but it needs DecidableRel g.Adj

[Kyle Miller]

It's an algorithm, but it's not a good one. It enumerates all walks up to a particular length (I think the number of vertices minus one).

[Kyle Miller]

It would be better if it did a real graph algorithm like BFS if you're wanting to evaluate it.

[Kyle Miller]

By the way, DecidableRel g.Adj is saying that there is a boolean function V -> V -> Bool that implements the adjacency relation for the graph. To decide whether two vertices are reachable from one another, certainly you need to be able to compute the adjacency relation, which is why it makes sense you would need this additional piece of data.

[Owen Randall]

Perfect, that's what I was looking for, thank you!
I skimmed through that connectivity file already but must have missed that, probably could have searched a little harder but I mistakenly assumed it would have shown up as an existing instance if it was already implemented.