Customize projection name

Stream: general

[Yaël Dillies]

Is it possible to customize the name of a structure projection? I have bar extending foo and would like to call the projection foo.bar, not foo.to_bar, in order to hide the fact that it's a structure as an implementation detail (it is Prop-valued and could have well been unbundled).
cc @Gabriel Ebner

[Andrew Yang]

A possible solution is

structure bar :=
(baz : ℕ)

structure foo extends barbar : bar

#check foo.barbar

#check foo.to_bar -- undefined

[Gabriel Ebner]

First of all, there are some changes in Lean 4 so that don't get to used the projections just yet.

[Kyle Miller]

It could be bar too:

structure bar :=
(n : ℕ)

structure foo extends bar : bar :=
(m : ℕ)

(Then foo.bar is the projection to the parent.)

[Gabriel Ebner]

I'm also not sure if changing projection names is high on the priority list.

[Gabriel Ebner]

That said, it should be a fairly straightforward change. I don't think there's any place where we check that a name begins with to_.

[Yaël Dillies]

I can do with one more lemma in the meantime.

[Reid Barton]

Doesn't extends have some other effects? Is it really something you can hide as an implementation detail?

[Reid Barton]

(The implied question being: why not just make the parent projection an actual field instead?)

[Yaël Dillies]

I don't think that registers the structure the same way for use with the { _ := _ } notation.

[Reid Barton]

If you had two fields (a : A) (b : B), then the notation would be { a := _, b := _ }. So I guess what you mean is that you don't actually want to hide the fact that (say) A is being extended, because you want to support different notation for { ... }?

[Reid Barton]

namely { b := _, .. _ }, I guess?

[Yaël Dillies]

In that case I have is_spectral_map (#12228) that extends docs#continuous and I would the to_continuous to be replaced by the docs#continuous.is_open_preimage one.

[Reid Barton]

That makes sense in principle but I'm a bit surprised because I would have thought that continuous f was the preferred way to say that f is continuous--indeed you use the fact that you can give a proof of continuous in is_spectral_map.comp for example

[Yaël Dillies]

Yes, so if you have continuous f, you use ⟨ ⟩ notation, and if you want to provide it directly, you use { _ := _ }.

[Reid Barton]

Hmm, that seems rather unexpected to me. Maybe I just like using {} because it tells me the field names--I wouldn't expect this kind of detail to differ

[Yaël Dillies]

I found the difference tremendously useful on my hom crusade.

[Reid Barton]

It seems a bit too clever. If you have a proof of is_open_of_whatever you can always just wrap it in a single pair of angle brackets to get to continuous.

[Yaël Dillies]

Yeah, sure, I'm not claiming any of this to be important.

[Reid Barton]

Well, I think it's bad. Every Lean user knows that ⟨x, y⟩ means mk x y means { a := x, b := y }. Sure, there are some edge cases where this isn't quite true due to unusual binder types or whatever, but that is the default expectation. Intentionally violating the expectation of users (= everyone besides yourself) in this way is just bad software engineering.

[Reid Barton]

And in this situation there doesn't even seem to be any real purpose to it, because continuous f is the standard form anyways--I can't speak to other situations because I haven't looked at them.

[Reid Barton]

It doesn't mean using extends is wrong here, only that you can't and shouldn't try to "hide" the fact that the structure uses extends. If you want to work as though continuous is really a field, don't play cute games with renaming projections--just make it a field.

[Gabriel Ebner]

Every Lean user knows that [...] mk x y means { a := x, b := y }

Every Lean user may believe that, but it has been wrong for years---since the structure command became the old structure command. The construction that Yaël outlines is exactly what's already happening, the only thing that the proposal would change is the naming of the subobjects.