Squash, Trunc

Stream: mathlib4

[Eric Rodriguez]

Why do we have the both of these? docs#Squash, docs#Trunc

[Eric Wieser]

The latter was ported from lean3's docs3#trunc

[Eric Wieser]

I guess lean 4 core independently decided it wanted this and invented a different name

[Eric Rodriguez]

I guess it's worth deduplicating, right?

[Kevin Buzzard]

My impression from talking to agda users is that trunc is a standard name? :-/

[Scott Morrison]

Squash is not used in Lean outside of a single test. It might be reasonable to simply remove it from Lean.

[Scott Morrison]

This feels like something that belongs in Std.

[Aaron Liu]

Has this been worked on yet?

[Aaron Liu]

I found #18952

[Violeta Hernández]

I redefined docs#Squash to take a Sort* argument some two months ago, but we never finished phasing out Trunc.

[Violeta Hernández]

I half recall trying to replace Trunc by Squash in some branch, and running into some issues, due to Squash being defined in terms of docs#Quot, while Trunc is defined in terms of docs#Quotient. It might be worth doing a core PR to upstream docs#trueQuotient and re-define Squash = Quotient trueQuotient (this is def-eq, but allows us to use the stronger theorems on Quotient). At that point, replacing Trunc by Squash should be a simple matter of copy-replace.

[Aaron Liu]

That looks like lean4#6642

[Eric Wieser]

I think there's some contention over whether the current Setoid / Quotient design is correct in general (eg, the pile of mk functions it results in everywhere), and upstreaming to core is going to make it way harder to change that.

[Eric Wieser]

I don't think the Trunc / Squash duplication is so bad that it warrants painting ourselves into a tighter corner for Quotient

[Violeta Hernández]

Eric Wieser said:

I think there's some contention over whether the current Setoid / Quotient design is correct in general (eg, the pile of mk functions it results in everywhere), and upstreaming to core is going to make it way harder to change that.

What would the alternative be?

[Kyle Miller]

Something I'd like to see gain traction is a QuotLike class where you can say that a certain type has the universal properties of a quotient, and all the Quotient/Quot theorems would be in terms of this class instead. If the relation is an outParam, then the theorems could even make sure the correct relation gets used in the theorems.

[Aaron Liu]

What kinds of instances do you expect to see for QuotLike?

[Eric Wieser]

QuotientGroup, Submodule.Quotient, Ideal.Quotient, RingCon.Quotient, ...

[Yury G. Kudryashov]

Also, I would like to see a QuotLike instance for the product of 2 groups with QuotLike instances.

[Yury G. Kudryashov]

(though this may be more questionable)

[Violeta Hernández]

Let's not forget about concrete types like Surreal which could also have QuotLike instances to avoid duplicating all the basic quotient API

[Edward van de Meent]

Concretely, I guess you get something like this?

universe u in
class QuotientLike (Q : Type*) (R : outParam (Type*)) (r : outParam(R -> R -> Prop)) where
  mk : R -> Q
  sound (a b : R) : r a b -> mk a = mk b
  lift {S : Sort u} (f : R -> S) (h : forall (a b : R), r a b -> f a = f b) : Q -> S
  lift_mk {S : Sort u} (f : R -> S) (h : forall (a b : R), r a b -> f a = f b) : forall (a : R), lift f h (mk a) = f a
  ind (P : Q -> Prop) (h : forall (r : R), P (mk r)(q : Q) : P q

[Edward van de Meent]

docs#Quot.sound

[Edward van de Meent]

I think this might actually have issues, since I think you'd need to know what universe you're going to eliminate into before you quotient?

[Aaron Liu]

Edward van de Meent said:

Concretely, I guess you get something like this?

universe u in
class QuotientLike (Q : Type*) (R : outParam (Type*)) (r : outParam(R -> R -> Prop)) where
  mk : R -> Q
  sound (a b : R) : r a b -> mk a = mk b
  lift {S : Sort u} (f : R -> S) (h : forall (a b : R), r a b -> f a = f b) : Q -> S
  ind {S : Sort u} (f : R -> S) (h : forall (a b : R), r a b -> f a = f b) : forall (a : R), lift f h (mk a) = f a

I don't think you get docs#Quotient.exists_rep this way? Might be wrong, didn't really check too hard.

[Mario Carneiro]

you do, you can prove it by induction

[Mario Carneiro]

oh, but the ind rule in that message is wrong, that's not docs#Quot.ind at all but rather docs#Quot.lift_mk

[Edward van de Meent]

Ah, you're right! (I wrote it on mobile, so had a hard time cross-referencing)

[Yury G. Kudryashov]

AFAIR, there is a series of PRs introducing this typeclass.

[Edward van de Meent]

i found #16421

[Edward van de Meent]

also, discussion for above PR at #mathlib4 > migrate to `QuotLike` API