Zulip Chat Archive

Stream: maths

Topic: image by permutation power


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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:04):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:04):

But then g is coerced to function too early

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:05):

Is this related to the recent changes to powers?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:07):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:07):

but g^i isn't a set

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:08):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:08):

That works indeed

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:08):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:09):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:10):

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

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:10):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:10):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:10):

wow

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:10):

strange

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:12):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:13):

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:13):

#check ⇑(g^i) '' U

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:15):

Do you understand what happens?

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

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:20):

And what happens when it does not work?

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:21):

I mean when we don't help Lean at all

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:29):

Thanks

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

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:31):

Yes, I understood that bit

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:32):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:32):

Not sure why '' has higher precedence than ^ though

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:32):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:32):

What about using the general has_coe?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:33):

it's way too underdetermined, I think

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:33):

That's what I feared

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:33):

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:33):

it's basically just a functor

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:33):

and there are loads of those

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:33):

I heard functor

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

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:35):

really?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:35):

Takeuti-Zaring Axiomatic Set Theory :P

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:35):

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:35):

I see

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:35):

that kind of books

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:35):

I think it's more about unambiguous notation

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:36):

it's not a beginners book

view this post on Zulip Patrick Massot (Apr 17 2018 at 09:36):

It seems to be a set theory book

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:37):

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 10:58):

Mathematicians have developed a really good system for overloading notation

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 10:59):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

I must be frank

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

I am not sure that it scales

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

I have seen problems with diamonds

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

I have seen problems with the wrong coercion being chosen

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

so my instinct is to

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:00):

(a) give up type classes to a large extent

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:01):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:01):

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:01):

and I have F.whatever_i_called_it for the function

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:02):

It looks a bit messier

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:03):

they would all be different notation

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:03):

and I would not moan about ''

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:03):

because f(U) doesn't really make sense

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:03):

The reason for me is a practical one

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:03):

I just want to write code that works

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:05):

You're right

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:05):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:05):

and in all cases I know the answers

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:05):

the issue is that they are both issues

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:05):

and I don't want to be dealing with issues

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:05):

and filling in the answers myself resolves them

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:06):

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:07):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:07):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:07):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:07):

but one of them is more widgety

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:07):

and one more fooey

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:08):

so one has some coercion from widgets to foos

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:08):

and the other a coercion from foos to widgets

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:08):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:09):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:09):

but I am also avoiding has_coe_to_fun

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:10):

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

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

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:11):

and then I learnt how to unravel things in some cases

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:11):

and then I got used to the unravelling

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 11:11):

and then I figured unravelling wasn't so bad

view this post on Zulip Patrick Massot (Apr 17 2018 at 11:58):

I'm not convinced unraveling everything will scale

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

view this post on Zulip Patrick Massot (Apr 17 2018 at 11:59):

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

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