## Stream: graph theory

### Topic: connectivity

#### Joseph Hua (Feb 18 2022 at 14:34):

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 (Feb 18 2022 at 14:51):

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.

#### Vincent Beffara (Feb 18 2022 at 14:53):

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 (Feb 18 2022 at 14:54):

This is the part most recently added: #11095

#### Kyle Miller (Feb 18 2022 at 14:55):

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

#### Vincent Beffara (Feb 18 2022 at 15:02):

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 (Feb 18 2022 at 15:11):

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 (Feb 18 2022 at 15:14):

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 (Feb 18 2022 at 15:15):

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 (Feb 18 2022 at 15:16):

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 (Feb 18 2022 at 15:16):

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

#### Kyle Miller (Feb 18 2022 at 15:17):

@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 (Feb 18 2022 at 15:18):

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

#### Vincent Beffara (Feb 18 2022 at 15:20):

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 (Feb 18 2022 at 15:20):

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

Ha! Good point.

#### Yakov Pechersky (Feb 18 2022 at 15:22):

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 (Feb 18 2022 at 15:23):

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

#### Vincent Beffara (Feb 18 2022 at 15:24):

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 (Feb 18 2022 at 15:25):

@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 (Feb 18 2022 at 15:26):

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 (Feb 18 2022 at 15:27):

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

#### Vincent Beffara (Feb 18 2022 at 15:29):

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 (Feb 18 2022 at 15:33):

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 (Feb 18 2022 at 15:34):

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

#### Vincent Beffara (Feb 18 2022 at 15:36):

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 (Feb 18 2022 at 15:39):

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 (Feb 18 2022 at 15:39):

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

#### Yakov Pechersky (Feb 18 2022 at 15:40):

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

#### Vincent Beffara (Feb 18 2022 at 15:41):

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 (Feb 18 2022 at 15:43):

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

#### Kyle Miller (Feb 18 2022 at 15:44):

@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 (Feb 18 2022 at 15:52):

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 (Feb 18 2022 at 16:02):

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 (Feb 18 2022 at 16:07):

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 (Feb 18 2022 at 16:12):

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 (Feb 18 2022 at 16:12):

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

#### Vincent Beffara (Feb 18 2022 at 16:16):

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 (Feb 18 2022 at 16:20):

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 (Feb 18 2022 at 16:23):

@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 (Feb 18 2022 at 16:24):

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

#### Joseph Hua (Feb 18 2022 at 16:24):

def induced_subgraph (s : set V) : G.subgraph :=
{ verts := s,
adj := λ u v, G.adj u v ∧ u ∈ s ∧ v ∈ s,
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 (Feb 18 2022 at 16:24):

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 (Feb 18 2022 at 16:25):

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

#### Kyle Miller (Feb 18 2022 at 16:26):

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

#### Kyle Miller (Feb 18 2022 at 16:27):

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 (Feb 18 2022 at 16:28):

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 (Feb 18 2022 at 16:29):

 def pullback (f : V → V') (G' : simple_graph V') : simple_graph V :=
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 (Feb 18 2022 at 16:30):

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

#### Kyle Miller (Feb 18 2022 at 16:30):

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 (Feb 18 2022 at 16:36):

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 (Feb 18 2022 at 16:39):

(top : G.subgraph).induced s

#### Joseph Hua (Feb 18 2022 at 16:39):

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 (Feb 18 2022 at 16:41):

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.

#### Kyle Miller (Feb 18 2022 at 16:41):

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 (Feb 18 2022 at 16:43):

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.

I do now :-)

#### Kyle Miller (Feb 18 2022 at 16:45):

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 (Feb 18 2022 at 16:54):

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 (Feb 18 2022 at 17:11):

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

#### Vincent Beffara (Feb 18 2022 at 17:35):

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 (Feb 18 2022 at 17:47):

walks <-> lists of darts should work in general

#### Vincent Beffara (Feb 18 2022 at 18:13):

Yes if you know the starting point

#### Vincent Beffara (Feb 18 2022 at 22:34):

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.

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 (Apr 10 2022 at 19:12):

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 (Oct 27 2022 at 18:00):

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 (Oct 27 2022 at 18:04):

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 (Oct 27 2022 at 18:12):

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

#### Kyle Miller (Oct 27 2022 at 18:16):

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

#### Kyle Miller (Oct 27 2022 at 18:18):

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 (Oct 27 2022 at 18:19):

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

#### Kyle Miller (Oct 27 2022 at 18:19):

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)

