Newbie lurker here, trying to restart

Stream: graph theory

[Ilmārs Cīrulis]

Hi, I'm trying to restart learning graph theory stuff and doing proofs about it.
What would you suggest to prove to learn more about the craft? (Things already in Mathlib is good to suggest, too. Though doing something for Mathlib is probably more on the topic here.)

For the start I reproved lemma about the degree sum being twice a number of edges, using induction on number of vertices, then induction on number of edges and finally by using double counting argument, although my attempt at double counting isn't as good as the Mathlib's proof and also not as nice as this version of the proof: https://thebook.zib.de/graph%20theory/2024/10/11/handshaking-lemma.html

[Ilmārs Cīrulis]

If this isn't appropriate topic, feel free to tell me that. :sweat_smile: Anyway, cheers!

[Rida Hamadani]

Is there a sub-area of graph theory you are interested in learning about and contributing to more than the others?

[Ilmārs Cīrulis]

Extremal graph theory, if such very broad answer is okay.

[Snir Broshi]

Perhaps reviewing #25841 is a good way to start contributing in extremal GT?

[Snir Broshi]

If you're not locked into extremal GT, check out #new members > Looking for a first project (Graph Theory / Combinatorics) @ 💬

[Ilmārs Cīrulis]

Am I bad at searching? I couldn't find any theorem about the upper limit for number of edges in bipartite graph. :thinking:

I mean, something like if G.IsBipartiteWith s t and s and t are finite sets, then G.edgeFinset.card <= s.card * t.card.

