slow elaboration

Stream: general

[Kenny Lau]

import algebra.group_ring_action linear_algebra.basis field_theory.subfield

universes u v

variables (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G)

def fixed : set F :=
{ x | ∀ g : G, g • x = x }

instance : is_subfield (fixed G F) :=
sorry

/-- Embedding induced by action. -/
def mul_action.to_fun : F ↪ (G → F) :=
⟨λ x m, m • x, λ x y H, one_smul G x ▸ one_smul G y ▸ by convert congr_fun H 1⟩

theorem linear_independent_smul_of_linear_independent {s : finset F}
  (hs : linear_independent (fixed G F) (λ i : (↑s : set F), (i : F))) :
  linear_independent F (λ i : (↑(s.map $ mul_action.to_fun G F) : set (G → F)), (i : G → F)) :=
sorry

[Kenny Lau]

the statement of the theorem is slow to elaborate

[Kenny Lau]

but profiler doesn't show any abnormality

[Kenny Lau]

if I use trace.class_instances there is this mysterious search for:

has_coe_to_fun ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s)

[Kenny Lau]

which I cannot find in the pp.all #print

[Kenny Lau]

is there anyway to somehow track the elaboration?

[Kevin Buzzard]

Does

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

help?

[Kevin Buzzard]

Wait, what version of Lean are you on? Everything is instant for me on 3.13.2

[Kenny Lau]

(3, (14, 0))

[Kevin Buzzard]

I do have some crazy search for the coercion though:

