dot notation

Stream: mathlib4

[Kenny Lau]

Should Polynomial.irreducible_X be Polynomial.Irreducible.X?

(the statement is Irreducible Polynomial.X)

[Jireh Loreaux]

How does that allow for dot notation?

[Kenny Lau]

presumably if you open Polynomial and your expected type is Irreducible X then you can just type .X

[Kenny Lau]

i suppose this is actually not very relevant because we don't have "stacked irreducible proofs"

[Jireh Loreaux]

Does that actually work?

[Kenny Lau]

it was more like for the Factors PR #30212 where if you have enough dot notations then you can prove Factors (3 * (X - 1) * (X - 4)) with .mul (.mul .ofNat .x_sub_one) .x_sub_ofNat

[Kenny Lau]

Jireh Loreaux said:

Does that actually work?

import Mathlib

open Polynomial

theorem Polynomial.Irreducible.X : Irreducible (X : ℤ[X]) :=
  irreducible_X

example : Irreducible (X : ℤ[X]) := .X

[Jireh Loreaux]

aha, I didn't realize anonymous dot notation respects open namespaces. Interesting.

[Kenny Lau]

it's a feature-bug

[Kenny Lau]

there are a few inconsistencies in its behaviour that is a bit annoying to me

[Jireh Loreaux]

Well, is it intended to be a feature, or is it actually a bug? Maybe you should ask about that in #lean4

[Aaron Liu]

there was a zulip thread about this

[Aaron Liu]

and I think there was also another one

[Kenny Lau]

@Jireh Loreaux I actually posted twice:

• #lean4 > dot notation and open
• #lean4 > open is confused

[Kyle Miller]

Kenny Lau said:

it's a feature-bug

It's a feature-feature (though if it causes big problems we'll reconsider)

[Kenny Lau]

well it isn't completely consistent

[Kenny Lau]

namely, it doesn't work with _root_

[Kenny Lau]

MWE:

axiom A.d : Nat → Nat

theorem A.bar : d 0 = d 0 := rfl

namespace C

theorem _root_.A.foo : d 0 = d 0 := rfl

end C

[Kyle Miller]

Right, that's the sort of thing discussed in the "dot notation and open" thread you discussed, if I remember correctly. There's still some work to do.

[Kenny Lau]

i thought i brought it up but i couldn't find it in the two threads I posted; should I just post again?

[Kyle Miller]

I'll just add a link to this thread for future reference, for the next time I get a chance to look at these name resolution issues.