## Stream: maths

### Topic: image by permutation power

#### Patrick Massot (Apr 17 2018 at 09:02):

variables (α : Type) (g : perm α) (i : ℕ) (U : set α)
#check g '' U         -- set α
#check g^i             -- perm α
#check g^i '' U     -- maximum class-instance resolution depth has been reached


I tried adding various type annotations and parentheses, getting a variety of error messages but no luck

#### Patrick Massot (Apr 17 2018 at 09:04):

Trying (g^i) '' U is probably a better start

#### Patrick Massot (Apr 17 2018 at 09:04):

But then g is coerced to function too early

#### Patrick Massot (Apr 17 2018 at 09:05):

Is this related to the recent changes to powers?

#### Mario Carneiro (Apr 17 2018 at 09:07):

did you try ((g^i:perm α):set α) '' U?

#### Kenny Lau (Apr 17 2018 at 09:07):

but g^i isn't a set

#### Patrick Massot (Apr 17 2018 at 09:08):

He means (g^i : perm α) '' U : set α

#### Patrick Massot (Apr 17 2018 at 09:08):

That works indeed

#### Mario Carneiro (Apr 17 2018 at 09:08):

huh. You're right, that's nonsense, but lean is okay with it for some reason

#### Patrick Massot (Apr 17 2018 at 09:09):

Of course I tried (g^i : perm α) '' U

#### Patrick Massot (Apr 17 2018 at 09:10):

But didn't think of giving : set α at the end

#### Mario Carneiro (Apr 17 2018 at 09:10):

This is weird. Apparently the second type ascription isn't checked at all, the only important thing is that it's a function type so coe_fn is inserted

#### Mario Carneiro (Apr 17 2018 at 09:10):

#check ((g^i:perm α):_ → unit) '' U --ok


#### Patrick Massot (Apr 17 2018 at 09:10):

At least I can continue. But I'd be interested in a shorter way

wow

strange

#### Patrick Massot (Apr 17 2018 at 09:12):

#check (↑(g^i : perm α)) '' U  also works

#### Patrick Massot (Apr 17 2018 at 09:13):

#check ↑(g^i) '' U also!

#### Mario Carneiro (Apr 17 2018 at 09:13):

#check ⇑(g^i) '' U

#### Patrick Massot (Apr 17 2018 at 09:15):

Do you understand what happens?

#### Patrick Massot (Apr 17 2018 at 09:17):

Actually I think it's not so far from stuff we already saw (but without me understanding enough to handle new instances of the problem)

#### Mario Carneiro (Apr 17 2018 at 09:18):

The explicit coercion gives no information to the expected type on the inside, so g^i : _ is inferred to g^i : perm A (usually it goes the other way around), so ⇑(g^i) gets the coe_fn instance for perm A which is A -> A, and it's simple from then on

#### Patrick Massot (Apr 17 2018 at 09:20):

And what happens when it does not work?

#### Patrick Massot (Apr 17 2018 at 09:21):

I mean when we don't help Lean at all

#### Mario Carneiro (Apr 17 2018 at 09:24):

Without a literal arrow, it first assumes the types match up. So (g^i) '' U : _ infers set ?B where g^i : A -> ?B (using U : set A). By the type of ^ we get g : A -> ?B and i : ?C which solves to i : nat and a coercion is inserted for g so ⇑g : A -> A. Finally, it tries to find has_pow (A -> A) nat and no such instance exists.

Thanks

#### Patrick Massot (Apr 17 2018 at 09:30):

Would it make any sense to try to define a coercion from perm X to set X -> set X and hope Lean would use that if I write g U or g^i U?

#### Mario Carneiro (Apr 17 2018 at 09:31):

The original instance resolution overflow is due to g^i '' U which by precedence quirks means g ^ (i '' U); it gets caught in a loop looking for has_coe_to_fun nat for some reason

#### Patrick Massot (Apr 17 2018 at 09:31):

Yes, I understood that bit

#### Mario Carneiro (Apr 17 2018 at 09:32):

No, coe_fn only takes one argument, the domain, unlike coe which has domain and target

#### Patrick Massot (Apr 17 2018 at 09:32):

Not sure why '' has higher precedence than ^ though

#### Mario Carneiro (Apr 17 2018 at 09:32):

