coloring

Stream: graph theory

[Arthur Paulino]

this lemma can be very helpful to prove lower bounds for the chromatic number

lemma chromatic_number_lower_bound (G' : simple_graph V) (h : G ≤ G') :
  G.chromatic_number ≤ G'.chromatic_number :=
begin
  sorry
end

[Kyle Miller]

That would follow from the fact that every coloring of G' gives a coloring of G by composing it with the (unimplemented?) induced graph homomorphism G ->g G'.

[Arthur Paulino]

I'm trying to prove this one:

lemma chromatic_number_le [fintype α] (C : G.proper_coloring α) :
  G.chromatic_number ≤ fintype.card α

But I couldn't find a simple example of how to deal with lattice infimums

[Arthur Paulino]

When I unfold the definition of chromatic_number I get a goal to which I don't know how to move towards

[Kyle Miller]

I think you can apply docs#Inf_le

[Arthur Paulino]

It says

invalid apply tactic, failed to unify
  Inf {n : ℕ | G.colorable n} ≤ fintype.card α
with
  Inf ?m_3 ≤ ?m_4
state:
V : Type u,
G : simple_graph V,
α : Type v,
_inst_1 : fintype α,
C : G.proper_coloring α
⊢ Inf {n : ℕ | G.colorable n} ≤ fintype.card α

[Yaël Dillies]

Yup because it's docs#cInf_le that you need here

[Arthur Paulino]

Baby step progress: https://github.com/leanprover-community/mathlib/blob/3998057d75c822c0e64824e3c446d923c3eb7426/src/combinatorics/simple_graph/coloring.lean

[Arthur Paulino]

There seems to be an obvious step here:

h: G.colorable (fintype.card α)
⊢ {n : ℕ | G.colorable n}.nonempty

[Arthur Paulino]

{card α} is not empty

[Arthur Paulino]

Got it.

@Kyle Miller some progress on the coloring as homomorphism branch: https://github.com/leanprover-community/mathlib/blob/dfacc1723b76a07129dc02ce34e5fbfc9076239e/src/combinatorics/simple_graph/coloring.lean

[Arthur Paulino]

I'm trying to produce a colored graph given the graph and a proper coloring for it (represented as a homomorphism)

variables {V : Type u} (G : simple_graph V)

abbreviation proper_coloring (α : Type v) := G →g complete_graph α

variables {G} {α : Type v} (C : G.proper_coloring α)

def proper_coloring.applied : simple_graph α := simple_graph.from_rel
  (λ c₁ c₂, G.adj ... ...)

I'm not being able to express the relation that will form the same structure from G but with colored vertices (of type α). How to recover the original structure?

[Arthur Paulino]

Oh, wait. Nevermind. The vertices can't be of type α

[Arthur Paulino]

Got this one

lemma zero_le_chromatic_number [nonempty V] [fintype α] (C : G.proper_coloring α) :
  0 < G.chromatic_number :=
begin
  rw [nat.lt_iff_add_one_le, chromatic_number, zero_add],
  apply le_cInf,
  { use fintype.card α,
    exact exists_fin_coloring_then_colorable C, },
  { intros n hn,
    by_contra h,
    simp at h,
    simp [h] at hn,
    rw colorable at hn,
    cases hn with α' hn,
    cases hn with hα' hn,
    cases hn with C' hf,
    simp at hf,
    let v := classical.arbitrary V, -- coloring this vertex requires at least 1 color
    have c := C' v,
    have hn : nonempty α', use c,
    tactic.unfreeze_local_instances,
    rw ← fintype.card_pos_iff at hn,
    rw hf at hn,
    exact nat.lt_asymm hn hn, },
end

[Yakov Pechersky]

In what cases, meaning under which type class constraints etc, will G.chromatic_number = 0? You can like use that together with nat.zero_le to prove this easier.

[Arthur Paulino]

According to the definition Kyle wrote:

/-- If `G` isn't colorable with finitely many colors, this will be 0. -/
noncomputable def chromatic_number (G : simple_graph V) : ℕ :=
  Inf { n : ℕ | G.colorable n }

