type class inference sadness

Stream: new members

[Jean Lo]

Made an attempt earlier to write down the definition of a derivative in Lean:

import analysis.normed_space.basic
import analysis.normed_space.bounded_linear_maps

variables {k : Type*} [normed_field k]
variables {U : Type*} [normed_space k U]
variables {V : Type*} [normed_space k V]

def deriv_at (a : U) (f : U → V) (df : U → V)
   [normed_space k U] [normed_space k V] [is_bounded_linear_map df] :=
∃ ε : U → V, (∀ h : U, f (a + h) = f a + df h + ∥ h ∥ • ε h) ∧
  (filter.tendsto ε (nhds 0) (nhds 0))

Without the (redundant?) [normed_space k U] [normed_space k V] arguments, Lean gives up on [is_bounded_linear_map df] because it fails to synthesise the normed_space instances.

Even with those arguments the file does not compile: Lean throws maximum class-instance depth has been reached on ε and h. Trying the obvious things:

• increasing the maximum search depth didn't seem to help, up until the point the errors turn instead into deterministic timeouts.
• set_option trace.class_instances true, curiously, prints nothing, and I have yet to figure out which instances exactly Lean was looking for and failing to find.

Could someone please point at any obvious mistakes I'm making? Also, in general, what is there that I can do to coerce Lean into seeing the instances it needs?

[Kevin Buzzard]

Eew.

import analysis.normed_space.basic
import analysis.normed_space.bounded_linear_maps

variables {k : Type*} [normed_field k]
variables {U : Type*} [normed_space k U]
variables {V : Type*} [normed_space k V]

example (df : U → V)
   [is_bounded_linear_map df] : Prop := sorry -- error
/-
failed to synthesize type class instance for
U : Type u_2,
V : Type u_3,
df : U → V
⊢ normed_space ?m_1 V
scratch.lean:9:4: error
failed to synthesize type class instance for
U : Type u_2,
V : Type u_3,
df : U → V
⊢ normed_space ?m_1 U
-/

[Johan Commelin]

@Jean Lo Try removing the * after Type.

[Johan Commelin]

All your types live in different universes, I don't think you want that.

[Kevin Buzzard]

Why not?

[Kevin Buzzard]

It doesn't fix it anyway

[Kevin Buzzard]

I bet there's a simple solution to the timeout

[Kevin Buzzard]

it will be one of those "oops I just coerced from int to nat and Lean hung" moments

[Kevin Buzzard]

Oh -- there's no "a"

[Kevin Buzzard]

no, there is an a :-(

[Johan Commelin]

Hmm crazy. I remember that some months ago Kenny had a very weird example, where the *s broke the type class system.

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclass.20problems/near/128168992

[Jean Lo]

this is probably a separate topic, but: how should I tell whether I want different universes? I'm convinced I've seen cases where it's important to have types live in separate places for generality purposes, or something.

[Kevin Buzzard]

I don't understand Johan's comment. I think what you had was fine -- you're supposed to be maximally polymorphic.

[Kevin Buzzard]

Of course I'm happy to be corrected in this instance :-)

[Kevin Buzzard]

I've found it.

[Kevin Buzzard]

#print notation ∥ -- has_norm.norm

[Kevin Buzzard]

#print has_norm.norm -- α → ℝ

[Kevin Buzzard]

The norm is real-valued, not k-valued. So Lean is hung up trying to find a coercion from the reals to k

[Johan Commelin]

I retract my comment. I was just reminded of the weird behaviour that Kenny discovered (see link above). But apparently it is orthogonal.

[Kevin Buzzard]

or trying to find a real vector space structure on U. I have used Lean enough to know that this is usually the problem with these weird time-outs -- you have written buggy code but Lean is not telling you the actual problem.

[Kevin Buzzard]

Jean, I am glad to see that you are thinking about $p$-adic Banach spaces, they are very important in the theory of $p$-adic modular forms :-)

[Kevin Buzzard]

I will never forget Guillermo's insanely weird timeout which was caused by him writing something like 0 <= x <= 1, and Lean figured 0 <= x was a Prop and then hung trying to coerce it into the real numbers :-)

[Kevin Buzzard]

Oh yeah thanks Johan for reminding me of that. That's one of those "probably Lean 4 will fix it" things; I think it's worth keeping these random problems at the back of your mind because whenever someone comes up with something weird and not working, these random things might be the answer.

[Kevin Buzzard]

But the failure of type class inference somehow troubles me more. It might mean that you can't use modules as variables any more.

[Johan Commelin]

But now it is fixed, right?

[Kevin Buzzard]

No, the "failed to synthesize type class instance" issue in my first post is not fixed, right?

[Kevin Buzzard]

Aah, I see. I can't write is_linear_map f for f an R-module homomorphism, I now have to write is_linear_map R f, which is good.

[Kevin Buzzard]

but apparently you can still write [is_bounded_linear_map df]

[Kevin Buzzard]

@Kenny Lau is it a problem that is_bounded_linear_map f extends is_linear_map k f? Should it be is_bounded_linear_map k fnowadays?

@Jean Lo I note that is_bounded_linear_map is a structure not a class, so you shouldn't be using [] with it, it should be a regular assumption.

[Kenny Lau]

yes it should be is_bounded_linear_map k f

[Kevin Buzzard]

[at least, it's a structure in the mathlib I'm using; I know these things sometimes change, indeed is_noetherian is a def in the mathlib I'm using but it changed to a class yesterday in mathlib master.

[Kevin Buzzard]

yes it should be is_bounded_linear_map k f

@Jean Lo there's a perfect PR for you :-)

[Johan Commelin]

Probably make it a class while you are at it.

[Jean Lo]

got myself even more confused trying to do the edits.

making k an explicit argument to is_bounded_linear_mapseemed to have been mostly replacing curly brackets with round ones and filling in extra arguments. Making it a class and refactoring the theorems to work started involving stuff I don't understand well enough & I asked about this during the Xena meeting tonight. We went and looked at some similar definitions, I realised that linear_map and is_linear_map both existed, and @Kenny Lau dropped some comments about is_linear_map being deprecated (?) and bundling stuff into structures (as done in linear_map) being the preferred way to do things now. I'm interested in attempting to write up a bounded_linear_map structure, but like. What might be a helpful (?) thing for me to try to do at this point?

[Jean Lo]

( so after the typechecking issue got pointed out yesterday, I've also realised to great embarrassment that I mucked up really badly with the quantifiers and the double-vertical-lines. I think the definition should have looked more like

def deriv_at (a : U) (f : U → V) (df : U → V) :=
  is_bounded_linear_map k f ∧ (∃ ε : U → ℝ, filter.tendsto
  (λ h, ∥ f (a + h) - f a + df h ∥ - ∥ h ∥ * (ε h)) (nhds 0) (nhds 0))

which, barring the remaining confusion about what is_bounded_linear_map should look like, is at least something Lean is happy with, and type class stuff seems to be working just fine even without the redundant normed_space arguments)