[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @list.bin_tree_to_list ?x_205
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := smt_tactic.has_coe ?x_206
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @lean.parser.has_coe ?x_207
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @tactic.ex_to_tac ?x_208
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @tactic.opt_to_tac ?x_209
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @expr.has_coe ?x_210 ?x_211
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := string_to_format
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := nat_to_format
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := string_to_name
failed is_def_eq

etc

[Kenny Lau]

I've never used those so I don't know what to look for

[Kevin Buzzard]

elaboration of linear_independent_smul_of_linear_independent took 0.0389ms

[Kenny Lau]

yeah profiler shows nothing

[Kenny Lau]

but I can see the orange bar

[Kenny Lau]

takes about 4 seconds for the orange bar to disappear

[Kenny Lau]

so maybe 1 second for you

[Kevin Buzzard]

It takes well under a second for mine to disappear. I'll upgrade to 3.14.

[Kevin Buzzard]

The trace output was huge though

[Kevin Buzzard]

Still fast for me

[Kenny Lau]

I upgraded mathlib and now it only takes 2 seconds for the orange bar to disappear

[Kenny Lau]

so this should be 0.5 seconds for you

[Kenny Lau]

which I guess would still be visible

[Kevin Buzzard]

Oh I see it, I can believe it's about a third of a second

[Kenny Lau]

import algebra.group_ring_action field_theory.subfield ring_theory.polynomial
import field_theory.minimal_polynomial field_theory.splitting_field

local attribute [instance] classical.dec

universes u v

variables (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G)

def fixed : set F :=
{ x | ∀ g : G, g • x = x }

instance fixed.is_subfield : is_subfield (fixed G F) :=
sorry

#check (1 : polynomial (fixed G F))

[Kenny Lau]

the check takes 3 to 4 seconds

[Kenny Lau]

I can't do anything if I can't even talk about 1

[Yury G. Kudryashov]

Elaboration of the inhabited instance in #2897 takes ~10s with lean -j1 on my laptop. It's more than the rest of the file.

[Johan Commelin]

What happened to our :racecar: fast lean?

[Gabriel Ebner]

I took a quick look. The following reduces the runtime from 8.5s to 2s on my laptop:

local attribute [instance, priority 1001] classical.prop_decidable

[Gabriel Ebner]

The reason is that split_if uses by_cases, which uses decidable even if the goal is a prop.

[Johan Commelin]

Aah, so would open_locale classical have avoided this problem?

[Gabriel Ebner]

There is already an open_locale classical.

[Yury G. Kudryashov]

I have open_locale classical but it adds classical.prop_decidable as a low prio instance.

[Yury G. Kudryashov]

Gabriel explains that I need to make it a high priority instance.

[Johan Commelin]

priorities are hard

[Gabriel Ebner]

And/or fix by_cases.

[Johan Commelin]

Ooh... I was still looking at Kenny's code

[Johan Commelin]

Is it the same problem?

[Johan Commelin]

I somehow assumed that Yury's post was a semireply to Kenny

[Sebastien Gouezel]

I have a good one. The beginning of the file analysis/specific_functions/pow.lean (after imports) is

open_locale classical real topological_space

namespace complex

/-- The complex power function `x^y`, given by `x^y = exp(y log x)` (where `log` is the principal
determination of the logarithm), unless `x = 0` where one sets `0^0 = 1` and `0^y = 0` for
`y ≠ 0`. -/
noncomputable def cpow (x y : ℂ) : ℂ :=
if x = 0
  then if y = 0
    then 1
    else 0
  else exp (log x * y)

noncomputable instance : has_pow ℂ ℂ := ⟨cpow⟩

@[simp] lemma cpow_eq_pow (x y : ℂ) : cpow x y = x ^ y := rfl

lemma cpow_def (x y : ℂ) : x ^ y =
  if x = 0
    then if y = 0
      then 1
      else 0
    else exp (log x * y) := rfl

With profiler on, I get 17.3s to elaborate cpow (and my computer is pretty fast, so I guess Kenny couldn't even open this file). Then, for cpow_def, the profiler tells me that it is less than one second, but the bar stays orange also for roughly 20s, so something is hidden here.

[Johan Commelin]

What on earth is so hard about cpow?

[Yury G. Kudryashov]

Probably it tries many decidable instances before using classical fallback.

[Yury G. Kudryashov]

@Sebastien Gouezel Did you try to make classical a high priority instance?

[Sebastien Gouezel]

Exactly. If you set local attribute [instance, priority 1001] classical.prop_decidable, everything becomes instant.

[Gabriel Ebner]

This also makes it instant:

instance : decidable_eq ℂ := λ _ _, classical.prop_decidable _

[Johan Commelin]

That's crazy...

[Johan Commelin]

@Kenny Lau Does this also fix your problems in this thread?

[Yury G. Kudryashov]

Should we add these instance for real and complex numbers?

[Gabriel Ebner]

Wow, this is also instant:

instance : decidable_eq ℂ := by apply_instance

[Sebastien Gouezel]

Don't look at the instance trace, it is definitely not for kids. with things like

[class_instances] (4) ?x_33 : nonneg_ring ℂ := @linear_nonneg_ring.to_nonneg_ring ?x_34 ?x_35

What's a nonneg_ring?!

[Gabriel Ebner]

The cause for this decidable tarpit is the eq.decidable instance, which derives decidable_eq α from decidable_linear_order α. And this searches through half of the tc hierarchy.

[Kenny Lau]

Gabriel Ebner said:

The cause for this decidable tarpit is the eq.decidable instance, which derives decidable_eq α from decidable_linear_order α. And this searches through half of the tc hierarchy.

oh!

[Sebastien Gouezel]

Should we downgrade its priority to 90 and put classical at 95?

[Johan Commelin]

What would happen if we completely unbundle all decidable stuff? So you only have decidable_{eq,prop} and linear_order, but not decidable_linear_order.

[Sebastien Gouezel]

For a long time, I have wanted to kill decidable_linear_order, but this in core, alas. Oh, wait :)

[Johan Commelin]

Oh, wait :)

Is that a promise?

[Mario Carneiro]

nonneg_ring should not be a class, that was a mistake

[Mario Carneiro]

and eq.decidable should be a local instance

[Bryan Gin-ge Chen]

I'm just catching up on this now. Is there a PR for this (in progress)? If not, can someone summarize what needs to be done?

[Johan Commelin]

Johan Commelin said:

What would happen if we completely unbundle all decidable stuff? So you only have decidable_{eq,prop} and linear_order, but not decidable_linear_order.

I really have no idea if this is feasable. But @Gabriel Ebner gave a :thumbs_up:, so I think we can/should try this.

[Kenny Lau]

import data.monoid_algebra
import ring_theory.algebra
import algebra.invertible
import algebra.char_p
import linear_algebra.basis

universes u

noncomputable theory
open module
open monoid_algebra

variables {k : Type u} [comm_ring k] {G : Type u} [group G]

variables {V : Type u} [add_comm_group V] [module (monoid_algebra k G) V]
variables {W : Type u} [add_comm_group W] [module (monoid_algebra k G) W]

#check (by apply_instance : semimodule k (restrict_scalars k (monoid_algebra k G) W))
#check @linear_map.{u u u} k (restrict_scalars k (monoid_algebra k G) W) (restrict_scalars k (monoid_algebra k G) V) _ _ _
/- restrict_scalars k (monoid_algebra k G) W →ₗ[k] restrict_scalars k (monoid_algebra k G) V :
  Π [_inst_4 : semimodule k (restrict_scalars k (monoid_algebra k G) W)]
  [_inst_5 : semimodule k (restrict_scalars k (monoid_algebra k G) V)], Type u

