Please stop adding generalized API around coercions

Stream: general

[Gabriel Ebner]

I've only just noticed #17048, which adds a lot of generalized infrastructure around the coe function. Problem is, we no longer have a coe function in Lean 4. So porting this is far from straightforward.

[Gabriel Ebner]

It is not completely clear to me what the goal of #17048 is (or what concrete problems it solves). So I'm not really sure what the best solution is here.

[Gabriel Ebner]

Either way, please hold off on adding lemmas about coe for now!

[Gabriel Ebner]

cc @Anne Baanen

[Winston Yin]

Sorry if this has been answered before. Is there somewhere an explanation of the changes to coe and casting in Lean4? I can’t find anything in https://leanprover.github.io/lean4/doc/lean3changes.html

[Kevin Buzzard]

A coercion is now syntactically equal to what it unravels to.

[Winston Yin]

So basically, no more up arrows?

[Mario Carneiro]

well no, the up arrows are still there in both input and output, they just don't represent applications of the coe function anymore

[Winston Yin]

Are has_coe instances now defined with a regular function definition marked with the attribute @[coe]?

[Gabriel Ebner]

No coercion instances are still defined with instance : Coe A B where coe := myCast. You need to say @[coe] def myCast := ... so that you get 1) the uparrow delaborator, and 2) norm_cast support.

[Gabriel Ebner]

The reason @[coe] doesn't automatically create the instance is because you need to choose between Coe/CoeTail/CoeHead/etc.

[Jireh Loreaux]

It's not my favorite idea, but do we need to consider reverting #17048? @Gabriel Ebner

[Kevin Buzzard]

There will be plenty of problems with coe whether or not we revert this recent PR, and we're going to have to learn how to deal with them anyway, so I don't immediately see an argument for reverting it. The same argument could be made for eg Damiano's recent addition of a new tactic in lean 3; that also will be hard to port because all tactics need energy to port. The problem is not really #17048, the problem is that mathlib3 is still growing faster than mathlib4 so right now every day the job of porting mathlib gets harder. Gabriel's observation is just that some days the amount by which it gets harder is larger than other days.

[Jireh Loreaux]

Kevin, that is very far from my interpretation of Gabriel's comment (although I could be wrong!). To me, it seems that Gabriel is saying: because coe (the function) doesn't exist in Lean 4, there is going to be massive headache porting anything related to Anne's new coe hom classes, and in fact, there likely won't be any analogue of these in Lean 4.

