## Stream: graph theory

### Topic: coloring

#### Arthur Paulino (Nov 08 2021 at 20:40):

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 (Nov 08 2021 at 20:53):

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 (Nov 08 2021 at 21:01):

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 (Nov 08 2021 at 21:02):

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

#### Kyle Miller (Nov 08 2021 at 21:25):

I think you can apply docs#Inf_le

#### Arthur Paulino (Nov 08 2021 at 21:39):

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 (Nov 08 2021 at 21:55):

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

#### Arthur Paulino (Nov 09 2021 at 03:02):

There seems to be an obvious step here:

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


#### Arthur Paulino (Nov 09 2021 at 03:03):

{card α} is not empty

#### Arthur Paulino (Nov 09 2021 at 03:27):

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 (Nov 10 2021 at 00:24):

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 (Nov 10 2021 at 00:35):

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

#### Arthur Paulino (Nov 10 2021 at 02:24):

Got this one

lemma zero_le_chromatic_number [nonempty V] [fintype α] (C : G.proper_coloring α) :
0 < G.chromatic_number :=
begin
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 (Nov 10 2021 at 03:48):

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 (Nov 10 2021 at 12:51):

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 (Nov 10 2021 at 12:52):

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 (Nov 10 2021 at 12:53):

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

#### Arthur Paulino (Nov 10 2021 at 12:54):

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 (Nov 10 2021 at 12:57):

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

#### Eric Rodriguez (Nov 10 2021 at 12:57):

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

#### Eric Rodriguez (Nov 10 2021 at 12:59):

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


I see

#### Arthur Paulino (Nov 10 2021 at 13:03):

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

#### Eric Rodriguez (Nov 10 2021 at 13:04):

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 (Nov 10 2021 at 13:04):

(off the top of my head)

#### Yakov Pechersky (Nov 10 2021 at 13:04):

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 (Nov 10 2021 at 13:05):

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

#### Arthur Paulino (Nov 10 2021 at 14:26):

@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 (Nov 10 2021 at 14:33):

easy way is to case on is_empty α or inhabited α

#### Arthur Paulino (Nov 10 2021 at 16:22):

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 (Nov 10 2021 at 16:31):

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

#### Arthur Paulino (Nov 10 2021 at 22:00):

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 (Nov 10 2021 at 22:12):

