Stream: GraphTheory

Topic: Questions about the formalization of Brook's Theroem

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 $C$ : {set $G$} is exactly a path between two specific vertex $v_i$ and $v_j$ (Lets call such a paths $C_{ij}$). I can see that using path_in_connected over $C$, $v_i$ and $v_j$, I can prove the existence of $p$ : Path $v_i$ $v_j$, then i just need to prove $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:

• If i legally change the color of some inner vertex $v_k$ of $C_{ij}$, then $C_{ij}$ would no longer be a path mantaining just two colours.
• Prove that ($C_{ij} - {v_i}$) is a path, and that if some vertex $v_k$ is coloured with the same colour as $v_i$, $C_{kj} \subseteq C_{ij} - {v_i}$.

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 $v_i, v_j \in C$, with $\delta(v_i) = \delta(v_j) = 1$, and for any other $v_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!

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)

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.

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.

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