Girth and Diameter Proof

Stream: graph theory

[Kiril Vinogradov]

Hi all, I'm planning on over the next few months to slowly tackle the formalization of the attached proof
diam.webp
[The proof that the girth of a graph is less than or equal to twice its diameter + 1]
I wanted to seek some advice from more experienced Lean users as to what are your thoughts on the best way to tackle this in regards to what type of object could be best suited for this problem. Would it be best to begin the implementation of it using a cycle graph, or by ways of using a cyclic subgraph, or moreover simply by defining it as a walk that starts and ends at the same vertex and then going from there? I appreciate any advice or thoughts on this matter.

[Daniel Weber]

I think it will be easiest to use docs#SimpleGraph.Walk.IsCycle

[Rida Hamadani]

I proved this lemma 6 months ago (#25834), but the proof is too messy to be merged into mathlib. Currently I'm working on tidying it up and would like to hear your opinions considering how to do it:
The proof relies on the fact that we can get a cycle by gluing two paths together (given that they start and end on the same vertex), and we should be able to say that such a cycle would have a size at most the sum of the paths.
I've noticed that @Yaël Dillies has added docs#SimpleGraph.Walk.cycleBypass recently which is close to what we want.
On this) branch I've uploaded some code defining the following:

• DivergentPt: the point where two walks that started from the same vertex stop agreeing. This is necessary if we want to create a cycle from two paths, because we should specify where the cycle starts/ends, and this point does that.
• getCycle: this takes two walks p q : G.Walk u v and returns a walk G.Walk (DivergentPt p q) (DivergentPt p q). The process is as follows: drop all vertices from p and q up to (DivergentPt p q), append p to the reverse of q, then perform cycleBypass on it.
  When p and q are both paths, and then are not identical, getCycle gives a cycle. This is proven in my branch at getCycle_isCycle (module a sorry).
  I would like to hear your opinions on this approach, do you think these definitions are worth adding to mathlib? Are there are suggestions to make it more modular or tidier? Do you think these additions deserve to be in a separate file and/or PR from the rest of the girth-diameter inequality proof?

[Rida Hamadani]

Another approach I've thought about in order to get cycles from 2 paths is to define a "Z-module of cycles on G " and then prove that G.Walk u v is an affine space over this Z-module, thus there exists a unique cycle v such that p = q + v for any p q : Walk u v. This is more elegant (and perhaps reusable in case someone wants to use graph homology in the future) but unfortunately I couldn't get it to work because in order to have a Z-modile of cycles, we will need to consider union of cycles and figure 8 as cycles which doesn't work with our definition of IsCycle, but I'm sharing this in case someone might have an idea to make this work.

[Shreyas Srinivas]

I was hoping we would be rid of the indexed version of walks tbh. This proof would be much shorter in the List.ischain version

[Shreyas Srinivas]

Why not just start with edge disjoint paths directly?

[Rida Hamadani]

Part of the reason for why the proof is long is having to construct cycles (and dealing with edge cases), I would like to be able to say "take these two walks, both of them are paths, and they aren't identical, thus they make a sufficiently small cycle", but if I wanted to prove that the paths are edge disjoint I'll probably have to construct them explicitly again in such a way that it would be similar to constructing the cycles.
I will think about how List.ischain can shorten the proof.

[Yaël Dillies]

Indeed, cycleBypass isn't quite enough for your purposes. Note that whatever you come up with will also greatly help #PR reviews > #33257 Odd Cycle Theorem, cc @Nick_adfor

[Yaël Dillies]

Whoops, cc @Nick_adfor

[Nick Adfor]

I've noticed some of bypass work in Mathlib and tried to understand its math background. What textbook should I refer to?

[Yaël Dillies]

I am not sure we followed any textbook

[Nick Adfor]

The picture in this post may be from some textbook that I can follow

[Nick Adfor]

Yet it might be right that for code in PR and Mathlib I cannot just refered to one book.

[Rida Hamadani]

The picture is from Diestel, but it does not define bypass like we do, Diestel's argument is not formalizable as it is and had to be modified quite a bit

[Rida Hamadani]

Yaël Dillies said:

