## Stream: maths

### Topic: bundling functions

#### Johan Commelin (Feb 12 2019 at 07:59):

@Mario Carneiro If you are interested, would you mind looking into why we can not use quotient_group.map _ _ id _ in the following definition: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuations.lean#L583
Currently we are using quotient_group.lift but this is a bit more roundabout then necessary I would say. Any attempt to use quotient_group.map results in deterministic timeouts or even frozen operating systems...

#### Mario Carneiro (Feb 12 2019 at 08:00):

how much of that file do I need?

#### Mario Carneiro (Feb 12 2019 at 08:02):

which quotient is here: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuations.lean#L427

#### Johan Commelin (Feb 12 2019 at 08:04):

That's quotient_group.quotient

#### Mario Carneiro (Feb 12 2019 at 08:06):

the first thing I would try is change quotient _ -> quotient _ before the refine

#### Johan Commelin (Feb 12 2019 at 08:06):

I think I already tried that at some point...

#### Mario Carneiro (Feb 12 2019 at 08:29):

minimized:

import group_theory.quotient_group data.finsupp

local attribute [instance, priority 0] classical.prop_decidable

variables (R : Type*) [comm_ring R]
#check (by apply_instance : is_group_hom (@id (multiplicative (R →₀ ℤ))))


#### Mario Carneiro (Feb 12 2019 at 08:29):

short term, you can replace the proof with is_group_hom.id

#### Mario Carneiro (Feb 12 2019 at 08:30):

i.e. refine @quotient_group.map _ _ _ _ _ _ _ _ id is_group_hom.id _,

#### Johan Commelin (Feb 12 2019 at 08:32):

Ouch... thanks for minimizing it! I tried but got stuck (both my hardware and my brainware)...

#### Mario Carneiro (Feb 12 2019 at 08:32):

oh shit, discrete_field.has_decidable_eq is an instance in core

#### Mario Carneiro (Feb 12 2019 at 08:33):

that's not good at all

#### Johan Commelin (Feb 12 2019 at 08:33):

Fork! Fork! Fork!

#### Johan Commelin (Feb 12 2019 at 08:33):

But is that the reason for your MWE failing?

#### Mario Carneiro (Feb 12 2019 at 08:33):

it's probably not the culprit, but it's responsible for a lot of wheel-spinning

#### Johan Commelin (Feb 12 2019 at 08:34):

Because that MWE looks very innocent. It's bit of a bad omen that Lean can't find that instance.

#### Kevin Buzzard (Feb 12 2019 at 08:34):

Just make an instance of has_undecidable_eq with higher priority

#### Mario Carneiro (Feb 12 2019 at 08:34):

especially since the instance for prop_decidable is at the end of the list and you use it all the time

#### Mario Carneiro (Feb 12 2019 at 08:34):

you might want to consider dropping the priority 0

#### Johan Commelin (Feb 12 2019 at 08:35):

I wouldn't mind a Lean feature

local attribute [-instance] foobar -- removes an instance locally


#### Johan Commelin (Feb 12 2019 at 08:35):

you might want to consider dropping the priority 0

That usually causes other breakage, doesn't it? I can try though.

#### Kevin Buzzard (Feb 12 2019 at 08:35):

Can one edit the database of instances somehow?

#### Kevin Buzzard (Feb 12 2019 at 08:36):

I mean, other than by adding to it?

#### Mario Carneiro (Feb 12 2019 at 08:36):

nope, at least not global instances

#### Mario Carneiro (Feb 12 2019 at 08:36):

the worry is that it makes import order matter

#### Johan Commelin (Feb 12 2019 at 08:36):

So far, no breakage in this file, if I drop the prio

#### Mario Carneiro (Feb 12 2019 at 08:37):

it does seem to improve the search, but it's still overflowing

#### Johan Commelin (Feb 12 2019 at 08:38):

Yeah, it doesn't solve the MWE

#### Mario Carneiro (Feb 12 2019 at 08:41):

oh, this is interesting:

[class_instances] (1) ?x_60 : @is_group_hom (multiplicative (R →₀ ℤ)) (multiplicative (R →₀ ℤ))
(@multiplicative.group (R →₀ ℤ)
(@finsupp.add_group R ℤ (λ (a b : R), classical.prop_decidable (a = b))
(λ (a b : ℤ), classical.prop_decidable (a = b))
(@domain.to_ring ℤ
(@to_domain ℤ
(@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
int.decidable_linear_ordered_comm_ring))))))))
(@multiplicative.group (R →₀ ℤ)
(@finsupp.add_group R ℤ (λ (a b : R), classical.prop_decidable (a = b))
(λ (a b : ℤ), classical.prop_decidable (a = b))
(@domain.to_ring ℤ
(@to_domain ℤ
(@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
int.decidable_linear_ordered_comm_ring))))))))
(λ (x : multiplicative (R →₀ ℤ)), x) := @is_group_hom.id ?x_283 ?x_284
failed is_def_eq


