bipartite iff does not contain an odd cycle

Stream: Is there code for X?

[Jakub Nowak]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Bipartite.html#TODO

I've started working on this as a project to learn Lean. I have proofs of

theorem SimpleGraph.IsBipartite.oddCycleFree (h : G.IsBipartite) :
    ∀ n, (cycleGraph (2*n + 3)).Free G

theorem SimpleGraph.IsBipartite.of_eachCycleEven [DecidableEq V]
    (h : ∀ {u : V} (p : G.Walk u u), p.IsCycle → ¬p.length.bodd)
    (hCon : G.Connected) :
    G.IsBipartite

I'm happy with what I learned so far. I can work further on this to contribute to mathlib. Do you think this would be valuable for mathlib? Also, maybe someone is already working on this?

[Bhavik Mehta]

There's slight discussion of this here: https://github.com/leanprover-community/mathlib4/pull/25837#discussion_r2285926375 so perhaps coordinating with @John Talbot would be sensible.

[John Talbot]

This sounds interesting!

We currently only have

lemma two_colorable_iff_forall_loop_even {α : Type*} {G : SimpleGraph α} :
    G.Colorable 2 ↔ ∀ u, ∀ (w : G.Walk u u), Even w.length

We really want something like this

lemma two_colorable_iff_forall_isCycle_even {α : Type*} {G : SimpleGraph α} :
    G.Colorable 2 ↔ ∀ u, ∀ (w : G.Walk u u), w.IsCycle → Even w.length

I have a proof of this here : https://github.com/jt496/mathlib4/blob/walks/Mathlib/Combinatorics/SimpleGraph/OddCycles.lean
but this is rather long since it goes via the following result (which says that any odd length closed walk contains an odd length cycle as a subwalk):

theorem exists_odd_cycle_subwalk {u : α} {w : G.Walk u u} (ho : Odd w.length) :
    ∃ (x : α) (c : G.Walk x x), c.IsCycle ∧ Odd c.length  ∧ c <+ w

I'd be very interested in seeing your version and hopefully we can get something suitable for mathlib!

[Jakub Nowak]

First proof is actually pretty simple.

import Mathlib

open SimpleGraph

universe u
variable {V : Type u} {G : SimpleGraph V} {u v : V}


