Dot notation with dots

Stream: lean4

[David Ang]

In Lean 3, we used to be able to do A^.B.C (e.g. if B.C is a field of a structure where A is a term of). Is it possible make it work now too?

[Henrik Böving]

just do A.C

[Kyle Miller]

Does that work with extended field notation in general? Sometimes you have a structure A and you have def A.B.C := ..., and for a : A you could write a^.B.C

[Kyle Miller]

@David Ang Could you give a MWE of what you want to do to ground this discussion?

[David Ang]

I’m on my phone right now but something like this is possible:

structure foo := (unfoo : \N)
variable (n : foo)
def foo.bar.unbar : \N := n.unfoo

I want to write n.bar.unbar, which I can’t, but in Lean 3 I can do n^.bar.unbar.

[Kevin Buzzard]

Wait -- so the (deprecated AFAIK) ^ notation in Lean 3 had a use?

[Eric Rodriguez]

It was common with ideal.quotient iirc

[David Ang]

It’s going to be very useful for me e.g. Weierstrass.Affine/Projective/Jacobian.(a lot of things) and Weierstrass.CoordinateRing.(a lot of things)

[Kevin Buzzard]

David Ang said:

I’m on my phone right now but something like this is possible:

structure foo := (unfoo : \N)
variable (n : foo)
def foo.bar.unbar : \N := n.unfoo

I want to write n.bar.unbar, which I can’t, but in Lean 3 I can do n^.bar.unbar.

oh wow that is indeed the case.

[James Gallicchio]

not really a solution, but you can replicate the behavior via something like

abbrev foo.Bar := foo
def foo.bar (n : foo) : foo.Bar := foo
def foo.Bar.unbar (n : foo.Bar) := n.unfoo

if the only goal is to organize theorems on foos into a hierarchy.

We could make a macro like namespace_def to automate this somewhat. but it would be cool to have something like this built into Lean4, where you could declare "sub-namespaces" that become disallowed as an identifier in that namespace but the namespace algorithm allows it as an intermediary in dot notation.

namespace_def foo.bar

def foo.bar.unbar ...

[James Gallicchio]

but i'm wondering if you can't accomplish the same end result just prefixing names with bar_ or whatever. the namespace search should prioritize those that start with bar_ when you type it out.

[David Ang]

James Gallicchio said:

not really a solution, but you can replicate the behavior via something like

abbrev foo.Bar := foo
def foo.bar (n : foo) : foo.Bar := foo
def foo.Bar.unbar (n : foo.Bar) := n.unfoo

if the only goal is to organize theorems on foos into a hierarchy.

Sorry I just saw this, but your code doesn’t seem to compile for me. Yes I really just want to organise the different defs and lemmas into separate namespaces. They happen to have rather long names so I prefer not to use underscores.

[David Ang]

In fact, it would be great if I could do something like n.unbar (or n^.unbar?) for n : foo provided I'm in the foo.bar namespace. Are there any tricks around this? Essentially I have tens of defs and lemmas with the same name but under different namespaces.

[David Ang]

Ah... I think I get you now, and it's pretty much what I'm looking for - thanks!