classes for symmetric transitive relation

Stream: Is there code for X?

[Rémi Bottinelli]

Hey! I have a symmetric transitive relation on a type, and I'd like to get the partition of “the type minus the non-reflexive points”. Is there a most efficient way to do this? The plan so far is to get rid of the non-reflexive points manually in order to get an equivalence relation, then setoid, then get its classes, and take them back to the original type.

[Yaël Dillies]

This sounds like an #xy problem. What's the context?

[Rémi Bottinelli]

I have a graph G on V and a subset K of V, I want to define the connected components of V-K. I feel like it's better to have everything living inside V (so that the connected components would be given by an element of set (set V)) because K will vary, and I will want to say e.g. that if C is such a component for a given K, it still is connected for a smaller K', hence contained in one of its components).

[Rémi Bottinelli]

But you're right, maybe I'm looking at this the wrong way.

[Rémi Bottinelli]

And I defined the equivalence as

def connected_outside (K : set V) (x y : V) : Prop :=
  ∃ w : walk G x y, disjoint K (w.support.to_finset : set V)

[Yaël Dillies]

Yeah so I would advise you to take the reflexive closure of your aforementioned connected_outside and then all vertices in K will give singleton connected components.

[Rémi Bottinelli]

And then get rid of them “by hand” ?

[Yaël Dillies]

Why do you want to get rid of them?

[Rémi Bottinelli]

huh, good question, actually. The end goal is to define the ends of my graph.

[Rémi Bottinelli]

It feels a bit wrong to keep them (“semantically”), but actually, I don't think it would necessarily mess with the construction. Thanks for #xy-ing me :)

[Vincent Beffara]

Well adding singleton connected components is not going to change the number of infinite components :-)

[Yaël Dillies]

One thing you could do is to define connected components of a subgraph and the -K operation on subgraphs.

[Rémi Bottinelli]

Right, I just figured they'd get discarded when dropping the finite components anyway, which simplifies business.

[Yaël Dillies]

But yeah I think that what you just described works simply.

[Vincent Beffara]

Yaël Dillies said:

One thing you could do is to define connected components of a subgraph and the -K operation on subgraphs.

I was about to make the same suggestion

[Rémi Bottinelli]

What would I gain from such a strategy? It seems it would add quite a few steps in the construction, _and_ induce a need for coercions later on, no? I guess the advantage is the possibility of generic/reusable constructions?

[Yaël Dillies]

I haven't thought much about it, but both solutions seem doable. Maybe try them out and see?

[Rémi Bottinelli]

I think I'll try and stick with the basic one for now.
I noticed it's much easier to have fewer constructions and lots of lemmas: you spend more time doing actual proofs and less time frustrated with not-so-easy boilerplate.
But I'll keep the other approach in mind for later, possibly :)

[Vincent Beffara]

I can also sell you this approach:

def pull (f : V → V') (G' : simple_graph V') : simple_graph V :=
{ adj := G'.adj on f,
  symm := λ _ _ h, G'.symm h,
  loopless := λ _, G'.loopless _ }

def select (P : V → Prop) (G : simple_graph V) : simple_graph (subtype P) :=
pull subtype.val G

def some_name (G : simple_graph V) (K : set V) := select (\lambda v, v \notin K) G

Where the pullback operation is generic and not part of your specific construction. But that is a little like reinventing subgraphs in a less usable way, probably.

[Vincent Beffara]

(Or replacing subtype.val by however the canonical inclusion map from a set to the ambient type is called.)

[Rémi Bottinelli]

heh, that's neat

[Yaël Dillies]

I think that's a very usable way to do subgraphs so long as you don't want to compare them.