K4 is planar help

Stream: graph theory

[Eavan Pattie]

Hello all! I'm still learning the in's and outs's of lean and it's community, so if this isn't the right place to post this then let me know. I recently set myself the challenge to try to prove a simple statement in lean3, namely that the complete graph on 4 vertices is planar. This is based off of @Vincent Beffara 's definition of planar that I found in an PR linked in this group.

Despite the triviality of the statement, the resulting proof was much longer (and harder) than I expected and it's current form is plagued by deterministic timeout and memory issues. As far as I can tell, the issues stem from my frequent usage of fin_cases, but I am not able to figure out a way around them.

I was wondering if anyone here had any ideas for how to reduce the load on lean?
The proof in it's current form can be found here.
Thanks in advance!

[Kevin Buzzard]

Where is the graph_theory.planar import? It's not on master.

[Kevin Buzzard]

I think your life would be a bit easier with def K4 := complete_graph (fin 4) rather than def K4 := complete_graph (finset.range 4); complete_graph is expecting to eat a type and you're giving it a quite a complex term which is then being coerced to a type, so you're already doomed to a bit of superfluous jumping through hoops.

[Kevin Buzzard]

def K4_to_plane : fin 4 → (ℤ × ℤ)
| ⟨0, _⟩ := (0,0)
| ⟨1, _⟩ := (0,1)
| ⟨2, _⟩ := (0,2)
| ⟨3, _⟩ := (1,1)
| ⟨n+4, h⟩ := false.elim (by linarith)

might be a less painful definition; then a lot of your identities are definitional.

[Kyle Miller]

@Kevin Buzzard It's here in the same branch. If I'm following it right, it's that there exists a subdivision of the graph that embeds in the infinite square lattice graph.

This doesn't seem to be the right definition for graphs that have vertices with degree greater than four.

[Eavan Pattie]

The definition of planar and the machinery around it are in the rest of the repo which is a fork of Vincent's work here. As Kyle mentions the definition of planar is that graph G is planar if there exists an embedding of G's vertices into the infinite square lattice and an embedding of G's edges into paths in the infinite square lattice such that paths don't intersect.
Although reconsidering this definition now, it is clear that this definition doesn't work for planar graphs with vertices with degree 5 or more.

Thanks @Kevin Buzzard for the improved definition for the mapping to the plane :)
I'm still a little unclear on the benefit of using fin 4 versus finset.range 4 as both seem to represent the same idea of {0,1,2,3}?

[Kevin Buzzard]

One is a (definitionally simple) type and one is a (definitionally complex) term. The function expects a type so why not give it a type, as opposed to be something which was designed to be a term and then is being promoted by you to a type via a coercion (the up-arrow which you will no doubt have seen everywhere in your approach and which isn't there in mine). In short "the canonical type with four elements is fin 4". This is just my opinion though and there are plenty of people here who understand definitional issues in lean 3 better than I do.

[Vincent Beffara]

Yes the definition of planar in that repo is definitely wrong for graphs with degree larger than 4. I was going for saying that planar meant being a minor of Z^2, but the path embedding definition was quicker to write so I used it temporarily then spent a lot of time defining minors, and forgot to update the definition afterwards. And then I let the code rot, I would actually be surprised if it still compiled with recent mathlib.

[Vincent Beffara]

I kind of lost track of where the graph API of mathlib is now, but maybe some of the contents of that repo would still be of value ...

[Kevin Buzzard]

I don't know of a purely combinatorial definition of planar graph (but I don't know the area at all). What does Gonthier do? I just remember the combinatorial hypermaps.

[Vincent Beffara]

I think he goes the triple of permutations way but I am not sure. Minor of Z2 felt like a natural choice but there might be issues for non locally finite graphs or such abominations. The most common definition I found used continuous paths in the plane and that certainly doesn't sound like something we want to use as a definition when formalizing ...

[Vincent Beffara]

Or we could sidestep the issue and say that a planar graph is a graph that has neither K5 nor K33 as a minor, and prove that such a graph has an embedding in the plane. (That was meant as a joke but not completely.)

[Vincent Beffara]

In any case, settling on a combinatorial definition feels like a good goal

[Yaël Dillies]

Is this related to flag algebras somehow?

[Vincent Beffara]

I am no specialist but flag algebras sound like they relate to forbidden subgraphs while planarity and such are more related to forbidden minors

[Yaël Dillies]

Hmm, you're probably right

[Vincent Beffara]

BTW, the statement of Kuratowski if planarity is defined as being a minor of Z2 is kind of cute

[Mario Carneiro]

Is it possible to have graphs that are non-planar because the cardinality is too high to embed them in R^2? For example, aleph_2 discrete points should almost certainly be planar by a combinatorial definition but you can't embed it in the plane if "without crossings" also implies that no points are coincident

[Mario Carneiro]

Personally I would be inclined to take a definition which makes these things planar, using the Kuratowski theorem as a guide if not a definition

[Vincent Beffara]

You can even build a connected abomination by adding a point that is connected to all your aleph_2 leaves to get an "oursin". I agree that this is should be accepted as a planar connected graph.

[Rémi Bottinelli]

Diestel's work might be of interest, e.g. this ?

[Vincent Beffara]

It could, although his graphs are all countable so it will not solve all our issues

[Rémi Bottinelli]

OK, this might be a stupid idea, but isn't an infinite graph planar iff all its finite subgraphs are?

[Vincent Beffara]

Depends on your definition of planar ... It is true for locally finite and countable graphs, but if your graph has more vertices than R2 has points you need to be careful

[Vincent Beffara]

Otoh, all finite subgraphs being planar (and for finite graphs there is no definitional issue for planarity) might well be a workable definition of planarity in the general case.

[Rémi Bottinelli]

As far as I understand, if the graph is not countable/locally finite, we're out of the standard definitions anyway, and on kind of terra incognita, no?

[pcpthm]

<s>Finite subgraph definition isn't compatible with the Kuratowski definition: consider K5 with each edge replaced by an infinite path.</s> Edit: no such thing as an infinite path.
Perhaps consider all finite minors instead?
Edit: finite subgraph definition and finite minor definition is equivalent if minor is defined by paths (not sure if any other definition exists) if I'm not wrong.

[pcpthm]

(that is equivalent to the Kuratowski definition)

[Kyle Miller]

Here's an old implementation of combinatorial maps: https://github.com/kmill/lean-graphs/blob/master/src/maps.lean

Planar graphs correspond to combinatorial maps whose euler characteristic (line 257) is equal to the number of connected components.

I think I have another implementation somewhere -- I thought I had started to write a statement of Sperner's lemma for combinatorial maps.

[Vincent Beffara]

pcpthm said:

finite subgraph definition and finite minor definition should be equivalent: for every finite minor G' of G, there exists a finite subgraph G'' of G such that G' is a minor of G''.

That sounds both true and reassuring :-)