Stream: Is there code for X?

Topic: Transitive symmetric relations

Peter Nelson (Feb 23 2021 at 22:32):

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 (Feb 23 2021 at 23:07):

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 (Feb 23 2021 at 23:16):

Doesn't transitivity and symmetry imply reflexivity?

Eric Wieser (Feb 23 2021 at 23:16):

At least, on a non-empty relation

Peter Nelson (Feb 23 2021 at 23:23):

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

Adam Topaz (Feb 24 2021 at 00:27):

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

Peter Nelson (Feb 24 2021 at 02:29):

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 (Feb 24 2021 at 03:26):

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 (Feb 24 2021 at 04:13):

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 (Feb 24 2021 at 11:58):

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 (Feb 24 2021 at 13:07):

@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 (Feb 24 2021 at 13:17):

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.

Last updated: May 16 2021 at 05:21 UTC