#### Mario Carneiro (Feb 12 2019 at 08:42):

it found the right answer and passed it over

#### Mario Carneiro (Feb 12 2019 at 08:43):

I think it's because id has been unfolded at this point, but it's not reducible

#### Johan Commelin (Feb 12 2019 at 08:43):

Your use of "interesting" is… interesting…

#### Mario Carneiro (Feb 12 2019 at 08:45):

looks like is_group_hom.comp is the culprit

#### Mario Carneiro (Feb 12 2019 at 08:45):

this should not be an instance, it is applied in stupid ways

#### Johan Commelin (Feb 12 2019 at 08:46):

But if it is not an instance then it causes breakage... in stupid ways

#### Mario Carneiro (Feb 12 2019 at 08:46):

I think group_hom should be a thing sooner rather than later

#### Johan Commelin (Feb 12 2019 at 08:46):

I'll be slamming my keyboard 10 times a day: "Come on Lean, you're composing two group homs... of course that's a group hom"

#### Mario Carneiro (Feb 12 2019 at 08:46):

the evidence continues to mount in favor of bundled functions

#### Johan Commelin (Feb 12 2019 at 08:46):

I think bundling is cool
(And I don't know what I'm talking about :grinning:)

#### Kenny Lau (Feb 12 2019 at 08:47):

nonononono it has nothing to do with is_group_hom.comp

#### Kenny Lau (Feb 12 2019 at 08:47):

[class_instances] (0) ?x_0 : @is_group_hom (multiplicative (ℤ →₀ ℤ)) (multiplicative (ℤ →₀ ℤ))
(@multiplicative.group (ℤ →₀ ℤ)
(@finsupp.add_group ℤ ℤ (λ (a b : ℤ), int.decidable_eq a b) (λ (a b : ℤ), int.decidable_eq a b)
(@domain.to_ring ℤ
(@to_domain ℤ
(@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
int.decidable_linear_ordered_comm_ring))))))))
(@multiplicative.group (ℤ →₀ ℤ)
(@finsupp.add_group ℤ ℤ (λ (a b : ℤ), int.decidable_eq a b) (λ (a b : ℤ), int.decidable_eq a b)
(@domain.to_ring ℤ
(@to_domain ℤ
(@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
int.decidable_linear_ordered_comm_ring))))))))
(λ (x : multiplicative (ℤ →₀ ℤ)), x) := @is_group_hom.id ?x_44 ?x_45
failed is_def_eq


#### Kenny Lau (Feb 12 2019 at 08:48):

import data.finsupp

set_option trace.class_instances true
example : is_group_hom (λ x : multiplicative (ℤ →₀ ℤ), x) := by apply_instance


#### Mario Carneiro (Feb 12 2019 at 08:48):

comp is reducible, if you try to unify id with f o g you get f = \lam x, x and g = id

#### Kenny Lau (Feb 12 2019 at 08:48):

but still yes for bundling

#### Mario Carneiro (Feb 12 2019 at 08:48):

it turned a perfectly normal first order problem into a higher order problem

#### Mario Carneiro (Feb 12 2019 at 08:49):

we could have an instance for is_group_hom (\lam x, x) which would also solve this problem but that's not the point

#### Mario Carneiro (Feb 12 2019 at 08:49):

type class searches with explicit lambdas is never a good idea

#### Kenny Lau (Feb 12 2019 at 08:50):

so do we support bundling?

#### Mario Carneiro (Feb 12 2019 at 08:50):

it worked for linear maps, I think it will work just as well if not better for group theory

#### Johan Commelin (Feb 12 2019 at 08:50):

That's going to be a major refactor...

yep

#### Johan Commelin (Feb 12 2019 at 08:51):

And let's do ring_hom at the same time

#### Johan Commelin (Feb 12 2019 at 08:51):

This is also moving "hands-on" mathlib closer to "categorical" mathlib

#### Johan Commelin (Feb 12 2019 at 08:51):

I think that's a good thing.

#### Mario Carneiro (Feb 12 2019 at 08:51):

the solution to higher order problems is to make them first order problems

#### Johan Commelin (Feb 12 2019 at 08:51):