Indeed, cycleBypass isn't quite enough for your purposes. Note that whatever you come up with will also greatly help #PR reviews > #33257 Odd Cycle Theorem, cc Nick_adfor

Thank you for pointing that out! In this case I will PR getCycle in a separate file (or maybe add it to Operations.lean in case that file doesn't get too big)

[Snir Broshi]

I like the divergent-point solution, but it's weird that we have multiple defs that manipulate walks (like bypass/cycleBypass and this suggestion) and there is no one-size-fits-all. for example, I think none of the above cover @Jakub Nowak's walk manipulation in #Is there code for X? > bipartite iff does not contain an odd cycle @ 💬, which can convert any odd walk to an odd cycle.
It's similar to cycleBypass, but it works in more cases.
It also seems pretty similar to getCycle, but it doesn't require any path assumptions.
I feel like surely there must be some magic function that generalizes all these super specific walk manipulations. They all revolve around converting walks to paths/cycles by deleting some parts

[Rida Hamadani]

That is precisely what prompted me to think about trying to do this by proving that G.Walk u v forms an affine space over the Z-module of "cycles". Perhaps another approach to try to make a more general tool is instead of defining a divergent point, we define a list of divergent points and another of convergent points, then prove that each index of the list induces a cycle, then we can for instance choose the smallest one, etc. This won't help with the manipulation you link but perhaps finding a one size that fits all is hopeless here and the best we can do is find a size that fits as most as possible.

[Rida Hamadani]

For now I will implement the single divergent point approach but I'll keep the list approach in head as a possible generalization that I might do in the future (perhaps once I'm done with making the girth-diameter proof mergeable).

[Nick Adfor]

I've noticed that Rida has become the of reviewer of #33257. Is there anything to merge in #25834?

[Jakub Nowak]

Maybe theory about rooted BFS trees would also be useful for this proof? See my comment here: #mathlib4 > Formalizing Graph Theory - The Odd Cycle Theorem in Lean @ 💬

[Matthew Coke]

@Rida Hamadani Can we bring talk about depth into the proof by making the claim that gluing two paths together produces two vertices that have a depth of 2 in contrast to the other vertices which have a depth of 1? I find it useful to associate depth with "anchor points"

[Nick Adfor]

Rida Hamadani said:

Part of the reason for why the proof is long is having to construct cycles (and dealing with edge cases), I would like to be able to say "take these two walks, both of them are paths, and they aren't identical, thus they make a sufficiently small cycle", but if I wanted to prove that the paths are edge disjoint I'll probably have to construct them explicitly again in such a way that it would be similar to constructing the cycles.
I will think about how List.ischain can shorten the proof.

Okay, as now my #33257 has all finished (the goal of this PR is to prove TODO in Bipartite.lean) , if there are some shortened proof in #25834, should #33257 be a branch of #25834 or conversely?

[Nick Adfor]

I've noticed that your takeAt

def Walk.takeAt {u v} (p : G.Walk u v) {i j : ℕ} (h : i ≤ j) :
    G.Walk (p.getVert i) (p.getVert j) :=
  ((p.drop i).take (j - i)).copy rfl <| by rw [p.drop_getVert i (j - i), Nat.sub_add_cancel h]

may introduce a new method to define lastCommonVertex in my post #mathlib4 > Formalizing Graph Theory - The Odd Cycle Theorem in Lean @ 💬

def lastCommonVertex (p : G.Walk r a) (q : G.Walk r b)
    (hp : p.IsPath) (hq : q.IsPath)
    (hp_min : p.length = G.dist r a)
    (hq_min : q.length = G.dist r b) : V := by ...

But as now your def Walk.takeAt cannot run as Nat.sub_add_cancel h showing

Tactic `rewrite` failed: Did not find an occurrence of the pattern
j - i + i
in the target expression
p.getVert (i + (j - i)) = p.getVert j

so I cannot finish my def.

[Nick Adfor]

Jakub said ""Since the first vertex of each of these walks is x there is a vertex z that is the last common vertex of these two walks" is not true." But the definition can be fixed to make it true. I don't know if it is workable and if you want to do more work (or co-work) to make your takeAt usable in the future PR.

