non-simple graphs

Stream: graph theory

[Vincent Beffara]

Hi, coming back to the question of the typeclass hierarchy for graphs. I have been trying to prove Menger's theorem for simple_graph as a way to practice and learn/test the API, but the proof I know involves tracking paths along graph contractions and that is really awkward to do on simple graphs because one has to prevent repeated vertices, so much so that I am getting really stuck (well, in addition I must be doing plenty of mistakes ...). So I would be much happier with a graph structure for which the arguments feel more natural. I realize there is one in the pipeline but in the meantime I am wondering about the best thing for me to do because a half-finished proof is always frustrating. I am hesitating between

• defining a lazy_walk that is allowed not to move, and writing the proof in terms of that (but that means no access to the walk API);
• defining a graph structure with just enough API for the proof to proceed (but that feels like a huge waste of time);
• soldiering on with simple_graph anyway, despite the impedance mismatch (at least that is practice ...)
• moving on for now :sad:

Any estimate on the timeframe when the new graphs would be in mathlib? I am volunteering if there is anything I can do to help!

[Yaël Dillies]

The refactor could fairly quick, but it will most likely take a while. By that I mean that #11000 can basically be merged as is, but that we still need to discuss in length what we expect from this hierarchy.

[Kyle Miller]

I haven't had time to help move things forward here... and it sounds like Menger's theorem is really hitting against the limitations.

Could you describe what kinds of graph contractions you're needing to deal with are?

[Yaël Dillies]

I have little time to give to Lean until mid-March (but I will anyway :upside_down:). So I guess it won't move much until then.

[Vincent Beffara]

Well for the Menger proof it is just contracting a single edge, but special-casing things just for that feels like the wrong thing to do.

[Kyle Miller]

When you contract the single edge, what are you carrying across to or from the contracted graph? It sounds like paths?

What are you thinking of this being a special case of? contracting arbitrary edge subsets? collapsing vertices together according to a partition? something else?

[Vincent Beffara]

Yes, a path in a graph maps to a path in the contracted graph (after cleaning up if it uses the edge), and a path in the contraction can be lifted to the original graph (up to surgery at the location of the contraction if needed).

At the moment I define a contraction as the push-forward by a function with connected cosets. (Not sure coset is the right word.)

[Kyle Miller]

How does this show up in the argument? Is it an induction on the number of vertices, and this is part of the inductive step?

If so, I'd suggest, for now, being OK with special casing contracting a single edge, if that makes things easier.

[Vincent Beffara]

The proof I am following (from Diestel's book) is an induction on the number of edges, and indeed this is a part of the inductive step. From what I tried, the special case of a single contracted edge is not in fact simpler in terms of lifting the path, but that may be because I am holding it wrong. But I will try again!

[Kyle Miller]

I was imagining you could also make a function to carry a path to a contracted graph by excising the edge that's being removed, and vice versa.

I can't say any of this is easier, just trying to better understand where you're stuck and maybe give you some ideas that may or may not help you make progress!

[Vincent Beffara]

Thanks for the suggestion!

[Vincent Beffara]

BTW I find myself in a situation very similar to https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/heq.20to.20eq/near/210649226 now...

[Bhavik Mehta]

Since you mentioned Menger's theorem specifically, it might be interesting to look at how this was done in 1998 in PVS: https://shemesh.larc.nasa.gov/fm/papers/Butler-TM-1998-206923-Graph-Theory-PVS.pdf

[Kyle Miller]

Yeah, you have to be careful with endpoints. If you're dealing with paths in general in a graph, you're meant to use the sigma type Σ (u v : V), G.walk u v, or otherwise find some way of keeping track of endpoints.

[Kyle Miller]

The whole API is for G.walk u v since it seems to be easier to go to sigma types than to go to subtypes.

[Kyle Miller]

(By the way, I just got around to looking at #11095 again, which has functions to cut apart walks at a vertex, if anyone wants to review it.)

[Kyle Miller]

Vincent Beffara said:

BTW I find myself in a situation very similar to https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/heq.20to.20eq/near/210649226 now...

Shortly after that, we'd tried a special equality operator that also equates the endpoints of the paths https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph/walks.lean

Most of that file seems to be about trying to relate walks defined inductively and walks defined as homomorphisms from the path graph...

[Vincent Beffara]

Yes, precisely. Of course modelling paths as homs from the line graph works much better with contractions when contractions are homs, and in general they are graph homs but not simple_graph homs ...

[Vincent Beffara]

Bhavik Mehta said:

Since you mentioned Menger's theorem specifically, it might be interesting to look at how this was done in 1998 in PVS: https://shemesh.larc.nasa.gov/fm/papers/Butler-TM-1998-206923-Graph-Theory-PVS.pdf

Thanks for the reference! I just had a look and read "The hard direction of Menger has only been formally proved for the K = 2 case" (which should probably contain most of the difficulty anyway), but they only give the statements and no technical info about implementation. They do explain their definition of paths, which are non-empty lists of vertices ("prepaths") with adjacency constraints rather than inductively defined.

[Vincent Beffara]

Kyle Miller said:

Yeah, you have to be careful with endpoints. If you're dealing with paths in general in a graph, you're meant to use the sigma type Σ (u v : V), G.walk u v, or otherwise find some way of keeping track of endpoints.

Is this even true?

example {u v w} {p : G.walk u w} {q : G.walk v w} : p == q -> u = v := sorry

[Vincent Beffara]

Or even this?

example {u v w} : G.walk u w = G.walk v w -> u = v := sorry

[Kyle Miller]

The first one is exactly why I asked the question that you linked earlier, and as I understand it, it's not provable (so true or false depending on how things are theoretically implemented!)

For example, this case:

example {u v : V} : (walk.nil : G.walk u u) == (walk.nil : G.walk v v) → u = v :=
sorry

In principle, whenever u is a vertex such that G.walk u u has only the nil path, then all such G.walk u u types might be equal. (Types with the same cardinality are allowed to be equal, as in there are no axioms that prevent it. Also none that require it.)

[Vincent Beffara]

This is very strange because this,

def start {u v : V} (p : G.walk u v) := u

gives different outcomes for walk.nil : G.walk u u and walk.nil : G.walk v v. I realize that this is really two constant functions, @start u u and @start v v, and that they only appear to be the same because of hidden implicit arguments, but it still feels couterintuitive ...

[Vincent Beffara]

Anyway, that is reason enough to have a sigma walk type in the graph API somewhere!

[Kyle Miller]

Yeah, the trick to your start function is that it's just returning u, the first implicit argument. The p : G.walk u v ends up just being a way to get the elaborator to fill in that implicit argument.

[Kyle Miller]

I think it might help to differentiate between "terms" and "elements" of a type (this is just something I've had in the back of my head -- I'm not a type theorist). A "term" is something you have constructed, and given a term you can work out its type in an algorithmic way. A "element" is something that has been given to you, or posited to exist, along with its type. On one hand, types are disjoint in that terms only belong to one type. On the other hand, types don't have to be disjoint in that they might share elements.

In short: terms are syntactic and elements are semantic.

[Kyle Miller]

I'm probably mixing things up here -- but in any case if we imagine types are implemented within set theory, then it makes sense to ask whether two types have shared elements.