Assorted renames

Stream: mathlib4

[Winston Yin (尹維晨)]

I've collected the following list of names that I believe should be changed.

1. docs#chartedSpace: It's the charted space instance for spheres. I suggest chartedSpaceSphere, mirroring docs#chartedSpaceSelf.
2. docs#smoothMfldWithCorners: It's the SmoothManifoldWithCorners instance for spheres. I suggest smoothManifoldCornersSphere
3. docs#funLike: It's only for MulChar, so either something like funLikeMulChar or let Lean generate an automatic instance name.
4. docs#PartialEquiv.trans_self_symm: I suggest PartialEquiv.self_trans_symm to mirror docs#Equiv.self_trans_symm. Similarly, rename docs#PartialEquiv.trans_symm_self to PartialEquiv.symm_trans_self.
5. docs#PartialHomeomorph.trans_self_symm: I suggest PartialHomeomorph.self_trans_symm to mirror docs#Homeomorph.self_trans_symm. Similarly, rename docs#PartialHomeomorph.trans_symm_self to PartialHomeomorph.symm_trans_self.
6. docs#Homeomorph.transPartialHomeomorph_symm_apply: I suggest Homeomorph.transPartialHomeomorph_symm_coe because there's no function application going on, just coecion. Similarly rename docs#Homeomorph.transPartialHomeomorph_apply, docs#PartialHomeomorph.transHomeomorph_symm_apply, and docs#PartialHomeomorph.transHomeomorph_apply.

Items 1-3 are currently confusing when searching in the docs, as the names are too general. Comments and opinions welcome. If people find these agreeable, I'll open a PR.

Another question is, how come dot notation works for Equiv.symm when rendered (e.g. e.symm.trans e') but not for Homeomorph or PartialHomeomorph?

[Kevin Buzzard]

Items 1-3: nice finds! Yes definitely open a PR.

[Patrick Massot]

About the last question, I'm not 100% sure I understand the question, but if I understand then it is a missing pp_dot attribute.

[Ruben Van de Velde]

3: MulChar.instFunLike

[Johan Commelin]

Similarly, I think Sphere.instChartedSpace, etc...

[Winston Yin (尹維晨)]

Looks like item 6 is autogenerated by @[simps! (config := .asFn)], so I'm not going to touch it.

[Winston Yin (尹維晨)]

Items 1-3 in #9429

Items 4-5 + @[pp_dot] in #9430

[Winston Yin (尹維晨)]

Johan Commelin said:

Similarly, I think Sphere.instChartedSpace, etc...

I've named it Metric.sphere.instChartedSpace, and so on.

[Eric Wieser]

Patrick Massot said:

About the last question, I'm not 100% sure I understand the question, but if I understand then it is a missing pp_dot attribute.

I think I tried this, but it means that for e : MulEquiv A B, e.toEquiv.symm prints the same way as e.symm, which is bad.

[Eric Wieser]

(old structures for morphisms, which is on my to-do list, would fix this)

[Winston Yin (尹維晨)]

@Eric Wieser I tested it, and this is the current behaviour of Equiv and MulEquiv, because Equiv has pp_dot. Should I hold off on marking Homeomorph, etc. with pp_dot until old structures for morphisms land?

[Winston Yin (尹維晨)]

By clicking symm in e.symm, I can see which structure's symm it is. This is probably not ideal.

[Eric Wieser]

Thanks for checking, I wasn't 100% certain myself.

[Eric Wieser]

Winston Yin (尹維晨) said:

Should I hold off on marking Homeomorph, etc. with pp_dot

I think that's probably best

until old structures for morphisms land?

I think this is a long way off since:

• It is a rather tiresome refactor (#6791 is an early attempt, but it would be better to build upon #8977)
• If the refactor is a success, then it requires lean4#2940 to be merged and released, which requires buy in from the FRO, in particular Leo who is apparently opposed to old structures.
• I seem to be the person most motivated to try it, but I have no time to do so in the next month

[Patrick Massot]

I would go on with pp_dot in the meantime.

[Eric Wieser]

I'm not convinced that having confusing goal states is better than having verbose goal states

[Eric Wieser]

A middle ground would be to write a custom delaborator that doesn't repeat the mistake that pp_dot makes of dropping the toEquiv

[Eric Wieser]

Maybe @Kyle Miller has some ideas on improving the delaborator here

[Patrick Massot]

I don't want to see that toEquiv by default. For me this is a feature, not a bug.

[Winston Yin (尹維晨)]

I’m torn because verbose goal states that don’t correspond to usual mathematical notation do lead to a non-insignificant slowdown in proof writing, but on the other hand, getting stuck on an incorrect rewrite lemma due to dot notation ambiguity can be truly frustrating.

[Winston Yin (尹維晨)]

For now in #9430 I’ve reverted the new pp_dot attributes. But I would like to have dot notation working for things like symm and trans ideally much before Eric’s refactor lands.

[Eric Wieser]

Patrick Massot said:

I don't want to see that toEquiv by default. For me this is a feature, not a bug.

I claim that it is not that you don't want to see it; but that you don't want it to be there at all.
As I understand it, the behavior matrix is:

	no pp_dot	pp_dot	what we had in lean 3
Simp-normal form	Homeomorph.symm e x	e.symm x	e.symm x
Non-simp-normal form	Equiv.symm e.toEquiv x	e.symm x	e.toEquiv.symm x

and we have to pick a column

[Winston Yin (尹維晨)]

It seems that the type of x will clue which .symm is being used here. If still unclear, clicking on .symm will reveal this info. Is this enough of a disambiguation? The second column looks far better for working with a load of nested/composed equivs.

[Winston Yin (尹維晨)]

Currently, I have to copy the goal state, paste it somewhere, manually turn it into the style of column 2, reason about it, and then continue with my proof.

[Eric Wieser]

I edited with a third column, which is the behavior we actually want