inconsistent ambiguous overload

Stream: general

[Bernd Losert]

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]

You have a typo in the last line

[Adam Topaz]

mem s l should be mem x s

[Adam Topaz]

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

[Yaël Dillies]

Why would that be typo?

[Yaël Dillies]

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]

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]

typo wasn't the right word, I guess.

[Adam Topaz]

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

[Bernd Losert]

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]

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]

Oops. I did it for is_open instead of is_closed. Yep, it helps.

[Bernd Losert]

Could this be a bug?

[Adam Topaz]

It's not a bug.

[Bernd Losert]

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]

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

[Adam Topaz]

We're fairly honest people :smiling_devil:

[Bernd Losert]

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

[Adam Topaz]

Ah ok, fair enough.

[Bernd Losert]

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

[Adam Topaz]

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]

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]

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

[Bernd Losert]

I think I'll just stick to writing [p : convergence_space a] and p.converges.

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

Writing p.converges is not the solution

[Bernd Losert]

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

[Adam Topaz]

That would be like writing e.to_has_mul.mul x y for e : group G instead of just x * y.

[Bernd Losert]

If I had a nice notation for converges, I would agree.

[Bernd Losert]

The p.converges actually reads better. In the literature, you find F p-converges to x, so it is similar.

[Adam Topaz]

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]

If you always want to refer to p, then convergence_space should be just a structure, and not a class.

[Bernd Losert]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

We're rewriting the literature

[Bernd Losert]

I didn't want to refer to p at all, but it caused so many issues that using it is better now.

[Adam Topaz]

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

[Kevin Buzzard]

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

[Bernd Losert]

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]

I made the error go away by using @converges and then I switched to using p.converges.

[Adam Topaz]

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]

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

[Adam Topaz]

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]

Yep.

[Bernd Losert]

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]

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]

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]

Nah. That was unrelated.

[Adam Topaz]

Again, an example would be helpful.

[Bernd Losert]

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

[Adam Topaz]

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]

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]

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]

Sure, using class fixes it, but then in the proof of partial_order I have to resort to using @converges.

[Bernd Losert]

So it's a trade off.

[Adam Topaz]

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]

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

[Bernd Losert]

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

[Adam Topaz]

The issue with your code here is that convergence_space.converges has an explicit first variable of type convergence_space a.

[Adam Topaz]

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]

Uh, converges should be a def, right?

[Adam Topaz]

It's prop valued

[Yaël Dillies]

So?

[Yaël Dillies]

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

[Adam Topaz]

I'm confused

[Adam Topaz]

A prop is a prop

[Yaël Dillies]

But Prop is not a Prop.

[Yaël Dillies]

It's a Type 0

[Adam Topaz]

Oh duh

[Adam Topaz]

Sorry

[Bernd Losert]

It should be a def.

[Adam Topaz]

Yeah you're right

[Bernd Losert]

That's what it was in my first post.

[Mario Carneiro]

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]

One sec...

[Adam Topaz]

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

[Bernd Losert]

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]

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]

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]

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]

I see. So instead of a structure with a def converges, I can use class with notation for @converges.

[Bernd Losert]

I started using structure because I was copying the topologies code by the way.

[Adam Topaz]

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]

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

[Bernd Losert]

Anyways, thanks alot everyone. Always appreciated.