[Kenny Lau]

Hi everyone, it's Kenny "Slow Elaboration" Lau again

[Kenny Lau]

the elaboration speed is ok here

[Kenny Lau]

until one puts two more underscores at the end to tell Lean to find the remaining instances

[Kenny Lau]

note how the first check tells you that Lean can find the instance in "normal" speed

[Kenny Lau]

but for some reason Lean is slow if I put the underscore at the end

[Kenny Lau]

so I cannot seem to isolate the problem

[Mario Carneiro]

both #checks are near instant for me

[Mario Carneiro]

that's on a slightly older version of mathlib though, maybe something changed recently

[Kenny Lau]

@Mario Carneiro even when you add two underscores at the end?

[Mario Carneiro]

oh I misunderstood

[Mario Carneiro]

Okay I can replicate.

-- fast
#check @linear_map.{u u u} k
  (restrict_scalars k (monoid_algebra k G) W)
  (restrict_scalars k (monoid_algebra k G) V) _ _ _
  (by apply_instance) (by apply_instance)

-- slow
#check @linear_map.{u u u} k
  (restrict_scalars k (monoid_algebra k G) W)
  (restrict_scalars k (monoid_algebra k G) V) _ _ _
  _ _

[Kenny Lau]

that's just fascinating

[Kenny Lau]

what's happening?

[Mario Carneiro]

This looks like it will require a C++ deep dive. I don't know what could make this happen besides elaboration order shenanigans as a result of using by

[Kenny Lau]

-- fast
#check @linear_map.{u u u} k
  (restrict_scalars k (monoid_algebra k G) W)
  (restrict_scalars k (monoid_algebra k G) V) _ _ _
  (by apply_instance)

-- slow
#check @linear_map.{u u u} k
  (restrict_scalars k (monoid_algebra k G) W)
  (restrict_scalars k (monoid_algebra k G) V) _ _ _
  infer_instance

[Mario Carneiro]

-- fast
example := @linear_map.{u u u} k
  (restrict_scalars k (monoid_algebra k G) W)
  (restrict_scalars k (monoid_algebra k G) V) _ _ _ _ _

-- slow
#check @linear_map.{u u u} k
  (restrict_scalars k (monoid_algebra k G) W)
  (restrict_scalars k (monoid_algebra k G) V) _ _ _ _ _

[Kenny Lau]

what :o

[Kenny Lau]

interesting

[Reid Barton]

what if you make the example a def, and #check it?

[Kevin Buzzard]

changing the example to a def makes it slow, in Mario's example. Kenny's last example freaks me out a bit more

[Mario Carneiro]

kenny's version makes sense to me only in the sense that it's testing the same thing as my example before that. There is something about switching to tactic mode here using by that makes it work out

[Kenny Lau]

import algebra.char_p data.polynomial

universe u

namespace polynomial

theorem C_nat_cast {R : Type u} [comm_semiring R] (n : ℕ) : C (n : R) = n :=
ring_hom.map_nat_cast C.to_ring_hom n

instance {R : Type u} [comm_semiring R] (p : ℕ) [h : char_p R p] : char_p (polynomial R) p :=
let ⟨h⟩ := h in ⟨λ n, by rw [← C_nat_cast, ← C_0, C_inj, h]⟩

-- fast
theorem frobenius_eq {R : Type u} [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] (f : polynomial R) :
  @frobenius (polynomial R) _ p _ (polynomial.char_p p) f = f.eval₂ C (X ^ p) :=
sorry

-- slow
theorem frobenius_eq {R : Type u} [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] (f : polynomial R) :
  @frobenius (polynomial R) _ p _ _ f = f.eval₂ C (X ^ p) :=
sorry

-- fast
theorem frobenius_eq'' {R : Type u} [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] (f : polynomial R) :
  by exact @frobenius (polynomial R) _ p _ _ f = f.eval₂ C (X ^ p) :=
sorry

end polynomial

[Kenny Lau]

is this the same bug?

[Kenny Lau]

(btw the theorem is false)

[Kenny Lau]

(edit: I guess I found the workaround)

[Johan Commelin]

What's going on with C_nat_cast? Shouldn't there be alg_hom.nat_cast instead?

[Kenny Lau]

right