# Zulip Chat Archive

## Stream: general

### Topic: inconsistent ambiguous overload

#### Bernd Losert (Dec 17 2021 at 23:37):

I have this code:

```
import tactic
import order.filter.partial
noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top has_mem
variable {a : Type*}
structure convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)
(pure_converges : forall x, converges (pure x) x)
(le_converges : forall {l l'}, l <= l' -> forall {x}, converges l' x -> converges l x) -- l <= l' means l' ⊆ l
attribute [ext] convergence_space
attribute [class] convergence_space
def converges [p : convergence_space a] (l : filter a) (x : a) : Prop :=
p.converges l x
open convergence_space
def is_open [convergence_space a] (s : set a) : Prop :=
forall {l} {x}, mem x s -> converges l x -> mem s l
def is_closed [convergence_space a] (s : set a) : Prop :=
forall {l} {x}, mem s l -> converges l x -> mem x s
```

For some reason, Lean is confused about the `converges l x`

in the definition of `is_closed`

. Why does it work with `is_open`

and not with `is_closed`

?

#### Adam Topaz (Dec 17 2021 at 23:44):

You have a typo in the last line

#### Adam Topaz (Dec 17 2021 at 23:44):

`mem s l`

should be `mem x s`

#### Adam Topaz (Dec 17 2021 at 23:45):

well, at least that's why one works and not the other

#### Yaël Dillies (Dec 17 2021 at 23:45):

Why would that be typo?

#### Yaël Dillies (Dec 17 2021 at 23:45):

I suspect this is a unification problem, given that changing the implication order fixes it. Try giving the types of `l`

and `x`

explicitly.

#### Adam Topaz (Dec 17 2021 at 23:46):

I was just commenting on why `is_open`

works but not the other.... I don't actually know what the mathematical content is

#### Adam Topaz (Dec 17 2021 at 23:46):

typo wasn't the right word, I guess.

#### Adam Topaz (Dec 17 2021 at 23:47):

I don't know why you're so against using unicode @Bernd Losert ... it makes your code very hard to read.

#### Bernd Losert (Dec 17 2021 at 23:49):

Yaël Dillies said:

I suspect this is a unification problem, given that changing the implication order fixes it. Try giving the types of

`l`

and`x`

explicitly.

Didn't help.

#### Adam Topaz (Dec 17 2021 at 23:49):

This

```
def is_closed [convergence_space a] (s : set a) : Prop :=
forall {l : filter a} {x}, mem s l -> converges l x -> mem x s
```

works for me...

#### Bernd Losert (Dec 17 2021 at 23:50):

Oops. I did it for `is_open`

instead of `is_closed`

. Yep, it helps.

#### Bernd Losert (Dec 17 2021 at 23:51):

Could this be a bug?

#### Adam Topaz (Dec 17 2021 at 23:51):

It's not a bug.

#### Bernd Losert (Dec 17 2021 at 23:51):

Adam Topaz said:

I don't know why you're so against using unicode Bernd Losert ... it makes your code very hard to read.

Nothing against Unicode. I'm just working with a crappy font inside a VM from the shell, so no fancy Unicode for me for now.

#### Adam Topaz (Dec 17 2021 at 23:52):

Do you not want to install lean on your own machine?

#### Adam Topaz (Dec 17 2021 at 23:52):

We're fairly honest people :smiling_devil:

#### Bernd Losert (Dec 17 2021 at 23:52):

This machine isn't mine. I will be ditching it soon.

#### Adam Topaz (Dec 17 2021 at 23:53):

Ah ok, fair enough.

#### Bernd Losert (Dec 17 2021 at 23:53):

Hmm... I guess we have another one of those gotchas. The number of gotchas seems to be increasing every day.

#### Adam Topaz (Dec 17 2021 at 23:54):

In any case, it's not a bug because when you write `mem s l`

without specifying what `l`

should be, then lean has no way of telling the type of `l`

. In the `is_open`

case, the first place where `l`

appears is in `converges`

, and then lean knows that it has to be a filter. In the `is_closed`

case, there are many options, since `mem s l`

is the first thing that lean finds.

#### Adam Topaz (Dec 17 2021 at 23:55):

In general, the error messages should be relatively helpful, so, in time, you will be able to know how to work around these "gotchas".

#### Bernd Losert (Dec 17 2021 at 23:55):

I see. I guess it could be smarter by looking at the entire type instead of the first thing only.

#### Bernd Losert (Dec 17 2021 at 23:56):

I think I'll just stick to writing `[p : convergence_space a]`

