working in namespace monoid

Stream: maths

[Jakob von Raumer]

What can I do about simp not doing the right thing here?

import algebra.group.defs

namespace monoid

example {R : Type*} [monoid R] (r : R) : r * (r * r) * r = (r * r) * (r * r) :=
begin
  simp [←mul_assoc],
end

end monoid

Or should I just not be working inside monoid?

[Yaël Dillies]

It works for me. What version of mathlib are you on?

[Floris van Doorn]

You want to use _root_.mul_assoc:

import algebra.group.defs

namespace monoid

example {R : Type*} [monoid R] (r : R) : r * (r * r) * r = (r * r) * (r * r) :=
begin
  simp only [←_root_.mul_assoc],
end

end monoid

[Yaël Dillies]

Ah wait, I get it now.

[Yaël Dillies]

monoid.mul_assoc should be protected.

[Floris van Doorn]

docs#monoid.mul_assoc is a field of the structure that should not be used.

[Jakob von Raumer]

Thanks for the explanation, yea it should be protected then, I guess. Should things about monoids which are a bit "out there" go into monoid or into its own namespace?

[Yaël Dillies]

What are you thinking of?

[Jakob von Raumer]

We formalised the ore localisation of monoids

[Eric Wieser]

If namespace monoid is making name resolution annoying, you can just use lemma monoid.foo instead in the root namespace

[Anne Baanen]

Semi-serious suggestion: should there be a close monoid command that undoes the (implicit) open monoid in namespace monoid?

[Jakob von Raumer]

Eric Wieser said:

If namespace monoid is making name resolution annoying, you can just use lemma monoid.foo instead in the root namespace

After looking at another few examples from mathlib, I now think that namespace ore_localization is actually the better choice anyway :)

[Eric Rodriguez]

Anne Baanen said:

Semi-serious suggestion: should there be a close monoid command that undoes the (implicit) open monoid in namespace monoid?

this is hard, right? because afair Lean implements open by removing all the monoid. from names in the local context, so it'd have to "remember" which ones it removed

[Julian Berman]

Not sure if it's any easier or saner but presuming declarations know their own names could also have an unshadow foo command which loops over declarations with conflicting names and removes the one that isn't from foo (and default foo to _root_)

[Reid Barton]

semigroup has protect_proj, probably it should just be added to monoid too, with an explicit list if there are names we want to not protect

[Kyle Miller]

@Eric Rodriguez It looks like open operates by adding aliases -- it doesn't remove anything.

I learned that open isn't fully documented in the Lean reference manual. Here's the BNF for the command:

open ident [as ident] ( (renaming (ident -> ident)* ) | (hiding ident * ) | ( ident * ) )*

(Square brackets mean it's optional, non-monospace parentheses are for grouping, postfix * means zero-or-more, and | indicates alternatives.)

• example: open foo as bar takes every name in the foo namespace and gives an alias in the bar namespace
• The three types of extra rules are called renames, exceptions, and explicits. There cannot simultaneously be renames/exceptions and explicits (the Lean error is about "mixing explicit and implicit open/export options"; not sure why they're called "implicit" in the error.)
  • If there are explicits: only the listed identifiers are given aliases
  • If there are renames/exceptions: everything but the exceptions are given aliases and the renames are processed (note: renames override exceptions; might be a bug)

[Kyle Miller]

It seems like in principle there could be a close command with the same syntax that erases aliases instead of adding them. (Aliases are special data attached to the current environment.)

[Kyle Miller]

The way export works is it's open but it also adds an "export declaration" to a particular namespace, and then the namespace foo command will look for all the export declarations and "replay" them by simulating the open command.

[Kyle Miller]

Anne Baanen said:

Semi-serious suggestion: should there be a close monoid command that undoes the (implicit) open monoid in namespace monoid?

I'm not sure this could work as an inverse to open -- as far as I understand, there's not an implicit open monoid in the namespace monoid command. Rather, when resolving a name the elaborator goes through the following steps:

1. look through the current stack of namespaces to find the declaration (so, if you're in foo.bar, look in foo.bar then foo)
2. check if it's an exact name (after removing _root_ from the front if present)
3. look for an alias with that name
4. try turning the name into field notation (example: if it's a.b, try resolving a and then get the b field).

There could be a close command to inhibit step 1, I suppose. It seems like a specialized feature though ("all declarations go into this namespace, but do not use it for name resolution").

[Kyle Miller]

I haven't looked at how it'd be implemented, but potentially protected namespace foo could permanently mark a namespace to not be used for name resolution by the elaborator (here's place it happens: https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/elaborator.cpp#L4092). I'm assuming mathport would rather this not be implemented however...