feat(combinatorics/simple_graph): connectivity

[kmill]

Provides walks, trails, paths, cycles, forests, and trees.

Walks are set up so that G.walk v w is the type of all walks between vertices v and w, and it is the type version of the transitive closure of the G.adj relation. It is expected that anyone who wants the type of all walks will use a sigma type.

The function walk.to_path converts walks to paths by excising loops wherever there are repeated vertices.

The prop version of G.walk v w is G.reachable v w. The quotient of the vertex type by this gives the type connected_component. A graph is defined to be connected when everything is related by G.reachable.

Naturally, acyclicity is defined as non-existence of cycles (which are nontrivial trails from a vertex to itself with no repeating vertices along the way) and there are characterizations of acyclicity as (1) every edge is a bridge edge and (2) uniqueness of paths between any given points.

A tree is a connected acyclic graph. There is a function to get the unique path between pairs of vertices, and with this we define the tree metric tree_dist.

This drew some inspiration from [Chou1994], which formalizes these things for multigraphs in HOL. The connectivity module should easily generalize to multigraphs (through application of elbow grease) once they're sorted out.

---

[kmill]

Many of the proofs are monstrosities right now. It seems like there are patterns in proofs that could be turned into lemmas, but I was just focused on getting the main theorems about acyclic graphs done.

Help wanted!

[barrettj12]

Hey @kmill, I might be able to help. Can you clarify what exactly you want help with?

[kmill]

@barrettj12 Thanks. I think what can be helpful at this point is to figure out how to simplify the proofs of the things starting around line 1000 of connectivity.lean. There are also a few things before then that should be nicer too. I suspect there are some missing lemmas that could clean them up (perhaps by finding better-thought-out proofs -- all I tried to do was get to the end).

A reason this is important is because I've been using these theorems to help guide and prove the design. There's still some chance some details of how things work might change depending on what the theorems might need.

I'm planning on carving out a much smaller PR with at least the definitions soon.