#### Rémi Bottinelli (Oct 27 2022 at 18:23):

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.
G.is_tree <-> G.connected /\ for all H <= G, H.connected /\ H.verts = univ -> H = G ?

#### Kyle Miller (Oct 27 2022 at 18:25):

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 (Oct 27 2022 at 18:26):

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

#### Jérémie Turcotte (Oct 27 2022 at 18:54):

@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 (Oct 27 2022 at 19:06):

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 (Oct 28 2022 at 14:39):

@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 (Oct 28 2022 at 14:49):

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

#### Rémi Bottinelli (Oct 28 2022 at 14:52):

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

#### Kyle Miller (Oct 28 2022 at 14:58):

Yes, that probably makes sense

#### Kyle Miller (Oct 28 2022 at 14:59):

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 (Oct 28 2022 at 15:33):

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

#### Jérémie Turcotte (Oct 28 2022 at 18:03):

@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 (Oct 28 2022 at 18:32):

@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 (Oct 28 2022 at 18:33):

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 (Oct 28 2022 at 18:42):

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 (Oct 28 2022 at 18:49):

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 (Oct 28 2022 at 18:54):

@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 (Oct 28 2022 at 18:54):

Nice to hear you have the more general version.

(deleted)

#### Yaël Dillies (Oct 28 2022 at 19:28):

Isn't connected components antitone from graphs to partitions?

#### Kyle Miller (Oct 28 2022 at 19:44):

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 (Oct 29 2022 at 06:20):

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 (Oct 30 2022 at 13:51):

@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 (Oct 31 2022 at 06:57):

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 (Nov 02 2022 at 10:26):

@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 (Nov 02 2022 at 10:31):

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 (Nov 02 2022 at 10:33):

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 (Nov 02 2022 at 10:48):

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 (Nov 03 2022 at 15:27):

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 (Nov 03 2022 at 15:36):

@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 (Nov 03 2022 at 16:08):

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 (Nov 03 2022 at 17:00):

@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 (Nov 03 2022 at 18:52):

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 (Nov 04 2022 at 04:12):

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 (Nov 04 2022 at 07:03):

@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 (Nov 04 2022 at 07:08):

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 (Nov 04 2022 at 08:07):

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 (Nov 04 2022 at 08:20):

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?

Thanks!

#### Rémi Bottinelli (Nov 06 2022 at 10:34):

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 (Nov 07 2022 at 07:45):

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 (Nov 07 2022 at 15:13):

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 (Nov 07 2022 at 15:39):

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 (Nov 07 2022 at 15:41):

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

#### Kyle Miller (Nov 07 2022 at 15:44):

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 (Nov 19 2022 at 18:25):

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

#### Jérémie Turcotte (Nov 21 2022 at 00:31):

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 (Nov 21 2022 at 00:33):

(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 (Nov 27 2022 at 10:46):

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 (Dec 17 2022 at 12:54):

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 (Dec 19 2022 at 15:24):

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 (Dec 19 2022 at 16:13):

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

#### Yaël Dillies (Dec 19 2022 at 19:54):

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 (Dec 19 2022 at 20:04):

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 (Dec 19 2022 at 20:06):

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

#### Yaël Dillies (Dec 19 2022 at 20:07):

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 (Feb 21 2023 at 07:46):

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?

Last updated: Aug 03 2023 at 10:10 UTC