Problem inferring usage of inf_le_left

Stream: mathlib4

[Bernd Losert]

I have this code:

import Mathlib.Order.Filter.Ultrafilter
import Mathlib.Algebra.Support
import Mathlib.Order.Filter.Lift
import Mathlib.Tactic.Continuity

set_option autoImplicit true

noncomputable section

open Set Filter

@[ext]
class ConvergenceSpace (α : Type*) where
  converges : Filter α → α → Prop
  pure_converges : ∀ x, converges (pure x) x
  le_converges : ∀ {F G}, F ≤ G → ∀ {x}, converges G x → converges F x

open ConvergenceSpace

@[simp]
instance : LE (ConvergenceSpace α) where
  le p q := sorry

instance : CompleteLattice (ConvergenceSpace α) := sorry

def continuousAt [ConvergenceSpace α] [ConvergenceSpace β] (f : α → β) (x : α) :=
∀ ⦃F⦄, converges F x → converges (map f F) (f x)

def continuous [ConvergenceSpace α] [ConvergenceSpace β] (f : α → β) : Prop :=
∀ ⦃x⦄, continuousAt f x

def continuous_ (p : ConvergenceSpace α) (q : ConvergenceSpace β)
  (f : α → β) : Prop :=
@continuous α β p q f

lemma continuous_le_dom {p p' : ConvergenceSpace α} {q : ConvergenceSpace β}
  {f : α → β} (hle : p' ≤ p) (hcont : continuous_ p q f) :
  continuous_ p' q f := sorry

lemma continuous_inf_dom_left {p p' : ConvergenceSpace α}
  {q : ConvergenceSpace β} {f : α → β} :
  continuous_ p q f → continuous_ (p ⊓ p') q f := by
intros hcont
exact continuous_le_dom inf_le_left hcont -- THIS PART IS COMPLANING

For some reason, inf_le_left doesn't work as written - I have to qualify it with using @inf_le_left. The Lean 3 version of this code was working without having to use @inf_le_left, so I am scratching my head wondering what happened. Help.

[Eric Wieser]

docs#inf_le_left, docs3#inf_le_left

[Kevin Buzzard]

instance : LE (ConvergenceSpace α) where
  le p q := sorry

instance : CompleteLattice (ConvergenceSpace α) := sorry

This is a diamond, right? If you filled in the sorries, does your problem still exist?

[Kevin Buzzard]

The error (which you could have posted, rather than just saying that Lean is complaining) is

application type mismatch
  continuous_le_dom inf_le_left
argument
  inf_le_left
has type
  @LE.le (ConvergenceSpace α) Preorder.toLE (p ⊓ p') p : Prop
but is expected to have type
  @LE.le (ConvergenceSpace α) instLEConvergenceSpace (p ⊓ p') p : Prop

which just says "you have defined two different <='s on the same object"

[Kevin Buzzard]

Just removing the LE instance makes the code compile.

[Bernd Losert]

In the real code, I have instances for basically every every lattice related class.

[Bernd Losert]

I can't remove the LE instance because that's where I am defining what <= means. The CompleteLattice instance should be making use of this instance. I'm not defining another one.

[Kevin Buzzard]

If my understanding is correct then CompleteLattice does not require LE, it extends LE, so I believe your claim that the complete lattice instance should be making use of the LE instance is false. If however your two definitions of LE coincide then the problem will go away. In your example above, they don't.

[Kevin Buzzard]

docs#CompleteLattice

[Kevin Buzzard]

Huh, I literally cannot see the definition in the docs on mobile because of some scrolling issue so I can't check if what I'm claiming above is true

[Sky Wilshaw]

One bit of the hierarchy is CompleteLattice > Lattice > SemilatticeSup > PartialOrder > Preorder > LE, where > denotes extends.

[Sky Wilshaw]

So indeed CompleteLattice transitively extends LE.

[Eric Wieser]

Kevin's initial point is that the act of using sorry to turn your code into a mwe is actually the cause of the problem

[Eric Wieser]

Perhaps the problem exists in your sorry-free code too, but the mwe you posted doesn't represent that any more (and so we need a new one without the sorrys)

[Eric Wieser]

In general you can almost always replace proofs with sorries when making a mwe, but replacing data with sorries often ruins things

[Kevin Buzzard]

Yes, that code would not work in lean 3 either.

[Bernd Losert]

OK, here is the code: https://gist.github.com/berndlosert/c04746c0b552b7cd5f620f2152e3edad. I tried making a MWE but it didn't have problem I am experiencing with the full code.

[Eric Wieser]

Your problem is

instance : LE (ConvergenceSpace α) where
  le p q := ∀ {F x}, converges_ p F x → converges_ q F x

[Eric Wieser]

Without the @, lean is filling the F and x arguments

[Eric Wieser]

You want

instance : LE (ConvergenceSpace α) where
  le p q := ∀ {{F x}}, converges_ p F x → converges_ q F x

[Eric Wieser]

(or the unicode for that)

[Bernd Losert]

Oh really? Wow, I would have never guessed that.

[Bernd Losert]

So {{ }} prevents lean from autoinfering those arguments? I don't remember.

[Bernd Losert]

Using {{ }} breaks some of the intros where I declare F x.

[Sky Wilshaw]

The {{ }} brackets mean that the implicit arguments will be filled only when the next argument is filled. Normal { } brackets fill the implicit arguments immediately.

def foo {α : Type _} : α → α := id
def bar ⦃α : Type _⦄ : α → α := id

#reduce foo -- fun a => a
#reduce bar -- fun ⦃α⦄ a => a

In the second example, using bar doesn't immediately try to fill in the value of α, but will only do so when given an argument.

[Bernd Losert]

The mechanics still baffles me. Suppose I have

p ≤ q := ∀ {{F x}}, converges_ p F x → converges_ q F x
p ≤' q := ∀ {F x}, converges_ p F x → converges_ q F x

and I am in a context with

hle : p ≤ q
hle': p ≤' q
hconv : converges_ p F x

How doeshle hconv differ from hle' hconv?

[Sky Wilshaw]

I don't think there should be any difference. If there's a problem, can you make a #mwe ?

def p : Type → Prop := sorry
def q : Type → Prop := sorry

def le : ∀ {α : Type}, p α → q α := sorry
def le' : ∀ ⦃α : Type⦄, p α → q α := sorry

example {α : Type} (h : p α) : le h = le' h := rfl -- type checks

[Bernd Losert]

Well, there is a difference because I was just told to use {{ }} instead.

[Sky Wilshaw]

Sky Wilshaw said:

The {{ }} brackets mean that the implicit arguments will be filled only when the next argument is filled. Normal { } brackets fill the implicit arguments immediately.

The difference is only before you fill in any arguments. Once you supply hconv to hle or hle', everything behaves the same.

[Sky Wilshaw]

The reason {{ }} is better here is because you will never end up with a context in which

hle' : ∀ {F x}, converges_ p F x → converges_ q F x

This is because Lean will fill in the F and x arguments for you, so you'll be left with a context of the form

hle' : converges_ p ? ? → converges_ q ? ?

[Bernd Losert]

That's what I though too, but it still complains like in this example:
Screenshot-2023-09-30-at-12.37.38.png

[Bernd Losert]

In order to fix that problem, I have to use @hle F x and @hle' F x.

[Sky Wilshaw]

In that case, it might be easier to just make the arguments explicit, or make a lemma converges_of_le that turns the {{ }} brackets into { } ones (i.e. filling the first two arguments). I think that using hle to mean two things (converges implies converges for all F and x, and converges implies converges for a particular F and x) is not good practice.

[Bernd Losert]

Yes, I'm also thinking of just making the arguments explicit to avoid all these problems.

[Bernd Losert]

Thank you everyone for your help.

[Bernd Losert]

One last question: It seems that the behavior with implicit arguments changed from Lean 3 to Lean 4 because I did not have these problems in the Lean 3 version of this code. Is this change in behavior documented somewhere?

[Sky Wilshaw]

Lean 3 and Lean 4 both had the same system for handling implicit arguments, but there might have been a difference in the way LE is elaborated.

[Sky Wilshaw]

It might not even have been LE, there are a few things in the code that could have subtly changed.

[Bernd Losert]

I see. Would mathport have caught this kind of problem and automagically fixed them?

[Kevin Buzzard]

I guess you could try and find out, but certainly in general mathport output would not compile and sometimes a large amount of work needed to be done to fix it. This is why the port of a million lines of code took 8 months.