Zulip Chat Archive

Stream: new members

Topic: namespace conflict


view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 10:47):

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?

view this post on Zulip Mario Carneiro (Jul 14 2020 at 10:49):

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

view this post on Zulip Mario Carneiro (Jul 14 2020 at 10:49):

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

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 10:50):

Mario Carneiro said:

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

How do I do that?

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 10:51):

I mean I do not understand "after the fact"

view this post on Zulip Mario Carneiro (Jul 14 2020 at 10:53):

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

view this post on Zulip Mario Carneiro (Jul 14 2020 at 10:54):

so there is no good place to put the word protected

view this post on Zulip Mario Carneiro (Jul 14 2020 at 10:57):

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

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 11:00):

Ok cool this works!!

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 11:00):

Thanks!

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 11:01):

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

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 11:23):

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

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 11:33):

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?

view this post on Zulip Rob Lewis (Jul 14 2020 at 11:34):

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

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 11:36):

Ok thanks!

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 11:45):

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).

view this post on Zulip Reid Barton (Jul 14 2020 at 11:46):

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

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 12:54):

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?

view this post on Zulip Reid Barton (Jul 14 2020 at 13:02):

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.

view this post on Zulip Reid Barton (Jul 14 2020 at 13:03):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 13:04):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 13:04):

This occurs many places in mathlib

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 13:23):

Ok thanks


Last updated: May 15 2021 at 00:39 UTC