and `p.converges`

.

#### Kevin Buzzard (Dec 17 2021 at 23:56):

The number of gotchas seems to be increasing every day.

I don't know if they're so much "gotchas" as simply the fact that lean has a pretty steep learning curve. I would urge you to start trying to understand the error messages you're seeing. They often tell you what's wrong, once you understand what they're saying. (Oh Adam beat me to it :-) )

#### Bernd Losert (Dec 17 2021 at 23:57):

I understood the error message. I was just wondering why it worked in the `is_open`

case but not in the `is_closed`

case.

#### Bernd Losert (Dec 17 2021 at 23:59):

The "gotchas" are part of the steep learning curve it seems.

#### Adam Topaz (Dec 17 2021 at 23:59):

Writing `p.converges`

is not the solution

#### Bernd Losert (Dec 18 2021 at 00:01):

I've been using that so far without issues. Before I was doing `@converges a p`

.

#### Adam Topaz (Dec 18 2021 at 00:01):

That would be like writing `e.to_has_mul.mul x y`

for `e : group G`

instead of just `x * y`

.

#### Bernd Losert (Dec 18 2021 at 00:02):

If I had a nice notation for `converges`

, I would agree.

#### Bernd Losert (Dec 18 2021 at 00:03):

The `p.converges`

actually reads better. In the literature, you find `F p-converges to x`

, so it is similar.

#### Adam Topaz (Dec 18 2021 at 00:04):

Okay, but you wouldn't write `U is-t-open in X`

for a set `X`

with a topology `t`

, rather you would just say `U is open in X`

.

#### Adam Topaz (Dec 18 2021 at 00:04):

If you always want to refer to `p`

, then `convergence_space`

should be just a structure, and not a class.

#### Bernd Losert (Dec 18 2021 at 00:05):

Yep. In the literature on convergence spaces, you also see `F converges to x in (X,p)`

.

#### Kevin Buzzard (Dec 18 2021 at 00:06):

The trick is not to stick to the literature, the trick is to learn how to write idiomatic lean code

#### Kevin Buzzard (Dec 18 2021 at 00:06):

We're rewriting the literature

#### Bernd Losert (Dec 18 2021 at 00:06):

I didn't want to refer to `p`

at all, but it caused so many issues that using it is better now.

#### Adam Topaz (Dec 18 2021 at 00:07):

Can you give me an example where it's an issue?

#### Kevin Buzzard (Dec 18 2021 at 00:07):

Remember "I can't make it work" is very different to "it can't be made to work"

#### Bernd Losert (Dec 18 2021 at 00:07):

In almost all the proofs I've written, I would get error messages saying "cannot instantiate type class instance" or something like that.

#### Bernd Losert (Dec 18 2021 at 00:08):

I made the error go away by using `@converges`

and then I switched to using `p.converges`

.

#### Adam Topaz (Dec 18 2021 at 00:09):

Bernd Losert said:

In almost all the proofs I've written, I would get error messages saying "cannot instantiate type class instance" or something like that.

This is just lean telling you that you didn't specify a convergence space structure to use, so it has no way of knowing what to do.

#### Bernd Losert (Dec 18 2021 at 00:10):

Yes. That's what it is, so I have to specify it and things are much better now after doing so.

#### Adam Topaz (Dec 18 2021 at 00:10):

```
example (G : Type*) (x y : G) : x * y := sorry
```

gives an error because I didn't tell lean what `has_mul G`

to use.

#### Bernd Losert (Dec 18 2021 at 00:11):

Yep.

#### Bernd Losert (Dec 18 2021 at 00:13):

There were some cases where it complained even though the instance was there. This seems to happen only in tactic mode. I suspect this is a limitation of Lean and it explains why you have things like introsI, letI, etc.

#### Adam Topaz (Dec 18 2021 at 00:14):

Yeah, when an instance is under a binder, then it can get annoying, at least in lean3. Lean4 is supposed to fix all that.

#### Yaël Dillies (Dec 18 2021 at 00:15):

That also seems to come from you putting stuff to the right of the colon while it could have been to the left.

#### Bernd Losert (Dec 18 2021 at 00:15):

Nah. That was unrelated.

#### Adam Topaz (Dec 18 2021 at 00:17):

Again, an example would be helpful.

#### Bernd Losert (Dec 18 2021 at 00:18):

Let me try the partial_order proof. I think that one was troublesome.

#### Adam Topaz (Dec 18 2021 at 00:21):

