can't open namespace AddMon

Stream: general

[Justus Springer]

Consider the following:

import algebra.category.Mon.basic

open AddMon --doesn't work: invalid namespace name 'AddMon'

namespace AddMon

end AddMon

open AddMon --now it works

#check of

My guess is: As long as the namespace AddMon has never been declared, it is considered invalid to open it. And AddMon has never been declared as a namespace because all the definitions it contains were created by to_additive, and not manually. Is this correct? And how can it be fixed?

[Johan Commelin]

@Gabriel Ebner :up: Is this something that should be fixed in core?

[Justus Springer]

If someone who knows how namespaces work could comment on this issue, that would be great! This is actually occurring in a project I'm working on about filtered colimits: First, I defined a bunch of stuff in the namespace Mon.filtered_colimits with @[to_additive] everywhere. Later, for semirings, I would like to both open the namespaces Mon.filtered_colimitsand AddMon.filtered_colimits.

[Yaël Dillies]

As a temporary fix, I guess you could define a dumb thing in AddMon to make it openable?

[Justus Springer]

I could fix it by either

• Making an explicit empty namespace AddMon.filtered_colimits as above, or
• Referencing all the definitions I need by their full name Add.filtered_colimits.xyz.
  While both of these options aren't terrible, they feel a little unsatisfactory...

[Justus Springer]

Yaël Dillies said:

As a temporary fix, I guess you could define a dumb thing in AddMon to make it openable?

Yes, that's the temporary fix I'm going with. But would this be acceptable in mathlib?

[Bryan Gin-ge Chen]

I think it's fine if you include a comment explaining it. I wouldn't wait for the issue to be fixed in Lean 3 (though it could be an easy patch, I have no idea).

[Yaël Dillies]

Maybe even a private def would do it? I haven't tried.

[Alex J. Best]

I think this can be patched on the mathlib side by modifying to additive to add the right namespace whenever it produces à la:

import tactic

run_cmd (do e ← tactic.get_env, tactic.set_env $ environment.add_namespace e `blah)
open blah

[Mario Carneiro]

lean#618

[Alex J. Best]

Oh to additive uses add decl, I take my comment back :smile:

[Mario Carneiro]

Hm, the PR reveals a thorny issue which might require some design work. In short: does the internal declaration foo.equations._eqn_1 in

def foo := 1

mean that foo and foo.equations should be namespaces? This affects the behavior of open:

def foo := 1

namespace bar
def foo.a := 1
open foo -- used to open bar.foo, now opens foo
#check a -- fail
end bar

[Justus Springer]

Wow, thank you @Mario Carneiro ! I would have never been able to fix this myself.

[Alex J. Best]

Should we try to come to some conclusion as to whether foo.equations should become a namespace? Or add the workaround to to_additive? I think I'm hitting this issue again in #9790 so it would be nice to resolve it either way. Of course I should be able to work around it for now

[Alex J. Best]

Actually I guess I misread the PR, @Mario Carneiro does this mean you've implemented option 2 there and are just waiting for review on the Lean PR?

[Mario Carneiro]

@Alex J. Best Sorry about the confusion. The PR lean#618 is "done", it just needs review. I probably scared away all the reviewers with a long comment talking about a design question