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.