But I guess if the graph has no vertices too

[Arthur Paulino]

Actually it's weird to talk about coloring of empty graphs since we're using homomorphisms and I'm not sure we can define functions on empty domains

[Yakov Pechersky]

What do you mean by inability to define functions on empty domains?

[Arthur Paulino]

This is the proposed definition of proper coloring:

abbreviation proper_coloring (α : Type v) := G →g complete_graph α

What happens if G has no vertices?

[Yakov Pechersky]

def f : fin 0 -> real := fun x, fin.elim0 x

[Eric Rodriguez]

there is a unique function α → β where α is empty, which is the elimination principle

[Eric Rodriguez]

import logic.is_empty

def asda {α β} [h : is_empty α] : α → β := h.elim

example {α β} [h : is_empty α] : ∀ f : α → β, f = asda :=
begin
  intro, funext, exact h.elim x
end

[Arthur Paulino]

I see

[Arthur Paulino]

So how would I state the condition for the chromatic number to be zero?
G.chromatic_number = 0 ↔ empty V \or ...

[Eric Rodriguez]

I mean, assuming fintype it's just empty V, and I can't think of a good condition on infinite graphs to have a finite colouring

[Eric Rodriguez]

(off the top of my head)

[Yakov Pechersky]

I wouldn't state it as an iff initially. Just one (or several) lemmas with some TC assumption, that says that G.chromatic_number = 0.

[Yakov Pechersky]

Another helpful API lemma would be that [subsingleton V] should imply chromatic_number <= 1

[Arthur Paulino]

@Yakov Pechersky how can I make use of subsingleton V to prove that G is colorable with at most 1 color?

V: Type u
G: simple_graph V
α: Type v
_inst_1: subsingleton V
C: G.proper_coloring α
⊢ G.colorable 1

[Eric Rodriguez]

easy way is to case on is_empty α or inhabited α

[Arthur Paulino]

Do you guys think it makes sense to define a graph with an applied coloring? I thought of a simple_graph whose vertices are 2-tuples of V × α:

def proper_coloring.applied : simple_graph (V × α) := simple_graph.from_rel
  (λ (p₁ : V × α) (p₂ : V × α), p₁.2 = C p₁.1 ∧ p₂.2 = C p₂.1 ∧ G.adj p₁.1 p₂.1)

C v is the color of v

[Arthur Paulino]

This looks a bit like something the homomorphism API would provide :thinking:

[Arthur Paulino]

Alright, I think I got some nice progress this time.
Please let me know what you think: https://github.com/leanprover-community/mathlib/blob/graph-coloring-homomorphism/src/combinatorics/simple_graph/coloring.lean

Help is appreciated!

[Kyle Miller]

