Connectedness

Stream: graph theory

[Peter Nelson]

Why is SimpleGraph.Connected not a class?

[Yaël Dillies]

Why would it be?

[Yaël Dillies]

The one reason I see for it to be a typeclass would be if you reasoned about the metric space induced by the simple graph. We don't have this yet, and it would need to go on a type synonym, so I'm not sure having SimpleGraph.Connected being a typeclass (rather than using Fact G.Connected) is particularly advised

[Peter Nelson]

I'm trying to define, for each G : SimpleGraph V and vertex a : V, a partial ordering on (a type synonym for) V, where $x \le y$ means that there is a shortest path from a to y that contains x. I'd like to use all the typeclass machinery for orderings (This is a Nat-graded order where covering implies adjacency etc etc), but things are only nice if the graph is connected.

[Peter Nelson]

Fact works of course, but what is the downside to it being a class?

[Kyle Miller]

An argument against it is that graphs tend to be manipulated using algebraic rules, but the typeclass system doesn't carry instances across equalities automatically. You can lose instances after rewriting.

Another argument against is that theorems that take Connected instances would only apply if you actually have a Connected instance in context. For example, if you apply such a theorem you wouldn't get a Connected goal, it would just fail.

On the other hand, some graphs are special, and it makes sense to permanently associate the fact it is Connected to it.

[Kyle Miller]

For you application, can't your type synonym include the hypothesis that G is connected?