cycles

Stream: graph theory

[Julian Berman]

Hi! (new user to the stream and mostly in general). I want to exhibit a (finite) directed graph and prove it's a cycle, and then prove a thing or two about paths on it. Is this possibly a reasonable thing to attempt given any of the graph theory code that's been written? I see most of the code is likely on graph-theory-related branches of mathlib right?

[Julian Berman]

Oh, also -- I should mention by "exhibit" I mean "I have a function from X \to (set X)", so I want to get my graph by inducing it from that function.

[Kyle Miller]

We don't have directed graphs yet -- most energy has been put into simple graphs because of some basic complications to them that needed solving.

One thing about directed graphs without multiedges is that they're essentially just relations (indeed, X -> set X is equivalent to X -> X -> Prop), so you might get a lot of mileage out of what mathlib already has about those. For example, paths correspond the transitive closure of the relation.

[Kyle Miller]

Because of this, directed graphs will probably be with multiple edges, something like

structure dgraph_on (V : Type*) :=
(E : Type*)
(s : E → V)
(t : E → V)

[Kyle Miller]

https://leanprover-community.github.io/mathlib_docs/logic/relation.html#relation.refl_trans_gen

[Julian Berman]

Aha, thanks! That looks like a great breadcrumb, will have a look.