Notation conflict in CW-complex PR

Stream: mathlib4

[Jiazhen Xia]

I've been working with @E. Dean Young on Whitehead theorem and we are very close to finishing the PR that defines relative CW-complexes.

We (@Yaël Dillies @Kim Morrison) think the following definitions are useful more generally than just for CW-complexes and we want to move them to Topology/Category/TopCat/Basic.lean.

/-- The `n`-sphere is the set of points in ℝⁿ⁺¹ whose norm equals `1`,
endowed with the subspace topology. -/
noncomputable def sphere (n : ℤ) : TopCat.{u} :=
  TopCat.of <| ULift <| Metric.sphere (0 : EuclideanSpace ℝ <| Fin <| Int.toNat <| n + 1) 1

/-- The `n`-disk is the set of points in ℝⁿ whose norm is at most `1`,
endowed with the subspace topology. -/
noncomputable def disk (n : ℤ) : TopCat.{u} :=
  TopCat.of <| ULift <| Metric.closedBall (0 : EuclideanSpace ℝ <| Fin <| Int.toNat n) 1

However, doing so results in a conflict between the Lean-3-style notation ⟪x, y⟫_𝕜 for inner product and the (Lean 4) notation x |_ₗ U ⟪e⟫ for TopCat.Presheaf.restrict, and hence a syntax error in line 125 of Topology/Sheaves/Presheaf.lean:

  x |_ₗ U ⟪e⟫
        -- ^ unexpected token '⟫'; expected ','

These two notations are simultaneously in effect thanks to the import links shown below, where the thick red link is new, needed for the EuclideanSpace in the definition of sphere and disk.

20240909_import_links_annotated.png

I tried making the Lean-3-style notation ⟪x, y⟫_𝕜 local, but this leads to more errors and I'm reluctant to modify existing code unrelated to CW-complexes.

(There is also a conflict in Topology/Category/TopCat/Limits/Basic.lean where the tactic by continuity presumably gets overwhelmed by newly imported lemmas. This can be fixed by using the lemma continuous_const instead of the tactic.)

Could anyone help us decide the best way to resolve these conflicts? Thank you!

[Kyle Miller]

I'm not sure what the issue is, but just FYI notation3 incidentally has a 3, and it does not have any relationship to Lean 3 anymore. For simple notations like these, notation and notation3 are the same, except notation3 creates better pretty printers. (I'm hoping to see this functionality incorporated into notation at some point.)

[Kyle Miller]

Here's a #mwe of the parsing conflict:

import Mathlib.Util.Notation3

def foo (x y z : Nat) : Nat := x + y + z

notation:max "⟪" x ", " y "⟫_" 𝕜:max => foo x y 𝕜
notation:80 x " |_ₗ " U " ⟪" e "⟫ " => foo x U e

#check 1 |_ₗ 2 ⟪ 3 ⟫
                --^ unexpected token '⟫'; expected ','

[Kyle Miller]

Changing the first :max on the first notation to :lead seems to fix it. This means "almost highest precedence, but can't be used as a function argument without parentheses". The highest defined precedences in order go lead, arg, max.

[Kyle Miller]

I'm not sure why this works though! I believe the only thing that would break is that you need to write f (⟪v,w⟫_k) instead of f ⟪v,w⟫_k.

[Kim Morrison]

Oof, we really need a test file with import Mathlib that exercises all the notation, and somehow in CI enforce that people who add new notation exercise that notation in the test file!

[Kim Morrison]

(The full compatibility of Mathlib with itself is a big deal, and a distinguishing feature from "libraries" in other languages.)

[Kim Morrison]

Is there some way we could allow people to register notation examples at the same time they set up the notation, and then we replay all registered examples with import Mathlib? (And some scheme for requiring that at least one such example is registered for every new notation?)

[Damiano Testa]

Maybe we can use a mechanism similar to the one for assert_not_exists, where there is a global check at the end, and something stored in an environment extension.

[Daniel Weber]

How long does parsing all of Mathlib take?

[Damiano Testa]

E.g. there could be a linter that warns on notation (and maybe also infix,...) that does not have a corresponding gadget that records its use and then a final check that the usages are compatible.

[Damiano Testa]

Daniel Weber said:

How long does parsing all of Mathlib take?

Parsing mathlib is probably not much faster than building it, since a lot of mathlib requires elaboration for correct parsing.

[Daniel Weber]

Do we actually need to check examples? Is it possible to directly check if there's ambiguous notation?

[Damiano Testa]

How do you check for ambiguous notation?

[Damiano Testa]

As for parsing time, maybe I retract a little what I said: you certainly need some elaboration, but byAsSorry may be enough for most notation purposes.

[Daniel Weber]

Damiano Testa said:

How do you check for ambiguous notation?

I don't know the details of the parser, but maybe it's possible to mathematically check for it

[Daniel Weber]

Although I see that checking if a CFG is ambiguous is undecidable, so that's probably not possible

[Jiazhen Xia]

If we were writing a math book we could just say at the beginning of a section that ⟪ ⟫ in this section means "restriction of a section of a presheaf" rather than "inner product". Or we could temporarily change the notation for one of the concepts if both concepts are needed in the same section. Maybe we could hope to see such features in a future version of Lean?

[Damiano Testa]

I think that this is what scoped is supposed to achieve, at least to some extent.

[Damiano Testa]

Maybe a low-key solution is to lint against non-scoped notation, so that "global" notation comes with the need of adding a set_option reminder before it.

[Damiano Testa]

I'm just not sure whether there is more notation that is expected to be global or more that is expected to be local.

[Damiano Testa]

Here is a link to a similar discussion.

[Jiazhen Xia]

Kyle Miller said:

Changing the first :max on the first notation to :lead seems to fix it. This means "almost highest precedence, but can't be used as a function argument without parentheses". The highest defined precedences in order go lead, arg, max.

Thanks! Lowering the precedence indeed works, and it involves adding parentheses to about 10 occurrences of ⟪x, y⟫_𝕜 in mathlib that are function arguments.

[Jiazhen Xia]

Thanks for all the ideas. I've implemented two solutions to resolve the conflict between ⟪x, y⟫_𝕜 and x |_ₗ U ⟪e⟫.

The first solution is to lower the precedence of ⟪x, y⟫_𝕜 and then add parentheses where necessary.

The second solution is to make ⟪x, y⟫_𝕜 a scoped notation within InnerProductSpace and then add open scoped InnerProductSpace wherever the notation is used.

Which one is better?

[Matthew Ballard]

Can we not create the new import?

[Jiazhen Xia]

That's also possible. As a third solution, we can place the new definitions (sphere and disk) in a new file (called Topology/Category/TopCat/Objects.lean or something).

[Matthew Ballard]

I think you will get notation collision no matter the choice (and that should be fixed) but I don't think basic files about the category of topological spaces need to know about inner products.

[Jiazhen Xia]

Matthew Ballard said:

I don't think basic files about the category of topological spaces need to know about inner products.

I think this point is partially addressed by my second solution, where ⟪x, y⟫_𝕜 becomes scoped within the InnerProductSpace namespace. In this way, although the inner product notation ⟪x, y⟫_𝕜 is imported into TopCat/Basic.lean, it is hidden ("not known") unless you explicitly open InnerProductSpace.

[Jiazhen Xia]

I opened PR #16672 making the inner product notation scoped.