Seeking help with the proof: A graph is bipartite iff it has

Stream: mathlib4

[Kilo0409]

Hi everyone,
I am currently working on formalizing the theorem: "A simple graph is bipartite if and only if all its cycles are of even length."
I have run into some difficulties while proving the sufficiency part (i.e., "if a graph contains only even cycles, then it is bipartite"). Specifically, I am stuck on the following lemma: "If a graph contains a closed walk of odd length, then it must contain an odd cycle."

theorem no_odd_cycles_implies_bipartite (h : ∀ (v : V) (c : G.Walk v v), c.IsCycle → Even c.length) :
    G.IsBipartite := by
  let color : V → Fin 2 := fun v =>  root
    let root := (G.connectedComponentMk v).out
    if (G.dist root v) % 2 == 0 then 0 else 1
  refine ⟨SimpleGraph.Coloring.mk color ?_⟩
  intro u v h_adj
  simp only [color]
  by_contra h_same_color
  let root := (G.connectedComponentMk u).out
  have h_root_eq : (G.connectedComponentMk v).out = root := by
    apply congr_arg Quot.out
    rw [SimpleGraph.ConnectedComponent.eq]
    exact SimpleGraph.Adj.reachable h_adj.symm
  simp only [h_root_eq] at h_same_color
  split_ifs at h_same_color with hu_even hv_even <;> try (simp at h_same_color; done)
  all_goals {
    have h_reach_u : G.Reachable root u := by
      rw [← SimpleGraph.ConnectedComponent.eq]
      exact (Quot.out_eq (G.connectedComponentMk u))
    have h_reach_v : G.Reachable root v := by
      rw [← SimpleGraph.ConnectedComponent.eq]
      rw [← h_root_eq]
      exact (Quot.out_eq (G.connectedComponentMk v))
    obtain ⟨p_u, hp_u⟩ := h_reach_u.exists_path_of_dist
    obtain ⟨p_v, hp_v⟩ := h_reach_v.exists_path_of_dist
    let w := p_u.append (SimpleGraph.Walk.cons h_adj p_v.reverse)
    have h_w_len_odd : Odd w.length := by
      rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
      SimpleGraph.Walk.length_reverse]
      rw [hp_u.2, hp_v.2]
      rw [← Nat.add_assoc, Nat.odd_add_one, Nat.not_odd_iff_even, Nat.even_add]
      simp only [Nat.even_iff]
      revert h_same_color
      simp_all
      omega
    have h_contains_odd_cycle : ∃ (root' : V) (c : G.Walk root' root'),
    c.IsCycle ∧ Odd c.length := by sorry
    obtain ⟨root', c, hc_cycle, hc_odd⟩ := h_contains_odd_cycle
    specialize h root' c hc_cycle
    rw [← Nat.not_odd_iff_even] at h
    exact h hc_odd }

I initially tried to prove the existence of an odd cycle using proof by contradiction, but I couldn't quite finish it. Could anyone point me in the right direction for proving this lemma? Alternatively, are there other common approaches to prove the sufficiency of the main theorem that might be easier to formalize in Lean?
Any guidance or snippets from Mathlib would be greatly appreciated!

---

[Yaël Dillies]

Hey! Are you aware of @Nick_adfor's efforts to prove this?

[Alfredo Moreira-Rosa]

Here is the PR #33257

[Kilo0409]

Yaël Dillies said:

Hey! Are you aware of Nick_adfor's efforts to prove this?

In fact, he's been working on this problem with us, but we still can't solve it, and he's currently busy with other things and can't get away. :smiling_face_with_tear:

[Nick Adfor]

Kilo0409 said:

Yaël Dillies said:

Hey! Are you aware of Nick_adfor's efforts to prove this?

In fact, he's been working on this problem with us, but we still can't solve it, and he's currently busy with other things and can't get away. :smiling_face_with_tear:

Oh, I was pretending I had a Christmas holiday when I was speaking English. This "holiday" I was killing time on pen-and-paper proof of some geometry problem offline.

[Nick Adfor]

