Zulip Chat Archive

Stream: maths

Topic: bundling functions


view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:00):

how much of that file do I need?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:04):

That's quotient_group.quotient

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:06):

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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:06):

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

view this post on Zulip 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  ))))

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:29):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:30):

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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:32):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:32):

oh shit, discrete_field.has_decidable_eq is an instance in core

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:33):

that's not good at all

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:33):

Fork! Fork! Fork!

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:33):

But is that the reason for your MWE failing?

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:33):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 08:34):

Just make an instance of has_undecidable_eq with higher priority

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:34):

you might want to consider dropping the priority 0

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:35):

I wouldn't mind a Lean feature

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 08:35):

Can one edit the database of instances somehow?

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 08:36):

I mean, other than by adding to it?

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:36):

nope, at least not global instances

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:36):

the worry is that it makes import order matter

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:36):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:37):

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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:38):

Yeah, it doesn't solve the MWE

view this post on Zulip 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))
        (@add_comm_group.to_add_group ℤ
           (@ring.to_add_comm_group ℤ
              (@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))
        (@add_comm_group.to_add_group ℤ
           (@ring.to_add_comm_group ℤ
              (@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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:42):

it found the right answer and passed it over

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:43):

Your use of "interesting" is… interesting…

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:45):

looks like is_group_hom.comp is the culprit

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:45):

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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:46):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:46):

I think group_hom should be a thing sooner rather than later

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:46):

the evidence continues to mount in favor of bundled functions

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:46):

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

view this post on Zulip Kenny Lau (Feb 12 2019 at 08:47):

nonononono it has nothing to do with is_group_hom.comp

view this post on Zulip 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)
        (@add_comm_group.to_add_group ℤ
           (@ring.to_add_comm_group ℤ
              (@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)
        (@add_comm_group.to_add_group ℤ
           (@ring.to_add_comm_group ℤ
              (@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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 12 2019 at 08:48):

but still yes for bundling

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:48):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:49):

type class searches with explicit lambdas is never a good idea

view this post on Zulip Kenny Lau (Feb 12 2019 at 08:50):

so do we support bundling?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:50):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:50):

yep

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:51):

And let's do ring_hom at the same time

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:51):

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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:51):

I think that's a good thing.

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:51):

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

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:51):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:52):

that becomes injective f

view this post on Zulip Patrick Massot (Feb 12 2019 at 08:52):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:52):

no

view this post on Zulip Patrick Massot (Feb 12 2019 at 08:53):

This would be for bundled structures but not bundled maps?

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:53):

A lot of type class searches will go away though

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:53):

no, the other way around

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:53):

maps bundled, structures unbundled

view this post on Zulip Patrick Massot (Feb 12 2019 at 08:54):

I meant unification hints would be for bundled structures

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:55):

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

view this post on Zulip Patrick Massot (Feb 12 2019 at 08:55):

exactly

view this post on Zulip Patrick Massot (Feb 12 2019 at 08:55):

this is what I understood in Amsterdam anyway

view this post on Zulip Patrick Massot (Feb 12 2019 at 08:55):

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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:56):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:58):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:58):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:58):

or maybe use a local notation for it

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:59):

Meh, ain't that ugly?

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:59):

Well... we'll see.

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:59):

I wouldn't mind trying uni-hints

view this post on Zulip Mario Carneiro (Feb 12 2019 at 08:59):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Feb 12 2019 at 09:01):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 09:01):

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

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:38):

ok so what do we want to bundle?

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:38):

can we come up with an explicit list?

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:38):

all morphisms between algebraic structures

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:39):

that's not an explicit list

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:39):

should I test it on is_field_hom?

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:39):

is_{,add_}group_hom, is_ring_hom

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:40):

is_{,add_}monoid_hom, similar for semigroups

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 12 2019 at 14:40):

FYI: I changed the topic of this discussion.

view this post on Zulip 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