Bipartite graphs don't contain odd cycles

Stream: graph theory

[Simon Strzoda]

Hi all,

over the holidays I started learning Lean and worked through the statement

theorem isBipartite_no_odd_cycle :
G.IsBipartite → ∀ n : ℕ, (SimpleGraph.cycleGraph (2*(n+1)+1)).Free G :=

which corresponds to one of the TODOs on the documentation page for IsBipartite. Since this is my first Lean project, the proof is still a bit chaotic, but the approach seems to work. If this direction is something mathlib would like to include, I’d be very happy to clean up the argument, pursue the backward implication as well, and eventually prepare a PR to fill in the missing pieces. I’d appreciate any feedback on whether this would be useful and how best to integrate it into the existing API.

[Jakub Nowak]

Hi!

I also worked on this to learn Lean. :D

There was already quite a lot of discussion about this:
#Is there code for X? > bipartite iff does not contain an odd cycle
#mathlib4 > Formalizing Graph Theory - The Odd Cycle Theorem in Lean

Would you like to share what was your approach? I'll be interested in it.

[Jakub Nowak]

Ah, you only proved this one implication. The other implication is I think harder and isn't yet proved in mathlib. ∀ n : ℕ, (SimpleGraph.cycleGraph (2*(n+1)+1)).Free G is equivalent to ∀ w : G.Walk u u, w.IsCycle → Even w.length. We already have even more general G.IsBipartite → (∀ w : G.Walk u u, Even w.length) in mathlib: SimpleGraph.two_colorable_iff_forall_loop_even

[Jakub Nowak]

We also have (∀ w : G.Walk u u, Even w.length) → G.IsBipartite. And what we doesn't have (yet merged) is (∀ w : G.Walk u u, w.IsCycle → Even w.length) → G.IsBipartite, which is a very similar to (∀ n : ℕ, (SimpleGraph.cycleGraph (2*(n+1)+1)).Free G) → G.IsBipartite.

[Simon Strzoda]

Hi Jakub, thanks for the quick reply!

At a high level, my approach for the direction I proved was to assume, for contradiction, that the graph contains an odd cycle and admits a coloring. From there, I showed that any coloring of a cycle must be alternating, and then used these two facts to conclude that two adjacent vertices must receive the same color—contradicting the assumption that the graph is colorable.

For the other direction, I planned to first handle the special case of connected graphs and then generalize to arbitrary graphs. To construct the coloring, I was considering the “shortest‑path parity coloring”. To show that this assignment is indeed a coloring, i.e. a graph homomorphism

(SimpleGraph.Hom G (completeGraph (Fin 2))

I would need to show that adjacent vertices in G map to adjacent vertices in completeGraph (Fin 2). My idea was to assume, for contradiction, that two adjacent vertices in G receive the same color, then use the walks arising from the shortest‑path construction to build an odd cycle in G, contradicting the assumption that G is odd‑cycle‑free.

Thanks again for the helpful reply! It seems the main ideas are already well covered, so I won’t pursue this direction further, but I really appreciated the insights. :)

[Nick Adfor]

About the discussion, I already had a PR #33257 proved by bypass in Mathlib. But I do not know what the PR should be used for. It's really that I cannot just upload a PR as a file storage, but I do not have the permission to merge it into Mathlib. "Merging is blocked: You're not authorized to push to this branch." That is what GitHub show me.

Maybe the most I can do is inspiring some new idea here in Zulip. Feel free to check if you think it is usable.

[Nick Adfor]

There's also another work from Rida (#graph theory > Girth and Diameter Proof ). Rida has a private definition about takeAt which I haven't checked carefully.

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]

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]

For textbook proof, there's one from Introductory Combinatorics. But this relies on well-definition about lastCommonVertex,

Nick Adfor said:

precise and concise proof.jpg

which @Jakub Nowak pointed out that it might be wrong (lack a well-definition). Click the blue part to see the origin.

Jakub Nowak said:

I think that "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.
This is because you can take the last vertex on the walk x⋯a that is common with the walk x⋯b, and you can take the last vertex on the walk x⋯b that is common with the walk x⋯a. And these two are not necessarily equal.

Maybe (just maybe) Rida's takeAt can solve the problem. But these days I lack time to check them all. Maybe you can bring these work together :)

[Iván Renison]

I took a look at #33257, and I was thinking that maybe it is also nice to have the theorem isBipartite_iff_all_loops_even : G.IsBipartite ↔ ∀ (v : V) (c : G.Walk v v), Even c.length, which I think it is also true

[Jakub Nowak]

Iván Renison said:

I took a look at #33257, and I was thinking that maybe it is also nice to have the theorem isBipartite_iff_all_loops_even : G.IsBipartite ↔ ∀ (v : V) (c : G.Walk v v), Even c.length, which I think it is also true

We already do have this: SimpleGraph.two_colorable_iff_forall_loop_even