Namespacing a synonym lemma under a prefix

Stream: lean4

[Yakov Pechersky]

For mathlib4 porting, we sometimes have lemmas under similar names yet namespaced. Here is a mwe of an error of recursion that is occurring, where Left.foo sees foo as referring to itself:

theorem foo : 1 = 1 := rfl

theorem Left.foo : 1 = 1 :=
  foo

This is on leanprover/lean4:nightly-2022-10-12

[Scott Morrison]

This may just be a change in behaviour in Lean 4 that we have to cope with while porting.

[Scott Morrison]

It is a bit annoying to have to write _root_.foo here.

[Gabriel Ebner]

Yes, the change is intentional. Although I don't remember exactly who asked for it or why.

[François G. Dorais]

It's a result of the implementation. In Lean 4, the snippet is shorthand for:

theorem foo : 1 = 1 := rfl

namespace Left
theorem foo : 1 = 1 :=
  foo
end Left

The two alternatives are using _root_ (or whatever overarching namespace):

theorem foo : 1 = 1 := rfl

theorem Left.foo : 1 = 1 :=
  _root_.foo

or using protect:

theorem foo : 1 = 1 := rfl

protected theorem Left.foo : 1 = 1 :=
  foo

IMHO, the latter usually makes more sense.

[Leonardo de Moura]

Gabriel Ebner said:

Yes, the change is intentional. Although I don't remember exactly who asked for it or why.

@Reid Barton It was you, right? when you visited MSR :big_smile:
I may be mistaken, but I have vivid memories of you and Daniel championing this feature.
I have to say I now love this feature.

[Reid Barton]

Hmm, I actually don't remember that, but I am happy to take credit for it anyways