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 (=/./_/←/→)?