SimpleGraph sub-walks

Stream: graph theory

[Vlad Tsyrklevich]

I haven't touched SimpleGraph in a bit but if I recall correctly there is no standard way of encoding that one walk is a sub-walk of another? I'm not sure if this was previously discussed, searching "subwalk" doesn't get many results. There are many equivalent formulations for sub-paths, for sub-walks I'm not sure off the top of my head what the right formulation should be.

[Rida Hamadani]

I needed this in #25834 and used support.Sublist, also see if the lemmas you need are in that PR and feel free to use them in separate PRs, just lmk so I make my PR depends on yours

[Shreyas Srinivas]

Basically you express both walks as subgraphs (there is a conversion function for this).

[Shreyas Srinivas]

subgraphs of the same SimpleGraph

[Shreyas Srinivas]

And then you declare that one subgraph is a subgraph of the other

[Shreyas Srinivas]

that sounds a bit round about, but you get the edge and vertex subset relations out of it

[Shreyas Srinivas]

(Aside : I would also suggest working on an extended definition of SimpleGraph that includes a vertex set and containment relations for vertices and incident edges.)

[Shreyas Srinivas]

The reason I prefer this representation is because it immediately helps me connect to other notions defined on subgraphs and simplegraphs like connectivity, matching, reachability etc.

[Rida Hamadani]

I ended up doing #26614 which proves some "sub-walk" lemmas related to take/drop.
Do people think its worth it having a subwalk definition in math? It might be a good idea if we will have more such lemmas.

[Rida Hamadani]

@Shreyas Srinivas honestly I don't think that approach is good because if you are talking about sub-walks, you are mostly interested in properties of walks instead of properties of subgraphs, so for example IsPath, IsCycle, etc, these are usually stated in terms of the support.

[Rida Hamadani]

Two candidate definitions are p.support.Sublist q.support, or using a new inductive type analogous to Sublist.
The advantage of the first definition is that we get properties such as IsPath from a subwalk of an IsPath immediately.
@Kyle Miller what do you think is the correct approach here?

[Vlad Tsyrklevich]

I think having a predicate would be nice. It feels like we are already trying to do this in a number of places, e.g. docs#SimpleGraph.Walk.support_takeUntil_subset and the following ~9 lemmas are really saying (p.dropUntil ...).IsSubwalk p and (p.takeUntil ...).IsSubwalk p and the statements about support/edges/darts/length are just properties of sub-walk.

Then things like docs#SimpleGraph.Walk.IsPath.of_append_left or the IsTrail equivalent can be stated for subwalks, and it's easier to use that then possibly finding a decomposition of your Path into two pieces to pass into such a lemma. Also docs#SimpleGraph.Walk.IsTrail.dropUntil and the take/Path equivalents are really again about subwalks.

[Kyle Miller]

@Rida Hamadani Using the support definition sounds reasonable to me. Custom inductively-defined predicates require some extra work to make sure they're actually encoding what you think they do. I like definitions that are 'obviously' correct.

Another reasonable definition would be that p.IsSubwalk q is defined to be

import Mathlib

variable {V : Type*} {G : SimpleGraph V}

def SimpleGraph.Walk.IsSubwalk {u v u' v' : V} (p : G.Walk u v) (q : G.Walk u' v') : Prop :=
  ∃ (ru : G.Walk u' u) (rv : G.Walk v v'), q = (ru.append p).append rv

In any case, so long as we have a theorem that states that the definition is equivalent to this, then we are good.

[Kyle Miller]

Oh, nevermind, I got the "obvious" definition wrong :-)

[Kyle Miller]

I wasn't thinking about a subwalk as being a walk that's a subgraph of another walk. I think we need theorems that use the concept to motivate how this should be formalized.

[Kyle Miller]

Possible variants of the subwalk concept:

• what I wrote, that p is derived from q by removing some prefix and suffix
• what Rida wrote, that p visits some possibly non-contiguous subsequence of vertices of q in order (note: it's possible that p will have edges that q doesn't!)
• a definition where p is a subgraph of q (note: p might visit vertices and edges in a different order, or in reverse!)

[Vlad Tsyrklevich]

Neither was I, and I thought Rida wasn't either though I just realized List.Sublist is for non-contiguous sub-lists. I thought we were talking about the first case.

[Vlad Tsyrklevich]

(The exact formulation Kyle used is exactly the case I needed for the lemma which inspired me to ask, though I thought it was too ugly to be a hypothesis and should really be a predicate, the definition of which is unimportant as long as there's an ext lemma for that walk decomposition.)

[Yakov Pechersky]

The list predicate is docs#List.IsInfix then

[Rida Hamadani]

I thought it is okay for a subwalks to contain non-contiguous sublist, but rethinking this, not including them is probably better. p.support.IsInfix q.support would be useful to have (so we can use docs#List.IsInfix.sublist immediately), perhaps as the definition or as a lemma saying that it is equivalent to Kyle's first point.

[Kyle Miller]

(Sublists would admit the following: consider a triangle graph ABC and the walk q from A to B to C. If p is the walk from A to C, then it would be a subwalk of q. )

[Rida Hamadani]

I used Kyle's first definition in #26655 and then proved that it is equivalent to p.support.IsInfix q.support, but the proof is so unnecessarily big right now, if anybody has ideas to make it smaller please lmk!

[John Talbot]

Following up on some discussion from #26655 about what to call contiguous subwalks / non-contiguous subwalks.
I don't have a strong opinon about exactly what to call contiguous subwalks, (e.g. Walk.IsInfix or IsContiguous etc..) but it might be good to reserve Walk.Subwalk for not-necessarily contiguous subwalks? (The only obvious example of such a non-contiguous subwalk currently in Mathlib would be Walk.bypass but they are pretty natural.)

/-- `p.Subwalk q` if `p` is a (not necessarily contiguous) subwalk of `q`
(This definition is modelled on `List.Sublist`.) -/
inductive Subwalk {V : Type*} {G : SimpleGraph V} : ∀ {u v x y}, G.Walk u v → G.Walk x y → Prop
  /-- The nil walk `u` is a Subwalk of any `u - v` walk. -/
  | nil {u v : V} {q : G.Walk u v} : (Walk.nil' u).Subwalk q
  /-- If `p` is a Subwalk of `q`, then it is also a Subwalk of `q.cons h`. -/
  | cons {u v x y z : V} {p : G.Walk u v} {q : G.Walk x y} (h : G.Adj z x) :
      p.Subwalk q → p.Subwalk (q.cons h)
  /-- If `p` is a Subwalk of `q`, then `p.cons h` is a Subwalk of `q.cons h`. -/
  | cons₂ {u v y z : V} {p : G.Walk u v} {q : G.Walk u y} (h : G.Adj z u) :
      p.Subwalk q → (p.cons h).Subwalk (q.cons h)

[Vlad Tsyrklevich]

I don’t like naming it Infix just because I myself never remember List.Infix, I have to hover over <:+: to remember it. So I think something with subwalk and contiguous or something that’s more directly descriptive seems better to me, but I don’t feel too strongly about it

[Rida Hamadani]

One reason I'm hesitant to reserve the name "subwalks" for non-contiguous subwalks is that they do not contain the edges of the walk.

[Vlad Tsyrklevich]

Perhaps we’re talking about different things, but my model is that they do contain a subset. If a walks support is (v1, v2, v3, v4, v2, v5) a non contiguous sub walk would be (v1, v2, v5) and all those edges are in the original walk

[Rida Hamadani]

I was thinking about something more along the lines of the previously proposed p.support.IsSublist q.support definition.

[Rida Hamadani]

But in the case where its a non-contiguous sub-walk that contains the edges, we can name it something like IsBypass, although honestly I cannot think of cases where this will be useful other than Walk.bypass.

[John Talbot]

I think there will be more examples. For instance if you have a contiguous closed subwalk p : G.Walk x x of a walk w then it seems natural to talk about the walk constructed from w by removing p. This would be a non-contiguous subwalk.

[Rida Hamadani]

Yes, that's a fair point.
I propose Walk.IsShortening as another candidate name too.

[Vlad Tsyrklevich]

In case anyone cares, just noting that #29369 and #29376 makes some small additions to the IsSubwalk API (and #29375 is a bit of golf)