connectivity

Stream: graph theory

[Joseph Hua]

Hi all, I'm thinking of doing some work on the graph theory library. Particularly I want to show that (vertex)-connectivity is less than or equal to edge-connectivity. I expected to find a definition for vertex-connectivity / k-connectivity in combinatorics/simple_graph/connectivity, but it seems that its work in progress. Do people have a particular plan in mind that I can flesh out?

[Vincent Beffara]

Hi, good timing :-) as a matter of fact I recently spent a lot of time formalizing Menger's theorem, and the proof first typechecked about an hour ago, but there is a huge amount of cleaning-up to be done. In particular, a nice definition of k-connectivity would be very useful.

[Kyle Miller]

I've been (slowly) adding things from a branch about connectivity. #8737

[Vincent Beffara]

The simplest basic version of connectivity would be

def linked (G : simple_graph V) := relation.refl_trans_gen G.adj

def connected (G : simple_graph V) := ∀ x y, linked G x y

plus a lemma like

lemma linked_iff : linked G x y <-> nonempty (walk G x y)

[Kyle Miller]

This is the part most recently added: #11095

[Kyle Miller]

connected: https://github.com/leanprover-community/mathlib/blob/8a46ed85b34a68d10b4f519416d11eb800b9dd28/src/combinatorics/simple_graph/connectivity.lean#L472

edge connectivity: https://github.com/leanprover-community/mathlib/blob/8a46ed85b34a68d10b4f519416d11eb800b9dd28/src/combinatorics/simple_graph/connectivity.lean#L491
(this needs to be modified)

[Vincent Beffara]

Some of those constructions (especially take_until and drop_until) taste much better with a sigma type for paths, especially when you want to generalize to the first hitting point of a subset

[Vincent Beffara]

So I ended up building a lot of lemmas around such a sigma type, in a way that feels very sub-optimal ... In particular, I could not find a way to prevent heq from popping up all over the place (especially when using ext), so I ended up encapsulating rec from walk and using that to reprove many basic things.

[Joseph Hua]

Nice! Thank you both for this. @Vincent Beffara what kind of results would you be interested in having? @Kyle Miller I'll probably try to build on this branch of mathlib

[Joseph Hua]

Vincent Beffara said:

Some of those constructions (especially take_until and drop_until) taste much better with a sigma type for paths, especially when you want to generalize to the first hitting point of a subset

what do you mean by "hitting point"?

[Kyle Miller]

This branch has unfortunately diverged from mathlib... I'm going to try getting the next batch of it into a PR the next couple days, though.

[Yakov Pechersky]

I still think that walks are just list.chain over the sequence of vertices. And drop and take should use list API.

[Kyle Miller]

@Vincent Beffara I've not needed heq with theorems about trees being loopless connected graphs. I'd like to see what's happening with what you're doing at some point

[Kyle Miller]

Maybe there's something missing from the library that would make everything nicer for you without all that extra work

[Vincent Beffara]

Joseph Hua said:

Vincent Beffara said:

Some of those constructions (especially take_until and drop_until) taste much better with a sigma type for paths, especially when you want to generalize to the first hitting point of a subset

what do you mean by "hitting point"?

I mean, you take a walk p and a subset X of V with the assumption that X \cap p.support is not empty, and you get the prefix of p until its first vertex that belongs to X

[Kyle Miller]

@Yakov Pechersky I'm going to assume you think this until you say otherwise

[Yakov Pechersky]

Ha! Good point.

[Yakov Pechersky]

Whether or not it's implemented that way, I do draw inspiration from the list API in thinking about the API of finite ordered subsequences

[Yakov Pechersky]

Not trying to bikeshed, but give color for Joseph's question.

[Vincent Beffara]

Kyle Miller said:

Vincent Beffara I've not needed heq with theorems about trees being loopless connected graphs. I'd like to see what's happening with what you're doing at some point

Specifically: I define the pushforward and pullback of graphs and want that the pushforward of the pullback of a walk is the walk you started from. With sigma types it is just a version of left_inverse, with G.walk a b it is complicated to state so I gave up. But then in the proof, showing that the equality between sigma types holds, a natural step would be to say ext but then the issue pops up again because it turns equality of the sigma type members into heq of the walk members.

