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

[Violeta Hernández]

Just got reminded of this.

[Violeta Hernández]

I have an open PR to core which is broken because of a label I don't know how to remove: https://github.com/leanprover/lean4/pull/6642

[Violeta Hernández]

I'm also not sure how to do the rebase Kim asked me to. Help welcome.

[Aaron Liu]

Violeta Hernández said:

I'm also not sure how to do the rebase Kim asked me to. Help welcome.

I just copy the git rebase command that the bot gives me

[Violeta Hernández]

Well I did that. Now how do I remove the awaiting-mathlib label?

[Violeta Hernández]

(Or alternatively, how do I ensure that this doesn't break mathlib?)

[Kim Morrison]

If you've rebased correctly, then the bot should remove the label after it verifies that Mathlib compiles against it.

It if doesn't, you need to push changes to the lean-pr-testing-6642 branch on the mathlib4-nightly-testing fork. (e.g. by making a PR to that fork and pinging someone)

[Violeta Hernández]

Why did Linux build for six hours and then fail? Why hasn't the label been removed yet? Did I do something wrong?

[Kim Morrison]

Github had an outage last night. :woman_shrugging:

[Violeta Hernández]

I'll retry CI.

[Aaron Liu]

Edward van de Meent said:

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?

Why not just

class QuotientLike (Q : Type*) (R : outParam (Type*)) (r : outParam(R -> R -> Prop)) where
  repr : Equiv Q (Quot r)

[Violeta Hernández]

Can someone please help me? I have no idea how to fix what's going on with my PR.

[Violeta Hernández]

https://github.com/leanprover/lean4/pull/6642

[Violeta Hernández]

Would it be better if I just re-opened this?

[Aaron Liu]

is there a problem here

[Aaron Liu]

it's both awaiting mathlib and breaks mathlib

[Violeta Hernández]

Yeah, I have no idea how to get rid of the tags on the PR, nor how to get it to build

[Violeta Hernández]

it should not be awaiting mathlib

[Kim Morrison]

The awaiting-mathlib label means it will not be merged until (at least) there is evidence that Mathlib can build against it.

The breaks-mathlib label means the last attempt to produce this evidence failed.

[Kim Morrison]

To fix this situation, you need to push or PR changes to the Mathlib lean-pr-testing-NNNN branch on the nightly-testing fork.