namespace conflict

Stream: new members

[Nicolò Cavalleri]

I am trying to work with continuous bundled functions. I have a problem with namespaces. I defined

structure continuous_map (α : Type*) (β : Type*)
[topological_space α] [topological_space β] :=
(to_fun       : α → β)
(continuous   : continuous to_fun)

However, in the namespace continuous_map continuous conflicts with the already existing continuous. In the algebra section this problem would be solved by renaming continuous to is_continuous. However this is a pretty drastic change. By now I renamed continuous in continuous_map to continuity, but this conflicts with Mathlib naming conventions. Any tip?

[Mario Carneiro]

I think it's possible to protect definitions after the fact as of some recent version

[Mario Carneiro]

that way continuous_map.continuous will not compete with continuous even if you open the continuous_map namespace

[Nicolò Cavalleri]

Mario Carneiro said:

I think it's possible to protect definitions after the fact as of some recent version

How do I do that?

[Nicolò Cavalleri]

I mean I do not understand "after the fact"

[Mario Carneiro]

Normally you would protect a definition by writing protected def ... but in this case the definition is the field of a structure, which is automatically generated

[Mario Carneiro]

so there is no good place to put the word protected

[Mario Carneiro]

There is possibly a more streamlined version of this, but here's a way to do it

structure foo := (A B : ℕ)

run_cmd tactic.updateex_env $ λ e, return $ e.mk_protected ``foo.B

namespace foo

#check A -- works
#check B -- fails
#check foo.B -- works

end foo

[Nicolò Cavalleri]

Ok cool this works!!

[Nicolò Cavalleri]

Thanks!

[Nicolò Cavalleri]

I guess it is fine if such a line is PRed to Mathlib

[Sebastien Gouezel]

Even better, you can use @[protect_proj] which is designed precisely for this.

[Nicolò Cavalleri]

Sebastien Gouezel said:

Even better, you can use @[protect_proj] which is designed precisely for this.

Can I use it to only protect continuous and not to_fun?

[Rob Lewis]

https://leanprover-community.github.io/mathlib_docs/attributes.html#protect_proj
@[protect_proj without ...] should work.

[Nicolò Cavalleri]

Ok thanks!

[Sebastien Gouezel]

Note that protecting to_fun also is probably a good idea, because you will never want to use to_fun directly, but instead you should register a coercion. This would mean that the field continuous should be renamed continuous' or continuous_to_fun in your structure, and the main lemma would be stated as continuity of the coerced function (and you can protect it directly).

[Reid Barton]

And even if you do use to_fun directly, it would mainly be in the form f.to_fun x

[Nicolò Cavalleri]

Sebastien Gouezel said:

Note that protecting to_fun also is probably a good idea, because you will never want to use to_fun directly, but instead you should register a coercion. This would mean that the field continuous should be renamed continuous' or continuous_to_fun in your structure, and the main lemma would be stated as continuity of the coerced function (and you can protect it directly).

Why using this trick to protect continuous instead that protect_proj as you suggested before?

[Reid Barton]

It's not about protecting but rather that, if the primary way to use f as a function is f x and not f.to_fun x, then you want f.continuous to be of the form continuous f and not continuous f.to_fun.

[Reid Barton]

You cannot define it this way in the structure because the coercion instance does not exist yet.

[Reid Barton]

But that's fine because dot notation also works with things that are not structure fields.

[Reid Barton]

This occurs many places in mathlib

[Nicolò Cavalleri]

Ok thanks