Transitive symmetric relations

Stream: Is there code for X?

[Peter Nelson]

Is there anything in mathlib to handle binary relations that are transitive and symmetric but not necessarily reflexive? Specifically, I'd like to construct the collection of 'equivalence classes', with disjointness, properties of transversals, etc etc. Clearly it's not rocket science to just do it myself, or even to reduce it to the equivalence relation case; I just don't want to reinvent any wheels.

[Heather Macbeth]

I believe one has the construction of "equivalence classes" built in for any relation, equivalence or not, as quot. I've never used it so am not 100% sure that it does what I think :). But see
https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients

[Eric Wieser]

Doesn't transitivity and symmetry imply reflexivity?

[Eric Wieser]

At least, on a non-empty relation

[Peter Nelson]

No - you can have singletons not related to anything. That’s it, though

[Adam Topaz]

I suggest using quot like Heather mentioned. The API is fairly pleasant to use

[Peter Nelson]

I don't think quot will work - from what I can see, it forgets the difference between elements on which the relation is irreflexive and ones where it is reflexive. I don't want irreflexive elements to give 'quotient' elements at all.

[Adam Topaz]

Yes that's right. Quote is just the quotient by the equivalence relation generated by the given relation. I guess I'm confused about what you want the quotient to actually be...

[Peter Nelson]

I didn't say I want a quotient, just a notion of 'equivalence classes', which make sense in that they form a partition of the elements for which the relation is reflexive. Using a quotient on an appropriate subtype will work to prove all this, but maybe it makes more sense just do do the proofs directly.

[Eric Wieser]

Are you looking for this?

example {α : Type*} (r : α → α → Prop) (hs : symmetric r) (ht : transitive r) :
  setoid {x // r x x} :=
⟨λ a b, r a b, λ x, x.prop, λ x y, @@hs, λ x y z, @@ht⟩

[Kevin Buzzard]

@Peter Nelson perhaps this discussion would move forward more smoothly if you were to write down in Lean some type or term or structure which you want to have, or have an API for, with a #mwe and some sorried lemmas.

[Peter Nelson]

I think my question is answered - what I want doesn't quite exist out of the box, but it's pretty close to quot. I'm writing a small API for what I need, which is all easy. I'm satisfied I'm not repeating anything already in mathlib, and this was the only point of my question.