Trees

Stream: graph theory

[Yaël Dillies]

@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]

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]

Why not just make an invariants repo?

[Yaël Dillies]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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]

Kyle, when are you moving in? :big_smile:

[Yaël Dillies]

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

[Yaël Dillies]

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

[Johan Commelin]

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

[Johan Commelin]

Do you think this can be cut into pieces?

[Yakov Pechersky]

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]

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]

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]

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

[Mauricio Collares]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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]

(@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]

@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]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Which is similar to your dart suggestion

[Kyle Miller]

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]

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]

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]

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]

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

[Kyle Miller]

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]

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]

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]

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

[Kyle Miller]

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]

#8780