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!

Hi @Mauricio Salichs , I strongly doubt that you're doing yourself a favor by avoiding the use of the `Path`

lemmas when reasoning about paths. Note that (by coercion) simple graphs are also digraphs, so the path lemmas in `digraph.v`

apply 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`

)

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.

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.

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: May 20 2022 at 10:03 UTC