protected

Stream: mathlib4

[Antoine Chambert-Loir]

What is the meaning and use of the protected attribute for theorems?
It seems that they force us to use the full namespace declaration to be usable and prevent to use the dot notation…

[Eric Wieser]

Can you give a #mwe showing it preventing dot notation?

[Antoine Chambert-Loir]

I'll try to get a #mwe (I'm adding Equivariant morphisms, so things happen here and there), but basically it seems to be related to the problem indicated before the code of docs#LinearMap.map_smulₛₗ :

-- Porting note: simp wasn't picking up map_smulₛₗ for LinearMaps without specifying
-- map_smulₛₗ f, so we marked this as @[simp] in Mathlib3.
-- For Mathlib4, let's try without the @[simp] attribute and hope it won't need to be re-enabled.

[Eric Wieser]

I think those problems are unrelated to protected

[Antoine Chambert-Loir]

Hence my question about the meaning of protected. (Because when I delete the protected, I get access to the stuff…)

[Eric Wieser]

Do you have a branch showing this behavior, if a mwe is too much work?

[Antoine Chambert-Loir]

Yes, this is branch#SMulSemiHom, you can have a look at line 588 of file Mathlib/Algebra/Hom/GroupAction.lean, see https://github.com/leanprover-community/mathlib4/blob/4682c890ebb31af7a22c856909d4c0c9e5c8259d/Mathlib/Algebra/Hom/GroupAction.lean

[Antoine Chambert-Loir]

https://github.com/leanprover-community/mathlib4/blob/4682c890ebb31af7a22c856909d4c0c9e5c8259d/Mathlib/Algebra/Hom/GroupAction.lean#L587

[Antoine Chambert-Loir]

(but you're right, that example does not show the problem with the dot notation).

[Antoine Chambert-Loir]

(I try to solve several problem at once :-())
The problem with the dot notation that I don't understand is on line 657, https://github.com/leanprover-community/mathlib4/blob/4682c890ebb31af7a22c856909d4c0c9e5c8259d/Mathlib/Algebra/Hom/GroupAction.lean#L657 .
If I type comp' g f, Lean understand what I means, but g.comp' f does not work (and works for another class).

[Eric Wieser]

Does removing protected make both work?

[Eric Wieser]

Or are you now agreeing that protected is unrelated?

[Antoine Chambert-Loir]

I think I definitively have to agree that it is unrelated…

[Antoine Chambert-Loir]

Can you explain what protected means ?
— why did #check map_smulₑ f fail while it succeeded if I removed protected?

[Antoine Chambert-Loir]

For the dot notation, I see that there, f is a DistribMulActionSemiHom while the namespace is DistribMulActionHom. (The former are additive maps which are equivariant for a morphism of the stuffs that act, the latter is the classic case of identity.)
I try to copy the principles of my generalization on what has been done for LinearMap, sometimes the adverb Semi is present, sometimes not, but I am not sure I do it consistently and in the right way.

[Antoine Chambert-Loir]

The goal is that LinearMap and whatever follows does require minimal adaptations. But maybe it's irrealistic.

[Ruben Van de Velde]

protected solves this issue

def _root_.foo := ...
def Bar.foo := ...
open Bar
#check foo -- error: which foo did you mean

[Antoine Chambert-Loir]

so all those foo which do not have the explicit namespace Bar are supposed to use _root_.foo?
That may solve many problems of mine where I had to include _root_. all over the place!

[Anatole Dedecker]

protected means that you have to use the full name, even if you have opened the corresponding namespace. It should work fine with doc notation though.

[Eric Wieser]

Note that you can override protected with open MyNamespace (a_protected_lemma)