## Stream: graph theory

### Topic: Trees

#### Yaël Dillies (Aug 17 2021 at 12:31):

@Kyle Miller, what's your opinion on defining trees and forests? We need trees for an Oxford Invariants problem before next Monday. We also need the fact that they are 2-colorable and that there's a unique avoiding path between any two points.

#### Yaël Dillies (Aug 17 2021 at 12:33):

I think we could define the typeclasses is_forest G and is_connected G somehow (wink wink your path definition) and then let is_tree G extend them both.

#### Kevin Buzzard (Aug 17 2021 at 12:36):

Why not just make an invariants repo?

#### Yaël Dillies (Aug 17 2021 at 13:12):

We definitely could, but I ought to silently push graphs things a little :innocent:

#### Kyle Miller (Aug 18 2021 at 09:19):

@Yaël Dillies Ok, here you go #8737

#### Kyle Miller (Aug 18 2021 at 09:20):

You should be able to get your 2-coloring with G.tree_dist. (Though colorings don't exist yet per se.)

#### Kyle Miller (Aug 18 2021 at 09:24):

I can't work on this anymore for now, but it can certainly stand to have some cleanup! Feel free to help refactor it or fill in missing functionality (ideally the kind that simplifies things).

My main goal was just to show that all the definitions work together to reasonably prove a few characterizations of acyclic graphs. My proofs aren't always locally so reasonable -- I just wanted to get to the end.

#### Kyle Miller (Aug 18 2021 at 09:27):

For now, I think it's better to use structures for is_tree and such instead of typeclasses. I'm not convinced it won't go through cycles of (un)bundling

#### Yaël Dillies (Aug 18 2021 at 10:44):

Kyle, when are you moving in? :big_smile:

#### Yaël Dillies (Aug 18 2021 at 10:45):

This is like... amazing. I really wish this gets in mathlib.

#### Yaël Dillies (Aug 18 2021 at 10:46):

One thing though, with your definition of path, eulerian paths are trails, but not paths. Is that on purpose?

#### Johan Commelin (Aug 18 2021 at 10:53):

It's a bit of a monster PR...

#### Johan Commelin (Aug 18 2021 at 10:53):

Do you think this can be cut into pieces?

#### Yakov Pechersky (Aug 18 2021 at 11:53):

Do you mind if I try to port walks to a list based defn? I think you wouldn't have to copy the API as much. And then cycles would be based on the cycle data structure.

#### Kyle Miller (Aug 18 2021 at 16:17):

Yaël Dillies said:

One thing though, with your definition of path, eulerian paths are trails, but not paths. Is that on purpose?

All I did was choose some pre-existing convention, and it seems every choice is awkward somewhere. Wikipedia says that an Eulerian path is also known as an Eulerian trail at least. Another awkward naming thing is Eulerian cycle, which would be called an Eulerian circuit (a circuit only has the no-repeating-edges condition -- I forgot to define them) though Wikipedia also mentions both names.

#### Kyle Miller (Aug 18 2021 at 16:17):

Another convention could be to have paths and simple paths instead of walks and paths. I suppose trails remain trails? With this, maybe it would be walk.is_path -> walk.is_simple and path -> simple_path.

#### Yaël Dillies (Aug 18 2021 at 16:22):

Okay sure :smiling_face: I'm not against having more words than the usual mathspeak to disambiguate notions.

#### Mauricio Collares (Aug 18 2021 at 16:25):

I think "path" and "simple path" is more popular in CS, while "walk" and "path" is more popular in mathematics (not that it matters, but I prefer "walk" and "path"). What people do in Combinatorics articles, I think, is to pick a book (for example, the introductory textbooks by Bollobás, Bondy and Murty or Harary) and use the basic definitions from the chosen book consistently.

#### Kyle Miller (Aug 18 2021 at 16:26):

Johan Commelin said:

It's a bit of a monster PR...

As the saying goes, "I apologize for such a long letter -- I didn't have time to write a short one." :smile: I think it can be shorter purely from being more careful about what's going on.

But also, yeah, it can (and probably should) be cut up. I just wanted to get to a point that would show everything actually fits together and proves useful basic theorems about acyclic graphs. (Fun fact: it's also going through the new subgraph module to define bridge edges. An edge is a bridge if when you remove it there is no longer a path between the vertices the edge was incident to. This is later characterized in a lemma as "an edge is a bridge if every walk between its incident vertices contains the edge.")

#### Kyle Miller (Aug 18 2021 at 16:29):

One thing I think I made a mistake with is defining walk.edges as taking values in G.edge_set, but I'm not completely sure. It could have easily been sym2 V along with a lemma to prove the edges like in G.edge_set. The reason it's a possible mistake is that it means you have to write (⟨⟦(v, w)⟧, h⟩ : G.edge_set) too frequently, even if you don't care about it specifically being an element of the edge set.

#### Kyle Miller (Aug 18 2021 at 16:45):

Yakov Pechersky said:

Do you mind if I try to port walks to a list based defn? I think you wouldn't have to copy the API as much. And then cycles would be based on the cycle data structure.

It seems like it's very important having "categorical lists" instead of plain lists, at least for me to have gotten to the end. A "categorical list" is a list-like structure where each end has a type, and you can only concatenate lists with compatible ends -- in other words they can be regarded as paths in a category. Plain lists are categorical lists with only a single type (so they're paths in a monoidal category).

I'm wondering whether it would make sense to define a clist type instead. It would be like docs#relation.refl_trans_gen but be Type-valued. Not sure I got the universes right:

universes u v
inductive clist {α : Type u} (r : α → α → Sort v) : α → α → Type (max u v)
| nil {x : α} : clist x x
| cons {x y z : α} (hd : r x y) (tl : clist y z) : clist x z


Reverse could look something like

namespace clist

protected def reverse_aux (f : Π {x y : α}, r x y → r y x) :
Π {u v w : α}, clist r u v → clist r u w → clist r v w
| _ _ _ nil q := q
| _ _ _ (cons h p) q := reverse_aux p (cons (f h) q)

def reverse {u v : α} (f : Π {x y : α}, r x y → r y x) (w : clist r u v) : clist r v u :=
w.reverse_aux @f nil

end clist


#### Kyle Miller (Aug 18 2021 at 16:46):

But I'm just telling you what I think. If porting it to lists makes things simpler, then I'll happily switch over to what you write.

#### Yakov Pechersky (Aug 18 2021 at 16:53):

I'm trying it out on the PR. Will report back!

#### Yakov Pechersky (Aug 18 2021 at 16:55):

Your clist is a Sort generalization of list.chain, which is what I'm using for walks over simple graphs, since our edges are in Prop here.

#### Kyle Miller (Aug 18 2021 at 16:56):

(@Mauricio Collares I actually happen to slightly prefer "path" and "simple path" but it seemed that "walk" and "path" were more traditional. If anything, your vote to leave it as-is matters quite a lot since it's broken the tie!)

#### Kyle Miller (Aug 18 2021 at 16:58):

@Yakov Pechersky We're going to need a type-valued version for multigraphs though. Is there something that can hold onto the edge?

#### Yaël Dillies (Aug 18 2021 at 17:01):

I thought about all this paths on multigraphs stuff, and I came to the conclusion that it was maybe desirable to have different definitions of paths for multigraph and simple graph or, at the very least, a solid API to describe multigraph paths in terms of vertices when the multigraph is simple.

#### Kyle Miller (Aug 18 2021 at 17:05):

clist by the way is essentially docs#quiver.path. The difference is that a quiver is a typeclass that gives the r argument in clist.

#### Yakov Pechersky (Aug 18 2021 at 17:16):

Clunkily, one can use a proposition of "edge between v and w is in my graph". In the case of a simple graph, that's just G.adj. Even in a directed graph, this should work. In multigraphs, it can be a set membership. But I don't want to bikeshed on that level of generality. Just trying to see whether making the equivalence with list.chain more explicit helps or hurts. My inclination to us lists is because of existing infrastructure for recursors, folds, maps, etc.

#### Kyle Miller (Aug 18 2021 at 17:22):

Just to help choose the color of shingles for this bikeshed, I know mathlib has headed in a classical direction, but I find it pleasing when concrete data can remain concrete data, like having paths that actually know their edges.

#### Kyle Miller (Aug 18 2021 at 17:22):

Something you might consider is having your lists consist of darts (docs#simple_graph.dart), and then all the chain needs to know is that adjacent darts are compatible, rather than having knowledge about the adjacency relation.

#### Kyle Miller (Aug 18 2021 at 17:27):

I guess this is different, since you're dealing with lists of the vertices, not of the edges.

#### Yakov Pechersky (Aug 18 2021 at 17:35):

Or the underlying list is [(vertex, edge)]

#### Yakov Pechersky (Aug 18 2021 at 17:35):

Which is similar to your dart suggestion

#### Kyle Miller (Aug 18 2021 at 17:39):

The reason darts contain the opposite vertex is so they're easy to reverse. It's not that big of a deal, but docs#sym2.mem.other is noncomputable, and then you'd have to rewrite with docs#sym2.other_invol

#### Kyle Miller (Aug 19 2021 at 17:20):

I did some amount of cleanup (including switching to sym2 V for walk.edges rather than G.edge_set), though there's still more to do.

#### Kyle Miller (Aug 19 2021 at 17:21):

Just to make the PR more of a monster, I've added

theorem adj_matrix_pow_apply_eq_card_walk (n : ℕ) (u v : α) :
(G.adj_matrix R ^ n) u v = fintype.card {p : G.walk u v // p.length = n}


in addition to definitions for Eulerian and Hamiltonian walks, k-edge-connectivity, and a proof that the G.reachable relation is equivalent to relation.refl_trans_gen G.adj.

#### Yakov Pechersky (Aug 20 2021 at 02:19):

I pushed branch#pechersky/walks_and_trees, where I added ~400 lines of list API to make the list.chain' defns work. I got up to subwalk_from.

#### Yakov Pechersky (Aug 20 2021 at 02:20):

Some of the docstrings might be wrong because I changed a few things and maybe forgot to change them back

#### Kyle Miller (Aug 20 2021 at 10:11):

Using lists for support and edges is a good idea. That way every path has both a list of vertices and a list of edges, and you can get stronger lemmas like

lemma reverse_edges {u v : V} (p : G.walk u v) : p.reverse.edges = p.edges.reverse


I switched #8737 over to using them instead of multisets.

#### Yakov Pechersky (Aug 20 2021 at 12:17):

If you define more through lists, the "rotate" is also easier to implement. And the property you have now of "support (p.rotate n) ~ support p" is actually stronger, "~r"

#### Kyle Miller (Aug 20 2021 at 17:25):

rotate is just one line though?

~r would be nice, but I can't find this lemma:

lemma list.is_rotated_append {l₁ l₂ : list α} : (l₁ ++ l₂) ~r (l₂ ++ l₁)


#### Yaël Dillies (Aug 20 2021 at 17:54):

Should be easy to get from something like list.rotate_eq_drop_append_take.

#### Kyle Miller (Aug 20 2021 at 17:54):

I guess it wasn't so hard to prove:

lemma is_rotated_append {l₁ l₂ : list α} : (l₁ ++ l₂) ~r (l₂ ++ l₁) :=
begin
use l₁.length,
rw rotate_eq_rotate',
induction l₁ generalizing l₂,
{ simp, },
{ simp [rotate', l₁_ih], },
end


#### Kyle Miller (Aug 20 2021 at 18:15):

#8780

Last updated: Dec 20 2023 at 11:08 UTC