[Rida Hamadani]

Jakub Nowak said:

Maybe theory about rooted BFS trees would also be useful for this proof? See my comment here: #mathlib4 > Formalizing Graph Theory - The Odd Cycle Theorem in Lean @ 💬

Interesting idea, I'll give it more thought next week after I'm done with my exams.

[Rida Hamadani]

Matthew Coke said:

Rida Hamadani Can we bring talk about depth into the proof by making the claim that gluing two paths together produces two vertices that have a depth of 2 in contrast to the other vertices which have a depth of 1? I find it useful to associate depth with "anchor points"

I'm not sure what you mean by depth, is it the same as the distance between two vertices?

[Rida Hamadani]

Nick Adfor said:

I've noticed that your takeAt

def Walk.takeAt {u v} (p : G.Walk u v) {i j : ℕ} (h : i ≤ j) :
    G.Walk (p.getVert i) (p.getVert j) :=
  ((p.drop i).take (j - i)).copy rfl <| by rw [p.drop_getVert i (j - i), Nat.sub_add_cancel h]

This will be fixed, in fact I'm hoping that I will be able to remove takeAt completely in favor of getCycle. I'm currently busy but will have more time to work on it in the upcoming weeks.

[Rida Hamadani]

takeAt feels a bit clunky to me, do you think it will be useful to you? Feel free to take it from my PR and add it to yours if it is.

[Matthew Coke]

@Rida Hamadani it would be more comparable to vertex degree rather than distance between vertices. Starting from a path, it could be considered to be how many vertices are stacked on top of each other creating "branch points" from any specific vertex

[Rida Hamadani]

I'm unfamiliar with this terminology, do we have it in mathlib?

[Matthew Coke]

@Rida Hamadani doubtful. Some of the choices I make in how I relate to graph theory might be somewhat unique

[Rida Hamadani]

It will be difficult for me to include a concept that I'm not familiar with, if this is important to your work, perhaps you can open a PR to mathlib defining it and developing an API for it, and after that I will think about whether it is realistic for me to relate it to this work.

[Matthew Coke]

@Rida Hamadani I agree with you. I'm relatively new here and don't know how to open a PR to mathlib yet. I'm not convinced that it's important to my work in digital space and with interactive theorem provers yet

[Jakub Nowak]

There was mention of bipartite iff no odd cycle theorem, unfortunately I think that Rida's getCycle won't work as is for that purpose, because the returned cycle won't necessarily have the same mod 2 value as the sum of length of p and q.

[Rida Hamadani]

That depends on p and q, do they have any intersections other than starting and ending points? If not then the returned cycle will satisfy that.

[Rida Hamadani]

This can be generalized: we can define the convergence point, in a similar fashion to the divergent point, to be the first point where the two paths meet after being separated, let p q : G.Walk u v be two paths, note that p.subgraph.dist u (DivergentPt p q) = q.subgraph.dist u (DivergentPt p q), then the equation becomes:

(getCycle  p q).length = p.length + q.length -  2 * (p.subgraph.dist u (DivergentPt p q)) - p.subgraph.dist (ConvergentPt p q) v - q.subgraph.dist (ConvergentPt p q)

[Nick Adfor]

Maybe later on January 25th-27th (my co-authors will have a conference with me) we can hold an online meeting about how many definitions we have and which one to choose...

[Rida Hamadani]

I'm not available in January and especially not on these days. I'm more available in February, however, I think that it is easier to navigate this in text form since it keeps track of everything discussed and gives as much time as necessary to think and try things out.

[Rida Hamadani]

Thanks to a very cool proof plan suggested by @Bhavik Mehta, #33506 now has a complete proof of the fact that a cycle could be constructed given two unequal paths, of length less or equal to the sum.
Instead of using the getCycle definition that was described above, it uses an existential statement.
However, the current proof depends on some ugly isPath_append_isCycle lemma that also depends on two other ugly lemmas, does anyone have any suggestions on what to do with these? Perhaps golfing ideas, or maybe an approach that removes the need for them?
I'd like to especially get rid of IsPath.exists_of_edges, or at least golf it and find a proper place for it in mathlib.