Grind annotations for reachability

Stream: graph theory

[Snir Broshi]

#31780 added grind annotations for length_{support,darts,edges}, and now I thought maybe we should tag Adj.symm/Adj.reachable/Reachable.refl/Reachable.symm/Reachable.trans.
This should help grind reason about which vertices are in the same connected component.
Maybe ConnectedComponent.eq/ConnectedComponent.sound/ConnectedComponent.exact are also useful.
Wdyt? Also how do I choose which modifier to put in the annotation (=/./_/←/→)?

[Jakub Nowak]

Snir Broshi said:

Also how do I choose which modifier to put in the annotation (=/./_/←/→)?

That's a good question. I usually use grind? and choose one that gives what I think is the best grind_pattern. Though, which is the best grind_pattern is yet another question. I try to think about possible scenarios in which theorem is useful and whether the particular grind_pattern would be matched in these scenarios.

[Snir Broshi]

To understand that explanation I'd first need to understand what grind_pattern is :sweat_smile: