simps config

Stream: mathlib4

[Yury G. Kudryashov]

@Floris van Doorn Did you recently change simps config? It looks like it needs toFun -> apply instead of, e.g., toLinearMap_toFun -> apply

[Yury G. Kudryashov]

Should we change these?

Mathlib/Analysis/NormedSpace/LinearIsometry.lean:initialize_simps_projections LinearIsometry (toLinearMap_toFun → apply)
Mathlib/Analysis/NormedSpace/LinearIsometry.lean:initialize_simps_projections LinearIsometryEquiv (toLinearEquiv_toFun → apply,
Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean:initialize_simps_projections AffineEquiv (toEquiv_toFun → apply, toEquiv_invFun → symm_apply,
Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean:initialize_simps_projections MulChar (toMonoidHom_toFun → apply, -toMonoidHom)
Mathlib/Topology/Algebra/Module/Basic.lean:initialize_simps_projections ContinuousLinearMap (toLinearMap_toFun → apply, toLinearMap → coe)
Mathlib/Topology/ContinuousFunction/Bounded.lean:initialize_simps_projections BoundedContinuousFunction (toContinuousMap_toFun → apply)
Mathlib/Topology/Homotopy/Basic.lean:initialize_simps_projections Homotopy (toContinuousMap_toFun → apply, -toContinuousMap)
Mathlib/Topology/Homotopy/Basic.lean:initialize_simps_projections HomotopyWith (toHomotopy_toContinuousMap_toFun → apply,
Mathlib/Topology/Homotopy/Equiv.lean:initialize_simps_projections HomotopyEquiv (toFun_toFun → apply, invFun_toFun → symm_apply,
Mathlib/Topology/MetricSpace/Isometry.lean:initialize_simps_projections IsometryEquiv (toEquiv_toFun → apply, toEquiv_invFun → symm_apply)

[Yury G. Kudryashov]

Also, sometimes simp fails to use lemmas generated by simps. I can't make an #mwe yet. I'll open an issue once I hit this bug again.

[Floris van Doorn]

Not recently, but yeah, that changed in Lean 4. The short version does exactly the same as the long version though. It was changed in !4#2042 and !4#2561 changed some existing initialize_simps_projections.

[Floris van Doorn]

Note that projections to parent structures are now disabled by default. So the -toContinuousMap and friends are also not needed anymore, since they're the default behavior. You have to now do +toContinuousMap explicitly if you want it, which is done in some category theory structures.

[Floris van Doorn]

When simp cannot apply the lemmas generated by simps, can you look at whether the output simps? produces looks reasonable?
Another thing I would check is whether Funlike.coe is the default coercion / simp-normal form in the case you're looking at.

[Yury G. Kudryashov]

Unfortunately, after toLinearMap_toFun -> apply it generates lemmas named *_toFun. I'll try to fix these initialize_simps_projections

[Yury G. Kudryashov]

AFAIR, simps? output looked good and rw was able to use them. I'll try to reproduce it later today.

[Yury G. Kudryashov]

(though fixing ContDiff is higher on my priority list)

[Floris van Doorn]

Oh I see, it's generating both _apply and _toFun lemmas? That sounds like a bug.

[Yaël Dillies]

I complained in my PR #19860 about simps never doing exactly what I want it to do, then @Floris van Doorn opened issue #19895, and now @Frederick Pu just opened #20029 to address that issue. I suggest we discuss here our expectations from the simps configuration syntax

[Frederick Pu]

hi

[Frederick Pu]

wait there's like two different discussions for simps config

[Yaël Dillies]

What do you mean?

[Frederick Pu]

image.png

[Frederick Pu]

or are they jhust grouped by days

[Yaël Dillies]

Oh! I see. Not sure what to do, I really want to talk about "simps config" :sweat_smile:

[Frederick Pu]

so fpvandoorn mentioned that he wanted to have the ability to have a config tuple before and after the projections tuple to indicate precedence

[Frederick Pu]

but a think a better approach would just be to always have the config tuple take precedence when there is a contradiction with projections or throw a warning when that occurs

[Frederick Pu]

also, we should probably consider having a separate NameMapExt for the config data since it'll give us more information for error logging (knowing if a conflict is between projection and config vs between projection and projection) as well as making it easier to enforce precendence of config options over projections

[Yaël Dillies]

Could we drop the initialize_simps_projections notation entirely? It's antiquated, hard to guess and unlike any other notation in lean/mathlib.

[Frederick Pu]

what is initialize_simps_projections even used for? is it just called by the @[simps ...]

[Frederick Pu]

so to be clear, initizlie_simps_projections is used for autogenerating simp lemmas from all of the projections (aka structure fields)

[Frederick Pu]

im still a bit confused about what the arrow notation for custom names is:
initialize_simps_projections AddConstMap (toFun → coe, as_prefix coe) is this saying that anytime you see AddConstMap.toFun you should rewrite it as Coe.coe, or coe just a temporary name. If coe comes from Coe.coe then how is lean able to infer it?

[Frederick Pu]

also what's the difference between @simp and @simps?

[Frederick Pu]

im thinking you should be able to just put @[simps (rules, ....) (configs, ...)] above any structure and using something similar to attribute [simp] otherwise

[Artie Khovanov]

Weird thing I just noticed: applying @[simps] to foo : Subsemiring R generates a lemma foo_coe, but applying the same attribute to foo : Submonoid R generates coe_foo.

[Artie Khovanov]

Why does this happen? Surely it is not intended behaviour.

[Artie Khovanov]

OK I found the issue, see #20451

[Kevin Buzzard]

I am surprised about this because mathlib has both

initialize_simps_projections Submonoid (carrier → coe, as_prefix coe)

and

initialize_simps_projections Subsemiring (carrier → coe, as_prefix coe)

[Artie Khovanov]

@Kevin Buzzard I meant Subsemigroup, mb! (As can be seen in the actual PR oops)

[Frederick Pu]

Yaël Dillies said:

I complained in my PR #19860 about simps never doing exactly what I want it to do, then Floris van Doorn opened issue #19895, and now Frederick Pu just opened #20029 to address that issue. I suggest we discuss here our expectations from the simps configuration syntax

is this PR still relevant or are we getting rid of initialize_simps_config altogether