(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 (Nov 10 2021 at 22:14):

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 (Nov 10 2021 at 22:16):

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 (Nov 10 2021 at 22:19):

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 (Nov 10 2021 at 22:23):

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 (Nov 10 2021 at 22:26):

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 (Nov 10 2021 at 22:27):

(Thanks for pursuing this project!)

#### Arthur Paulino (Nov 10 2021 at 23:13):

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 (Nov 10 2021 at 23:23):

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 (Nov 10 2021 at 23:26):

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 (Nov 10 2021 at 23:26):

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 (Nov 10 2021 at 23:27):

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

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


#### Kyle Miller (Nov 10 2021 at 23:27):

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

#### Kyle Miller (Nov 10 2021 at 23:28):

The final goal will be docs#le_refl

#### Arthur Paulino (Nov 10 2021 at 23:29):

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 (Nov 10 2021 at 23:29):

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

#### Kyle Miller (Nov 10 2021 at 23:30):

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

#### Kyle Miller (Nov 10 2021 at 23:30):

This will launder out the universe variable

#### Arthur Paulino (Nov 10 2021 at 23:31):

Like this?

  rw colorable,
rw ←colorable,
rw colorable,


#### Arthur Paulino (Nov 10 2021 at 23:31):

Same issue as before

#### Kyle Miller (Nov 10 2021 at 23:33):

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 (Nov 10 2021 at 23:34):

(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 (Nov 10 2021 at 23:35):

Now it accepts α

#### Arthur Paulino (Nov 10 2021 at 23:37):

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

#### Arthur Paulino (Nov 10 2021 at 23:37):

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

#### Kyle Miller (Nov 10 2021 at 23:37):

There are a few options. One is fsplit, assumption

#### Kyle Miller (Nov 10 2021 at 23:38):

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

#### Kyle Miller (Nov 10 2021 at 23:38):

use uses fsplit anyway, if I remember correctly

#### Kyle Miller (Nov 10 2021 at 23:39):

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

#### Arthur Paulino (Nov 10 2021 at 23:40):

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 (Nov 10 2021 at 23:40):

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

#### Kyle Miller (Nov 10 2021 at 23:41):

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

Nice

#### Kyle Miller (Nov 10 2021 at 23:42):

The formatting rule is that types get indented:

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


#### Kyle Miller (Nov 10 2021 at 23:45):

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

#### Arthur Paulino (Nov 10 2021 at 23:45):

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

#### Arthur Paulino (Nov 10 2021 at 23:46):

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

#### Arthur Paulino (Nov 11 2021 at 00:29):

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

#### Kyle Miller (Nov 11 2021 at 08:51):

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 (Nov 11 2021 at 09:03):

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 (Nov 11 2021 at 09:14):

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

#### Arthur Paulino (Nov 11 2021 at 22:48):

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

#### Kyle Miller (Nov 11 2021 at 22:51):

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

#### Arthur Paulino (Nov 11 2021 at 22:54):

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

#### Kyle Miller (Nov 11 2021 at 23:00):

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 (Nov 11 2021 at 23:09):

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

#### Arthur Paulino (Nov 11 2021 at 23:09):

because it's a specific graph structure

#### Arthur Paulino (Nov 11 2021 at 23:12):

(and there are many particular structures)

#### Arthur Paulino (Nov 11 2021 at 23:13):

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

#### Arthur Paulino (Nov 11 2021 at 23:31):

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

#### Arthur Paulino (Nov 12 2021 at 12:25):

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 (Nov 12 2021 at 20:31):

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

#### Arthur Paulino (Nov 12 2021 at 20:37):

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

#### Mauricio Collares (Nov 12 2021 at 21:14):

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 (Nov 12 2021 at 22:00):

@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 (Nov 12 2021 at 22:18):

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 (Nov 12 2021 at 22:19):

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 (Nov 12 2021 at 22:24):

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

#### Kyle Miller (Nov 12 2021 at 22:49):

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 (Nov 12 2021 at 22:52):

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

#### Kyle Miller (Nov 12 2021 at 22:54):

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 (Nov 12 2021 at 22:59):

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 (Nov 12 2021 at 23:06):

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 (Nov 13 2021 at 01:44):

@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 (Nov 13 2021 at 01:45):

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

#### Kyle Miller (Nov 13 2021 at 01:47):

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

#### Kyle Miller (Nov 13 2021 at 01:48):

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

#### Kyle Miller (Nov 13 2021 at 01:50):

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 (Nov 13 2021 at 01:53):

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 (Nov 13 2021 at 01:54):

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 (Nov 13 2021 at 01:55):

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

#### Arthur Paulino (Nov 13 2021 at 01:57):

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 (Nov 13 2021 at 02:00):

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 (Nov 13 2021 at 02:02):

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

#### Kyle Miller (Nov 13 2021 at 02:04):

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 (Nov 13 2021 at 02:07):

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

#### Kyle Miller (Nov 13 2021 at 02:08):

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 (Nov 13 2021 at 02:09):

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 (Nov 13 2021 at 02:09):

docs#setoid.ker_def proves that

#### Arthur Paulino (Nov 13 2021 at 02:11):

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 (Nov 13 2021 at 02:12):

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

#### Kyle Miller (Nov 13 2021 at 02:12):

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 (Nov 13 2021 at 02:13):

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

AAAAh!

#### Kyle Miller (Nov 13 2021 at 02:14):

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

#### Arthur Paulino (Nov 13 2021 at 02:17):

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 (Nov 13 2021 at 03:09):

: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 (Nov 14 2021 at 17:08):

@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 (Nov 14 2021 at 17:11):

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 (Nov 14 2021 at 17:20):

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


Wow

Time to learn

#### Arthur Paulino (Nov 14 2021 at 17:23):

Thank you very much!

#### Kyle Miller (Nov 14 2021 at 17:33):

@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:

#### Arthur Paulino (Nov 14 2021 at 17:51):

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

#### Arthur Paulino (Nov 14 2021 at 17:53):

I'm gonna try to create a from_coloring function

#### Kyle Miller (Nov 14 2021 at 18:58):

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],
end

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


#### Arthur Paulino (Nov 14 2021 at 21:13):

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

#### Arthur Paulino (Nov 14 2021 at 21:15):

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 (Nov 14 2021 at 21:23):

The second sorry can actually be replaced by obviously

#### Kyle Miller (Nov 14 2021 at 21:27):

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

#### Kyle Miller (Nov 14 2021 at 21:28):

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

#### Arthur Paulino (Nov 14 2021 at 21:31):

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 (Nov 14 2021 at 21:32):

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 (Nov 14 2021 at 21:33):

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

#### Kevin Buzzard (Nov 14 2021 at 21:34):

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

#### Kevin Buzzard (Nov 14 2021 at 21:34):

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

#### Kyle Miller (Nov 14 2021 at 21:34):

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

#### Yakov Pechersky (Nov 14 2021 at 21:34):

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

#### Kevin Buzzard (Nov 14 2021 at 21:35):

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

#### Yakov Pechersky (Nov 14 2021 at 21:35):

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

#### Arthur Paulino (Nov 14 2021 at 21:37):

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

#### Arthur Paulino (Nov 14 2021 at 21:47):

    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 (Nov 14 2021 at 21:57):

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 (Nov 14 2021 at 22:00):

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

#### Kyle Miller (Nov 14 2021 at 22:04):

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?)

that will do it

#### Mario Carneiro (Nov 14 2021 at 22:05):

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

#### Arthur Paulino (Nov 14 2021 at 22:14):

exact rfl worked too :tada:

#### Arthur Paulino (Nov 14 2021 at 23:16):

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

#### Arthur Paulino (Nov 18 2021 at 04:05):

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?

Last updated: Aug 03 2023 at 10:10 UTC