Stream: GraphTheory

Topic: Questions about the formalization of Brook's Theroem

view this post on Zulip Mauricio Salichs (Apr 10 2021 at 19:44):

Hi everyone! I'm glad that i can be a part of this group!

Christian, just in case you don't remember, i'm working on my grade thesis having Daniel as director and Ricardo as co-director, proving some theorems of graph theory in Coq. I would like to ask you some things you might know about, that could help me trough this :)

I'm working on the proof of Brook's Theorem about coloring, which uses path theory of graphs. I saw that you made some work on that subject on sgraph, but i couldn't fully understand how it works exactly. Also, you defined a connected set of vertex using fingraph's connect definition, which I understand is not used so much nowadays. Can i prove lemmas over connected sets using that definition easily?

Brook's theorem uses and manipulates specific components of subgraphs induced by two different colors. This components are always ij-paths (where i and j are the colours).

(1) I wonder how to describe that some component CC : {set GG} is exactly a path between two specific vertex viv_i and vjv_j (Lets call such a paths CijC_{ij}). I can see that using path_in_connected over CC, viv_i and vjv_j, I can prove the existence of pp : Path viv_i vjv_j, then i just need to prove Cp C \subseteq p to complete the idea. Is this the best way to do it? What i need of this Path structure is to prove the following:

I tried to avoid using the specific path theory you did, and workaround the definition of path in (1) in a way that abstracts the concepts i need later (e.g. having vi,vjCv_i, v_j \in C, with δ(vi)=δ(vj)=1\delta(v_i) = \delta(v_j) = 1, and for any other vkC,δ(vk)=2v_k \in C, \delta(v_k) = 2). But this didn't make it easier to prove the further sublemmas.

I tried to abstract this questions as much as i could, so i dont have to explain the entire context... but if they are not clear, please let me know!

view this post on Zulip Christian Doczkal (Apr 10 2021 at 20:55):

Hi @Mauricio Salichs , I strongly doubt that you're doing yourself a favor by avoiding the use of the Pathlemmas when reasoning about paths. Note that (by coercion) simple graphs are also digraphs, so the path lemmas in digraph.vapply to simple graphs as well. This includes quite a few lemmas about splitting and concatenating paths as well as lemmas about irredundant paths (the definition of Path permits paths with cycles.
In light of that, I would indeed define a path-shaped component as a component satisfying something along the lines of:

Definition is_path (x y : G) (P : {set G}) := exists (p : Path x y), irred p /\ P =i p.

Indeed, if P is also a component (i.e., closed under (--)), it should not be too hard to prove that the degree of x and y is 1 and that every vertex in interior p has degree 2. Have a look at isplitP and splitL/splitR. (assuming x != y)

view this post on Zulip Christian Doczkal (Apr 10 2021 at 21:08):

As for connect, I would consider it the natural boolean predicate to use for things being connected, and there are view lemmas for all the commonly occurring patterns. In particular, there are view lemmas for the

connect (restrict _ edge_rel) _ _

pattern used in the definition of connected sets.

view this post on Zulip Christian Doczkal (Apr 10 2021 at 21:15):

Note that there is the type (family) IPath x y of irredundant paths. Unlike Path x y, this has a finType structure, so one can use it with boolean quantifiers.

view this post on Zulip Mauricio Salichs (Apr 11 2021 at 06:33):

Ok! That's great! I will look closely at all the definitions and lemmas of digraph.v, and will try to rewrite the definitions using the Path structure. Thanks!!

Last updated: Feb 09 2023 at 03:06 UTC