(I'm still reproving basic things - to get more experience. :sweat_smile:)

[Ilmārs Cīrulis]

If it isn't in Mathlib, maybe that's good enough fact/theorem to prove and put into Mathlib?

[Ilmārs Cīrulis]

This, and that too.

import Mathlib

theorem T₀ {V : Type u_1} {G : SimpleGraph V} {s t : Finset V} [Fintype V]
    [DecidableRel G.Adj] (h : G.IsBipartiteWith ↑s ↑t) :
    G.edgeFinset.card ≤ s.card * t.card := sorry

theorem T₁ {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V]
    [DecidableRel G.Adj] (h : G.IsBipartite) :
    4 * G.edgeFinset.card ≤ Fintype.card V ^ 2 := sorry

[Snir Broshi]

Can you use Set.encard instead of assuming everything is finite?

import Mathlib
namespace SimpleGraph
variable {V : Type*} {G : SimpleGraph V}

theorem IsBipartiteWith.encard_edgeSet_le {s t : Set V} (h : G.IsBipartiteWith s t) :
    G.edgeSet.encard ≤ s.encard * t.encard := by
  sorry

theorem IsBipartite.four_mul_encard_edgeSet_le (h : G.IsBipartite) :
    4 * G.edgeSet.encard ≤ ENat.card V ^ 2 := by
  sorry

[Ilmārs Cīrulis]

Yes, I will try that right now.

[Jakub Nowak]

You can use SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges and SimpleGraph.isBipartiteWith_degree_le I think. For the Fintype version at least. I think these two theorems could also be generalized in terms of encard?

[Jakub Nowak]

Not sure if we want that though? What's your motivation for working with infinite graphs @Snir Broshi? From my experience working with encard is quite annoying.

[Ilmārs Cīrulis]

That I have done, I believe. Now messing around with encard version.

import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Data.Int.Star

theorem T₀ {V : Type u_1} {G : SimpleGraph V} {s t : Finset V} [Fintype V] [DecidableRel G.Adj]
    (h : G.IsBipartiteWith ↑s ↑t) : G.edgeFinset.card ≤ s.card * t.card := by
  rw [← SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges h]
  have h : ∀ v ∈ s, G.degree v ≤ t.card := by
    intros v hv
    apply SimpleGraph.isBipartiteWith_degree_le' h.symm hv
  apply Finset.sum_le_sum at h
  simp at h; exact h

theorem T₁ {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (h : G.IsBipartite) : 4 * G.edgeFinset.card ≤ Fintype.card V ^ 2 := by
  rw [SimpleGraph.isBipartite_iff_exists_isBipartiteWith] at h
  obtain ⟨s, t, h⟩ := h
  have inst_s : Fintype ↑s := Fintype.ofFinite ↑s
  have inst_t : Fintype ↑t := Fintype.ofFinite ↑t
  have h' : G.IsBipartiteWith s.toFinset t.toFinset := by
    simp; exact h
  apply T₀ at h'
  have h₀ : Disjoint s.toFinset t.toFinset := by
    simp; exact h.disjoint
  have h₁ : s.toFinset ∪ t.toFinset ⊆ Finset.univ (α := V) := by simp
  have h₂ : s.toFinset.card + t.toFinset.card ≤ Fintype.card V := by
    rw [← Finset.card_union_eq_card_add_card] at h₀
    exact le_of_eq_of_le h₀.symm (Finset.card_le_card h₁)
  have h₃ : (s.toFinset.card + t.toFinset.card) ^ 2 ≤ Fintype.card V ^ 2 :=
    Nat.pow_le_pow_left h₂ 2
  have h₄ : 4 * (s.toFinset.card * t.toFinset.card) ≤ (s.toFinset.card + t.toFinset.card) ^ 2 := by
    by_cases h₅ : s.toFinset.card ≤ t.toFinset.card <;> nlinarith
  linarith

[Snir Broshi]

Jakub Nowak said:

Not sure if we want that though? What's your motivation for working with infinite graphs Snir Broshi? From my experience working with encard is quite annoying.

I have the opposite experience: working with Fintype/Finset/DecidableRel is annoying, and Nat.card/ENat.card/Set.ncard/Set.encard is great.
Also Mathlib encourages generalizing.

[Jakub Nowak]

Interesting, my main problem is that tactics like simp +arith or omega deal very well with Nat, but perform poorly with ENat.

[Ilmārs Cīrulis]

The proof of the first theorem. Probably ugly. :sweat_smile:

import Mathlib

namespace SimpleGraph
variable {V : Type*} [instV : DecidableEq V] {G : SimpleGraph V} [instG : DecidableRel G.Adj]

theorem IsBipartiteWith.edgeSet_ncard_le_of_finsets {s t : Finset V} (hG : G.IsBipartiteWith ↑s ↑t) :
    G.edgeSet.Finite ∧ G.edgeSet.ncard ≤ s.card * t.card := by
  revert instG hG G
  induction s using Finset.cons_induction with
  | empty =>
    intros G instG hG
    have hG₀ : G = ⊥ := by
      ext x y; simp; intros hxy; apply hG.mem_of_adj at hxy; simp at hxy
    subst G; simp
  | cons a s h iH =>
    intros G instG hG
    set G' : SimpleGraph V :=
      ⟨(fun x y => G.Adj x y ∧ x ≠ a ∧ y ≠ a),
       by intros x y hxy; tauto,
       by intros x h; exact G.irrefl h.1⟩
    simp at hG
    have instG' : DecidableRel G'.Adj := by
      simp [G']; intros x y; simp; have inst := instG x y; exact instDecidableAnd
    have hG' : G'.IsBipartiteWith ↑s ↑t := by
      constructor
      · have h₀ := hG.disjoint
        simp at h₀; simp; exact h₀.2
      · intros x y hxy; simp
        have h₀ := hG.mem_of_adj
        simp at h₀; simp [G'] at hxy
        obtain ⟨h₁, h₂, h₃⟩ := hxy
        apply h₀ at h₁
        grind
    obtain ⟨hG'₀, hG'₁⟩ := @iH G' instG' hG'
    have h₀ : G.edgeSet = G'.edgeSet ∪
        (t.filter (G.Adj a)).map ⟨fun u => s(u, a), by intros u w; simp; grind⟩ := by
      simp [G']; ext e; simp; constructor <;> intro h₁
      · cases e; rename_i x y; simp at *; simp [h₁]
        cases (instV x a) <;> cases (instV y a) <;> rename_i h₂ h₃
        · simp [h₂, h₃]
        · simp [Ne.symm h₂, h₃]; subst a
          have h₃ := hG.mem_of_adj h₁.symm; simp [h₂] at h₃
          simp [h₁.symm]; obtain h₃ | ⟨h₃, h₄⟩ := h₃
          · exact h₃
          · have h₅ := hG.disjoint (x := {y}) (by simp) (by simp; exact h₃)
            simp at h₅
        · simp [h₂, Ne.symm h₃]; subst a; simp [h₁]
          have h₄ := hG.mem_of_adj h₁; simp [h₃] at h₄
          obtain h₄ | ⟨h₄, h₅⟩ := h₄
          · exact h₄
          · have h₆ := hG.disjoint (x := {x}) (by simp) (by simp; exact h₄)
            simp at h₆
        · simp [h₂, h₃]; subst x y; exact G.irrefl h₁
      · cases e; rename_i x y; simp at h₁ ⊢
        obtain h₁ | h₁ := h₁
        · exact h₁.1
        · obtain ⟨w, h₁, ⟨h₂, h₃⟩ | ⟨h₂, h₃⟩⟩ := h₁
          · subst w a; exact h₁.2.symm
          · subst w a; exact h₁.2
    rw [h₀]; simp [hG'₀]
    constructor
    · apply Set.Finite.image (fun u => s(u, a))
      apply Set.Finite.inter_of_left
      exact Set.finite_mem_finset t
    · have h₁ : {x | x ∈ t ∧ G.Adj a x}.Finite := by
        apply Set.Finite.inter_of_left
        apply Finset.finite_toSet
      have h₂ : Finite ↑{x | x ∈ t ∧ G.Adj a x} := h₁
      have h₃ : ((fun u => s(u, a)) '' {x | x ∈ t ∧ G.Adj a x}).Finite := by
        exact Set.Finite.image (fun u => s(u, a)) h₁
      have h₄ : Finite ↑((fun u => s(u, a)) '' {x | x ∈ t ∧ G.Adj a x}) := h₃
      rw [Set.ncard_union_eq (hs := hG'₀) (ht := h₄)]
      · simp [h]; rw [Nat.succ_mul]
        have h₅ : ((fun u => s(u, a)) '' {x | x ∈ t ∧ G.Adj a x}).ncard ≤ {x | x ∈ t ∧ G.Adj a x}.ncard := by
          apply Set.ncard_image_le
          exact h₁
        have h₆ : {x | x ∈ t ∧ G.Adj a x}.ncard ≤ (SetLike.coe t).ncard := by
          apply Set.ncard_inter_le_ncard_left
          exact Set.finite_mem_finset t
        simp at h₆
        linarith
      · rw [Set.disjoint_iff_inter_eq_empty]
        ext e; cases e; rename_i x y; simp; grind


theorem IsBipartiteWith.encard_edgeSet_le {s t : Set V} (h : G.IsBipartiteWith s t) :
    G.edgeSet.encard ≤ s.encard * t.encard := by
  by_cases hst : s.Finite ∧ t.Finite
  · obtain ⟨hs, ht⟩ := hst
    have inst_s := hs.fintype; have inst_t := ht.fintype
    have hs' : s = ↑(s.toFinset) := by simp
    have ht' : t = ↑(t.toFinset) := by simp
    rw [hs', ht'] at h
    apply IsBipartiteWith.edgeSet_ncard_le_of_finsets at h
    obtain ⟨h₀, h₁⟩ := h
    have h₂ : G.edgeSet.encard = ↑G.edgeSet.ncard := (Set.Finite.cast_ncard_eq h₀).symm
    have h₃ : s.encard = ↑(s.toFinset.card) := Set.encard_eq_coe_toFinset_card s
    have h₄ : t.encard = ↑(t.toFinset.card) := Set.encard_eq_coe_toFinset_card t
    rw [h₂, h₃, h₄]; norm_cast
  · have hst' : s.Infinite ∨ t.Infinite := by tauto
    obtain hs | ht := hst'
    · simp [hs]
      by_cases ht₀ : t.encard = 0
      · simp [ht₀]; ext x y; simp; intro hxy
        apply h.mem_of_adj at hxy; simp at ht₀; simp [ht₀] at hxy
      · simp [ht₀]
    · simp [ht]
      by_cases hs₀ : s.encard = 0
      · simp [hs₀]; ext x y; simp; intro hxy
        apply h.mem_of_adj at hxy; simp at hs₀; simp [hs₀] at hxy
      · simp [hs₀]

[Ilmārs Cīrulis]

The Decidable instances can be "removed" by use of Classical, I believe. I left them here for now.

[Ilmārs Cīrulis]

The proof of IsBipartite.four_mul_encard_edgeSet_le should be much easier, but i'm taking a rest.

[Ilmārs Cīrulis]

Here (on Github) is the proof with linter warnings (except those about Decidables in type) fixed.

And next to it in the same folder is my try to use Classical - to completely get rid of linter warnings.

I will think how to refactor it somehow, to make it into smaller parts. :thinking:

[Ilmārs Cīrulis]

I didn't want to post these big proofs here, as they take so much space...

[Kevin Buzzard]

Jakub Nowak said:

Interesting, my main problem is that tactics like simp +arith or omega deal very well with Nat, but perform poorly with ENat.

If you write a test suite of 5 or so goals which you are finding annoying to prove about ENat then you might be able to find someone who's prepared to write a tactic which will make your life easier. The general algorithm might be "case every variable for being a natural or infinity, simp the infinities away, then norm_cast back into Nat and use omega" and it could be called eomega or whatever. But it starts with the test suite of goals which you're finding annoying and want to be one-liners.

[Jakub Nowak]

Kevin Buzzard said:

If you write a test suite of 5 or so goals which you are finding annoying to prove about ENat then you might be able to find someone who's prepared to write a tactic which will make your life easier. The general algorithm might be "case every variable for being a natural or infinity, simp the infinities away, then norm_cast back into Nat and use omega" and it could be called eomega or whatever. But it starts with the test suite of goals which you're finding annoying and want to be one-liners.

That's a good point, but I'll just wait for non-terminal grind because there's a chance it will make many tactics obsolete, including this eomega.

[Ilmārs Cīrulis]

Refactored a proof (with Classical), now it looks better, in my opinion. :partying_face:
Although I didn't know how to name stuff (aux₀ to aux₄) best... :thinking:

Does Mathlib's graph theory part uses Classical much? As far as I looked, there are mostly instances of Decidable things, not Classical.

[Snir Broshi]

Using the lowercase tactic classical inside the proof is preferred, unless the statement of the theorem requires classical logic, in which case Decidable things are usually preferred.
But in your case this is only a problem since you're using Finset, as you can see your results with Set.encard are fine without any annoying classicals.

[Ilmārs Cīrulis]

Ok, good to know. :) Changed it to lowercase classical; only one was necessary.

[Snir Broshi]

Why do you need the Finset statements? The last two theorems are looking great with sets, do they need the previous theorems?

[Ilmārs Cīrulis]

I used the Finset statement (IsBipartiteWith.edgeSet_ncard_le_of_finsets) in the proof of IsBipartiteWith.encard_edgeSet_le - in the case when both sets are Finite. Should I think of some better approach?

[Ilmārs Cīrulis]

Are these two theorems about upper limit on number of edges in bipartite graph good for Mathlib? Should I try making a PR? :thinking:
Also, I thought a bit and decided that corresponding theorems or criterions for equality in these two cases aren't necessary in Mathlib (even if the inequalities are, possibly). Am I right?

I'm okay with it either way, no matter what consensus is. :thumbs_up:

[Ilmārs Cīrulis]

Another idea - replace the last theorem with this one (changeENat.card V to G.support.encard), making it stronger.

import Mathlib

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

theorem IsBipartite.four_mul_encard_edgeSet_le (h : G.IsBipartite) :
    4 * G.edgeSet.encard ≤ G.support.encard ^ 2 := by sorry

[Bhavik Mehta]

I think you should make a PR for them, they look useful!

[Ilmārs Cīrulis]

Is there a notion already in Mathlib of this "restriction" of vertices of G : SImpleGraph Vto G.support:

  set G' : SimpleGraph ↑G.support :=
    ⟨fun x y => G.Adj x.val y.val,
      by intros x y hxy; exact hxy.symm,
      by intros x hx; exact G.irrefl hx⟩

Maybe with some general Set V instead of G.support? That's one approach I have imagined for proving the last theorem with 4 * G.edgeSet.encard ≤ G.support.encard ^ 2.

[Ilmārs Cīrulis]

O, I found it: SimpleGraph.induce

[Mitchell Horner]

Ilmārs Cīrulis said:

Extremal graph theory, if such very broad answer is okay.

A few people have been talking about a TODO I left in Bipartite.lean to prove that a graph is bipartite if and only if it does not contain an odd cycle here and here and here and here.

Lots of this is written in terms of Walk.IsCycle right now but I hope to eventually see the statement in terms of containment a la G.IsBipartite ↔ ∀ n ≥ 2, Odd n → (cycleGraph n).Free G.

If you would like to get your hands dirty, contributing some equivalences that link cycleGraph and Walk.IsCycle is valuable work. I.e,

def Walk.IsCycle.toCopy {v} {p : G.Walk v v} (h : p.IsCycle) : Copy (cycleGraph p.length) G
def Walk.IsCycle.ofCopy (f : Copy (cycleGraph n) G) (i : Fin n) : G.Walk (f i) (f i)
theorem Walk.IsCycle.ofCopy_isCycle (f : Copy (cycleGraph n) G) (i : Fin n) : (Walk.IsCycle.ofCopy f i).IsCycle
theorem Walk.IsCycle.exists_iff : ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ n = p.length + 1 ↔ cycleGraph n ⊑ G

I proved one of these here.

Moreover, contributing equivalences that link a Copy of a simple graph to some predicate is valuable work that helps link some extremal graph theory problems to existing definitions.

[Snir Broshi]

Mitchell Horner said:

Moreover, contributing equivalences that link a Copy of a simple graph to some predicate is valuable work that helps link some extremal graph theory problems to existing definitions.

Does #33121 help?

[Mitchell Horner]

@Snir Broshi Yep.

[Kevin Buzzard]

Just to comment that discussing several different questions all under one generically-named thread makes for poor search later on. Perhaps someone wants to consider splitting off various questions here into other threads in this channel (any user can do this) and giving them more searchable names.

[Jakub Nowak]

Kevin Buzzard said:

any user can do this

Are you sure? Last time I've tried moving someone else messages it didn't work. Unless it works in #graph theory ?

[Aaron Liu]

it works within the same channel

[Rida Hamadani]

it even has a hotkey (press m while the message to be moved is highlighted)

[Ilmārs Cīrulis]

I tried to do that (splitting and etc.) but it seems I can't move my own messages.

[Vlad Tsyrklevich]

Mitchell Horner said:

theorem Walk.IsCycle.exists_iff : ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ n = p.length + 1 ↔ cycleGraph n ⊑ G

I hadn't seen this message until Snir just pointed me to it but I have this in #35255 (I'm busy for the next few days and then will update it to get it on the review queue.)