That's a different story, because when you're talking about the poset of convergence space structures, you need to speak about more than one such structure, so typeclasses don't help here. I suggest looking at the code for the lattice of topologies that we have in mathlib

#### Bernd Losert (Dec 18 2021 at 00:26):

Nope. It wasn't that one. It was this:

```
import tactic
import order.filter.partial
noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top has_mem
variables {a b : Type*}
structure convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)
(pure_converges : forall x, converges (pure x) x)
(le_converges : forall {l l'}, l <= l' -> forall {x}, converges l' x -> converges l x) -- l <= l' means l' ⊆ l
attribute [ext] convergence_space
attribute [class] convergence_space
open convergence_space
def convergence_space.induced (f : a -> b) [convergence_space b] : convergence_space a := {
converges := fun l x, converges (map f l) (f x),
pure_converges := by simp [filter.map_pure, pure_converges],
le_converges := begin
assume l l' : filter a,
assume le1 : l <= l',
assume x : a,
assume h : converges (map f l') (f x),
have le2 : map f l <= map f l', apply map_mono le1,
apply le_converges le2 h,
end,
}
```

#### Adam Topaz (Dec 18 2021 at 00:28):

fixed

```
import tactic
import order.filter.partial
noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top has_mem
variables {a b : Type*}
class convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)
(pure_converges : forall x, converges (pure x) x)
(le_converges : forall {l l'}, l <= l' -> forall {x}, converges l' x -> converges l x) -- l <= l' means l' ⊆ l
attribute [ext] convergence_space
open convergence_space
def convergence_space.induced (f : a -> b) [convergence_space b] : convergence_space a := {
converges := fun l x, converges (map f l) (f x),
pure_converges := by simp [filter.map_pure, pure_converges],
le_converges := begin
assume l l' : filter a,
assume le1 : l <= l',
assume x : a,
assume h : converges (map f l') (f x),
have le2 : map f l <= map f l', apply map_mono le1,
apply le_converges le2 h,
end,
}
```

#### Bernd Losert (Dec 18 2021 at 00:29):

Sure, using `class`

fixes it, but then in the proof of `partial_order`

I have to resort to using `@converges`

.

#### Bernd Losert (Dec 18 2021 at 00:29):

So it's a trade off.

#### Adam Topaz (Dec 18 2021 at 00:30):

The point is that you will only prove a partial order once, but you want to use a convergence space structure many many times without referring to it explicitly. So you need to decide which tradeoff is less painful, and I claim that using `class convergence_space ...`

is the right way to go.

#### Adam Topaz (Dec 18 2021 at 00:31):

Or, you could be a bit more careful with your variables.

#### Bernd Losert (Dec 18 2021 at 00:32):

You may be right. I'll need to flesh out more code and see what happens.

#### Adam Topaz (Dec 18 2021 at 00:34):

The issue with your code here is that `convergence_space.converges`

has an explicit first variable of type `convergence_space a`

.

#### Adam Topaz (Dec 18 2021 at 00:35):

E.g. the following works

```
import tactic
import order.filter.partial
noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top has_mem
variables {a b : Type*}
structure convergence_space (a : Type*) :=
(converges' : filter a -> a -> Prop)
(pure_converges : forall x, converges' (pure x) x)
(le_converges : forall {l l'}, l <= l' -> forall {x}, converges' l' x -> converges' l x) -- l <= l' means l' ⊆ l
attribute [class, ext] convergence_space
open convergence_space
lemma converges (a : Type*) [convergence_space a] (f : filter a) (x : a) : Prop :=
converges' ‹_› f x
def convergence_space.induced (f : a -> b) [convergence_space b] : convergence_space a := {
converges := fun l x, converges (map f l) (f x),
pure_converges := by simp [filter.map_pure, pure_converges],
le_converges := begin
assume l l' : filter a,
assume le1 : l <= l',
assume x : a,
assume h : converges (map f l') (f x),
have le2 : map f l <= map f l', apply map_mono le1,
apply le_converges le2 h,
end,
}
```

#### Yaël Dillies (Dec 18 2021 at 00:35):

Uh, `converges`

should be a `def`

, right?

#### Adam Topaz (Dec 18 2021 at 00:36):

It's prop valued

#### Yaël Dillies (Dec 18 2021 at 00:36):

So?

#### Yaël Dillies (Dec 18 2021 at 00:36):

It's Prop-valued, but it's not a Prop.

#### Adam Topaz (Dec 18 2021 at 00:37):

I'm confused

#### Adam Topaz (Dec 18 2021 at 00:37):

A prop is a prop

