Decidable whether there is cycle in directed graph?

Stream: mathlib4

[aron]

Hi :wave: I've been playing with Lean for a while now although I have mostly not touched anything in Mathlib. Most of the stuff in there is quite intimidating to me, probably because I am not a mathematician :sweat_smile:

The project I'm working on entails something that is effectively a directed graph, on which I want to be able to check whether it contains cycles. I can model the prop for "there are no cycles starting from this point" using an inductive. But actually writing a function that returns a Decidable for it is turning out to be really really hard. I'm wondering if there is anything already in Mathlib that could help me?

I posted my original question here #new members > How to decide no loops in list of references but the key parts of it are:

inductive LeafOrRef
  | leaf : LeafOrRef
  | ref : Nat → LeafOrRef
  deriving DecidableEq, BEq


/-- Proves that `i` is not contained in `lor` or any of the items it points to.
This prop also contains proofs for any refs we find along the way, so it indeed
proves not only that `i` isn't contained along the paths, but there are no
loops anywhere along the path. -/
inductive NoLoop (list : List LeafOrRef) : (i : Nat) → (lor : LeafOrRef) → Prop
  | leaf : NoLoop list i .leaf

  | ref {prf : j < list.length} :
    i ≠ j →
    NoLoop list i list[j] → -- doesn't contain the ref that this thing is about
    NoLoop list j list[j] → -- also doesn't contain the current ref, recursively
    NoLoop list i (.ref j)


/-- How to implement this -/
def NoLoop.decide list i lor : Decidable (NoLoop list i lor) := by
  sorry

[aron]

I've also tried with the opposite approach, hoping it would be easier:

inductive Walk (list : List LeafOrRef) : (origin : Nat) → (dest : Nat) → Prop
  | direct {prf} :
    list[origin]'prf = .ref dest → -- if `origin` and `dest` are the same then the thing directly references itself
    Walk list origin dest

  | indirect :
    (walk₁ : Walk list a b) →
    (walk₂ : Walk list b c) →
    Walk list a c

but although this does make some things easier, I haven't had any more luck implementing a function that returns Decidable (Walk ctx origin dest) than I've had with NoLoop

[Tomaz Mascarenhas]

(deleted)