## Stream: maths

### Topic: normed_space timeouts

#### Kevin Buzzard (Dec 03 2019 at 23:17):

Not actually timeouts but stuff taking a lot of time. Is there a way to shortcut this:

import analysis.normed_space.banach
import analysis.normed_space.basic
import linear_algebra.basic
import linear_algebra.basis
import linear_algebra.dimension
import linear_algebra.finite_dimensional
import topology.subset_properties
import set_theory.cardinal
import data.real.basic
import topology.sequences
import order.bounded_lattice
import analysis.specific_limits
import analysis.normed_space.finite_dimension

noncomputable theory
open_locale classical

open metric set

variables
{V : Type} [normed_group V] [normed_space ℝ V]

set_option trace.class_instances true
example : has_scalar ℝ V := by apply_instance -- (message too long, truncated at 262144 characters)


There is a noticeable pause before Lean can figure out that a normed real vector space has an action of the reals, and the log message is astronomical. Is there just a way of cunningly helping Lean to see the way? How do I go about finding it?

@Lambert A'Campo this is something which was making your code slow.

#### Sebastien Gouezel (Dec 04 2019 at 07:47):

Is this specific to ℝ? A way out would be to prove the theorem in its right generality, i.e., over any nondiscrete normed field (hint: if a ball in a vector space is compact, then either the dimension is 0 and the space is indeed finite-dimensional, or the dimension is positive and then one can deduce that the field is locally compact, therefore complete, and all you did on ℝ should go through).

#### Kevin Buzzard (Dec 04 2019 at 16:26):

@Lambert A'Campo there's your homework ;-)

#### Kevin Buzzard (Dec 04 2019 at 16:38):

I have minimised the issue:

import analysis.normed_space.basic

universe u

variables {k : Type u} [normed_field k] {V : Type u} [normed_group V] [normed_space k V]

set_option class.instance_max_depth 36 -- 35 gives max class-instance res depth error
set_option trace.class_instances true
example : has_scalar k V := by apply_instance -- (message too long, truncated at 262144 characters)


@Sebastien Gouezel it is not specific to $\mathbb{R}$. Type class resolution is going crazy here. It is a miracle that Lambert got to the end of his proof. He just didn't know that it wasn't supposed to be this horrible. It's one of those situations where every time you write a new line you have to wait for several seconds for the orange bars to disappear. I don't really care why it's happening any more, I have this vague idea that it will all be fixed in Lean 4 and until then I just want to know some way of changing some priority to 37 or 10000 to make it all happen immediately for Lambert.

#### Kevin Buzzard (Dec 04 2019 at 16:42):

typeclass trace here (first 262144 characters of it anyway). I still cannot read these mysterious incantations. Is this the one which is a prolog-like search or is that simp? I am still so ignorant of these matters. I just want it to work.

#### Sebastien Gouezel (Dec 04 2019 at 16:49):

Maybe #1729 will make a difference, who knows...

#### Patrick Massot (Dec 04 2019 at 16:49):

This is one more toy for @Daniel Selsam . Note that example : has_scalar k V := mul_action.to_has_scalar k V is instantaneous, so this is really this instance that is long to find.

#### Kevin Buzzard (Dec 04 2019 at 16:51):

I note that Lean starts off by spending a lot of time trying to prove that the normed group V is (deep breath): a ring, a normed ring, a normed field, a domain, a division ring, a field, a linear_ordered field, a discrete_field, a linear_ordered ring, a linear_ordered_comm_ring, a decidable_linear_ordered_comm_ring, a discrete_linear_ordered_field, an integral_domain, a euclidean_domain, a nondiscrete_normed_field, and it just keeps going. V does not have a multiplication so it is obviously none of these things. There is no has_mul!

#### Kevin Buzzard (Dec 04 2019 at 16:54):

A normalisation domain, a gcd_domain, a normed_field, an ordered ring, a comm_ring, a nonzero_comm_ring...

#### Floris van Doorn (Dec 04 2019 at 16:56):

Yes, I think #1729 will improve this. However, we are reaching the limits of the Lean 3 type class inference search here, and the problems will get worse...

#### Kevin Buzzard (Dec 04 2019 at 16:57):

The madness with V starts on line 73 of the typeclass trace link above, and it takes up all the remaining 4000+ lines of the trace.

#### Floris van Doorn (Dec 04 2019 at 16:57):

As I describe in #1561, I think the problem is even worse for real than for a variable V, because of all the shortcut-instances we have for real.

#### Patrick Massot (Dec 04 2019 at 16:58):

I guess you mean variable k.

#### Kevin Buzzard (Dec 04 2019 at 16:58):

How do I cheat? Patrick has told us the instance I need. How do I just make Lean use that instance and not ask any questions?

#### Floris van Doorn (Dec 04 2019 at 16:58):

Oops, yes I meant k.

#### Kevin Buzzard (Dec 04 2019 at 16:58):

There might be bubs everywhere in Lambert's code.

#### Floris van Doorn (Dec 04 2019 at 16:59):

Does something like the following work? (I don't have Lean running right now)

local attribute [instance, priority 0] module.to_has_scalar
local attribute [instance, priority 200] vector_space.to_module


#### Kevin Buzzard (Dec 04 2019 at 17:00):

Can someone remind me of the set_option option for seeing how long code takes to be elaborated/compiled/whatever the thing is that is taking a long time?

#### Floris van Doorn (Dec 04 2019 at 17:00):

set_option profiler true

#### Floris van Doorn (Dec 04 2019 at 17:01):

Sorry, I meant

local attribute [instance, priority 0] algebra.to_has_scalar
local attribute [instance, priority 200] vector_space.to_module


#### Kevin Buzzard (Dec 04 2019 at 17:03):

Compile time goes down from 453ms to 287ms but still takes over 262144 characters of trace.

#### Sebastien Gouezel (Dec 04 2019 at 17:06):

local attribute [instance, priority 10000] mul_action.to_has_scalar distrib_mul_action.to_mul_action
semimodule.to_distrib_mul_action module.to_semimodule vector_space.to_module normed_space.to_vector_space


:)

#### Rob Lewis (Dec 04 2019 at 17:06):

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/visualizations/near/178373092 . There's hope for the future.

#### Rob Lewis (Dec 04 2019 at 17:07):

The referenced example is something from the sensitivity proof.

#### Rob Lewis (Dec 04 2019 at 17:08):

I think it's the same idea as Kevin's example.

#### Floris van Doorn (Dec 04 2019 at 17:12):

Here is what I found:

local attribute [instance, priority 0] algebra.has_scalar algebra.to_module algebra.to_has_scalar
local attribute [instance, priority 200] vector_space.to_module normed_group.to_add_comm_group


And yes, the main bottleneck here is the same issue as the one Rob references.

#### Sebastien Gouezel (Dec 04 2019 at 17:12):

Oops, sorry, I forgot one. It should have been

local attribute [instance, priority 10000] mul_action.to_has_scalar distrib_mul_action.to_mul_action
semimodule.to_distrib_mul_action module.to_semimodule vector_space.to_module normed_space.to_vector_space