## Stream: graph theory

### Topic: walks

#### Alena Gusakov (Feb 22 2021 at 23:46):

Why not define walks as lists with a chain constraint? Then you get lots of defns and lemmas for free

#### Alena Gusakov (Feb 22 2021 at 23:47):

@Yakov Pechersky what do you mean by this exactly?

#### Yakov Pechersky (Feb 22 2021 at 23:50):

Something like a structure that takes a g : graph V, start : V, seq : list V, with the constraint that seq.chain start g.adj

#### Yakov Pechersky (Feb 22 2021 at 23:51):

Then for a path, you say nodup (start :: seq) or something like that

#### Yakov Pechersky (Feb 22 2021 at 23:51):

I just started reading Bollobas (Bhavik suggested it), so these could be very naive questions

#### Alena Gusakov (Feb 23 2021 at 00:01):

I haven't tried using the chain API so I'm not really sure! I'll have to try it at some point

#### Alena Gusakov (Feb 23 2021 at 00:02):

Didn't know it existed tbh

#### Yakov Pechersky (Feb 23 2021 at 00:12):

Then cycles are a constraint that is like (∀ h : seq ≠ []), seq.last h ≠ start

#### Yakov Pechersky (Feb 23 2021 at 00:13):

That would be is_cycle

#### Alena Gusakov (Feb 23 2021 at 00:14):

Could also take advantage of list defs too, like count

#### Alena Gusakov (Feb 23 2021 at 00:15):

Which is super convenient

#### Bhavik Mehta (Feb 23 2021 at 00:17):

Ah I mentioned this a while ago - iirc the problem with that is that it doesn't generalise nicely to labelled graphs

#### Bhavik Mehta (Feb 23 2021 at 00:18):

Probably @Kyle Miller can be more helpful

#### Alena Gusakov (Feb 23 2021 at 00:20):

Wacky idea but what if we also used chains to describe walks in labelled graphs where incidence between edges is the relation instead of adjacency

#### Alena Gusakov (Feb 23 2021 at 00:21):

That would fit into the design choice of treating edges as their own objects (useful for matroids)

#### Alena Gusakov (Feb 23 2021 at 00:31):

Suppose edges are defined as sets of vertices, that would allow for things like hypergraphs eventually too

#### Yakov Pechersky (Feb 23 2021 at 00:48):

Can't labeled graphs be done with sigma types?

#### Bhavik Mehta (Feb 23 2021 at 00:55):

But for labelled multigraphs, you'll end up with some heterogeneous list type, at which point you might as well use the inductive type Kyle suggested in the first place

#### Kyle Miller (Feb 23 2021 at 01:20):

@Yakov Pechersky If you think that structure would be better, I'd suggest trying to prove that if two vertices are connected by a walk, then they are also connected by a path. That module I wrote was primarily to work out how to do that in as clean a way as I knew how.

There are a couple nice properties about that definition. The first is that it gives a category of walks on the graph. The second is that the definition of a path involves defining the support, which seems like it would be a useful finset to have around anyway.

#### Kyle Miller (Feb 23 2021 at 01:23):

It seems like it could be useful taking the inductive type I wrote and generalize it to arbitrary relations, then specialize it for simple graphs. I think there's still a walk->path result in the general case.

#### Kyle Miller (Feb 23 2021 at 01:30):

Actually, rather than generalizing it to relations, it might be nice to generalize it to directed multigraphs (i.e., "relations" of type a -> a -> Sort*)

#### Alena Gusakov (Feb 23 2021 at 02:02):

I haven't tried using the chain API so I'm not really sure! I'll have to try it at some point

#### Kyle Miller (Feb 24 2021 at 19:13):

I forgot to mention that my code for walks was mostly based on https://github.com/leanprover-community/mathlib/blob/hedetniemi/src/graph_theory/paths.lean

#### Yakov Pechersky (Feb 24 2021 at 19:14):

I'm testing it out right now, adding a lot of walk API that probably isn't really needed. There's missing list.chain API to do so that would be nice to have anyway. Thanks for the pointer.

#### Yakov Pechersky (Feb 24 2021 at 19:15):

An example of what I have right now:

@[simp] lemma last_coe (G : simple_graph V) (v : V) :
(v : G.walk).last = v := rfl


Last updated: May 08 2021 at 22:13 UTC