so you can only coerce to one kind of function for a given object

#### Patrick Massot (Apr 17 2018 at 09:32):

What about using the general has_coe?

#### Mario Carneiro (Apr 17 2018 at 09:33):

it's way too underdetermined, I think

#### Patrick Massot (Apr 17 2018 at 09:33):

That's what I feared

#### Mario Carneiro (Apr 17 2018 at 09:33):

Any function can be treated as a set function by applying image

#### Mario Carneiro (Apr 17 2018 at 09:33):

it's basically just a functor

#### Mario Carneiro (Apr 17 2018 at 09:33):

and there are loads of those

I heard functor

#### Patrick Massot (Apr 17 2018 at 09:34):

Even without the perm layer, this f '' U notation is definitely the part of my file that looks further away from usual mathematical notation

#### Mario Carneiro (Apr 17 2018 at 09:34):

I know at least one math book which uses double open quotes as an infix operator for image

really?

#### Mario Carneiro (Apr 17 2018 at 09:35):

Takeuti-Zaring Axiomatic Set Theory :P

#### Patrick Massot (Apr 17 2018 at 09:35):

I guess it makes sense to have some kind of specific notation for beginners

I see

#### Patrick Massot (Apr 17 2018 at 09:35):

that kind of books

#### Mario Carneiro (Apr 17 2018 at 09:35):

I think it's more about unambiguous notation

#### Mario Carneiro (Apr 17 2018 at 09:36):

it's not a beginners book

#### Patrick Massot (Apr 17 2018 at 09:36):

It seems to be a set theory book

#### Patrick Massot (Apr 17 2018 at 09:37):

of course if you pretend to be serious when you say everything is a set then you need contortions everywhere

#### Mario Carneiro (Apr 17 2018 at 09:37):

Or if you pretend to be serious when you say everything you write is well typed

#### Kevin Buzzard (Apr 17 2018 at 10:58):

