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 : {set } is exactly a path between two specific vertex and (Lets call such a paths ). I can see that using path_in_connected
over , and , I can prove the existence of : Path , then i just need to prove 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 , with , and for any other ). 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: Feb 09 2023 at 03:06 UTC