theorem Colorable.of_hom {V' : Type*} {G' : SimpleGraph V'} (f : G →g G') {n : ℕ}
    (h : G'.Colorable n) : G.Colorable n :=
  ⟨(h.toColoring (by simp)).comp f⟩

theorem SimpleGraph.chromaticNumber_mono_of_hom {V' : Type*} {G' : SimpleGraph V'}
    (f : G →g G') : G.chromaticNumber ≤ G'.chromaticNumber :=
  chromaticNumber_le_of_forall_imp fun _ => Colorable.of_hom f

theorem SimpleGraph.chromaticNumber_mono_subgraph {V' : Type*} {G' : SimpleGraph V'}
    (h : G ⊑ G') : G.chromaticNumber ≤ G'.chromaticNumber :=
  chromaticNumber_mono_of_hom h.some.toHom


theorem SimpleGraph.IsBipartite.oddCycleFree (h : G.IsBipartite) :
    ∀ n, (cycleGraph (2*n + 3)).Free G := by
  intro n hC
  have : (3 : ℕ∞) ≤ (2 : ℕ∞) := calc
    3 = (cycleGraph (2*n + 3)).chromaticNumber := by
      symm
      apply chromaticNumber_cycleGraph_of_odd
      · omega
      · apply Even.add_odd
        exact even_two_mul n
        exact Nat.odd_iff.mpr rfl
    (cycleGraph (2*n + 3)).chromaticNumber ≤ G.chromaticNumber := chromaticNumber_mono_subgraph hC
    G.chromaticNumber ≤ 2 := h.chromaticNumber_le
  have : 3 ≤ 2 := ENat.coe_le_coe.mp this
  contradiction

If we want to relate cycleGraph with cycles in a graph we would probably need some lemma about isomorphisms of cycleGraph with subgraphs generated by support of cycles.

My second proof also has the same lemma as yours, but it's only one implication and only for connected graphs, so it seems like your work is more advanced. I'll put it here if you want to check it out live.lean-lang.org.

I've used Nat.bodd instead of Odd/Even, because it has more useful @simp lemmas so it was easier to work with. It might be also worthwhile to look into this and and some more @simp lemmas for Nat, or more generally structures where Odd a XOR Even a is true.

There's https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Coloring.html#SimpleGraph.Colorable.of_embedding in mathlib, but embedding is an unnecessary assumption there. The same proofs works for just any homomorphism.

I was thinking, that maybe it would be useful to abstract away induction principle I've used in my proof of odd_cycle_of_odd_walk. This would look something like that:

SimpleGraph.Walk.bypassRec :
  ((p : G.Walk u v) → p.IsPath → motive p) →

  ({w : V} → (pref : G.Walk u w) → (mid : G.Walk w w) → (suf : G.Walk w v) →
    pref.IsPath → (mid.IsCycle ∨ ∃ {w' : V} (h : G.Adj w w'), mid = .cons h h.symm.toWalk) → motive (pref.append suf) →
    motive ((pref.append mid).append suf)) →

  (p : G.Walk u v) → motive p

This induction principle might potentially be useful for other proofs about subwalks.

[Jakub Nowak]

SimpleGraph.Walk.cons_isCycle_of_path_length_ne_1 might be an useful addition to mathlib maybe? I think it has much simpler assumption than SimpleGraph.Walk.cons_isCycle_iff.

[Jakub Nowak]

Oh, homOfConnectedComponents from the linked PR was exactly what I was missing to get my proof to work for non connected graphs. :D

[John Talbot]

My second proof also has the same lemma as yours, but it's only one implication and only for connected graphs, so it seems like your work is more advanced. I'll put it here if you want to check it out live.lean-lang.org.

This looks really nice! In particular odd_cycle_of_odd_walk_step looks like a great way to get an odd length cycle from an odd length closed walk.

There is plenty from here that would be great for mathlib so please go ahead and open a PR!

You could also start a new thread in #narrow/channel/252551-graph-theory where other people interested in graph theory will see it.

[Jakub Nowak]

@Snir Broshi I will answer your question here.

Snir Broshi said:

I'm interested to learn how you managed to get an odd cycle from an odd walk, can you share the body of that function? This might enhance #31217

Here's the implementation: live.lean-lang.org
It's implemented by following the walk, until first repetition of a vertex. This gives either a cycle, or a A -> B -> A walk. If it's an odd cycle, then we get an odd cycle, otherwise it has even length, we can recurse on the walk with the repetition bypassed, and the length of the whole walk is still kept odd. At some point we must end up with odd length cycle, because .nil has even length.

If you try to apply similar algorithm to any closed walk, to get any cycle, the problem that arises is that we could always end up with A -> B -> A case. I think that the exact condition for when it is possible to extract cycle from closed walk isn't easy to formulate. E.g., you can't extract a cycle from such a walk: A -> B -> C -> B -> C -> D -> C -> E -> F -> E -> C -> B -> A. I think IsTrail is a good, simple condition. Odd length is another. Maybe another simple condition, weaker then IsTrail, is to require that the walk does not contain a back-and-forth A -> B -> A subwalk (this would require implementing similar recursive algorithm, the implementation from #31217 won't work).

[Snir Broshi]

Relevant: #32185
This proves IsTree → IsBipartite, and can probably be extended to IsAcyclic → IsBipartite by coloring each connected component separately

[Oliver Nash]

Noting the graph theory progress, and in particular results about trees, I can't resist suggesting that someone consider classifying the graphs underlying Dynkin diagrams. It's a valuable concrete result and would validate the general theory. Furthermore, Mathlib already knows that these diagrams classify root systems: docs#RootPairing.Base.equivOfCartanMatrixEq

[Vlad Tsyrklevich]

Do you need multiple edges between vertices? Because then mathlib has almost no theory established at all.

[Jakub Nowak]

Snir Broshi said:

Relevant: #32185
This proves IsTree → IsBipartite, and can probably be extended to IsAcyclic → IsBipartite by coloring each connected component separately

Ah, yes, when I started writing my proof, I believed that proof via trees would be simpler, but mathlib didn't have theory about trees at that moment.

[Snir Broshi]

Snir Broshi said:

Relevant: #32185
This proves IsTree → IsBipartite, and can probably be extended to IsAcyclic → IsBipartite by coloring each connected component separately

#32568 extends it to IsAcyclic → IsBipartite

[Snir Broshi]

I believe IsAcyclic.dist_ne_of_adj characterizes graphs without odd cycles. Does anyone have any ideas for proving the following?

import Mathlib
theorem SimpleGraph.isBipartite_iff_dist_ne {V : Type*} (G : SimpleGraph V) :
    G.IsBipartite ↔ ∀ u v w, G.Adj v w → G.Reachable u v → G.dist u v ≠ G.dist u w := by
  sorry

[Jakub Nowak]

Snir Broshi said:

I believe IsAcyclic.dist_ne_of_adj characterizes graphs without odd cycle. Does anyone have any ideas for proving the following?

import Mathlib
theorem SimpleGraph.isBipartite_iff_dist_ne {V : Type*} (G : SimpleGraph V) :
    G.IsBipartite ↔ ∀ u v w, G.Adj v w → G.Reachable u v → G.dist u v ≠ G.dist u w := by
  sorry

I think that right to left implication is almost the same proof as SimpleGraph.two_colorable_iff_forall_loop_even. You create bi-coloring for a connected component, by picking any vertex r in it, and taking dist r v % 2 as a color. You would use SimpleGraph.Connected.diff_dist_adj combined with assumption to prove that colors are different.

[Jakub Nowak]

And for left-to-right implication you can prove (∀ (u : α) (w : G.Walk u u), Even w.length) → ∀ u v w, G.Adj v w → G.Reachable u v → G.dist u v ≠ G.dist u w. Assume dist u v = dist u w. Then, you get odd closed walk u ~> v -> w ~> u, which is in contradiction with assumption about even. Well, almost, last time I've tried using Even/Odd I noticed lack of Even iff not Odd lemma for Nat.

[Jakub Nowak]

@Snir Broshi I think, it's more like this characterizes graphs without odd closed walk, rather than odd cycle (although, the two are equivalent).

[Jakub Nowak]

Do we have some lemmas about spanning tree / BFS trees in mathlib now? A tree, rooted in a given vertex r, where dist r u is the same in the tree as in the original graph for every u. And some lemmas about least common ancestor. Because I think this would make for a much simpler proof of bipartite iff no odd cycles than what I currently have.

[Snir Broshi]

Jakub Nowak said:

Do we have some lemmas about spanning tree / BFS trees in mathlib now? A tree, rooted in a given vertex r, where dist r u is the same in the tree as in the original graph for every u. And some lemmas about least common ancestor. Because I think this would make for a much simpler proof of bipartite iff no odd cycles than what I currently have.

Not sure if that's what you're looking for but #32041 and #32043 have some results about spanning trees/forests (maximal acyclic graphs contained in another graph)