Pretty printing of equivalence classes

Stream: Is there code for X?

[Vincent Beffara]

When working with several equivalence relations on the same type, it often happens that we have ⟦u⟧ = ⟦v⟧ in the context, ⟦u⟧ = ⟦v⟧ in the goal but they have different meanings. One can always click in the info view and figure it out, but is there a way to always have it displayed?

[Sebastien Gouezel]

It sounds like an #xy problem. Normally, you should never work with different equivalence relations on a tpy e(and most often you won't work with equivalence relations at all). Can you explain quickly what you are trying to do?

[Vincent Beffara]

Yes, definitely an XY problem here... I am trying to clean up composition of equivalence relations, I have this:

def setoid.comp {V : Type} (s : setoid V) (t : setoid (quotient s)) : setoid V :=
let f : V → quotient s := quotient.mk,
    g : quotient s → quotient t := quotient.mk
in setoid.ker (g ∘ f)

and I want to prove this:

def setoid.comp.iso {V : Type} (s : setoid V) (t : setoid (quotient s)) :
    quotient (s.comp t) ≃ quotient t := sorry

(i.e., somehow ⟦⟦u⟧⟧ = ⟦⟦v⟧⟧ <-> ⟦u⟧ = ⟦v⟧)

[Vincent Beffara]

Maybe doing something like let V' : Type := V somewhere would help, but as I understand it that would change the definition and I would have to trade my problem for a lot of (x : V') all over the place to select which relation I am talking about.

[Vincent Beffara]

Following a previous hint here, I am in fact doing let f : V -> quotient s := quotient.mk' and replacing the bracket notation with f u, which makes input clearer but confuses rw a lot

[Vincent Beffara]

(and then applying lemmas from mathlib ends up with brackets in the context anyway)

[Sebastien Gouezel]

If you are trying to clean up composition of equivalence relations, I am not surprised you run into difficulties related to equivalence relations. To un-xy even more, why would you want to work with equivalence relations? (Essentially, these show up very seldom, and that's probably why you run into API problems).

[Vincent Beffara]

I am playing around with graphs and I want to define the transitivity of the contraction operation (as in, the contraction of a contraction can be obtained as a contraction of the initial graph). It felt natural to define the contraction of a graph as a graph on the quotient by whatever I am contracting.

[Vincent Beffara]

Like so,

def quotient_graph (G : simple_graph V) (S : setoid V) : simple_graph (quotient S) :=
{
    adj := λ x y, x ≠ y ∧ ∃ x' y' : V, ⟦x'⟧ = x ∧ ⟦y'⟧ = y ∧ G.adj x' y',
    symm := λ x y ⟨h₀,x',y',h₁,h₂,h₃⟩, ⟨h₀.symm,y',x',h₂,h₁,h₃.symm⟩,
    loopless := λ x ⟨h₀,h⟩, h₀ rfl
}

[Vincent Beffara]

Do you imply that I should rather do this instead,

def push_graph (G : simple_graph V) (f : V -> V') (h : surjective f) : simple_graph V'

or something similar?

[Sebastien Gouezel]

Yes, your last proposition would seem more natural (since it is strictly more general). But I've not played at all with our graph library, so I am not in a good position to give a better advice, sorry!

[Yaël Dillies]

Indeed it is better that way because it doesn't constrain the end type.

[Vincent Beffara]

Ah, and in addition push G (f.comp g) ends up being exactly the same as push (push G g) f rather than isomorphic by some abstract nonsense stuff.