[Kyle Miller]

@Yakov Pechersky Something I've imagined is having a list.chain interface on top so that you can manipulate things freely without all the dependent type constraints. The type constraints are useful for a lot of things, I've found, so I wouldn't want to lose that in general.

[Yakov Pechersky]

For the heq stuff, you might get away with a helper lemma that uses the forgetfulness into just the underlying list of vertices, without the adjacency constraints.

[Yakov Pechersky]

If two walks have pointwise exactly the same underlying sequence of vertices, then they must be equal (on a simple graph)

[Vincent Beffara]

Yes, that's certainly an option (and with the current API, that would mean using walk.support to get the list of vertices, but then one needs to take care of propagating the list.chain part, IIUC).

[Yakov Pechersky]

The point I'm making about equality of walks is that it means equality of supports, so you lose needing to talk about the chain aspect

[Yakov Pechersky]

Because whether or not they're "chain", iff the supports aren't equal, the walks aren't.

[Vincent Beffara]

Sure, I get that. I'm more worried about having some constructions ending up as a convoluted construction of a list of vertices, and then a proof that the list is a walk (which would look very much like the construction itself).

[Vincent Beffara]

Would it make sense to have two definitions, the current inductive one and another one based on lists of vertices, with a nice isomorphism between G.walk a b and {p : chainy_walk G // p.start = a \and p.end = b} or is it looking for trouble?

[Yakov Pechersky]

Then I didn't understand the use cases. Are you constructing walks or are proving two constructed walks are equal?

[Yakov Pechersky]

Probably constructing the actual walk should be made relevant instead of going through the equiv to the subtype

[Vincent Beffara]

I do both, I constructed a walk and I wanted to show that it was equal to another one but in a situation where the equality of the endpoints was not defeq.

[Joseph Hua]

Why would you want an equality between two graphs as oppose to an equivalence?

[Kyle Miller]

@Vincent Beffara When you say the endpoints weren't defeq, were you able to do a rewrite to make the endpoints coincide? That usually works in some way to avoid heq

[Vincent Beffara]

I would need to fish around for a mwe because I ended up using my ad-hoc sigma type anyway, but it was something like

def lift_path : walk (push f G) x' y' → Π (x y : V), f x = x' → f y = y' → walk G x y := sorry
def push_path : walk G x y -> walk (push f G) (f x) (f y) := sorry
example (p : walk (push f G) x' y') (x y : V) (hx : f x = x') (hy : f y = y') : push_path (lift_path p x y hx hy) == p

where the left-hand is a G.walk (f x) (f y) and the left-hand is a G.walk x' y'. I couldn't find a way to state the identity without either a heq or sigma type.

[Vincent Beffara]

In retrospect, my impression is that if walks had been defined from the start as lists with conditions, my life would have been easier at a few places. But that probably says more about my still limited lean abilities than about the simple_graph API.

Anyway, my code is here, https://github.com/vbeffara/lean/blob/main/src/graph_theory/menger.lean and I would be very glad to get some comments (although there are many places where I already see changes to be made). @Kyle Miller I will look around in your branch for things that I can use :-)

[Kyle Miller]

Thanks, I'll take a look later. (It's good to hear what you're running into -- you're bound to have come up against limitations, and from what you've said so far there must be missing things, just not sure what yet.)

[Kyle Miller]

Joseph Hua said:

vertex-connectivity

I'm not sure what the best way is for this yet... One idea I'd considered is defining the removal of a subset of vertices from a docs#simple_graph.subgraph and then using connectedness of the subgraph coerced to a graph (docs#simple_graph.spanning_coe), but I'm not too keen on the fact the vertex types will be subtypes, but maybe that's just because we haven't built up ways to move walks back and forth from a subgraph yet.

[Kyle Miller]

Did you have some theorem in mind when you asked about that?

[Vincent Beffara]

Kyle Miller said:

Thanks, I'll take a look later. (It's good to hear what you're running into -- you're bound to have come up against limitations, and from what you've said so far there must be missing things, just not sure what yet.)

One thing that I found useful was a type for walk steps (i.e. ordered pairs of adjacent vertices) as opposed to a type sym2 V for edges, in general I found that working with G.edges was not very pleasant. I was probably holding them wrong.

[Joseph Hua]

Kyle Miller said:

Did you have some theorem in mind when you asked about that?

Yes, I was going to "do my graph theory coursework properly" by proving that k-vertex-connectivity -> k-edge-connectivity I feel like taking the induced subgraph of a set of vertices is the right way to talk about k-vertex connectivity. Alternatively maybe "walks in the ambient graph that don't enter a subset" could generalize the current definition of walks, though I feel like this is not as clean as making an API for the first option

[Kyle Miller]

@Joseph Hua All we have right now regarding induced graphs is the predicate docs#simple_graph.subgraph.is_induced. It would be great to have subgraphs induced by a vertex set

[Kyle Miller]

and basic things surrounding that, like that if A subset B then G.induced A <= G.induced B.

[Joseph Hua]

def induced_subgraph (s : set V) : G.subgraph :=
{ verts := s,
  adj := λ u v, G.adj u v ∧ u ∈ s ∧ v ∈ s,
  adj_sub := by obviously,
  edge_vert := by obviously }

def delete_vertices (s : set V) : G.subgraph :=
induced_subgraph G (sᶜ)

/-- A graph is *k-vertex-connected* if it remains connected whenever
fewer than k vertices are removed. -/
def vertex_connected (k : ℕ) : Prop :=
∀ (s : finset V), s.card < k → (G.delete_vertices s).connected

[Kyle Miller]

A design question: when inducing a subgraph, do we think we will do induced subgraphs of subgraphs, too? or for applications would it be sufficient to have simple_graph.induced?

[Kyle Miller]

(one answer is: that's sufficient for now, and we can revisit it later)

[Kyle Miller]

The induced subgraph also defines an embedding into the original graph, and every embedding is onto an induced subgraph, I believe.

[Kyle Miller]

In your definition of adj, there might be pre-existing definitions in the relations part of mathlib to restrict a relation to a set, which we should find.

[Joseph Hua]

Kyle Miller said:

A design question: when inducing a subgraph, do we think we will do induced subgraphs of subgraphs, too? or for applications would it be sufficient to have simple_graph.induced?

Yeah, I think I should generalize the above and the definition of delete_edges to take in a subgraph first

[Vincent Beffara]

How about

 def pullback (f : V → V') (G' : simple_graph V') : simple_graph V :=
{ adj := G'.adj on f,
  symm := λ _ _ h, G'.symm h,
  loopless := λ _, G'.loopless _ }

and def induced (s : set V) (G : simple_graph V) : simple_graph s := pullback coe G?

[Vincent Beffara]

Or do we really need the subgraph as a subgraph rather than as a graph with an embedding?

[Kyle Miller]

Regarding where to put induced: I suppose we can always take the induced graph from the Top subgraph, and then define an abbreviation simple_graph.induced to do this

[Joseph Hua]

Kyle Miller said:

Regarding where to put induced: I suppose we can always take the induced graph from the Top subgraph, and then define an abbreviation simple_graph.induced to do this

what do you mean by this? Doesn't Top just give the original graph back?
I see, you're making the version of induced that I gave using our generalization

[Kyle Miller]

(top : G.subgraph).induced s

[Joseph Hua]

Vincent Beffara said:

Or do we really need the subgraph as a subgraph rather than as a graph with an embedding?

I think we want a subgraph, I think embeddings could get messy once we need to do something like "remove F a set of edges and U a set of vertices" where F and U might not have anything to do with each other

[Yaël Dillies]

Vincent Beffara said:

One thing that I found useful was a type for walk steps (i.e. ordered pairs of adjacent vertices) as opposed to a type sym2 V for edges, in general I found that working with G.edges was not very pleasant.

Do you know about docs#simple_graph.dart?

[Kyle Miller]

It's nice having this V type to sort of cohere all the different subgraphs into being part of the same graph. For example, you'd want the elements of s to somehow be vertices of the induced graph without too much fanfare

[Vincent Beffara]

Yaël Dillies said:

Vincent Beffara said:

One thing that I found useful was a type for walk steps (i.e. ordered pairs of adjacent vertices) as opposed to a type sym2 V for edges, in general I found that working with G.edges was not very pleasant.

Do you know about docs#simple_graph.dart?

I do now :-)

[Kyle Miller]

It seems like it would make a lot of sense to add walk.darts and make walk.edges be defined in terms of it.

[Joseph Hua]

Should we be using lemmas for subsets and then translating the results to finsets? (I'm going to only work with finsets for k-connectivity)

[Kyle Miller]

if definitions and lemmas don't need finsets, I'd suggest sticking with sets

[Vincent Beffara]

BTW, saying that two walks visiting the same list of vertices are equal is something we want on simple graphs, but not necessarily on multigraphs or weighted graphs or whatever in the hierarchy

[Kyle Miller]

walks <-> lists of darts should work in general

[Vincent Beffara]

Yes if you know the starting point

[Vincent Beffara]

Vincent Beffara said:

Yaël Dillies said:

Vincent Beffara said:

One thing that I found useful was a type for walk steps (i.e. ordered pairs of adjacent vertices) as opposed to a type sym2 V for edges, in general I found that working with G.edges was not very pleasant.

Do you know about docs#simple_graph.dart?

I do now :-)

Hmm, it is in degree_sum.lean which is not intuitive, I would have expected to find such a definition in basic.lean

[Kyle Miller]

There are a few more slices of #8737, if anyone wants to take a look:

• #13304 that nth powers of the adjacency matrix count walks of length n
• #13306 for deleting edges from a simple_graph.subgraph
• #13310 for pushing walks forward through a graph homomorphism

There's also #12766 (connected components), which I think @Bhavik Mehta wanted to do something with.

[Kyle Miller]

There's also now #17213 for acyclic graphs and trees (so finally got around to the "trees" part of the "walks_and_trees" branch)

[Kyle Miller]

I defined acyclicity in terms of nonexistence of cyclic walks, though in the future we can also have a theorem characterizing it in terms of the non-existence of cyclic subgraphs. Cyclic subgraphs haven't been defined yet, though I have a tentative definition in a branch somewhere (as a subgraph that has the same vertices and edges as a cyclic walk).

[Rémi Bottinelli]

Would "a tree is a maximal connected graph on its support" fit there too?

[Kyle Miller]

Yeah, that would be a nice additional theorem in this module (though with "minimal" of course!)

[Kyle Miller]

I suppose (using the PR theorem names) you could use is_acyclic_iff_forall_is_bridge to say every edge in a tree is a bridge, then use the definition of is_bridge itself, which is that removing it makes two vertices become unreachable from one another (hence the graph is not connected).

[Rémi Bottinelli]

So one direction is easily covered (looks like a fun exercise, I might give it a try!)

[Kyle Miller]

Just for completeness, I'm imagining the formulation G.is_tree <-> for all H <= G, H.is_tree -> H = G (or however we're supposed to say something is minimal with some property)

[Kyle Miller]

Yeah, please do!

[Rémi Bottinelli]

still wrong I believe? Or maybe we just don't have the same definition in mind? I was thinking of the "maximal tree = minimal connected subgraph" equivalence.
What about
G.is_tree <-> G.connected /\ for all H <= G, H.connected /\ H.verts = univ -> H = G ?

[Kyle Miller]

We don't need H.verts since this is for H : simple_graph V such that H <= G, which has the fact it's a spanning subgraph built in

[Kyle Miller]

This is the somewhat awkward (but still often convenient) thing that there are two notions of subgraphs

[Jérémie Turcotte]

@Kyle Miller This seems great! I was working on something similar actually. I've defined the number of connected components (as the card of connected_components) and was showing that it either goes up by 0 or 1 when removing an edge. There is a good overlap with what you have done here. I would just suggest is_bridge, is_bridge_iff_forall_walk_mem_edges, is_bridge_iff_forall_cycle_not_mem.aux, is_bridge_iff_forall_cycle_not_mem be put in the main connectivity file maybe? As they are more related with connectivity than trees in my opinion, and because I would like to use them there.

[Jérémie Turcotte]

I also have one concern about your definition for bridge. Under your current definition, even non edges of G could be bridges, right? I would add G.adj u v (or something else equivalent) in the definition. Let me know what you think.

[Kyle Miller]

@Jérémie Turcotte Yes, I had it so that non-adjacent vertices could be considered to be bridge edges, since I had felt it simplified a number of statements, since otherwise you need to add conjunctions with G.adj v w.

In any case, I've change the definition in #17213 to one on sym2 V, using a sym2 function that was introduced since I'd first written this (docs#sym2.lift).

[Kyle Miller]

I've also moved is_bridge to connectivity.lean, but I do worry that the file is getting rather long!

[Rémi Bottinelli]

Couldn't the walk,paths,circuit stuff be moved to walks.lean, and then perhaps even splitthe part about subgraphs?

[Kyle Miller]

Yes, that probably makes sense

[Kyle Miller]

It might also make sense to have walk_defs.lean for just the definitions of all the functions, though some of the functions depend on a handful of lemmas in their definitions.

[Yaël Dillies]

I think it's better to keep lemmas and definitions together

[Jérémie Turcotte]

@Kyle Miller Great thanks! Once your changes are accepted and are on the main branch, I'll add my stuff as well on the number of connected components, since I've rewritten it some of it to use what you did.

[Rémi Bottinelli]

@Jérémie Turcotte It's only clicking now, but what's your aim with your code? With @Anand Rao we've been working on the construction of ends of a graph and hence have very similar code to "removing an edge only increases the number of connected component".

[Rémi Bottinelli]

I'm now wondering how best to use what mathlib provides for our purposes, and whether/how we could piggyback on your work (I mean, our code works already for this, but we didn't figure a very convincing way to define it in a way that could be upstreamed to mathlib)

[Jérémie Turcotte]

In a broad sense our aim is to add the contents of a standard introductory graph theory class to mathlib. For this question specifically, I defined the number of connected components (using fintype.card) with the aim of showing the standard equivalences between definitions of cut edges (or bridges), such as removing a cut edge increases the number of connected components by exactly 1, and for non cut edges by 0 (the latter by just showing it doesnt affect reachability). Then, using this we have a standard inductive proof that in a forest the number of edges is equal to the number of vertices minus the number of connected components. We are mostly concerned about finite graphs (or at least, graphs with a finite number of components), so I'm not sure if this can be useful for you given you are working with ends. Let me know what you think.

[Rémi Bottinelli]

Ah, indeed, your applications seem quite independent from ours, too bad! I'm still wondering about/hoping for some construct that we could commonly build upon, but it's probably useless.
Here is our code, by the way.

[Kyle Miller]

@Jérémie Turcotte In the walks_and_trees branch there's a proof of that result about finite trees (but not forests) using the uniqueness of paths property

[Kyle Miller]

Nice to hear you have the more general version.

[Kyle Miller]

(deleted)

[Yaël Dillies]

Isn't connected components antitone from graphs to partitions?

[Kyle Miller]

Yes (though set or subgraph partitions, not docs#simple_graph.partition), which is consistent with how cutting an edge can increase the number of connected components by one. This contravariance is used (or can be used) for the definition of ends of a graph.

Btw, I have the partition of a graph into connected subgraphs here in a rather disorganized branch, though it doesn't explicitly have the partition or the fact the map is antitone.

[Rémi Bottinelli]

Mmh, I tried checking out your pull request to play with it but it makes codium/lean crash. Is there anything particular to it that may cause that?

[Rémi Bottinelli]

@Kyle Miller I'm giving this characterization of trees a go here and have a few questions:

• There is delete_edges in the API, but no add_edges. Could we add such a construction?

• There is to_delete_edges to map a walk avoiding the deleted edges to a walk in the resulting graph.
  At some point I wrote this to deal with mapping paths to subgraphs. Would it make sense to port this code so that to_delete_edges is actually just a special case of mapping to a subgraph? In my code here I didn't really use .edges, but I think it should be easy to port it to this kind of formulation, say:
  def map_induced (H ≤ G) (w : G.walk x y) (disjonit w.edges H.edge_set) : H.walk x y := sorry

• Finally, would the statements as written in my stub fit or were you looking for something else?

[Rémi Bottinelli]

Here is what I have in mind for mapping walks between graphs:

import combinatorics.simple_graph.connectivity
import combinatorics.simple_graph.basic

open function

namespace simple_graph

variables {V : Type*} {G : simple_graph V} {u v : V}


namespace walk

lemma cons_is_cycle_iff {u v : V} (p : G.walk v u) (h : G.adj u v) :
  (p.cons h).is_cycle ↔ p.is_path ∧ ¬ ⟦(u, v)⟧ ∈ p.edges :=
begin
  split,
  { simp only [walk.is_cycle_def, walk.cons_is_trail_iff, ne.def, not_false_iff, walk.support_cons,
               list.tail_cons, true_and, simple_graph.walk.is_path_def],
    tauto, },
  { exact λ ⟨hp,he⟩, path.cons_is_cycle (⟨p,hp⟩ : G.path v u) h he, },
end

end walk

namespace walk

@[simp] def induce : Π {u v : V} (p : G.walk u v) {H : simple_graph V}
  (h : ∀ e, e ∈ p.edges → e ∈ H.edge_set), H.walk u v
| _ _ (walk.nil) H h := walk.nil
| _ _ (walk.cons a p) H h := by
  { refine walk.cons _ (p.induce _);
    simp only [walk.edges_cons, list.mem_cons_iff, forall_eq_or_imp, mem_edge_set] at h,
    exact h.1, exact h.2, }

variables (w : V) (p : G.walk u v) (q : G.walk v w)
  {H : simple_graph V} (h : ∀ e, e ∈ p.edges → e ∈ H.edge_set)

lemma induce_id : p.induce (λ e ep, edges_subset_edge_set p ep) = p := by
{ induction p, simp, simp [p_ih], }

lemma induce_eq_map_spanning_subgraphs (GH : G ≤ H) :
  p.induce h = p.map (simple_graph.hom.map_spanning_subgraphs GH) := by
{ induction p, simp, simp [p_ih], }

@[simp] lemma induce_edges : (p.induce h).edges = p.edges := by
{ induction p, simp, simp [p_ih], }

@[simp] lemma induce_support : (p.induce h).support = p.support := by
{ induction p, simp, simp [p_ih], }

lemma is_path_induce (hp : p.is_path) : (p.induce h).is_path := by
{ induction p, simp, simp [cons_is_path_iff] at hp ⊢, simp [p_ih, hp], }

def is_cycle_induce {u : V} (p : G.walk u u) {H : simple_graph V}
  (h : ∀ e, e ∈ p.edges → e ∈ H.edge_set) (hp : p.is_cycle) : (p.induce h).is_cycle := by
{ cases p,
  { simp at hp ⊢, exact hp, },
  { simp [cons_is_cycle_iff] at hp ⊢,
    refine ⟨_,hp.right⟩,
    apply is_path_induce,
    exact hp.left, }, }

end walk

end simple_graph

[Kyle Miller]

@Rémi Bottinelli Some thoughts on PRs

For this one:

• It would be great to have is_acyclic.le and connected.le (that could be a short PR). You might swap the H ≤ G with the property argument so that it's clearer to see how they're functorial (dot notation will still work), and I think Yael would suggest calling them is_acyclic.anti and connected.mono.

• The rest of the theorem statements look like something we would want too. I'm wondering if we want something more general, where rather than min_connected it's a predicate that means the subgraph's inclusion map induces a bijection on pi_1. That way min_whatever_its_called is equivalent to having an acyclic spanning subgraph.

Regarding mapping to subgraphs, I think your idea to change to_delete_edges to be a special case is a good one. I have a bit of a different definition somewhere for a path being contained in a subgraph that I think would fit into existing API better (that p.to_subgraph ≤ H, where to_subgraph gives the subgraph with the same vertices and edges), and maybe I'll dust that off and merge in some of what you have in that file?

[Rémi Bottinelli]

Re. mapping to subgraphs, I've changed the definition to something more general here, and there is even a reimplementation of to_delete_edges (but p.to_subgraph ≤ His pretty neat)

[Rémi Bottinelli]

Re. is_acyclic.le and connected.le, I guess is_acyclic.le is dependent on your PR in any case, so probably the easiest is for you to directly include that?

[Rémi Bottinelli]

One lemma I really needed here was this one about extracting a path connecting two ends of an edge out of a cycle containing that edge.
Is there code for it? how would it fit in mathlib if there isn't?

[Rémi Bottinelli]

I'm thinking of doing a PR with the induce code instead of lazily waiting for things to happen. Does that work for you @Kyle Miller ?

[Kyle Miller]

@Rémi Bottinelli That seems like a reasonable way forward to get something to happen. Once you have it, at some point I might help and add enough to get p.to_subgraph ≤ H to work if you don't mind.

[Rémi Bottinelli]

OK, I might as well use that directly. Let me give it a go, and I'll keep you updated!
Actually, I'll stick with my method for now, to_subgraph might be more complicated than expected.

[Kyle Miller]

@Rémi Bottinelli Please write your PR as you're writing it, but I thought I'd let you know that I created a walk.to_path PR from what I had in a branch (#17325).

It's worth you doing what you're doing so that we get a chance to evaluate multiple designs, and if we switch to walk.to_path I expect it to be quick to transform.

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/17326
I'm done for today, but here is most of it I guess? I'll look more closely at getting correct names and what other lemmas should be added tomorrow.
In the meantime, what's the correct way to handle my private lemmas here?

[Jérémie Turcotte]

Let me note that my code for number of connected components and all that is basically ready, but given it is dependant on the is_bridge PRs, I'll wait for those to be merged before PRing that (I don't have enough git experience to attempt making a PR dependent on those). We're going to work on other stuff in graph theory in the meantime.

[Kyle Miller]

@Jérémie Turcotte Feel free to create that PR. There aren't really any special features for PRs depending on others except for a way in the PR text to declare PRs that should be merged first. We can help get that right.

[Kyle Miller]

Also, you and/or Remy might consider reviewing the PR(s) you're depending on, which should accelerate the process. There are not many combinatorics reviewers (and I shouldn't review my own PRs!), but maintainers with another expertise might be comfortable merging them if they've been reviewed.

[Rémi Bottinelli]

I can give reviewing a go, but am not sure I have the credentials/knowledge to be of any use. Is there any kind of checklist/guide to making useful reviews?

[Johan Commelin]

Here are some general guidelines for reviewing (stolen from a list that Kyle put together at some point):

• Does it adhere to mathlib style?
• Do declarations follow the naming convention?
• Are declarations generally in the right files? Do they not already exist elsewhere under a different name or level of generality?
• Are there any obvious opportunities to split off supporting lemmas or definitions?
• Is it maintainable code that follows accepted practices?
• Does it provide a sensible API?
• Has it been generalized to support known future needs?
• Does it fit into the design and collective vision of the library?
• Is it formalizing something from the literature?

[Rémi Bottinelli]

Thanks!

[Rémi Bottinelli]

This is a bit simp-heavy, but would it be PR-able?

lemma cons_is_cycle_iff_nodup : Π {u v: V} (a : G.adj v u) (p : G.walk u v),
  (walk.cons a p).is_cycle ↔ 2 ≤ p.length ∧ p.support.nodup
| _ _ a walk.nil :=  (a.ne rfl).elim
| _ _ a (walk.cons b walk.nil) := by
  { simp only [cons_is_cycle_iff, support_nil, list.mem_singleton, edges_cons, edges_nil,
               quotient.eq, sym2.rel_iff, eq_self_iff_true, or_true, not_true, and_false,
               length_cons, length_nil, zero_add, support_cons, list.nodup_cons, list.not_mem_nil,
               not_false_iff, list.nodup_nil, and_true, false_iff, not_and, not_not],
    rintro h, exfalso,
    linarith only [h], }
| _ _ a (walk.cons' x _ _ b (walk.cons' y z w c q)) := by
  { simp [cons_is_cycle_iff, is_path_def, nat.succ_le_succ_iff],
    push_neg,
    rintros ⟨xny, xnq⟩ ynq qnd,
    simp only [xny, ne.def, not_false_iff, implies_true_iff, true_and, and_true],
    have wny : w ≠ y, by
    { rintro h,
      simpa only [←h, end_mem_support, not_true] using ynq },
    simp only [wny, not_false_iff, is_empty.forall_iff, true_and],
    exact λ h, xnq (snd_mem_support_of_mem_edges _ h),
  }

lemma is_cycle_iff_nodup {u : V} (p : G.walk u u) :
  p.is_cycle ↔ 3 ≤ p.length ∧ p.support.tail.nodup :=
begin
  cases p,
  { simp only [is_cycle.not_of_nil, length_nil, le_zero_iff, nat.bit1_ne_zero, false_and], },
  { simp only [nat.succ_le_succ_iff, length_cons, support_cons, list.tail_cons],
    exact cons_is_cycle_iff_nodup _ _, },
end

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/17402 <- Short PR to allow mapping walks to supergraphs as discussed with @Kyle Miller.
I didn't use the code you provided for is_cycle_of_injective mostly since this one was already working for me and was thus less work.

[Rémi Bottinelli]

By the way, the connectivity file actually takes quite a lot of time to check. How would simp only everywhere reduce compilation time?

[Kyle Miller]

I'm not sure -- if it's a concern, probably the right thing to do is use the profiler to find the worst offenders and measure how much of an affect squeezed simps would have.

It's also just a big module. I'd like for everything that's about walks/paths/trails/cycles to eventually go into a new module, maybe combinatorics/simple_graph/walk.lean. Then the connectivity module would pick up at the definition of reachable.

[Kyle Miller]

I'm imagining the definitions of vertex connectivity and edge connectivity would eventually be in the connectivity module as well.

[Kyle Miller]

Side note: I think we have docs#simple_graph.walk.copy mis-named. Other examples of "copy" involve changing internal data, but this function is only changing the external data -- the indices. It's more analogous to docs#fin.cast.

I'm leaning toward renaming it to simple_graph.walk.cast. Are there any other possibilities?

[Kyle Miller]

@Jérémie Turcotte FYI, bridges, acyclic graphs, and trees are now all merged.

docs#simple_graph.is_bridge docs#simple_graph.is_acyclic docs#simple_graph.is_tree

[Jérémie Turcotte]

Great! I've done a PR, see #17654 . This is the first time I PR anything, so please let me know if I'm going anything wrong. Thanks!

[Jérémie Turcotte]

(The result comparing the # of edges, vertices, components in forests still needs a bit of cleaning up but will be done soon.)

[Rémi Bottinelli]

I've finished a version of the characterization of trees as maximal acyclic/minimal connected here but I'm not totally satisfied with the proofs: they look quite dirty. I would welcome some refactoring ideas if anyone wants to have a look!

[Rémi Bottinelli]

Side question: Why not make connected and preconnected into classes? That would be quite natural and allow to get metric_space as an instance for a graph too. No?

[Kyle Miller]

If you've got G : simple_graph V, it's not clear how you'd automatically get a metric_space V instance -- by just looking at V you can't (and shouldn't) automatically figure out you should be considering G. I say "shouldn't" because there isn't a uniquely interesting simple graph structure on V.

[Rémi Bottinelli]

Mmh, so there is friction coming from the different perspective between metric spaces and graphs I guess.

[Yaël Dillies]

The solution is to make a type synonym of V depending on G. Then we could register a pseudo-metric space instance, and Rémi's suggestion would allow to register a metric space one.

[Kyle Miller]

I didn't mention that because it's not clear it's the right thing to do, but it's certainly a valid design. To be clear, you wouldn't have metric_space V, but something like metric_space G.verts. A significant downside is that if you have v w : V then you can't use typeclass inference to immediately get the correct distance function; you'd have to have some mechanism to "cast" v and w to have the literal type G.verts for typeclass inference to get the correct distance function.

[Yaël Dillies]

That's inherent to having simple_graph not a class, I'm afraid.

[Yaël Dillies]

I already did something very similar for marked groups over at branch#geometric-group-theory, and the design I mentioned is painless.

[Rémi Bottinelli]

I tried this and it seems to work well enough : https://github.com/bottine/mathlib/blob/bottine/combinatorics.simple_graph.metric/some_lemmas/src/combinatorics/simple_graph/metric.lean

What was the motivation for defining simple_graph.dist in its truncated form?