protected as attribute

Stream: general

[Johan Commelin]

I think it has been discussed, but before the community fork: can we make protected an attribute? And if so, how hard would it be? (Maybe we can still support the current syntax of protected lemma ...?)

[Gabriel Ebner]

Can you elaborate on what the advantages of @[protected] would be?

[Johan Commelin]

@Gabriel Ebner One example would be: copy init.algebra.ring, replace all alphas by int, and mark all the proven lemmas as protected at the end. This way you don't have to replace every occurence of add_comm by int.add_comm, etc...

[Johan Commelin]

Better example: we have topological_space.is_open and _root_.is_open. Currently, if you open topological_space, this leads to conflicts.

[Johan Commelin]

Really, we would want to mark topological_space.is_open as protected after creating the class.

[Gabriel Ebner]

Oh, and also local attribute [protected] I guess.

[Rob Lewis]

It's not an attribute, but there's environment.mk_protected right now, so you can do this with a command. Can't remove it though.

[Johan Commelin]

Aha, maybe that's good enough for now.

[Reid Barton]

I don't think you can remove an attribute either. (Would you really want to make something protected locally? There's also open hiding.)

[Johan Commelin]

What does open hiding do? Does it locally unprotect things?

[Johan Commelin]

Because I might want to locally unprotect things

[Rob Lewis]

Hmm, the doc string for user_attribute says something about attributes being unremovable if you give an after_set without a before_unset. I thought this had to do with when you could use local attribute, but apparently not.

[Reid Barton]

No, it locally protects things (I think?)

[Reid Barton]

Locally unprotecting would be more like open showing (which doesn't exist)

[Reid Barton]

"Even though the person who wrote the library says I don't want to automatically import these names to top-level, I want to do it anyways"

[Reid Barton]

With an attribute you couldn't locally unprotect things anyways, could you?

[Johan Commelin]

Yeah, I see now

[Sebastian Ullrich]

Why, would local attribute [-protected] not work?

[Reid Barton]

Oh, I was under the impression that syntax doesn't exist or doesn't actually do anything or something like that.

[Sebastian Ullrich]

It doesn't work for all attributes, but there's no reason it shouldn't for a [protected] attribute

[Johan Commelin]

What should I do to make lean happy?

run_cmd environment.mk_protected int.neg_mul_eq_mul_neg
/-
basic.lean:47:0: error
don't know how to synthesize placeholder
context:
⊢ Type
basic.lean:47:8: error
type mismatch at application
  environment.mk_protected int.neg_mul_eq_mul_neg
term
  int.neg_mul_eq_mul_neg
has type
  ∀ (a b : ℤ), -(a * b) = a * -b : Prop
but is expected to have type
  environment : Type
Additional information:
/home/jmc/data/math/mathlib/src/init_/data/int/basic.lean:47:8: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    ?m_1.mk_protected
  has type
    name → environment
  but is expected to have type
    tactic ?m_1
-/

[Mario Carneiro]

run_cmd do env ← tactic.get_env,
  tactic.set_env $ env.mk_protected ``int.neg_mul_eq_mul_neg

[Johan Commelin]

Thanks! And when I want to do this for a whole list of names?

[Johan Commelin]

I'll need some fold, I guess?

[Mario Carneiro]

run_cmd do env ← tactic.get_env,
  tactic.set_env $ [``nat, ``int].foldl environment.mk_protected env

[Johan Commelin]

Thanks again!