# Zulip Chat Archive

## Stream: general

### Topic: Setoid hell

#### Eric Wieser (Jun 20 2021 at 21:43):

I don't think it's what the term usually refers to, but in my opinion there's still a setoid-based hell centered around implicit vs typeclass arguments:

`a ≈ b`

(docs#setoid_has_equiv) vs`some_setoid.rel a b`

(docs#setoid.rel) vs`setoid.r a b`

(docs#setoid.r)`quot.mk`

(docs#quot.mk) vs`quotient.mk`

(docs#quotient.mk) vs`quotient.mk'`

(docs#quotient.mk') vs`submodule.quotient.mk`

(docs#submodule.quotient.mk) vs ...

The end result is that you can almost never apply the lemma you want to with `rw`

, because the spelling in the lemma never seems to match the spelling that ends up in the goal view. Is there any way we can make this less bad? Perhaps by splitting `setoid`

into `structure setoid`

and `class has_canonical_setoid`

, so that we can't accidentally write lemmas that mix the conventions?

cc @Bhavik Mehta, since you brought this to my attention in #7910

#### Eric Wieser (Jun 20 2021 at 21:46):

(Shoutout to the lost soul of that hell which is the tautological lemma docs#submodule.quotient.mk_eq_mk)

#### Anne Baanen (Jun 21 2021 at 08:54):

The only advantage I see for preferring `setoid`

quotients over `quot`

s by an arbitrary relation is easier automation on `quotient`

: since `quotient`

assumes the relation is an equivalence relation, it might be a bit easier to create `simp`

lemmas. I feel that `quotient`

is essentially just adding on proofs where we only need the data (namely the relation).

#### Anne Baanen (Jun 21 2021 at 08:56):

Moreover, we have classes like docs#is_refl and docs#is_equiv so for `simp`

there's no need to bundle that information into the constructor of the quotient type.

#### Anne Baanen (Jun 21 2021 at 08:59):

docs#submodule.mkq makes sense to have as a definition, since it specifies the quotient map is indeed linear, so why do we also have docs#submodule.quotient.mk? (To help inferring implicit arguments like docs#submodule.quotient_rel?)

#### Anne Baanen (Jun 21 2021 at 09:06):

So basically, I'm wondering whether it's not a good idea to choose `quot.mk`

as the `simp`

normal form for all quotient-like operators and try to replace `quotient`

with `quot`

everywhere.

#### Kevin Buzzard (Jun 21 2021 at 09:22):

Related: Kenny Lau has often suggested that the mathlib approach of localising a ring at a submonoid should just be replaced by localising a ring at [the submonoid generated by] an arbitrary subset.

#### Gabriel Ebner (Jun 21 2021 at 09:23):

:+1: for removing the setoid typeclass and the quotient wrapper.

#### Anne Baanen (Jun 21 2021 at 09:27):

(Ah, I think I figured out a good reason for having `submodule.quotient.mk`

: if we just wrote `quot.mk`

then `submodule.quotient`

has to be reducible for automation to work well.)

#### Mario Carneiro (Jun 21 2021 at 11:28):

The intent has been to have each quotient define its own `mk`

wrapper function, which has the correct type, and use that as the simp normal form. The downside is that you have to duplicate the quotient API, and if you get lazy and use quot lemmas instead then you enter this coercion hell

#### Mario Carneiro (Jun 21 2021 at 11:29):

I think the original sin here was that `setoid`

should never have been a class, and `setoid.r`

shouldn't exist

#### Mario Carneiro (Jun 21 2021 at 11:29):

If the basic quotient lemmas just used `r`

directly, it would be the user's relation and no rewriting would be needed

#### Eric Wieser (Jun 21 2021 at 11:36):

I'm not sure what your suggestion regarding `setoid.r`

is

#### Mario Carneiro (Jun 21 2021 at 11:38):

Any theorem about a type with a setoid structure that refers to `setoid.r`

should instead be a theorem about a type with a relation `r`

(possibly with `equivalence r`

as a typeclass arg) and refer to `r`

in the statement

#### Mario Carneiro (Jun 21 2021 at 11:39):

with that, we wouldn't even need `quotient`

#### Kyle Miller (Jun 21 2021 at 16:02):

I've used `quotient`

over `quot`

before to get the `⟦...⟧`

notation, which has been nice to use even if it's occasionally frustrating due to setoids. Arguably each quotient type should have its own bespoke constructor or notation, though.

Maybe having an opt-in notation typeclass would be a good alternative?

```
namespace quot_notation
universes u v
/-- Representing terms of `β` by terms of `α` -/
-- It might make sense for one of these parameters to be an out_param
class has_repr (α : Sort u) (β : Sort v) :=
(from_repr : α → β)
local notation `⟦`:max a `⟧`:0 := has_repr.from_repr a
-- Example of unordered pairs
def swap {α : Type*} : α × α → α × α
| (x, y) := (y, x)
def r {α : Type*} (p : α × α) (q : α × α) : Prop := p == q ∨ swap p == q
def unordered_pair (α : Type u) := @quot (α × α) r
instance unordered_pair.has_repr (α : Type*) : has_repr (α × α) (unordered_pair α) :=
⟨quot.mk r⟩
example : unordered_pair ℕ := ⟦(2, 3)⟧
end quot_notation
```

#### Johan Commelin (Jun 21 2021 at 16:03):

Here `\beta`

has to be an out-param, right?

#### Gabriel Ebner (Jun 21 2021 at 16:04):

Or α in case you want to write `⟦42⟧`

?

#### Mario Carneiro (Jun 21 2021 at 16:07):

Using a notation typeclass causes the same issues around having to unfold `has_repr.from_repr`

for each particular quotient though

#### Mario Carneiro (Jun 21 2021 at 16:08):

I think it makes more sense for alpha to be the out param for quotients

#### Eric Rodriguez (Jun 21 2021 at 16:19):

Johan Commelin said:

Here

`\beta`

has to be an out-param, right?

what is an out-param? I saw them in the defn of the notation typeclasses

#### Yaël Dillies (Jun 21 2021 at 16:20):

It's a type parameter of a class that we can let Lean infer. But the experts will know better than me.

#### Eric Wieser (Jun 21 2021 at 16:25):

docs#out_param, not that that will help much

#### Eric Rodriguez (Jun 21 2021 at 16:28):

yeah, I've seen it before for a very unhelpful docstring :b

#### Kyle Miller (Jun 21 2021 at 16:46):

Mario Carneiro said:

Using a notation typeclass causes the same issues around having to unfold

`has_repr.from_repr`

for each particular quotient though

Isn't this essentially the same issue as defining your own `mk`

wrapper function per type, though? I might have misunderstood what you were proposing.

#### Mario Carneiro (Jun 21 2021 at 16:52):

If you have your own wrapper function then there is nothing to unfold, because it's already in the correct form

#### Mario Carneiro (Jun 21 2021 at 16:54):

The problem with using raw `quot.mk`

directly is that it has type `quot r`

instead of `my_quot`

, which means that if `my_quot`

has e.g. an addition structure because it's a ring or something then the typeclass will get confused

#### Mario Carneiro (Jun 21 2021 at 16:55):

`has_repr`

doesn't have that issue, but it's not clear to be whether we can have generalized lemmas over it for all quotients without writing the type as `quot r`

#### Eric Wieser (Jun 21 2021 at 16:57):

Is there a reason the addition structure can't be put directly on `quot r`

instead of `my_quot`

in that case?

#### Eric Wieser (Jun 21 2021 at 16:57):

If `my_quot`

is `@[reducible]`

then that would still work, right?

#### Mario Carneiro (Jun 21 2021 at 16:58):

you could, but I would worry about conflicts because `quot r`

isn't "your" type

#### Mario Carneiro (Jun 21 2021 at 17:00):

the relation `r`

is "yours" but I don't think that's sufficient because relations can be all sorts of things and they are generally not newtyped

#### Eric Wieser (Jun 21 2021 at 17:04):

"newtyping" the relation feels like it would be less annoying than newtyping the quotient

#### Johan Commelin (Jun 21 2021 at 17:14):

@Eric Rodriguez Usually, if you have a `class foo (X : Type) (Y : Type)`

, then we want a unique instance for `foo X Y`

for every pair `X, Y`

. Now if you have `class foo (X : Type) (Y : out_param $ Type)`

, then we want a unique instance for `foo X Y`

for every `X`

. This way, typeclass inference can determine `Y`

, once `X`

is known.

#### Kyle Miller (Jun 21 2021 at 17:35):

@Mario Carneiro I'm still not quite understanding the difference between a wrapper function and a `has_repr`

instance. My idea with the typeclass is just to give a canonical name to the wrapper function, and I didn't mean to suggest it would let you have generalized quotient lemmas. I just figured that if you're wanting to abolish `quotient`

, then this might be a nice alternative that's more controllable than the old notation.

Last updated: Aug 03 2023 at 10:10 UTC