From that point of view, it seems to make sense to me that we could simplify porting by undoing this change now (especially before the revert commit would rot horribly, if it hasn't already), instead of manually untangling this every time we encounter a coe hom class situation.

[Jireh Loreaux]

I mean, I understand that coercions in general are a lot different and will cause some overhead (I did just port data.{nat, int}.cast.defs so I got some familiarity with it), but direct uses of coe the function (as opposed to some application of a specific coercion) are much stickier.

[Anatole Dedecker]

Kevin, I think you’re being a bit too pessimistic about the port process. I think the relative growing speeds of mathlib3 and mathlib4 will naturally reverse as it gets more and more painful to make PRs to mathlib3 because of the synchronization requirements. Basically my hope is that at some point it will require more energy to do the work twice than to just port what’s missing and do everything in Lean4.

[Anatole Dedecker]

Of course we will never have enough people helping with the ports, but I’m not super bothered by mathlib3 still moving faster

[Gabriel Ebner]

@Kevin Buzzard We know how to port tactics, it's merely laborious. And if we don't want to or manage to port them, we can always prove things manually as a plan B.

[Gabriel Ebner]

With library design changes like this, figuring out how to make it work in Lean 4 is roughly as much work as it took Anne to figure out the Lean 3 design. And we can't fall back to doing things manually in a couple of places because the PR in question touches dozen of type classes, changes simp lemmas etc. (The only fall back would be to revert.)

[Gabriel Ebner]

Ideally we wouldn't have spent effort on that PR in the first place, and instead looked into a better Lean 4 solution.

[Gabriel Ebner]

It already took plenty of time to figure out how to do Nat.cast/numerals in Lean 4. I'm not excited about adding roadblocks to mathlib3 right at the point where people are motivated and start to port files. And Nat.cast is right on the critical path of almost everything.

[Gabriel Ebner]

Maybe we should have marked data.nat.cast etc. as "frozen" months ago.

[Gabriel Ebner]

I'm not sure if we need to revert the PR, but we'll certainly need to rewrite the new type classes.

[Gabriel Ebner]

(That's why I pinged @Anne Baanen to hear more about the motivation behind the PR so that we can port this right.)

[Eric Wieser]

I think the underlying motivation for Anne's change was to eliminate and generalize algebra_map in favor of coe (unifying it with nat.cast); down the line this could get rid of matrix.scalar and polynomial.C if we wanted too. Of course, the whole idea hinges on making coe the simp-normal form, which doesn't work if Lean4 unfolds it back to its implementation. Maybe Anne had a better picture of how things might work in Lean 4 though.

[Eric Wieser]

My hunch is that eventually in Lean4 we'll actually want to go back to the unbundled morphism design if the new simplifier permits it; and then we won't need the coe typeclasses at all, which are really just special cases of it.

[Eric Wieser]

But that's not remotely explorable until the port is over

[Scott Morrison]

I think we should consider reverting this one. It's a shame to discard Anne's work, but I think we all know Anne's work is great, and Anne knows we know that, and this is just a unfortunate situation arising in the porting process.

[Scott Morrison]

Relatedly, I wonder if we should just adopt a "no new tactics PRs" for mathlib 3. (Of course bugfixes and backports would be welcome.)

[Eric Wieser]

I think positivity and norm_num extensions are probably ok as porting one should be much like porting the rest, but brand new tactics probably not so much.

[Mario Carneiro]

New tactics are fine. We are definitely porting tactics faster than they are written, especially nontrivial ones

[Mario Carneiro]

The tactic list has seen some substantial reduction, I'm hopeful we will have most of the tactics done by the end of the year

[Mario Carneiro]

besides, I don't see any reason to say no to making lean 4 better

[Yaël Dillies]

I think in the case of #17048, the Lean 4 solution is to declare coercions from bundled operators. Then there will syntactically be a whatever_hom.to_fun available.

[Yaël Dillies]

And then if an instance something_hom_class (whatever_hom ...) ... exists, Anne's general lemmas apply.

[Scott Morrison]

My thought with "no new tactics" was more along the lines of telling people who want to write new tactics to just write them in Lean 4 to begin with...

[Jireh Loreaux]

Yaël, I couldn't quite put that together in my head. Can you elaborate a bit, maybe with a simple example?

[Anne Baanen]

First of all, feel free to revert #17048 while we figure out how to deal with the porting situation. Nothing major should depend on this yet.

[Anne Baanen]

Subclassing has_lift_t in this way immediately allows us to solve the concrete problem that we have a huge multitude of lemmas like docs#nnrat.coe_sum docs#nnreal.coe_sum docs#submodule.coe_sum docs#add_submonoid.coe_finset_sum docs#nat.cast_sum. These all have the same mathematical content but are redundantly stated and proved on an ad-hoc basis, so they are unavailable half of the time that you need them, so there is no docs#subring.coe_sum.

At the same time, we've figured out thanks to the docs#algebra class that the right way to treat many inclusions of rings and fields in a uniform way is to assume the existence of a canonical homomorphism (algebra_map in this case). There are quite a few places in group theory where the same strategy should apply.

Finally, there are types with such a canonical homomorphism that is defeq to both coe and algebra_map (if it exists) but spelled differently: docs#polynomial.C, docs#adjoin_root.of docs#subring.subtype docs#nat.cast_ring_hom. etc. Apart from yet again more duplication and inconsistencies in all these implementations, it's terribly annoying to have coe in the goal and a simp lemma involving polynomial.C or vice versa. Arguably algebra_map itself also counts as a weird spelling of this canonical homomorphism.

As I said, subclassing has_lift_t in this way immediately allows us to solve the first problem, which means coe is now a viable candidate to serve as the canonical map that we need for the other two points. On the other hand, those more abstract goals can also be achieved without coe.

[Anne Baanen]

About unbundled morphisms: these will be much more useful in Lean 4 but still come with limitations. Toy example:

import Mathlib

class IsZeroHom {A B : Type _} (f : A → B) [Zero A] [Zero B] :=
  (map_zero : f 0 = 0)

open IsZeroHom

instance [AddGroupWithOne R] : IsZeroHom (Int.cast : ℤ → R) where
  map_zero := Int.cast_zero

instance [Zero A] : IsZeroHom (id : A → A) where
  map_zero := rfl

instance [Zero A] [Zero B] [Zero C] (f : B → C) (g : A → B)
    [IsZeroHom f] [IsZeroHom g] : IsZeroHom (f ∘ g) where
  map_zero := by simp [Function.comp_apply, map_zero]

#synth IsZeroHom (id : ℤ → ℤ) -- succeeds

set_option trace.Meta.Tactic.simp true in
example [AddGroupWithOne R] : (↑(0 : ℤ) : R) + (0 : R) = 0 :=
  by simp only [add_zero, IsZeroHom.map_zero] -- succeeds, but tries to unify `?f 0` with every subterm
example [AddGroupWithOne R] : (↑(0 : ℤ) : R) + (0 : R) = 0 :=
  by rw [add_zero, IsZeroHom.map_zero] -- failed, pattern is a metavariable

Since Function.id and Function.comp are no longer reducible, there is no more looping on trying to synthesise IsZeroHom (id ∘ id ∘ id ∘ id ∘ ...) and the simplifier now accepts lemmas with a metavariable as head (rw still doesn't though).

However, we still have two objections to unbundled maps that remain unchanged from Lean 3:

• Since ?f 0 could unify potentially with any subterm of the goal, the simplifier has to scan through everything, which I expect will have the same performance impacts as it did in Lean 3. (At least it doesn't seem to find a IsZeroHom instance on each subterm.)
• The collection of morphisms is still an interesting object in its own right, so we still want to have some level of bundled maps to e.g. put a group structure on the automorphisms of a vector space.

[Anne Baanen]

Honestly, I don't know what the right plan is at the moment: it would be easy enough to redo the classes in a way that doesn't mention coe. Due to various other projects I have to finish at the moment, I don't particularly feel motivated to do so, especially without some reassurance that there are no further secret breakages in Lean 4.

[Anne Baanen]

I don't want to go off on a whole rant but each of my encounters with the Lean 4 port has been frustrating, despite all the advantages I know Lean 4 is supposed to bring. :(

[Kevin Buzzard]

I totally agree that porting files is frustrating, precisely because we don't notice all the stuff which works and only have to bang our head against the wall dealing with the stuff which doesn't work :-)

[Gabriel Ebner]

I'm sorry this is frustrating you. I should have raised this issue earlier before you had invested so much time into it, but the PR flew completely under my radar.

[Gabriel Ebner]

it's terribly annoying to have coe in the goal and a simp lemma involving polynomial.C or vice versa.

This is exactly what moving to Lean 4 would have fixed automatically: the elaborator now produces polynomial.C so there's no annoying mismatch.

[Eric Wieser]

What it doesn't solve is having to repeat coe_add/coe_sum lemmas for types where the canonical map can't always be bundled

[Jireh Loreaux]

I would guess those are relatively rare, right? What situations do you have in mind where this map can't be bundled?

[Yaël Dillies]

... whenever different bundlings hold in different generalities, which is a ubiquitous situation

[Eric Wieser]

The one that comes to mind immediately is docs#matrix.scalar, but nat.cast is another good example since docs#nat.cast_mul doesn't hold as often as docs#nat.cast_add.

[Eric Wieser]

But certainly we shouldn't attempt to solve this problem mid-port

[Eric Rodriguez]

Gabriel Ebner said:

it's terribly annoying to have coe in the goal and a simp lemma involving polynomial.C or vice versa.

This is exactly what moving to Lean 4 would have fixed automatically: the elaborator now produces polynomial.C so there's no annoying mismatch.

I mean but I think the issue is that now we need to have simp lemmas for all these normal forms of the coercions as opposed to just having a "coercion" simp lemma, which removes a hell of a lot of boilerplate

[Eric Rodriguez]

plus I don't think humans want to see goals with stuff like adjoin_root.of (nat.cast k) * r, because to them that is just k * r

[Jireh Loreaux]

Note that ↑ still appears in the tactic state, but that doesn't address the boilerplate issue.

[Yaël Dillies]

Yeah, having a single coe function had the appeal that we could write lemmas about it.

[Eric Rodriguez]

Jireh Loreaux said:

Note that ↑ still appears in the tactic state, but that doesn't address the boilerplate issue.

sometimes not; I've not seen it work a single time with equiv.toFun, for example

[Mario Carneiro]

did the function get tagged as @[coe]?

[Jireh Loreaux]

Yaël, can we just write lemmas involving the coe attribute though? (I have no idea, just flailing in the dark)

[Eric Rodriguez]

Mario Carneiro said:

did the function get tagged as @[coe]?

image.png

I don't think so, this seems the only close-to-related thing in equiv's files. should we have a line attribute [coe] Equiv.toFun?

[Mario Carneiro]

yes

[Mario Carneiro]

we'll have a linter for this at some point

[Yaël Dillies]

Jireh Loreaux said:

Yaël, can we just write lemmas involving the coe attribute though? (I have no idea, just flailing in the dark)

It doesn't even make sense to state that some function is tagged with coe though, right?

[Eric Rodriguez]

I wonder if this is what was causing the issues with EmbeddingLike and also map_one

[Mario Carneiro]

Yaël Dillies said:

Jireh Loreaux said:

Yaël, can we just write lemmas involving the coe attribute though? (I have no idea, just flailing in the dark)

It doesn't even make sense to state that some function is tagged with coe though, right?

it does

[Yaël Dillies]

How can I state that a function is tagged with coe?

[Mario Carneiro]

I mean, you can have a metaprogram look for the attribute

[Mario Carneiro]

I'm not sure what you are after here

[Mario Carneiro]

why does the fact that a function is a coe have anything to do with the lemmas that are provable for it?

[Eric Rodriguez]

Mario Carneiro said:

yes

image.png

this cannot be right

[Mario Carneiro]

that appears to be a bug in the coe delaborator

[Mario Carneiro]

it's actually a somewhat challenging issue because the @[coe] attribute doesn't know whether toFun : Equiv A B -> A -> B is supposed to be a coe from A to B or Equiv A B to A -> B

[Mario Carneiro]

cc: @Gabriel Ebner

[Mario Carneiro]

I think it is safe to say that we should look at the first explicit argument of the function as the source and the rest as the destination

[Gabriel Ebner]

Yeah, the attribute doesn't support function corrections yet.

[Gabriel Ebner]

E.g. the FunLike.coe function is registered manually.

[Gabriel Ebner]

The explicit argument heuristic sounds good to me. This covers everything we've got. And in the worst case you can always fall back to registering it manually.

[Floris van Doorn]

I would personally like coercions to functions (and sorts?) to not appear in the tactic state at all. In all non-artificial situations there is only one way to treat an object as a function (or a sort), and from the context 99% of the time it is clear that you are treating an object as a function, since you're e.g. applying it to an argument. (An exception is a lemma like f = g ↔ ⇑f = ⇑g.)

[Yaël Dillies]

But if they do not appear in the tactic state, they are not inspectable, so you can't jump to where the coercion is defined, etc

[Floris van Doorn]

Maybe I'm wishful thinking, but for me the ideal behavior would be that clicking on the term with the hidden coercion does show the coercion application in the pop-up (if you want to get to the non-coercion application you click the corresponding argument of the coercion to open a second pop-up).

[Yaël Dillies]

That can be (and already is?) a pp option. Of course typing set_option ... in every file you inspect is not a solution, so it would be nice to make pp options persistently configurable from the VScode extension.

[Floris van Doorn]

I think there is an option for removing all coercion arrows. But the normal coercion arrows (not to functions or sorts) are useful (since they often convey information not contained in the rest of the expression), and I want to keep those.

[Floris van Doorn]

I agree that user-configurable default pp options in the extension would be useful.

[Yaël Dillies]

Then we should make suboptions for each type of coercion.

[Yury G. Kudryashov]

I see that the discussion moved from "what can be used by simp etc" to "what a user sees in the tactic state". Do I understand correctly that we can write lemmas about FunLike coercions because Lean only unfolds it up to FunLike.coe, not to Equiv.toFun etc? So, we're emulating Lean 3 here.

[Yury G. Kudryashov]

About the original issue: can we teach Lean 4 simp that a lemma about coe applies to any function tagged with @[coe]?

[Yury G. Kudryashov]

This would make all those general coe_add/coe_sum lemmas useful again.

[Meow]

What is the best way to unfold local definitions?

[Meow]

I usually use simp only [] now.

[Martin Dvořák]

Yeah, I hate this stuff.

[Anne Baanen]

Yury G. Kudryashov said:

About the original issue: can we teach Lean 4 simp that a lemma about coe applies to any function tagged with @[coe]?

An idea I got while away from the computer, so untested: would it be possible to use unification hints for this purpose? Not sure how they work in Lean 4, let alone in combination with tactics, but it would be nice to be able to say that @Nat.cast _ _ n =?= @coe _ _ _ n should unify, and have simp/rw/etc. respect that