#### Yaël Dillies (Dec 18 2021 at 00:37):

But `Prop`

is not a Prop.

#### Yaël Dillies (Dec 18 2021 at 00:37):

It's a `Type 0`

#### Adam Topaz (Dec 18 2021 at 00:37):

Oh duh

#### Adam Topaz (Dec 18 2021 at 00:37):

Sorry

#### Bernd Losert (Dec 18 2021 at 00:37):

It should be a def.

#### Adam Topaz (Dec 18 2021 at 00:38):

Yeah you're right

#### Bernd Losert (Dec 18 2021 at 00:38):

That's what it was in my first post.

#### Mario Carneiro (Dec 18 2021 at 00:39):

What's this partial order structure example? I'm not sure about all the context but `convergence_space`

should definitely be a class

#### Bernd Losert (Dec 18 2021 at 00:39):

One sec...

#### Adam Topaz (Dec 18 2021 at 00:41):

Mario, I think it's given by implication on converges

#### Bernd Losert (Dec 18 2021 at 00:41):

This is what I have now:

```
import tactic
import order.filter.partial
noncomputable theory
open set filter classical
open_locale classical filter
open has_sup has_top has_mem
variables {a b : Type*}
structure convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)
(pure_converges : forall x, converges (pure x) x)
(le_converges : forall {l l'}, l <= l' -> forall {x}, converges l' x -> converges l x) -- l <= l' means l' ⊆ l
attribute [ext] convergence_space
attribute [class] convergence_space
open convergence_space
instance : has_le (convergence_space a) := {
le := fun p q, forall {l} {x}, q.converges l x -> p.converges l x
}
instance : partial_order (convergence_space a) := {
le_refl := begin
assume p : convergence_space a,
assume l : filter a,
assume x : a,
assume h : p.converges l x,
exact h,
end,
le_trans := begin
assume p q r : convergence_space a,
assume le1 : p <= q,
assume le2 : q <= r,
assume l : filter a,
assume x : a,
assume h : r.converges l x,
exact (le1 (le2 h))
end,
le_antisymm := begin
assume p q : convergence_space a,
assume le1 : p <= q,
assume le2 : q <= p,
ext l x,
exact iff.intro le2 le1,
end,
..convergence_space.has_le
}
```

#### Bernd Losert (Dec 18 2021 at 00:44):

If I change it to `class`

, I have to write:

```
instance : has_le (convergence_space a) := {
le := fun p q, forall {l} {x}, @converges a q l x -> @converges a p l x
}
```

#### Mario Carneiro (Dec 18 2021 at 00:52):

Oh, that partial order. Yes, when dealing with the space of all convergence spaces you will need another notation to make the argument explicit. In topologies, this is done with a local notation. I would suggest something like this:

```
@[ext] class convergence_space (a : Type*) :=
(converges : filter a → a → Prop)
(pure_converges : ∀ x, converges (pure x) x)
(le_converges : ∀ {{l l'}}, l ≤ l' → ∀ {{x}}, converges l' x → converges l x) -- l <= l' means l' ⊆ l
open convergence_space
section
local notation `convs` := @converges _
instance : has_le (convergence_space a) :=
{ le := λ p q, ∀ {{l x}}, convs q l x → convs p l x }
instance : partial_order (convergence_space a) :=
{ le_refl := λ p l x h, h,
le_trans := λ p q r pq qr l x h, pq (qr h),
le_antisymm := λ p q pq qp, by ext l x; exact ⟨@qp _ _, @pq _ _⟩,
..convergence_space.has_le }
end
```

#### Mario Carneiro (Dec 18 2021 at 00:54):

Also, when writing lean you should really get used to unicode. There are lots of things that can't be worked around with ascii notation, and every lean input method I am aware of has built in abbreviation expansion

#### Bernd Losert (Dec 18 2021 at 00:57):

I see. So instead of a `structure`

with a `def converges`

, I can use `class`

with notation for `@converges`

.

#### Bernd Losert (Dec 18 2021 at 00:58):

I started using `structure`

because I was copying the topologies code by the way.

#### Adam Topaz (Dec 18 2021 at 00:59):

With docs#topological_space we have an external API and we don't really refer to the fields in the structure defining a topological space. Your case is different because you want to actually use the `converges`

field.

#### Bernd Losert (Dec 18 2021 at 01:01):

Yes. That wasn't apparent to me though when I started.

#### Bernd Losert (Dec 18 2021 at 01:01):

Anyways, thanks alot everyone. Always appreciated.

Last updated: Dec 20 2023 at 11:08 UTC