Zulip Chat Archive

Stream: graph theory

Topic: cycles


view this post on Zulip Julian Berman (Oct 23 2020 at 23:09):

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?

view this post on Zulip Julian Berman (Oct 23 2020 at 23:12):

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.

view this post on Zulip Kyle Miller (Oct 24 2020 at 01:05):

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.

view this post on Zulip Kyle Miller (Oct 24 2020 at 01:06):

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)

view this post on Zulip Kyle Miller (Oct 24 2020 at 01:12):

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

view this post on Zulip Julian Berman (Oct 24 2020 at 02:31):

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


Last updated: May 08 2021 at 21:09 UTC