Splitting `Walk.lean`

Stream: graph theory

[Snir Broshi]

It's about time to split Walk.lean as it's one of the longest files in Mathlib.
Thoughts on how?

We can do Walks/Defs.lean and Walks/Basic.lean, but this kinda hurts definitions which rely on theorems.

Here's my suggestion:

• Basic.lean just for the basic definitions and theorems about them, without modifying the walks: Walk, Nil, length, getVert, support, darts, edges, edgeSet, snd, penultimate, firstDart, lastDart
• WalkDecomp.lean: this is an existing file that should be moved into the new Walks folder. it defines takeUntil, dropUntil, rotate
• Operations.lean: similar to the existing WalkDecomp.lean, this will define operations on walks: copy, append, concat, reverse, take, drop, tail, dropLast. The name of the file matches SimpleGraph/Operations.lean which defines operations on graphs.
• Maps.lean: Operations that map the walk to another graph: map, mapLe, transfer, induce, toDeleteEdges, toDeleteEdge. The name of the file matches SimpleGraph/Maps.lean which defines similar maps on graphs.
• Subwalks.lean: the definition of IsSubwalk and theorems about it
• Paths.lean: this is an existing file that should be moved into the new Walks folder. it defines types of walks: trails, circuits, cycles. I also suggest renaming it, maybe to Kinds.lean or Types.lean or Predicates.lean.

Wdyt?

[Bryan Gin-ge Chen]

Since no one else has commented: let me say that having seen this file drift back and forth across the long file linter limit multiple times, I am very glad that you've started work on this and would happy to approve almost any reasonable split. I would recommend moving / renaming Paths.lean in a separate PR from the one that splits Walk.lean though.

[Snir Broshi]

Split PR #31573

[Shreyas Srinivas]

Can we actually define Walk on Subgraphs in general and specialize it to a graph later. I am beginning to find in my Berge lemma formalisation that defining everything on subgraphs is way more convenient.

[Shreyas Srinivas]

The idea is that when you want to talk about a simple graph, you just talk about its trivial subgraph (every edge and vertex included)

[Snir Broshi]

Shreyas Srinivas said:

The idea is that when you want to talk about a simple graph, you just talk about its trivial subgraph (every edge and vertex included)

Is it related to the topic? In general I agree that subgraphs vs regular graphs are awkward, but maybe moving to docs#Graph is the solution (and deprecating SimpleGraph). Knowing that two graphs have the same vertex set is probably not necessary for most theorems, so SimpleGraph should be the special case rather than the main API

[Shreyas Srinivas]

I was hoping we could have a subgraph definition of walk

[Shreyas Srinivas]

and use my suggestion to extend it to graphs

[Snir Broshi]

Can you create another thread to discuss it?

[John Talbot]

I just had look through #31573 and the split looks very sensible to me.

You mention also possibly splitting off the getVert material from Basic.lean and I think that would be great too!

[Bryan Gin-ge Chen]

Leaving a comment like that as a review on the PR would be appreciated!

[Snir Broshi]

Walk is now split :tada:
(sorry for the merge conflicts)