Aah, and continuous can finally be continuous, instead of secretly meaning is_continous...

#### Johan Commelin (Feb 12 2019 at 08:52):

But previously we could mix [is_group_hom f] with injective f... will that kind of things become nastier after this refactor?

#### Mario Carneiro (Feb 12 2019 at 08:52):

that becomes injective f

#### Patrick Massot (Feb 12 2019 at 08:52):

Does it mean we'll have unification hints all over the place?

no

#### Patrick Massot (Feb 12 2019 at 08:53):

This would be for bundled structures but not bundled maps?

#### Mario Carneiro (Feb 12 2019 at 08:53):

A lot of type class searches will go away though

#### Mario Carneiro (Feb 12 2019 at 08:53):

no, the other way around

#### Mario Carneiro (Feb 12 2019 at 08:53):

maps bundled, structures unbundled

#### Patrick Massot (Feb 12 2019 at 08:54):

I meant unification hints would be for bundled structures

#### Mario Carneiro (Feb 12 2019 at 08:54):

right... it's a good question if there are any applications for unification hints as a consequence of bundling structures

#### Mario Carneiro (Feb 12 2019 at 08:55):

I guess the analogue is "guess the linear map whose function part is id"

exactly

#### Patrick Massot (Feb 12 2019 at 08:55):

this is what I understood in Amsterdam anyway

#### Patrick Massot (Feb 12 2019 at 08:55):

and we can still ask Assia or Cyril, they would be delighted to help

#### Mario Carneiro (Feb 12 2019 at 08:55):

but that's not nearly as common a problem as "guess the group whose type is int"

#### Mario Carneiro (Feb 12 2019 at 08:56):

because here we will usually be specifying the linear maps directly rather than talking about lambdas

#### Johan Commelin (Feb 12 2019 at 08:57):

I guess it would mean that we can still write id, instead of writing group_hom.id

#### Mario Carneiro (Feb 12 2019 at 08:58):

you may be able to, depends on how well the disambiguation goes

#### Mario Carneiro (Feb 12 2019 at 08:58):

I would be inclined to protect group_hom.id and just say that

#### Mario Carneiro (Feb 12 2019 at 08:58):

or maybe use a local notation for it

#### Johan Commelin (Feb 12 2019 at 08:59):

Meh, ain't that ugly?

#### Johan Commelin (Feb 12 2019 at 08:59):

Well... we'll see.

#### Johan Commelin (Feb 12 2019 at 08:59):

I wouldn't mind trying uni-hints

#### Mario Carneiro (Feb 12 2019 at 08:59):

it is, but having id overloaded usually just means you can't use either one

#### Mario Carneiro (Feb 12 2019 at 09:00):

like when I typed quotient in your proof it complained about the overload, I had to write quotient_group.quotient (or _root_.quotient if I wanted the other one)

#### Mario Carneiro (Feb 12 2019 at 09:01):

In a lot of cases you can circumvent this with projection notation

#### Mario Carneiro (Feb 12 2019 at 09:01):

like ideal.quotient means you can write I.quotient where I : ideal A

#### Kenny Lau (Feb 12 2019 at 13:38):

ok so what do we want to bundle?

#### Kenny Lau (Feb 12 2019 at 13:38):

can we come up with an explicit list?

#### Johan Commelin (Feb 12 2019 at 13:38):

all morphisms between algebraic structures

#### Kenny Lau (Feb 12 2019 at 13:39):

that's not an explicit list

#### Johan Commelin (Feb 12 2019 at 13:39):

whether we also want to touch topology, I don't know. Let's wait to hear the opinion of @Reid Barton

#### Kenny Lau (Feb 12 2019 at 13:39):

should I test it on is_field_hom?

#### Johan Commelin (Feb 12 2019 at 13:39):

is_{,add_}group_hom, is_ring_hom

#### Johan Commelin (Feb 12 2019 at 13:40):

is_{,add_}monoid_hom, similar for semigroups

#### Reid Barton (Feb 12 2019 at 14:38):

whether we also want to touch topology, I don't know. Let's wait to hear the opinion of @Reid Barton

My only question about bundling functions with their properties is what the plan is for when we want to combine properties. For example, take continuous homomorphisms between topological groups.

#### Johan Commelin (Feb 12 2019 at 14:40):

FYI: I changed the topic of this discussion.

#### Chris Hughes (Feb 12 2019 at 14:47):

Can we use unification hints for this? I.e. so I can use group him lemmas for ring homs etc.

Last updated: May 09 2021 at 09:11 UTC