bipartite_implies_even_cycles now has a short good proof in my PR, but the other side (it is here named as no_odd_cycles_implies_bipartite) in my version relies deeply on Aristotle AI and hard to read (refine' and induction') and thus not so good for Mathlib. Here the no_odd_cycles_implies_bipartite can be a good improvement to my lengthy proof if the sorry can be filled.

But as I've discussed with others in other post, since your most hard part

have h_contains_odd_cycle : ∃ (root' : V) (c : G.Walk root' root'),
    c.IsCycle ∧ Odd c.length := by sorry

relies on the well-definition of lastCommonVertex yet it is not in Mathlib so both other coders and Aristotle chose to avoid this. (For ones don't know where lastCommonVertex raises, I'd like to mention Introductory Combinatorics by Richard Brualdi, theorem 11.4.1, also in my photo post in my previous post.)

[Nick Adfor]

Here's a new file generated by Aristotle to fix some problems in my PR.
Aristotle's origin-output.lean.txt

The technique I choose is just removing induction' and refine' and still following bypass because of my curiosity to bypass (yes, a somehow ridiculous reason).

Or to be more reasonable, it is to show respect to bypass in Mathlib, yet I should say that it is a kind of proof not in any textbook so we should take more time to think of its mathematical explanation.

[Nick Adfor]

I've submitted new PR, what with yellow line is in the comment:

import Mathlib

open SimpleGraph

open Walk

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

lemma IsPath.length_eq_one_of_mem_edges
{u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : s(u, v) ∈ p.edges) : p.length = 1 := by
  by_contra h_non_simple_cycle
  have h_cycle : ∃ q : G.Walk u u, q.IsCycle := by
    rcases p with ( _ | ⟨_, _, p⟩ )
    · aesop
    · aesop
    · aesop
      -- I don't know what happened here, `aesop` change `p✝` to `p`,
      -- but `aesop?` cannot generate anything benifit.
      have := by exact SimpleGraph.Walk.fst_mem_support_of_mem_edges p h_3
      exact Classical.not_forall_not.mp fun a ↦ right this
  obtain ⟨q, hq⟩ := h_cycle
  cases q <;> simp_all +decide only [isCycle_def, IsTrail.nil, ne_eq, not_true_eq_false,
    support_nil, List.tail_cons, List.nodup_nil, and_true, and_false]
  cases p <;> simp_all +decide only [isTrail_def, edges_cons, List.nodup_cons, reduceCtorEq,
    not_false_eq_true, support_cons, List.tail_cons, true_and, isPath_iff_eq_nil, edges_nil,
    List.not_mem_nil]
  simp_all only [cons_isPath_iff, List.mem_cons, Sym2.eq, Sym2.rel_iff',
  Prod.mk.injEq, true_and, Prod.swap_prod_mk, length_cons, Nat.add_eq_right]
  obtain ⟨left, right⟩ := hq
  obtain ⟨left_1, right_1⟩ := hp
  obtain ⟨left, right_2⟩ := left
  cases h with
  | inl h_3 =>
    cases h_3 with
    | inl h =>
      subst h
      simp_all only [length_eq_zero_iff, isPath_iff_eq_nil]
    | inr h_4 => simp_all only [SimpleGraph.irrefl]
  | inr h_4 => exact right_1 ( SimpleGraph.Walk.fst_mem_support_of_mem_edges _ h_4 )

[Notification Bot]

5 messages were moved from this topic to #mathlib4 > author names in mathlib by Yuyang Zhao.

[Kilo0409]

Nick_adfor said:

I've submitted new PR, what with yellow line is in the comment:

import Mathlib

open SimpleGraph

open Walk

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

lemma IsPath.length_eq_one_of_mem_edges
{u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : s(u, v) ∈ p.edges) : p.length = 1 := by
  by_contra h_non_simple_cycle
  have h_cycle : ∃ q : G.Walk u u, q.IsCycle := by
    rcases p with ( _ | ⟨_, _, p⟩ )
    · aesop
    · aesop
    · aesop
      -- I don't know what happened here, `aesop` change `p✝` to `p`,
      -- but `aesop?` cannot generate anything benifit.
      have := by exact SimpleGraph.Walk.fst_mem_support_of_mem_edges p h_3
      exact Classical.not_forall_not.mp fun a ↦ right this
  obtain ⟨q, hq⟩ := h_cycle
  cases q <;> simp_all +decide only [isCycle_def, IsTrail.nil, ne_eq, not_true_eq_false,
    support_nil, List.tail_cons, List.nodup_nil, and_true, and_false]
  cases p <;> simp_all +decide only [isTrail_def, edges_cons, List.nodup_cons, reduceCtorEq,
    not_false_eq_true, support_cons, List.tail_cons, true_and, isPath_iff_eq_nil, edges_nil,
    List.not_mem_nil]
  simp_all only [cons_isPath_iff, List.mem_cons, Sym2.eq, Sym2.rel_iff',
  Prod.mk.injEq, true_and, Prod.swap_prod_mk, length_cons, Nat.add_eq_right]
  obtain ⟨left, right⟩ := hq
  obtain ⟨left_1, right_1⟩ := hp
  obtain ⟨left, right_2⟩ := left
  cases h with
  | inl h_3 =>
    cases h_3 with
    | inl h =>
      subst h
      simp_all only [length_eq_zero_iff, isPath_iff_eq_nil]
    | inr h_4 => simp_all only [SimpleGraph.irrefl]
  | inr h_4 => exact right_1 ( SimpleGraph.Walk.fst_mem_support_of_mem_edges _ h_4 )

thank you

[Snir Broshi]

How does #33431 fit into this? It seems to be by one of your co-authors, and contains almost the same theorems with similar proofs, but in a different file? And its docstring talks about multigraphs all of a sudden? I'm confused about the coordination among the 3 co-authors here

[Nick Adfor]

Snir Broshi said:

How does #33431 fit into this? It seems to be by one of your co-authors, and contains almost the same theorems with similar proofs, but in a different file? And its docstring talks about multigraphs all of a sudden? I'm confused about the coordination among the 3 co-authors here

If represent others to PR code, it will cause problem like this. Anyway, I'm tired of discussing distribution but I just want to make sure that everyone here are able to find the authors' Zulip and GitHub account and email. If there's any merge work in the future, community members are easy to contact the author.

[Nick Adfor]

As bypass is more suitable (just because it is already in the Mathlib before), I will deal with an old PR more relevant to bypass #25834 later I have time.

[Snir Broshi]

Nick Adfor said:

I'm tired of discussing distribution but I just want to make sure that everyone here are able to find the authors' Zulip and GitHub account and email

Can you ping Sun Yue here then?

[Snir Broshi]

(I wasn't able to find her Zulip)

[Nick Adfor]

Snir Broshi said:

Nick Adfor said:

I'm tired of discussing distribution but I just want to make sure that everyone here are able to find the authors' Zulip and GitHub account and email

Can you ping Sun Yue here then?

It's a problem that not all the Chinese can accept this social discipline in Zulip to be open access to everyone. Having one's not-so-mature work published here and accepting others to make review or even criticism on it need a lot of courage. In the origin we just want to finish the code as homework privately but since now our work gains some attention and might be helpful to Mathlib, some improvement should be made.

Sun Yue is the author of #33431. She forgets to leave her email yet you can find it in my #33257. Huang Jiayi is the post owner here. If one is confused why there are a lot of names and cannot find who is who, the discussion is posted here.

[Nick Adfor]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/author.20names.20in.20mathlib

[Snir Broshi]

Okay, what does that mean about #33431 vs #33257? Which one should be closed? Neither?

Nick Adfor said:

It's a problem that not all the Chinese can accept this social discipline in Zulip to be open access to everyone. Having one's not-so-mature work published here and accepting others to make review or even criticism on it need a lot of courage

What does that mean in terms of reviewing #33431? Usually opening a PR means accepting reviews, is that not the case here? Or are GitHub reviews okay but joining Zulip is less so?

[Nick Adfor]

Maybe because of language barrier
:(