dot notation not working with top

Stream: general

[Bernd Losert]

I have the following:

import tactic
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top

variable a : Type*

class convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)

open convergence_space

instance : has_top (convergence_space a) := {
  top := {
    converges := fun l x, l <= pure x,
  }
}

def discrete_convergence_space (a : Type*) : convergence_space a := {
  converges := fun l x, top.converges l x,
}

but I get an error error: invalid field notation, type is not of the form (C ...) where C is a constant. Even if I write converges top l x, I still get an error. In order to pacify Lean I have to write @converges a top l x. What is the problem here? Is it because top is not a "constant"?

[Johan Commelin]

Does it work if you write (⊤ : convergence_space a).converges?

[Johan Commelin]

Aah, (foo : convergence_space a) is not an explicit argument of convergence_space.convergence (You can #check it to see the type signature). So it will not work.

[Bernd Losert]

If I switch to a structure, then converges top l x works.

[Bernd Losert]

But top.converges still doesn't work.

[Adam Topaz]

Lean has no way of knowing the type of top just by itself

[Adam Topaz]

Many types have a has_top instance. Even better, in you case convergence_space A has a has_top instance for every A, so how should lean know what A is if you only write top.converges?

[Adam Topaz]

The reason converges top l x works is because lean is able to infer A from l and/or x.

[Bernd Losert]

Isn't top.converges l x just sugar for converges top l x though?

[Bernd Losert]

In my mind, they should behave the same since it's just syntax sugar.

[Adam Topaz]

import tactic
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top

variable a : Type*

class convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)

open convergence_space

instance : has_top (convergence_space a) := {
  top := {
    converges := fun l x, l <= pure x,
  }
}

def discrete_convergence_space (a : Type*) : convergence_space a := {
  converges := fun l x, by letI : convergence_space a := ⊤; exact converges l x,
}

[Adam Topaz]

Take a look at the type of converges by using #check converges

[Bernd Losert]

I'm using structure convergence_space now and #check says converges : convergence_space ?M_1 → filter ?M_1 → ?M_1 → Prop.

[Johan Commelin]

Bernd Losert said:

Isn't top.converges l x just sugar for converges top l x though?

Too a first approximation X.converges l x is sugar for <the type of X>.converges X l x. (In fact, X doesn't need to be the first explicit argument, in general.)

[Johan Commelin]

So Lean needs to know the type of X before it can find the right declaration.

[Johan Commelin]

If you have definitions foo.quux and bar.quux, and you write X.quux, what does it mean? It depends on the type of X...

[Johan Commelin]

In theory, Lean cannot use l and x to figure this out, because it doesn't yet know to which declaration it is feeding them.

[Bernd Losert]

I guess this is another gotcha that I have to keep in mind. Thanks guys.