Fintype of RelHom and RelIso

Stream: Is there code for X?

[Joseph Tooby-Smith]

Do we have anything like the following?

import Mathlib

instance {α β : Type} [Fintype α] [DecidableEq α] [Fintype β]
    (S : Setoid α) (T : Setoid β) :
    Fintype (T.Rel →r S.Rel) := by
  sorry

instance {α β : Type} [Fintype α] [DecidableEq α] [Fintype β]
    (S : Setoid α) (T : Setoid β) :
    Fintype (T.Rel ≃r S.Rel) := by
  sorry

One can fill in the sorry's by using the equivalent non-rel versions of these lemmas and taking subtypes. However, this is grossly inefficient when working with certain specific examples.

[Yaël Dillies]

This came up today: https://github.com/leanprover-community/mathlib4/pull/12273#discussion_r1644797534

[Joseph Tooby-Smith]

The result linked to there SimpleGraph.Hom.instFintype is doing this using the equivalence to a subtype. I believe this is not the most efficient way of tackling this problem. (Efficient in terms of speed and memory usage of generating the list of elements, rather than length of code).

[Yaël Dillies]

I agree, although I wonder what general solution you have to offer

[Joseph Tooby-Smith]

For the case of Fintype (T.Rel ≃r T.Rel), at least, the problem reduces to finding permutations within equivalence classes, and then `stitching' them together.

[Yaël Dillies]

Yes, so this is not a general solution, making it unsuitable for a general instance. I suspect you would be better off not relying on Fintype here

[Joseph Tooby-Smith]

A T.Rel →r S.Rel is determined by it's map on equivalence classes $F : S / \sim \to T/\sim$ and the maps $e \to F e$ for each $e \in S / \sim$. This can likely be turned into an equivalence of types between T.Rel →r S.Rel and the Pi type determined by the map on equivalence classes and those between individual corresponding equivalence classes. This Pi type is a Fintype uses of Pi.fintype.

[Joseph Tooby-Smith]

Similar for T.Rel ≃r S.Rel.

In what sense is this not a general solution?

[Yaël Dillies]

It's not a general solution in the sense that it won't work to eg replace docs#SimpleGraph.Hom.instFintype

[Yaël Dillies]

In general, computation typeclasses like docs#Fintype walk a fine line between generality and optimisation. When reasoning about them, you want them general. When computing, you want them specific.

[Yaël Dillies]

Here you have a specific use case in mind (partitions), which clashes with the general reasoning we want to do about relation homomorphisms. The solution I'm offering is to not shoehorn your optimisation into the general reasoning framework, but instead to write your own framework

[Joseph Tooby-Smith]

I understand why docs#SimpleGraph.Hom.instFintype will not work with my solution.

I'm not suggesting to put my solution into Mathlib. I'm simply asking if a optimised solution exists out there anywhere. Sorry for the miscommunication about this.

[Yaël Dillies]

I think the issue is independent on whether you are planning on contributing your optimised solution: When mathlib acquires a general solution, it will interfere with your optimised one regardless of whether that's in mathlib or in your project

[Yaël Dillies]

Joseph Tooby-Smith said:

I'm simply asking if a optimised solution exists out there anywhere

Not to my knowledge

[Joseph Tooby-Smith]

Is the issue you describe a general one about having two instances of the same thing on the same type? If so, I can surely get around this using priorities? Just checking there is nothing more subtle going on which I'm missing.

[Kevin Buzzard]

It's not as easy as you're suggesting because sometimes you use lemmas which have the "bad" instance baked in or for which typeclass inference finds the bad instance anyway (if X has low priority and Y has high priority there are still ways of asking typeclass inference to find an instance and it finds X before Y, perhaps because there was a decision taken much earlier to go down the X route for other reasons). But if you're aware of the issue and know how to test for it by hovering over terms and looking in them, then you should be fine.