(Btw, I hadn't mentioned one motivation for homomorphisms, which is for fractional colorings. I guess they can be represented by graph homomorphisms to Kneser graphs, complete graphs being a special case, so with homomorphisms we easily get a fractional coloring from a coloring. Just leaving this comment here in case someone searches Zulip for "fractional coloring".)

[Kyle Miller]

For

lemma coloring.valid (v w : V) (h : G.adj v w) : C v ≠ C w :=
  C.map_rel h

and

noncomputable def chromatic_number (G : simple_graph V) : ℕ :=
  Inf { n : ℕ | G.colorable n }

the formatting rule is that types are indented, but bodies are not (something that took me a bit of getting used to.

lemma coloring.valid (v w : V) (h : G.adj v w) : C v ≠ C w :=
C.map_rel h

noncomputable def chromatic_number (G : simple_graph V) : ℕ :=
Inf { n : ℕ | G.colorable n }

[Kyle Miller]

For the proof of exists_fin_coloring_then_colorable, it would be easier to use the definition of colorable directly and use C at the beginning.

[Kyle Miller]

For empty_graph_trivially_colorable, it might be worth pulling out a definition for a coloring of a graph with no vertices, like def colorable_of_empty {V : Type*} (G : simple_graph V) (he : is_empty V) : G.coloring α := sorry

[Kyle Miller]

Another coloring that might help is the "tautological" coloring where vertices are colored by themselves. def self_coloring (G : simple_graph V) : G.coloring V. When V is a fintype this can be used to prove that {n | G.colorable n}.nonempty, which would also be a good lemma to have.

[Kyle Miller]

I think I was wrong to suggest defining colorable the way I did due to some universe variables reasons -- this shouldn't affect your work in the meantime, but I think I'll at some point soon do some refactoring of the branch to correct this.

[Kyle Miller]

(Thanks for pursuing this project!)

[Arthur Paulino]

Thanks for the input!
One thing I want to say is that since we're going straight into a definition of coloring as a graph homomorphism, it didn't make much sense to state intermediary definitions such as partial/complete/proper/feasible (because every coloring that we state is feasible according to Lewis' book). That's why I renamed every occurrence of "proper_coloring" to simply "coloring". Ultimately it's the coloring that we're always interested in anyways.

[Kyle Miller]

Oh right, I didn't notice the change (I usually call non-proper colorings "vertex labelings"). Make sure the doc strings mention that these are proper colorings, since some people do make a distinction. (Also be prepared to rename it proper_coloring if consensus lands on that.)

[Kyle Miller]

Also, docs#complete_graph has a reminder that the definition should be

abbreviation coloring (α : Type v) := G →g (⊤ : simple_graph α)

That ⊤ is the "top" of the simple graph lattice.

[Arthur Paulino]

Kyle Miller said:

For the proof of exists_fin_coloring_then_colorable, it would be easier to use the definition of colorable directly and use C at the beginning.

I'm pretty sure I didn't understand what you meant here. If I do rw colorable, use C, Lean says

failed to instantiate goal with C
state:
V : Type u,
G : simple_graph V,
α : Type v,
_inst_1 : fintype α,
C : G.coloring α
⊢ ∃ (α_1 : Type u_1) [_inst_1_1 : fintype α_1] (C : G.coloring α_1), fintype.card α_1 ≤ fintype.card α

[Kyle Miller]

Incidentally, this would be a vertex labeling (a non-proper coloring)

abbreviation labeling (α : Type v) := G →g (⊥ : simple_graph α)

[Kyle Miller]

I meant use for the third part of the existential. Start with use α

[Kyle Miller]

The final goal will be docs#le_refl

[Arthur Paulino]

When I try use α it says

failed to instantiate goal with α
state:
V : Type u,
G : simple_graph V,
α : Type v,
_inst_1 : fintype α,
C : G.coloring α
⊢ ∃ (α_1 : Type u_1) [_inst_1_1 : fintype α_1] (C : G.coloring α_1), fintype.card α_1 ≤ fintype.card α

[Arthur Paulino]

Maybe it's related to the universe issues you mentioned?

[Kyle Miller]

Oh, indeed. Ok, the quick fix is to use the rw you have already, then rw it backwards.

[Kyle Miller]

This will launder out the universe variable

[Arthur Paulino]

Like this?

  rw colorable,
  rw ←colorable,
  rw colorable,

[Arthur Paulino]

Same issue as before

[Kyle Miller]

Sorry I wasn't specific enough, I meant the one that's still pushed to GitHub, with rw colorable_iff_nonempty_fin_coloring

[Kyle Miller]

(That rewrites it into a form without the universe variable, and when you rewrite it back you're free to use any universe you want.)

[Arthur Paulino]

Now it accepts α

[Arthur Paulino]

What's the right way to use this: _inst_1: fintype α without relying on those automatically provided names?

[Arthur Paulino]

In other words, is there a way to do it that's not use _inst_1?

[Kyle Miller]

There are a few options. One is fsplit, assumption

[Kyle Miller]

(fsplit is like split but it keeps things in order)

[Kyle Miller]

use uses fsplit anyway, if I remember correctly

[Kyle Miller]

If the fintype is in the instance cache, you might be able to get away with use [infer_instance]

[Arthur Paulino]

lemma exists_fin_coloring_then_colorable [fintype α] (C : G.coloring α) :
G.colorable (fintype.card α) :=
begin
  rw colorable_iff_nonempty_fin_coloring,
  rw ← colorable_iff_nonempty_fin_coloring,
  rw colorable,
  use α,
  use [infer_instance],
  use C,
end

is accepted :+1:

[Kyle Miller]

use [α, infer_instance, C] is how you can do multiple uses

[Kyle Miller]

and you don't need to unfold the definition of colorable, so you can remove the third line

[Arthur Paulino]

Nice

[Kyle Miller]

The formatting rule is that types get indented:

lemma exists_fin_coloring_then_colorable [fintype α] (C : G.coloring α) :
  G.colorable (fintype.card α) :=
begin
  ...
end

[Arthur Paulino]

About the "coloring" vs "proper_coloring" issue, what is your suggestion?

[Kyle Miller]

I say leave it until someone wants to put it up for a vote. I'm fine with "coloring" myself.

[Arthur Paulino]

Alright, I will just clarify it in the docstring eve further then

[Arthur Paulino]

I'm gonna follow up on the other points you mentioned. Will get back soon

[Arthur Paulino]

Done https://github.com/leanprover-community/mathlib/blob/graph-coloring-homomorphism/src/combinatorics/simple_graph/coloring.lean

For the 3 last lemmas, I don't know how to proceed :sad:

[Kyle Miller]

I guess we're able to state what the chromatic polynomial is now (modulo some instance definitions):

noncomputable
def chromatic_poly (G : simple_graph V) (R : Type*) [ring R] : polynomial R :=
∑ G' in finset.univ.filter (λ G', G' ≤ G),
  (-1) ^ (G'.edge_finset.card) * polynomial.X ^ fintype.card (quot G'.adj)

lemma chromatic_poly_eq (G : simple_graph V) (n : ℕ) :
  polynomial.eval (n : ℤ) (G.chromatic_poly ℤ) = fintype.card (G.coloring (fin n)) :=
sorry

I think it should be possible to formalize something like the contradiction-deletion proof (even though we only have simple graphs) by making an auxiliary chromatic polynomial that takes two graphs and sums over the graphs between -- deletion corresponds to deleting an edge from the top graph, and contraction corresponds to adding an edge to the bottom graph. You'd also define a version of coloring for a graph/subgraph pair, where adjacent vertices of the subgraph must get the same color, but vertices not adjacent in the subgraph must get different colors. The auxiliary polynomial counts these kinds of colorings.

Then you induct on the difference in the number of edges of the two graphs, choose an edge that's only in the top graph, and split the sum up into two, one for deletion and one for contraction. This is a difference, and you need to see this is actually the cardinality of the difference of two sets of colorings.

noncomputable
def chromatic_poly.aux (G₀ G : simple_graph V) (R : Type*) [ring R] :
  polynomial R :=
∑ G' in finset.univ.filter (λ G', G₀ ≤ G' ∧ G' ≤ G),
  (-1) ^ ((G'.edge_finset \ G₀.edge_finset).card) * polynomial.X ^ fintype.card (quot G'.adj)

[Kyle Miller]

This auxiliary polynomial is actually has to do with mobius inversion on the lattice of spanning subgraphs, so maybe working out that theory of convolution products on lattices would be a useful. Henry Crapo has a couple of papers on that (including one on the Tutte polynomial) from 1968 and 1969.

[Yaël Dillies]

For the instance, just leaving _ in the use/refine should trigger typeclass inference.

[Arthur Paulino]

Kyle, I'm gonna read your changes in more detail and then try to move the things you suggested

[Kyle Miller]

(Regarding chromatic polynomials, those can wait until later. There's a fair amount of work to develop them properly still.)

[Arthur Paulino]

Do you think we could make a smaller PR without them? I think we've already got something worth merging

[Kyle Miller]

Yeah, just remove the things about chromatic polynomials for now. (Including open_locale big_operators and the import for algebra.big_operators.basic)

[Arthur Paulino]

My intuition is making me a bit reluctant about moving complete_bipartite_graph into basic.lean

[Arthur Paulino]

because it's a specific graph structure

[Arthur Paulino]

(and there are many particular structures)

[Arthur Paulino]

I'm gonna put it inside basic.lean and then we can decide later, when the PR is open

[Arthur Paulino]

https://github.com/leanprover-community/mathlib/pull/10287

[Arthur Paulino]

Hey Kyle, would it be better if we had a separate bipartite.lean file in which we put the complete_bipartite_graph builder, a is_bipartite definition and a proof that a complete bipartite graph is bipartite?

Then in the coloring.lean file we'd prove that the chromatic number of any bipartite graph is 2

[Arthur Paulino]

Something like this:
https://github.com/leanprover-community/mathlib/pull/10301

[Arthur Paulino]

Eventually we can generalize this to n-partite graphs, but I think this structure is slightly better for a solid first step

[Mauricio Collares]

Looks like you already kave k-colorable graphs, which is basically the same definition as being k-partite. Adding some functions to get the color classes (i.e., k-partition) out of a k-colorable graph and vice-versa should make it pretty comfortable to work with k-partite graphs.

[Kyle Miller]

@Mauricio Collares What I was thinking is how it's the equivalence between indexed families of types \iota -> Type and functions from a type to some labeling type \alpha -> \iota. It's not hard going back and forth, but it's also not completely painless (you can't really round trip the transformation).

It makes a lot of sense to define an \iota-partition of a graph to be an \iota-coloring (like \alpha -> \iota), and that's even how we'd defined them in a very old branch, though maybe just with fin 2 for bipartitions.

It would be nice to have an interface for \iota -> Type style colorings, too (though as \iota -> set V). I'm not sure how we write \iota-indexed partitions of types in mathlib, but in any case it would be a function c : \iota -> set V whose images are disjoint and their union is all of V, and pairs of vertices in each c i are non-adjacent.

The equivalence between \iota-colorings and these sorts of partitions would implement color classes.

[Mauricio Collares]

In "paper math" we'd have the coloring be a function $\chi \colon V \to \iota$ with some restriction that $c(u) \neq c(v)$ whenever uv is an edge (or the equivalent thing stated as a homomorphism, like @Arthur Paulino is doing) and your function c would associate to every $i \in \iota$ the inverse image $\chi^{-1}(i)$. So, a couple of naïve questions: This doesn't round trip for type theory-related reasons, I think? Or you're saying mathlib already has this sort of equivalence in greater generality somewhere, but it doesn't round trip in general? It would certanly be very useful to have some interface to be able to pass between the two forms easily.

[Mauricio Collares]

Speaking of which, I would like to try my hand at something math-simple like Turán's theorem in the near future, to get some practice. What's the protocol for that? On what branch do I base the work upon?

[Mauricio Collares]

(I know math-simple stuff can be very hard in Lean!)

[Kyle Miller]

The round tripping failure's just when you have an actual indexed family of types, rather than subsets of the same type. Having the indexed family beset V valued saves us here. (Otherwise it's just that there's an equivalence of categories.)

[Arthur Paulino]

Just for the record, the coloring as a homomorphism was Kyle's recommendation!

[Kyle Miller]

The way you go from $c:\iota \to \mathrm{Type}$ to an $\iota$-valued function to define $(\sum_{i\in\iota} c(i))\to \iota$ by sigma.fst, and to go back from a $\chi:V\to\iota$ you define $c$ by $c(i) = \{v : V // \chi( v) = i\}$. The sigma of all these subtypes isn't provably equal to V (and it's likely not equal).

[Kyle Miller]

Mauricio Collares said:

Speaking of which, I would like to try my hand at something math-simple like Turán's theorem in the near future, to get some practice. What's the protocol for that? On what branch do I base the work upon?

It seems like you can base your work on the master branch for this, though it looks like you'll need cliques, which Yael seems to be working on. You could probably define what you need and then post hoc try to merge things together.

Once you have an invite for the mathlib repository (just ask, and an maintainer will bestow one) you can do development in your own branch, named something like mauricio_turan

[Arthur Paulino]

According to what Mauricio said, it seems like we don't need to define bipartite graphs at all. So instead have a raw definition for k-partitionable graphs and prove that k-partitionable graphs are k-colorable? And in the middle way provide the interchanging functions Mauricio mentioned?

[Arthur Paulino]

@Kyle Miller do you think these can be useful?

def coloring.color_rel: V → V → Prop := λ v w, C v = C w

lemma coloring.color_rel_reflexive : reflexive (C.color_rel) :=
by obviously

lemma coloring.color_rel_symmetric : symmetric (C.color_rel) :=
by {intros _ _ h, exact eq.symm h, }

lemma coloring.color_rel_transitive : transitive (C.color_rel) :=
by {intros _ _ _ hvw hvu, exact eq.trans hvw hvu, }

def coloring.color_rel_equivalence : equivalence C.color_rel :=
⟨C.color_rel_reflexive, C.color_rel_symmetric, C.color_rel_transitive⟩

[Arthur Paulino]

I'm trying to build up what we might need to define a function that returns the partitions induced by a coloring

[Kyle Miller]

That happens to be docs#setoid.ker applied to C

[Kyle Miller]

A setoid is a relation along with a proof that it's an equivalence relation

[Kyle Miller]

I also found docs#indexed_partition for indexed partitions, but it's not quite right since we don't want the some field

[Kyle Miller]

This is a way to define color classes:

def coloring.color_class (C : G.coloring α) (c : α) : set V := C ⁻¹' {c}  -- or equivalently {v | C v = c}

(I don't know much about setoid.ker and the kinds of partitions it gives you.)

[Kyle Miller]

Maybe it makes sense to define simple_graph.partition like indexed_partition along with the requirement that vertices from the same partition are non-adjacent, and then we can define an equivalence between G.partition \alpha and G.coloring \alpha.

[Kyle Miller]

so, generalizing bipartition to this notion of partitioning a graph into an indexed set of vertices

[Arthur Paulino]

I was expecting to have something that we could feed with an equivalence relation and a set and it would return the equivalence classes from that set

[Kyle Miller]

I guess there's another approach, which is to prove that the color_classes form a partition of V as a lemma, and then create a constructor for coloring that uses the indexed-family-of-sets interface (def coloring.of_partition ...).

(One reason to have both coloring and partition would be to have some things be true by definitional equality, but I'm not sure when or where that might matter yet.)

[Kyle Miller]

The setoid interface also has something about getting the set of partitions, which you can get somehow from the setoid.ker C

[Kyle Miller]

There's a design question in all of this: in an n-partite graph, are the partitions distinguishable?

I don't really have any theorems in mind where you need the partitions to be indistinguishable, so I've been thinking about indexed sets.

[Arthur Paulino]

I'm not understanding the setoid.ker API very well

[Kyle Miller]

Supposing there's a reason for both, then the way it could work is coloring is specifically for distinguishable partitions of vertices and partition is specifically for indistinguishable partitions (so has a set (set V) to partition it). There is a map from coloring to partition from forgetting colors and taking the color classes.

(There's surprisingly a map from partition to coloring by coloring each vertex with the partition the vertex is a member of.)

[Kyle Miller]

docs#setoid.ker is exactly the thing you proved, but wrapped up as a setoid. eq on C is \lambda v w, C v = C w

[Kyle Miller]

docs#setoid.ker_def proves that

[Arthur Paulino]

But by saying setoid.ker C, I'm feeding it with something i've just built. How does it know C forms an equivalence relation?

[Arthur Paulino]

It just checks this?
(setoid.ker f).rel x y ↔ f x = f y

[Kyle Miller]

def coloring.color_setoid : setoid V := setoid.ker C
def coloring.color_rel : V → V → Prop := (coloring.color_setoid C).rel
lemma coloring.color_rel_equivalence : equivalence C.color_rel :=
(coloring.color_setoid C).iseqv
lemma coloring.color_rel_def (v w : V) :
  coloring.color_rel C v w ↔ C v = C w := iff.rfl

[Kyle Miller]

The idea is that every function defines an equivalence relation given by whether things map to the same thing.

[Arthur Paulino]

AAAAh!

[Kyle Miller]

I don't think you really need to go through equivalence relations, though, since for functions we call the partitions "preimages"

[Arthur Paulino]

Yeah, not really. At least not for now. My motivation was just getting to the point of having an equivalence relation at hand, then search on mathlib API for something that would partition sets for me

[Arthur Paulino]

:thinking:

def coloring.color_class (c : α) : set V := {v : V | C v = c}

def coloring.color_classes : set (set V) := {(C.color_class c) | c : α}

[Arthur Paulino]

@Kyle Miller I'm trying to create a coloring from a partition with your idea of coloring every vertex in a subset of vertices with the subset itself but i'm not being able to figure out that last sorry

https://github.com/leanprover-community/mathlib/pull/10321

[Arthur Paulino]

hn states that v and w belong to the same subset:

hn: G.subset_of_vertex hp v = G.subset_of_vertex hp w

I also have sv: set V, h_sv_in_P: sv ∈ P and h_v_in_sv: v ∈ sv

The goal is to prove that w ∈ sv

[Kyle Miller]

lemma subset_of_vertex_spec (hp : G.is_partition P) (v : V) :
  G.subset_of_vertex hp v ∈ P ∧ v ∈ G.subset_of_vertex hp v :=
begin
  obtain ⟨⟨h1, h2⟩, h3⟩ := (hp.valid.2 v).some_spec,
  exact ⟨h1, h2.1⟩,
end

lemma different_subsets_of_adjacent {v w : V} (hp : G.is_partition P) (h : G.adj v w) :
  G.subset_of_vertex hp v ≠ G.subset_of_vertex hp w :=
begin
  have aa := hp.valid.2,
  intro hn,
  have hv := G.subset_of_vertex_spec hp v,
  have hw := G.subset_of_vertex_spec hp w,
  have h1 := hp.independent _ hv.1,
  rw ←hn at hw,
  exact h1 v hv.2 w hw.2 (G.ne_of_adj h) h,
end

[Arthur Paulino]

Wow

[Arthur Paulino]

Time to learn

[Arthur Paulino]

Thank you very much!

[Kyle Miller]

@Arthur Paulino I think in this case it would be better if partition were a struct that held the set, rather than being a predicate:

/-
Copyright (c) 2021 Arthur Paulino. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, Kyle Miller
-/

import combinatorics.simple_graph.coloring
import data.setoid.partition
import order.antichain

universes u v

namespace simple_graph
variables {V : Type u} (G : simple_graph V)

structure partition :=
(parts : set (set V))
(is_partition : setoid.is_partition parts)
(independent : ∀ (s ∈ parts), is_antichain G.adj s)

namespace partition
variables {G} (P : G.partition)

def part_of_vertex (v : V) : set V :=
classical.some (P.is_partition.2 v)

lemma part_of_vertex_mem (v : V) : P.part_of_vertex v ∈ P.parts :=
begin
  obtain ⟨h, -⟩ := (P.is_partition.2 v).some_spec.1,
  exact h,
end

lemma mem_part_of_vertex (v : V) : v ∈ P.part_of_vertex v :=
begin
  obtain ⟨⟨h1, h2⟩, h3⟩ := (P.is_partition.2 v).some_spec,
  exact h2.1,
end

lemma part_of_vertex_ne_of_adj {v w : V} (h : G.adj v w) :
  P.part_of_vertex v ≠ P.part_of_vertex w :=
begin
  have aa := P.is_partition.2,
  intro hn,
  have hw := P.mem_part_of_vertex w,
  rw ←hn at hw,
  have h1 := P.independent _ (P.part_of_vertex_mem v) _ (P.mem_part_of_vertex v),
  exact h1 w hw (G.ne_of_adj h) h,
end

def to_coloring : G.coloring (set V) :=
coloring.mk P.part_of_vertex
begin
  intros _ _ hvw,
  exact P.part_of_vertex_ne_of_adj hvw,
end

end partition

end simple_graph

[Arthur Paulino]

Makes sense. It was my approach because if we have "a coloring" then we'd like to have "a partition"

[Arthur Paulino]

I'm gonna try to create a from_coloring function

[Kyle Miller]

There's a stricter version of to_coloring by the way, where the target is parts coerced to a type. You can use it to show that an n-partite graph is n-colorable:

def to_coloring : G.coloring P.parts :=
coloring.mk (λ v, ⟨P.part_of_vertex v, P.part_of_vertex_mem v⟩)
begin
  intros _ _ hvw,
  rw [ne.def, subtype.mk_eq_mk],
  exact P.part_of_vertex_ne_of_adj hvw,
end

lemma to_colorable [fintype P.parts] :
  G.colorable (fintype.card P.parts) :=
coloring.to_colorable P.to_coloring

[Arthur Paulino]

Now I'm stuck with some (apparently simple) sorrys

[Arthur Paulino]

I'm trying to prove that the set of color classes is a partition. I've successfully proved that it's an independent set w.r.t. G.adj tho

[Arthur Paulino]

The second sorry can actually be replaced by obviously

[Kyle Miller]

You might instead try proving C.color_classes = (setoid.ker C).classes, and then this partition lemma would be a quick consequence

[Kyle Miller]

(but don't let that stop you from proving this lemma directly since it's not a bad exercise in itself)

[Arthur Paulino]

I'm struggling with things that I believe should be simple.
For instance, in this state:

V: Type u
G: simple_graph V
α: Type v
C: G.coloring α
v: V
⊢ ¬{v_1 : V | ⇑C v_1 = ⇑C v} = ∅

That set on the left obviously contains v and thus is not empty

[Arthur Paulino]

And on this state:

V: Type u
G: simple_graph V
α: Type v
C: G.coloring α
vw: V
hcvw: ⇑C v = ⇑C w
⊢ {v : V | ⇑C v = ⇑C w} = {v_1 : V | ⇑C v_1 = ⇑C v}

I want to substitute C v by C w using hcvw but the subst tactic doesn't work when I do subst hcvw,
It says:

subst tactic failed, hypothesis 'hcvw' is not of the form (x = t) or (t = x)

[Kevin Buzzard]

docs#set.ne_empty_iff_nonempty helps with the first one, and just rw hcvw for the second?

[Kevin Buzzard]

oh, it's under a binder maybe? simp_rw [hcvw]?

[Kevin Buzzard]

I never know what is a binder and what isn't.

[Kyle Miller]

(subst is a way to eliminate a variable completely, and neither C v nor C w are variables.)

[Yakov Pechersky]

It's tricksy, the v on the LHS of the goal is not the v in hcvw, btw.

[Kevin Buzzard]

I guess congr' would also do it for the second one

[Yakov Pechersky]

For set equality, good ole' ext, simp should work. With ext, simp [hcvw].

[Arthur Paulino]

Basically all of your suggestion for the second one worked :+1:

[Arthur Paulino]

    rw ← set.not_nonempty_iff_eq_empty,
    simp only [not_not],
    use v,
    obviously,

did the trick for the first one. thanks everyone!

[Kyle Miller]

Try using dsimp to see what that last goal is before obviously (which is more often written as tidy, by the way). There's a short proof that doesn't use such a heavy tactic.

Also, the simp only can be replaced by rw, so you can merge the first two lines into a rw [..., ...]

[Arthur Paulino]

⇑C v = ⇑C v so a refl did it

[Kyle Miller]

I didn't look into why exactly, but if you don't have dsimp it seems you need exact rfl rather than refl. (Maybe because the goal isn't syntactically a relation?)

[Mario Carneiro]

that will do it

[Mario Carneiro]

refl looks at the (syntactic) type of the expression to determine which reflexivity lemma to apply, it's not always rfl

[Arthur Paulino]

exact rfl worked too :tada:

[Arthur Paulino]

Alright, the PR has been updated with content for partitions:
https://github.com/leanprover-community/mathlib/pull/10287

[Arthur Paulino]

Kyle do you think we could remove the formalization that's specifically about bipartite graphs since we have a generalization on k-partites on the roadmap?