## Stream: new members

### Topic: type class inference sadness

#### Jean Lo (Feb 07 2019 at 14:00):

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 (Feb 07 2019 at 14:05):

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 (Feb 07 2019 at 14:07):

@Jean Lo Try removing the * after Type.

#### Johan Commelin (Feb 07 2019 at 14:07):

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

Why not?

#### Kevin Buzzard (Feb 07 2019 at 14:08):

It doesn't fix it anyway

#### Kevin Buzzard (Feb 07 2019 at 14:08):

I bet there's a simple solution to the timeout

#### Kevin Buzzard (Feb 07 2019 at 14:09):

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

#### Kevin Buzzard (Feb 07 2019 at 14:09):

Oh -- there's no "a"

#### Kevin Buzzard (Feb 07 2019 at 14:09):

no, there is an a :-(

#### Johan Commelin (Feb 07 2019 at 14:10):

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

#### Johan Commelin (Feb 07 2019 at 14:12):

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

#### Jean Lo (Feb 07 2019 at 14:13):

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 (Feb 07 2019 at 14:13):

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

#### Kevin Buzzard (Feb 07 2019 at 14:14):

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

I've found it.

#### Kevin Buzzard (Feb 07 2019 at 14:15):

#print notation ∥ -- has_norm.norm

#### Kevin Buzzard (Feb 07 2019 at 14:15):

#print has_norm.norm -- α → ℝ

#### Kevin Buzzard (Feb 07 2019 at 14:16):

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 (Feb 07 2019 at 14:17):

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 (Feb 07 2019 at 14:17):

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 (Feb 07 2019 at 14:19):

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 (Feb 07 2019 at 14:21):

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 (Feb 07 2019 at 14:23):

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 (Feb 07 2019 at 14:24):

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 (Feb 07 2019 at 14:25):

But now it is fixed, right?

#### Kevin Buzzard (Feb 07 2019 at 14:26):

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

#### Kevin Buzzard (Feb 07 2019 at 14:27):

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 (Feb 07 2019 at 14:30):

but apparently you can still write [is_bounded_linear_map df]

#### Kevin Buzzard (Feb 07 2019 at 14:33):

@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 (Feb 07 2019 at 14:34):

yes it should be is_bounded_linear_map k f

#### Kevin Buzzard (Feb 07 2019 at 14:34):

[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 (Feb 07 2019 at 14:35):

yes it should be is_bounded_linear_map k f

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

#### Johan Commelin (Feb 07 2019 at 14:36):

Probably make it a class while you are at it.

#### Jean Lo (Feb 07 2019 at 21:16):

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 (Feb 08 2019 at 23:30):

( 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)

Last updated: May 11 2021 at 21:10 UTC