## 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?

It's not a bug.

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

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.

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?

It's prop valued

So?

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

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

I'm confused

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

Oh duh

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

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: Aug 03 2023 at 10:10 UTC