bundling functions

Stream: maths

[Johan Commelin]

@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]

how much of that file do I need?

[Mario Carneiro]

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

[Johan Commelin]

That's quotient_group.quotient

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

oh shit, discrete_field.has_decidable_eq is an instance in core

[Mario Carneiro]

that's not good at all

[Johan Commelin]

Fork! Fork! Fork!

[Johan Commelin]

But is that the reason for your MWE failing?

[Mario Carneiro]

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

[Johan Commelin]

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

[Kevin Buzzard]

Just make an instance of has_undecidable_eq with higher priority

[Mario Carneiro]

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

[Mario Carneiro]

you might want to consider dropping the priority 0

[Johan Commelin]

I wouldn't mind a Lean feature

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

[Johan Commelin]

you might want to consider dropping the priority 0

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

[Kevin Buzzard]

Can one edit the database of instances somehow?

[Kevin Buzzard]

I mean, other than by adding to it?

[Mario Carneiro]

nope, at least not global instances

[Mario Carneiro]

the worry is that it makes import order matter

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

Yeah, it doesn't solve the MWE

[Mario Carneiro]

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

[Mario Carneiro]

it found the right answer and passed it over

[Mario Carneiro]

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

[Johan Commelin]

Your use of "interesting" is… interesting…

[Mario Carneiro]

looks like is_group_hom.comp is the culprit

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

I think group_hom should be a thing sooner rather than later

[Johan Commelin]

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]

the evidence continues to mount in favor of bundled functions

[Johan Commelin]

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

[Kenny Lau]

nonononono it has nothing to do with is_group_hom.comp

[Kenny Lau]

[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

[Kenny Lau]

import data.finsupp

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

[Mario Carneiro]

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

[Kenny Lau]

but still yes for bundling

[Mario Carneiro]

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

[Mario Carneiro]

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]

type class searches with explicit lambdas is never a good idea

[Kenny Lau]

so do we support bundling?

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

yep

[Johan Commelin]

And let's do ring_hom at the same time

[Johan Commelin]

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

[Johan Commelin]

I think that's a good thing.

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

that becomes injective f

[Patrick Massot]

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

[Mario Carneiro]

no

[Patrick Massot]

This would be for bundled structures but not bundled maps?

[Mario Carneiro]

A lot of type class searches will go away though

[Mario Carneiro]

no, the other way around

[Mario Carneiro]

maps bundled, structures unbundled

[Patrick Massot]

I meant unification hints would be for bundled structures

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

exactly

[Patrick Massot]

this is what I understood in Amsterdam anyway

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

or maybe use a local notation for it

[Johan Commelin]

Meh, ain't that ugly?

[Johan Commelin]

Well... we'll see.

[Johan Commelin]

I wouldn't mind trying uni-hints

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kenny Lau]

ok so what do we want to bundle?

[Kenny Lau]

can we come up with an explicit list?

[Johan Commelin]

all morphisms between algebraic structures

[Kenny Lau]

that's not an explicit list

[Johan Commelin]

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

[Kenny Lau]

should I test it on is_field_hom?

[Johan Commelin]

is_{,add_}group_hom, is_ring_hom

[Johan Commelin]

is_{,add_}monoid_hom, similar for semigroups

[Reid Barton]

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]

FYI: I changed the topic of this discussion.

[Chris Hughes]

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