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:

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 quots 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