Search for all declarations in a namespace

Stream: general

[Heather Macbeth]

In branch#tendsto_namespacing I am correcting a few lemmas which I noticed were namespaced as tendsto.*** rather than filter.tendsto.***, and thus couldn't be used with projection notation.

Is there a way to do this more systematically -- to generate a list of all lemmas in mathlib in the should-not-exist namespace tendsto?

[Johan Commelin]

@Heather Macbeth I think you can generate a name of all declarations using leanproject

[Johan Commelin]

@Heather Macbeth you can run leanproject decls, this creates decls.yaml which should contain all the info you need.

[Mario Carneiro]

Doesn't #print prefix tendsto suffice?

[Mario Carneiro]

You will have to import all first

[Johan Commelin]

grep "^tendsto[.]" decls.yaml
tendsto.const_add:
tendsto.mul_const:
tendsto.add_const:
tendsto.inv_tendsto_zero:
tendsto.const_mul:
tendsto.min:
tendsto.inv_tendsto_at_top:
tendsto.max:

[Bryan Gin-ge Chen]

For future reference, the mathlib docs site also hosts a text file which contains all the declarations in mathlib: https://leanprover-community.github.io/mathlib_docs/decl.txt

(This is used by the search bar.)

[Heather Macbeth]

Thank you all! Funnily enough, these 8 were the ones I had already found :)

[Patrick Massot]

Thank you very much for doing this Heather. This is the kind of things I notice from time to time but I never have enough courage to stop what I'm doing, fix it and PR.

[Heather Macbeth]

You're welcome. By the way, there are also 6 lemmas with the namespace ennreal.tendsto:

ennreal.tendsto.mul
ennreal.tendsto.const_mul
ennreal.tendsto.mul_const
ennreal.tendsto.div
ennreal.tendsto.const_div
ennreal.tendsto.div_const

Does this serve any purpose? Should they be renamed to, say, filter.tendsto.mul_ennreal, etc?

[Yury G. Kudryashov]

I think that having aliases in the filter.tendsto namespace is a good idea.

[Heather Macbeth]

@Yury G. Kudryashov thanks -- is there a reason you're suggesting the alias rather than just changing the name?

[Yury G. Kudryashov]

Because it's hard to add a lemma to filter.tendsto inside namespace ennreal ... end ennreal. If you prefer to close/open namespace, this is fine with me.

[Kevin Buzzard]

Then you lose all your variables!

[Floris van Doorn]

Unless you declare the variables before starting the namespace :)

[Eric Wieser]

You also lose all your private declarations if you close and reopen a namespace, IIRC

[Scott Morrison]

It's a pity we're not allowed to write def _root_.XXX ....

[Yakov Pechersky]

Could we write some simplemeta code a la to_additive that looks like

@[to_namespace filter]
lemma tendsto.mul ...

[Eric Wieser]

Is there any way to remove declarations from meta code?

[Yakov Pechersky]

We have support for what I'm saying:

protected lemma tendsto.mul {f : filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞}
  (hma : tendsto ma f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ⊤) (hmb : tendsto mb f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ⊤) :
  tendsto (λa, ma a * mb a) f (𝓝 (a * b)) :=
show tendsto ((λp:ℝ≥0∞×ℝ≥0∞, p.1 * p.2) ∘ (λa, (ma a, mb a))) f (𝓝 (a * b)), from
tendsto.comp (ennreal.tendsto_mul ha hb) (hma.prod_mk_nhds hmb)

run_cmd tactic.transform_decl_with_prefix_fun some
  `ennreal.tendsto.mul `filter.tendsto.ennreal.mul []

example {f : filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞}
  (hma : tendsto ma f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ⊤) (hmb : tendsto mb f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ⊤) :
  tendsto (λa, ma a * mb a) f (𝓝 (a * b)) :=
filter.tendsto.ennreal.mul hma ha hmb hb

[Eric Wieser]

Does that delete the original lemma though?

[Yakov Pechersky]

Nope. I second your earlier question.

[Scott Morrison]

I very much doubt there is a mechanism to delete declarations, or ever would be.

[Yakov Pechersky]

A possibility is setting the previous decl as private

[Johan Commelin]

I like the idea of (ab)using private as a hack around this. The resulting attribute is so useful that I don't mind the hack

[Yakov Pechersky]

Instead of doing it via an attribute, what's wrong with alias as a stopgap?

[Yakov Pechersky]

I don't yet see a way of changing a is_private for an existing declaration.

[Eric Wieser]

If the original declaration is marked private by the user, then the copy could presumably be copied without that attribute?

[Yakov Pechersky]

I think that's correct the way 'alias' works