error after upgrade

Stream: general

[Bernd Losert]

I just upgrade mathlib and this lemma of mine is now broken:

lemma mem_inv_iff [has_involutive_inv α] {f : filter α} :
  ∀ s, s ∈ f⁻¹ ↔ ∃ t ∈ f, t⁻¹ ⊆ s :=

There's a red squiggly line under has_involutive_inv and the error says:

function expected at
  has_involutive_inv
term has type
  has_involutive_inv (filter ?m_1)

I don't understand what to make of this.

[Adam Topaz]

#mwe

[Bernd Losert]

Here you go:

import algebra.group.extra
import data.set.extra
import data.set.pointwise
import order.filter.basic
import order.filter.pointwise

open filter function
open_locale filter pointwise

variables {α β G M : Type*}

namespace filter

lemma mem_inv_iff [has_involutive_inv α] {f : filter α} :
  ∀ s, s ∈ f⁻¹ ↔ ∃ t ∈ f, t⁻¹ ⊆ s := sorry

end filter

[Eric Rodriguez]

_root_.has_involutive_inv

[Adam Topaz]

lemma mem_inv_iff [_root_.has_involutive_inv α] {f : filter α} :
  ∀ s, s ∈ f⁻¹ ↔ ∃ t ∈ f, t⁻¹ ⊆ s := sorry

[Adam Topaz]

It's a namespace issue

[Bernd Losert]

What's this _root_ business?

[Eric Rodriguez]

seems someone added filter.has_involutive_inv so it prioritises it... I think in these sorts of cases the instances should be named differently to avoid clashes

[Eric Rodriguez]

_root_ means go to the root namespace

[Eric Rodriguez]

docs#filter.has_involutive_inv

[Adam Topaz]

import order.filter.pointwise

#check filter.has_involutive_inv
#check has_involutive_inv

[Bernd Losert]

I don't get it. What is the root namespace. I'm inside the filter namespace.

[Adam Topaz]

The root namespace contains the stuff that was not defined inside of some namespace

[Riccardo Brasca]

_root_.foo means foo with nothing before, so not bar.foo. If you have open bar and both foo and bar.foo exist Lean gets confused.

[Bernd Losert]

Ah, I get it. Hmm... but filter.has_involutive_inv belongs to the filter namespace, not the _root_ namespace.

[Eric Rodriguez]

you want to say that you want an instance of docs#has_involutive_inv. However, the way Lean resolves names, as you have the filter namespace open, it'll prefer the term docs#filter.has_involutive_inv for the literal text has_involutive_inv, at which point it gets confused as it's not a function that takes a Type*

[Bernd Losert]

I see... I guess this is new behavior because it was working before.

[Eric Rodriguez]

the instance is new, the behaviour is old

[Bernd Losert]

Oh right. So updating mathlib brought in the new instance. Hmm... but I'm pretty sure that instance was already there though in some form.

[Eric Rodriguez]

--lemma test.decidable_eq : 123 = 123 := rfl

namespace test

example [decidable_eq ℕ] : nat := 12

end test

[Eric Rodriguez]

Bernd Losert said:

Oh right. So updating mathlib brought in the new instance. Hmm... but I'm pretty sure that instance was already there though in some form.

afaik, Yael added it fairly recently

[Bernd Losert]

Alright. I learned something new today. Thanks for the help.

[Eric Rodriguez]

#14398 should fix this. are instances protected by default?

[Adam Topaz]

@Eric Rodriguez yes I think they are

[Adam Topaz]

well, at least if they are declared as instance ...

[Bernd Losert]

I'm confused about something. filter.has_involutive_inv is not defined as an instance. It's just a regular def.

[Eric Rodriguez]

open_locale filter makes it an instance.

[Eric Rodriguez]

but only with the attribute, so it's not protected

[Bernd Losert]

Aha. OK

[Bernd Losert]

I wonder why Yael did it this way. I find it confusing.

[Yaël Dillies]

Whoops, my bad. I forgot to protect the instances I localised

[Yaël Dillies]

@Eric Rodriguez, can you check file#data/set/pointwise and file#data/finset/pointwise as well?

[Eric Rodriguez]

I'll have a look in a couple hours

[Eric Rodriguez]

all of the rest seem fine!