## Stream: graph theory

### Topic: Graph minors and contractions

#### Vincent Beffara (Jan 19 2022 at 18:29):

Hi! After a year-long break from lean, I came back to my project of formalizing things in graph theory and adapted what I already had to the simple_graph API. I managed to show for instance that graph minors form a transitive relation, but what I wrote feels wrong ... I would be glad if someone had a look at my code here https://github.com/vbeffara/lean and give me pointers to improve it :-)

I will slice it into smaller bits and submit it to mathlib but as of now there is too much refactoring needed ...

#### Kyle Miller (Jan 19 2022 at 18:42):

I'll take a closer look later to see what you've been working on, and think about how we might merge things into mathlib. Nice to see work toward Kuratowski's theorem.

#### Yaël Dillies (Jan 19 2022 at 18:52):

Hey! We haven't met yet.

#### Vincent Beffara (Jan 19 2022 at 20:16):

Yes Kuratowski-Wagner is what I am planning to try to do. Just 5 pages of Diestel's book, should not take too long :grinning: (And then on to Robertson-Seymour? Just kidding ...)

#### Vincent Beffara (Jan 20 2022 at 08:55):

BTW in retrospect, I am defining the contraction of a graph along a collection of edges given as a smaller simple_graph on the same vertex type, but that is probably not the best way to proceed. I now believe it would be better to define a simple_graph structure on any quotient of the vertex type of a graph by a setoid, see what extends to that setting, and then say more specific stuff when the setoid has connected classes.

One slightly annoying aspect of the construction is that there is in general no projection that is also a graph rel_hom (because of the loopless part), so this is one place where working on graphs without the loopless assumption would be more natural. As it is now, for instance proving that the contraction of a connected graph is connected is a bit awkward - at least the way I do it by constructing paths, there is probably a better way.

#### Vincent Beffara (Jan 20 2022 at 08:59):

(Alternatively, a lazy_walk defined as a walk that is also allowed to sometimes stay where it is could be useful when looking at connectivity properties. But then transforming it into a usual walk involves decidable equality AFAICT.)

#### Yaël Dillies (Jan 20 2022 at 12:04):

Have you seen the graph refactor I proposed? This would allow easily adding/removing the irreflexivity condition.

#### Vincent Beffara (Jan 20 2022 at 12:20):

I haven't, but I will have a look

#### Kyle Miller (Jan 20 2022 at 16:52):

@Vincent Beffara One version of a simple graph is known as a "reflexive graph," where the relation is reflexive. Walks in a reflexive graph are allowed to stay put because of this. More generally, the image of a graph homomorphism of reflexive graphs is a graph contraction.

#### Bryan Gin-ge Chen (Jan 20 2022 at 17:00):

I haven't been following closely enough to know how relevant it is here, but @Peter Nelson and his collaborators worked hard on formalizing matroid minors in Lean last year: https://www.youtube.com/watch?v=FzJuoXy5cG0

#### Kyle Miller (Jan 20 2022 at 17:04):

@Vincent Beffara It's small, but you could start with collecting your sym2 lemmas (like this one) and PRing them. Or just that, if it's the only one.

#### Bhavik Mehta (Jan 20 2022 at 17:08):

Kyle Miller said:

Vincent Beffara It's small, but you could start with collecting your sym2 lemmas (like this one) and PRing them. Or just that, if it's the only one.

#### Kyle Miller (Jan 20 2022 at 17:16):

Well, it looks like you're 19 hours ahead of me then :smile:

#### Kyle Miller (Jan 20 2022 at 17:24):

@Vincent Beffara There are some PRs about walks and connectivity in the works, and this file has some overlap. I'll get back to you on this one.

Once the definition of a connected graph is in mathlib, then you should be free to PR metrics

I think Yael suggested adj.symm a couple weeks ago, and this would make a nice quick PR.

#### Kyle Miller (Jan 20 2022 at 17:29):

Design question time: should graphs have a connected_graph typeclass, or is it fine carrying around a G.connected proof?

For: connected graphs are sort of the "default" for a lot of theory, so we want to make it easy to pass connectedness around.

Against: if we do pass the hc : G.connected proof around, then we can put lemmas about connectedness in the connected namespace then refer to them with hc.lemma_name, and that's fine.

Fact typeclasses like this are reasonably common; I just hadn't considered using them here myself: what do others think?

#### Bhavik Mehta (Jan 20 2022 at 17:32):

imo we should pass around a G.connected proof; I think a fair comparison here is the use of continuity in topology

#### Kyle Miller (Jan 20 2022 at 17:37):

What if this is more like docs#irreducible than continuity?

#### Bhavik Mehta (Jan 20 2022 at 17:41):

It could well be, but it looks like that's also passed around as a proof rather than put into the typeclass system

#### Bhavik Mehta (Jan 20 2022 at 17:45):

Perhaps an example to the contrary is docs#is_domain, since that's usually a class, and it's a property of the whole structure (like connectedness) rather than elements (like irreducible) or morphisms (like continuity)

#### Vincent Beffara (Jan 20 2022 at 20:41):

If graph is a class, and e.g. metric_space is a class, but a graph is only a metric space when it is connected, then if feels more natural to say that connectivity should also be a class (for chaining)

#### Bhavik Mehta (Jan 20 2022 at 21:05):

graph isn't a class though!

#### Vincent Beffara (Jan 20 2022 at 21:13):

Ah, my mistake, without having looked yet at the PRs my understanding was to make it one (and that the design question was intended for after the transition)

#### Bhavik Mehta (Jan 20 2022 at 21:14):

