Graph minors and contractions

Stream: graph theory

[Vincent Beffara]

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]

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]

Hey! We haven't met yet.

[Vincent Beffara]

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]

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]

(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]

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

[Vincent Beffara]

I haven't, but I will have a look

[Kyle Miller]

@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]

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]

@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]

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.

Just in case you hadn't seen, Vincent already has! #11563

[Kyle Miller]

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

[Kyle Miller]

@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]

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]

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

[Kyle Miller]

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

[Bhavik Mehta]

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]

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]

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]

graph isn't a class though!

[Vincent Beffara]

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]

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

[Yaël Dillies]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

@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]

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]

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]

I should however mention the solution of using docs#fact

[Kyle Miller]

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]

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]

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.