Setoid hell

Stream: general

[Eric Wieser]

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]

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

[Anne Baanen]

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]

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]

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]

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]

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]

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

[Anne Baanen]

(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]

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]

I think the original sin here was that setoid should never have been a class, and setoid.r shouldn't exist

[Mario Carneiro]

If the basic quotient lemmas just used r directly, it would be the user's relation and no rewriting would be needed

[Eric Wieser]

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

[Mario Carneiro]

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]

with that, we wouldn't even need quotient

[Kyle Miller]

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]

Here \beta has to be an out-param, right?

[Gabriel Ebner]

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

[Mario Carneiro]

Using a notation typeclass causes the same issues around having to unfold has_repr.from_repr for each particular quotient though

[Mario Carneiro]

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

[Eric Rodriguez]

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]

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

[Eric Wieser]

docs#out_param, not that that will help much

[Eric Rodriguez]

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

[Kyle Miller]

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]

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

[Mario Carneiro]

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]

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]

Is there a reason the addition structure can't be put directly on quot r instead of my_quot in that case?

[Eric Wieser]

If my_quot is @[reducible] then that would still work, right?

[Mario Carneiro]

you could, but I would worry about conflicts because quot r isn't "your" type

[Mario Carneiro]

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]

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

[Johan Commelin]

@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]

@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.