Data.Dfinsupp.Basic !4#1829

Stream: mathlib4

[Johan Commelin]

Lean 4 is refusing to coerce an AddEquiv to a function. I don't really understand why. It's the cause of 80% of the remaining errors in this PR.

[Eric Wieser]

Note that this PR will need to pick up some classical/decidable changes from mathlib master

[Eric Wieser]

Ah nevermind, I see you already did that!

[Eric Wieser]

Don't forget to update the SHA to match

[Eric Wieser]

Maybe we need a shortcut FunLike instance?

[Eric Wieser]

In Lean 3 we had shortcuts for has_coe_fn instances, but those are no longer safe in Lean4. Shortcut FunLike instances should be fine though, as they still unfold to FunLike.coe

[Johan Commelin]

I don't understand the whole coe hierarchy. If someone else could help there, that would be great!

[Eric Wieser]

In mathlib3:

• Classes like add_equiv_class inherit from fun_like, and ultimately are just a to_fun field along with the necessary hom properties. There's some extra stuff for equivs but that shouldn't matter here.
• There is a docs#fun_like.has_coe_to_fun instance which turns any of the derived hom classes into a has_coe_to_fun instance
• In practice, typeclass search is bad at finding this instances, so we have shortcuts like docs#add_equiv.has_coe_to_fun

In Mathlib4

• Same as above
• docs4#FunLike.instCoeFun is now unfolded during elaboration, so when you write f x for some hom f you're actually writing FunLike.coe f x which gives us the head symbol we need for lemmas to match
• The shortcut instances as written in Mathlib3 are now bad as they'd unfold to f.to_fun x not FunLike.coe f x
• We can add new versions of these shortcut instances, either by implementing them as FunLike.coe, or by adding shortcut instances to FunLike instead

[Patrick Massot]

We probably need this explanation in the porting wiki.

[Kevin Buzzard]

I think it would be nice to have some documents like the "extras" (e.g. this) explaining how things like coercions work now. Over in the "What is an outParam" thread I'm figuring out how type class inference works in Lean 4 (by people explaining it to me) and coercions is something else which I'm very hazy on.

[Chris Hughes]

It's also true that for normal coercions, it's often useful to add a new function for the coercion, and then define the has coe to be that function instead of some more complicated term.

[Jireh Loreaux]

@Chris Hughes Can you point to an example where this comes up in practice?

[Gabriel Ebner]

Don't forget to tag that function @[coe] to make norm_cast work.

[Chris Hughes]

Jireh Loreaux said:

Chris Hughes Can you point to an example where this comes up in practice?

One that springs to mind was the coercion A -> WithTop A. In Lean3 this was defined to be Option.some which works because WithTop A is defined to be Option A. This caused elaboration problems. I think there was an example where the coercion was more than one symbol before the new function was defined but I can't find it.

[Johan Commelin]

Error free!

[Johan Commelin]

Thanks to @Anne Baanen for some help!

[Johan Commelin]

Ready for review