Quotient.mk vs .mk' vs .mk''

Stream: mathlib4

[Eric Wieser]

We currently have three different ways to build an element of Quotient s. Not only is this one more than we had in Lean 3, but the new names are permuted with respect to the old names:

Setoid argument	Lean 3	Lean 4
(s : setoid _)		docs#Quotient.mk (core, ⟦a⟧)
{s : setoid _}	docs3#quotient.mk'	docs#Quotient.mk'' (mathlib)
[setoid _]	docs3#quotient.mk (⟦a⟧)	docs#Quotient.mk' (core)

Should we eliminate some of these?

[Ruben Van de Velde]

I started eliminating mk'' in a branch not so long ago, but got distracted

[Ruben Van de Velde]

Btw, the meaning of ⟦a⟧ also changed between 3 and 4

[Eric Wieser]

It's now Quotient.mk'' but used to be quotient.mk, right?

[Kyle Miller]

-- Porting note: in mathlib3 this notation took the Setoid as an instance-implicit argument,
-- now it's explicit but left as a metavariable.
-- We have not yet decided which one works best, since the setoid instance can't always be
-- reliably found but it can't always be inferred from the expected type either.
-- See also: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/confusion.20between.20equivalence.20and.20instance.20setoid/near/360822354
@[inherit_doc]
notation:arg "⟦" a "⟧" => Quotient.mk _ a

[Kyle Miller]

I think the problem with Quotient.mk'' now is that Lean wants to resynthesize the Setoid instance from scratch, and it refuses to pick it up from the expected type.

[Eric Wieser]

Oh, so mk'' x : Quotient s doesn't work?

[Kyle Miller]

I don't believe so

[Eric Wieser]

I don't see why mk _ would be any different

[Kyle Miller]

Lean 4 resynthesizes instances, even for metavariables that have been solved for, and then checks that the value of the metavariable is defeq to the resynthesized instance.

[Kyle Miller]

With mk _, it's not an instance argument, so it won't try resynthesizing.

[Eric Wieser]

mk'' also isn't an instance argument

[Eric Wieser]

Ah sorry, I'm getting my primes confused

[Eric Wieser]

The table above was wrong, I've corrected it

[Kyle Miller]

Yeah, there's no difference in behavior between using Quotient.mk _ a and Quotient.mk'' a, except perhaps that Quotient.mk'' doesn't unfold to Quotient.mk

[Eric Wieser]

That seems like a very strong reason to eliminate one of mk and mk'' entirely

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/compare/quotient-mk?expand=1

[Eric Wieser]

You may as well use the notation there, right?

[Kyle Miller]

Something we've discussed before is making the notation be a notation typeclass. That would help keep Quotient from leaking, if every type that has a quotient could specify exactly how it wants the result type to be represented. Plus this would work for non-Quotient quotients (i.e., types that categorically are a quotient).

[Eric Wieser]

I'm confused about how that would be any different from Setoid being a typeclass, which it already is?

[Kyle Miller]

The second part, where you can choose a different type for the quotient than Quotient.

[Eric Wieser]

I don't think mathlib has any places where it wants to do that?

[Kyle Miller]

Aren't there at least a lot of abbreviations for Quotient?

[Eric Wieser]

I guess docs#RingQuot is the only example that comes to mind

[Eric Wieser]

But I was trying to eliminate that in favor of docs#RingCon anyway

[Kyle Miller]

Wherever you have an abbreviation for Quotient and you use the ⟦x⟧ notation, you get an API leak, since the notation naturally has type Quotient ... rather than your abbreviation.

[Kyle Miller]

One of the issues though is you want some bidirectional communication during elaboration -- an outParam isn't enough (and maybe not even ideal). Given ⟦x⟧ : Q you want to derive from Q an X to help elaborate x with expected type X.

(It's not completely clear that you want X to determine Q, since you might want to use the notation for the quotient into multiple quotient types, though perhaps if you're working with multiple quotient groups you'd want the subgroups you're quotienting by to be explicit in the notation.)

[Eric Wieser]

By "abbreviation", do you mean "def but not abbrev"?

[Eric Wieser]

Because if you're using abbrev then the "leak" is by design

[Kyle Miller]

I mean the difference between for example QuotientGroup.mk x : G ⧸ s and ⟦x⟧ : Quotient someSetoidInst

[Kyle Miller]

Even if (⟦x⟧ : G ⧸ s) elaborates, the type of this term is syntactically Quotient ...

[Kyle Miller]

Wouldn't it be better if ⟦x⟧ could have a type that's syntactically what we want in a given context? Seeing a Quotient type in the middle of a proof about groups seems very much like a leaked implementation detail to me.

[Eric Wieser]

Alternatively we could replace HasQuotient with a HasToSetoid class, and make R ⧸ S be notation for Quotient (HasSetoid.toSetoid S)

[Newell Jensen]

Was there ever a decision on this?