TopLevelA.TopLevelB

Stream: mathlib4

[Johan Commelin]

I was talking with Bhavik a moment ago. He mentioned that the following is a bit annoying

import Mathlib.Data.Finset.NatAntidiagonal

open Finset
open Nat

-- haha, you have just opened `Finset.Nat`...

I'm not convinced we actually really want this behaviour.

1. Is there a good reason why we want lemmas to be called Finset.Nat.foobar?
2. How many examples of this pattern are there? I guess it must be easy to generate a list of all toplevel namespaces, and then find all examples of TopLevelA.TopLevelB.foobar that actually occur in Mathlib.

[Ruben Van de Velde]

Like docs#Std.PRange.Nat.size_rio ?

[Chris Henson]

More generally, is the condition we want to avoid here that any nested namespace matches a top-level one?

[Bryan Gin-ge Chen]

I think this pattern is sometimes used so dot notation can be used for specialized defs e.g. when writing tactics. One recent example: docs#Mathlib.Tactic.GuessName.String.splitCase

[Kenny Lau]

@Johan Commelin
23399 examples

import Mathlib
-- import Lean

open Std Lean Elab Command

#eval show CommandElabM Unit from do
  let mut top : HashSet Name := ∅
  let consts := (← getEnv).constants
  let mut names : HashSet Name := ∅
  for (name, _) in consts do
    if name.isInternalDetail || name.isMetaprogramming then continue
    let n₁ :: _ :: _ := name.components | continue
    names := names.insert name
    top := top.insert n₁
  let mut count := 0
  let mut result := ""
  let mut pre : HashSet Name := ∅
  for name in names do
    let n₁ :: n₂ :: _ :: _ := name.components | continue
    if n₂ ∈ top then
      count := count + 1
      result := result ++ s!"{name}\n"
      pre := pre.insert (.str n₁ n₂.toString)
  IO.println s!"{count} offending names"
  IO.println s!"{pre.size} offending prefixes"
  IO.println "Sample:"
  let mut i := 0
  for name in pre do
    i := i + 1
    if i == 30 then break
    IO.println name
  -- IO.println result

[Bhavik Mehta]

I think that some of these are accidentally misnamed lemmas, such as EReal.ENNReal.rpow_eq_exp_mul_log and Set.Subtype.range_coind. It seems like Pi.GCongr is not so helpful either, although many of the others appear somewhat reasonable imo?

[Johan Commelin]

23399 examples

I hope there aren't 23399 unique (TopLevelA, TopLevelB) pairs!

[Kenny Lau]

@Johan Commelin no, that's the second output in the code, which is around 900

[Christian Merten]

I have been playing around with this in the case where TopLevelA = AlgebraicGeometry and TopLevelB = CategoryTheory to make special constructions for docs#CategoryTheory.PreZeroHypercover for the special case of Schemes. I think this is quite a useful feature and we should not forbit its usage.