normed_space timeouts

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Floris van Doorn]

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]

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]

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]

I guess you mean variable k.

[Kevin Buzzard]

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]

Oops, yes I meant k.

[Kevin Buzzard]

There might be bubs everywhere in Lambert's code.

[Floris van Doorn]

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]

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]

set_option profiler true

[Floris van Doorn]

Sorry, I meant

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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]

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

[Rob Lewis]

The referenced example is something from the sensitivity proof.

[Rob Lewis]

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

[Floris van Doorn]

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]

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]

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