This is all (both Patrick's coercion issue and the weird '' notation) part of one underlying problem.

#### Kevin Buzzard (Apr 17 2018 at 10:58):

Mathematicians have developed a really good system for overloading notation

#### Kevin Buzzard (Apr 17 2018 at 10:59):

Patrick is exactly right about '' -- I've never seen it used to mean image so it doesn't surprise me that he hasn't, and it also doesn't surprise me that the only place Mario has is some set theory book (as opposed to what Patrick and I would call mathematics)

#### Kevin Buzzard (Apr 17 2018 at 10:59):

In maths the notation for the image of U under f : X -> Y is of course just f(U)

#### Kevin Buzzard (Apr 17 2018 at 10:59):

but I am well aware that life is not so easy in Lean

#### Kevin Buzzard (Apr 17 2018 at 11:00):

What the current fix seems to be is this exotic type class system plus clever coercions

I must be frank

#### Kevin Buzzard (Apr 17 2018 at 11:00):

I am not sure that it scales

#### Kevin Buzzard (Apr 17 2018 at 11:00):

I have seen problems with diamonds

#### Kevin Buzzard (Apr 17 2018 at 11:00):

I have seen problems with the wrong coercion being chosen

#### Kevin Buzzard (Apr 17 2018 at 11:00):

so my instinct is to

#### Kevin Buzzard (Apr 17 2018 at 11:00):

(a) give up type classes to a large extent

#### Kevin Buzzard (Apr 17 2018 at 11:01):

and (b) to give up on mathematician's overloading

#### Kevin Buzzard (Apr 17 2018 at 11:01):

With my schemes repo I've not made any attempt to do anything clever like this

#### Kevin Buzzard (Apr 17 2018 at 11:01):

If F is a sheaf then F is not the function on open sets, it's some other thing

#### Kevin Buzzard (Apr 17 2018 at 11:01):

and I have F.whatever_i_called_it for the function

#### Kevin Buzzard (Apr 17 2018 at 11:02):

It looks a bit messier

#### Kevin Buzzard (Apr 17 2018 at 11:02):

but I am coming round to the idea that it is not the end of the world to actually begin distinguishing between these things

#### Kevin Buzzard (Apr 17 2018 at 11:02):

In particular if I were writing the code Patrick is writing I simply would not attempt to identify the permutation, the bijection and the function

#### Kevin Buzzard (Apr 17 2018 at 11:03):

they would all be different notation

#### Kevin Buzzard (Apr 17 2018 at 11:03):

and I would not moan about ''

#### Kevin Buzzard (Apr 17 2018 at 11:03):

because f(U) doesn't really make sense

#### Kevin Buzzard (Apr 17 2018 at 11:03):

The reason for me is a practical one

#### Kevin Buzzard (Apr 17 2018 at 11:03):

I just want to write code that works

#### Kevin Buzzard (Apr 17 2018 at 11:04):

so I don't want to get bogged down with all the issues Patrick is running into just to make it look more like mathematics

#### Sean Leather (Apr 17 2018 at 11:04):

@Kevin Buzzard I think you should be sure that you're distinguishing between coercion issues and type class issues. I'm not sure they're the same.

You're right

#### Kevin Buzzard (Apr 17 2018 at 11:05):

but in some sense they are both solved by filling in the answers myself

#### Kevin Buzzard (Apr 17 2018 at 11:05):

and in all cases I know the answers

#### Kevin Buzzard (Apr 17 2018 at 11:05):

the issue is that they are both issues

#### Kevin Buzzard (Apr 17 2018 at 11:05):

and I don't want to be dealing with issues

#### Kevin Buzzard (Apr 17 2018 at 11:05):

and filling in the answers myself resolves them

#### Kevin Buzzard (Apr 17 2018 at 11:06):

I am very happy with how { H : blah} works

#### Kevin Buzzard (Apr 17 2018 at 11:06):

because if I have {U : set X} (OU : is_open U) then Lean is going to be able to guess what U is

#### Kevin Buzzard (Apr 17 2018 at 11:07):

but I am becoming more and more suspicious of user-added coercions

#### Kevin Buzzard (Apr 17 2018 at 11:07):

I cannot see a viable way of stopping different users creating loops

#### Kevin Buzzard (Apr 17 2018 at 11:07):

What if person X and person Y are both interested in widgets and foos

#### Kevin Buzzard (Apr 17 2018 at 11:07):

but one of them is more widgety

#### Kevin Buzzard (Apr 17 2018 at 11:07):

and one more fooey

#### Kevin Buzzard (Apr 17 2018 at 11:08):

so one has some coercion from widgets to foos

#### Kevin Buzzard (Apr 17 2018 at 11:08):

and the other a coercion from foos to widgets

#### Kevin Buzzard (Apr 17 2018 at 11:08):

and all of a sudden we have two pieces of incompatible code

#### Kevin Buzzard (Apr 17 2018 at 11:09):

user-added type class inference I guess I'm talking about here

#### Kevin Buzzard (Apr 17 2018 at 11:09):

but I am also avoiding has_coe_to_fun

#### Kevin Buzzard (Apr 17 2018 at 11:10):

and this more cautious approach solved a lot of problems for me

#### Sean Leather (Apr 17 2018 at 11:10):

I agree with what you're saying in a purely practical sense. However, I think it stems in general from Lean using elaboration (esp. but not solely via coercions and type-class instance resolution) to guess what you mean. It gets it right most of the time, but it's those few times that it doesn't that wind up frustrating you.

#### Kevin Buzzard (Apr 17 2018 at 11:11):

I think that what happened was that in these cases where it didn't work I first got completely stuck

#### Kevin Buzzard (Apr 17 2018 at 11:11):

and then I learnt how to unravel things in some cases

#### Kevin Buzzard (Apr 17 2018 at 11:11):

and then I got used to the unravelling

#### Kevin Buzzard (Apr 17 2018 at 11:11):

and then I figured unravelling wasn't so bad

#### Patrick Massot (Apr 17 2018 at 11:58):

I'm not convinced unraveling everything will scale

#### Patrick Massot (Apr 17 2018 at 11:59):

And, up to now, I've always been able to solve those kind of issue (well, Mario has always been able...)

#### Patrick Massot (Apr 17 2018 at 11:59):

And I'm very happy to see how it looks like now

#### Patrick Massot (Apr 17 2018 at 12:00):

Ok, it's summer here and I have a lot of maths to read. I'll be trying the IHES garden as a working place, without bringing a computer. See you. :sunglasses:

Last updated: May 12 2021 at 08:14 UTC