Ah you might be right, I was thinking about the design question with relation the current state of affairs!

#### Yaël Dillies (Jan 20 2022 at 21:19):

graph isn't meant to be a class, but there indeed be a graph_class. However I think that's unrelated to whether we want connection to be an instance or not.

#### Bhavik Mehta (Jan 20 2022 at 21:29):

Yaël Dillies said:

graph isn't meant to be a class, but there indeed be a graph_class. However I think that's unrelated to whether we want connection to be an instance or not.

I don't think it's unrelated; if graph is meant to be a class then it's probably sensible for connected to be a class too - I don't think there are many cases through mathlib of a mathematical object which is a class but properties are carried around explicitly.

#### Yaël Dillies (Jan 20 2022 at 21:31):

I maintain. The class is stating that a graph-like object is a graph, but the graph-like object is already graph-like without.

#### Kyle Miller (Jan 20 2022 at 22:05):

Vincent Beffara said:

and that the design question was intended for after the transition

I meant it to be a question independent of how graphs are implemented (and, like Yael, I think the answer is independent, too).

#### Kyle Miller (Jan 20 2022 at 22:09):

I thought your having it being a class was an interesting enough idea that it should have further consideration.

(I'm thinking that for now we ought to not have this class, and if for some reason we find threading connectedness through things does end up being pervasive, we can revisit this.)

#### Yakov Pechersky (Jan 20 2022 at 22:50):

Downside of connectivity being a class means that on-the-fly constructed graphs like excision of a point would need haveI like statements of connectivity

#### Kyle Miller (Jan 20 2022 at 22:58):

Oops, I really failed to say what the idea was. If we have connected as a plain old property, then we can also have a class

class connected_graph (G : simple_graph V) :=
(conn : connected G)

export connected_graph


and then if you do G.conn, it tries to obtain the proof of connectedness by some means (typeclass argument, typeclass search, or what have you).

#### Kyle Miller (Jan 20 2022 at 22:59):

but then the tradeoff is that when you have a graph constructed on-the-fly like Yakov said, you need to haveI or something to be able to use the corresponding lemma/def.

#### Yaël Dillies (Jan 21 2022 at 07:42):

I was never against the idea of a graph.connected class. I am against seeing it as a natural continuation of the refactor.

#### Vincent Beffara (Jan 21 2022 at 08:39):

To be fair, the whole reason that there is a connected class in my file is that I once talked with Sébastien Gouëzel about formalizing Cayley graphs, he told me something along the lines of "the best way to do that is to have a graph class and to construct an instance of if on top of a group" and then bridging this to metric spaces made more sense with a class as well for connectivity. No big design idea or anything. (My initial approach was to have a graph structure, rather like it is now in mathlib.)

But then, trying to show that two different Cayley graphs of the same group are quasi-isometric, I struggled a lot with juggling with two instances of the same class on the same object, with code like this,

def Cayley gen G : Type := G
instance {gen} {G} : graph (Cayley gen G) := sorry -- actual implementation


and casting id into Cayley gen1 G -> Cayley gen2 G and so on. Felt rather unnatural to me, as opposed to having two graph structures on the same underlying type. Going to the mathlib API when it appeared, I kept the typeclass more out of laziness than anything else :sweat_smile:

#### Vincent Beffara (Jan 21 2022 at 08:44):

BTW, assuming we know how to build an instance like this,

instance bla [graph_class g] (h : g.connected) : metric_space g := sorry


and within a proof we get (h : g.connected) in the context and need the metric, will typeclass resolution work it out or do we need to letI : metric_space g := bla h by hand?

#### Kyle Miller (Jan 21 2022 at 08:56):

@Vincent Beffara I'm not sure if you've had a chance to take a look at them, but the sorts of graph classes that are independently under consideration might not be what you expect. They're classes for the type of graphs themselves, rather than classes for individual graphs (which have the problems you ran into). So it would be, say, that there's an instance graph_class (simple_graph V) V, or something like that, and then that would give you generic functions and lemmas for terms of type simple_graph V.

#### Kyle Miller (Jan 21 2022 at 08:59):

Your example for metric_space is interesting puzzle... We won't want metric_space V, since multiple simple graphs have the same vertex type, and we probably want to compare metric space structures with varying graphs.

I guess for that, we'll want some function that gets the vertex type from a graph, so it would look like metric_space G.V or something.

This instance is also a point in favor of having this connected_graph class that wraps up a proof of G.connected.

#### Yaël Dillies (Jan 21 2022 at 09:00):

I have to agree with Kyle here. If ever you want to reuse the metric_space machinery, you need this instance and turn connection into a class.

#### Yaël Dillies (Jan 21 2022 at 09:02):

I should however mention the solution of using docs#fact

#### Kyle Miller (Jan 21 2022 at 09:04):

Yaël Dillies said:

I was never against the idea of a graph.connected class. I am against seeing it as a natural continuation of the refactor.

Was there something you were disagreeing with here by restating your position? I've been trying to figure out what it was

#### Yaël Dillies (Jan 21 2022 at 09:05):

This is what I was disagreeing with.
Bhavik Mehta said:

I don't think it's unrelated; if graph is meant to be a class then it's probably sensible for connected to be a class too - I don't think there are many cases through mathlib of a mathematical object which is a class but properties are carried around explicitly.

#### Kyle Miller (Jan 21 2022 at 09:09):

Oh, that makes sense that it goes with your prior comment, thanks. I wasn't sure if it was referring to what Yakov or I said, since your quoted comment seems to have appeared after ours.

Last updated: Dec 20 2023 at 11:08 UTC