Zulip Chat Archive

Stream: maths

Topic: normed_space timeouts


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Dec 04 2019 at 16:26):

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

view this post on Zulip 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 R\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.

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Dec 04 2019 at 16:49):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 04 2019 at 16:58):

I guess you mean variable k.

view this post on Zulip 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?

view this post on Zulip Floris van Doorn (Dec 04 2019 at 16:58):

Oops, yes I meant k.

view this post on Zulip Kevin Buzzard (Dec 04 2019 at 16:58):

There might be bubs everywhere in Lambert's code.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Floris van Doorn (Dec 04 2019 at 17:00):

set_option profiler true

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 04 2019 at 17:03):

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

view this post on Zulip 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

:)

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 04 2019 at 17:07):

The referenced example is something from the sensitivity proof.

view this post on Zulip Rob Lewis (Dec 04 2019 at 17:08):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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