# Zulip Chat Archive

## 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):

What about

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 ring.to_monoid normed_ring.to_ring normed_field.to_normed_ring add_group.to_add_monoid add_comm_group.to_add_group normed_group.to_add_comm_group ring.to_semiring add_comm_group.to_add_comm_monoid

:)

#### 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 add_comm_group.to_add_comm_monoid

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 ring.to_monoid normed_ring.to_ring normed_field.to_normed_ring add_group.to_add_monoid add_comm_group.to_add_group normed_group.to_add_comm_group ring.to_semiring add_comm_group.to_add_comm_monoid normed_field.to_discrete_field

Then there is no failure at all in the instance search, and it just takes a few lines.

#### Johan Commelin (Dec 04 2019 at 19:58):

I'm looking forward to a mathlib in which we manually reset the priority of 253 instances every 7 lines.

Last updated: May 11 2021 at 15:12 UTC