Zulip Chat Archive

Stream: general

Topic: TC hell in FLT-regular

Eric Rodriguez (Dec 26 2021 at 18:19):

in here, I seem to be running into a lot of problems with typeclasses; the thing seems to work, if pushed, but you really have to tell Lean exactly everything for it to work, and I don't know why. Do I have to re-derive the no_zero_smul_divisors instance for ring_of_integers? Is there an algebra diamond? There's some comments around there that are helpful, and I've got a 250K line output ot trace_instances saved if it helps debugging. I really have no clue where to start looking.

Yakov Pechersky (Dec 27 2021 at 00:42):

There's a problem even outside of your ring_of_integers usage: this doesn't typecheck

import ring_theory.roots_of_unity

#check @is_primitive_root.of_map_of_injective _ _ _ _ _ _ _
  (no_zero_smul_divisors.algebra_map_injective _ _) _

Yakov Pechersky (Dec 27 2021 at 00:46):

I had to do the following to get it to be happy

import ring_theory.roots_of_unity

variables {R S : Type*} [comm_ring R] [comm_ring S] [nontrivial S] [algebra R S]
  [no_zero_smul_divisors R S]

#check is_primitive_root.of_map_of_injective
  (no_zero_smul_divisors.algebra_map_injective R S) _

Yakov Pechersky (Dec 27 2021 at 01:03):

Here's your proof restated to show more explicitly the TC issue you've identified:

lemma zeta_primitive_root :
  is_primitive_root (zeta n K : ring_of_integers (cyclotomic_field n K)) n :=
begin
  suffices : is_primitive_root
    (algebra_map (ring_of_integers $ cyclotomic_field n K) (cyclotomic_field n K)
      ((zeta n K) : ring_of_integers $ cyclotomic_field n K)) n,
  { refine this.of_map_of_injective _,
    apply @no_zero_smul_divisors.algebra_map_injective _ _ _ _ _ _ _,
    { -- nontrivial (cyclotomic_field n K)
      apply_instance -- fast
    },
    {
      -- no_zero_smul_divisors ↥(ring_of_integers (cyclotomic_field n K)) (cyclotomic_field n K)
      apply_instance -- slow
    },
  },
  exact zeta'_primitive_root n _ _
end

Yakov Pechersky (Dec 27 2021 at 01:14):

I get ~63 seconds for the second apply_instance in this case:

elaboration: tactic execution took 63.8s
num. allocated objects:  487
num. allocated closures: 1446
63763ms   100.0%   tactic.istep
63763ms   100.0%   tactic.step
63763ms   100.0%   tactic.with_ast
63763ms   100.0%   _interaction
63763ms   100.0%   tactic.istep._lambda_1
63763ms   100.0%   _interaction._lambda_2
63763ms   100.0%   scope_trace
63602ms    99.7%   tactic.solve1
63602ms    99.7%   _interaction._lambda_5
63518ms    99.6%   tactic.apply_instance
63518ms    99.6%   _interaction._lambda_4
63499ms    99.6%   tactic.mk_instance
  190ms     0.3%   tactic.to_expr
  124ms     0.2%   tactic.interactive.suffices
  124ms     0.2%   tactic.interactive.have._lambda_1
   54ms     0.1%   tactic.interactive.apply._lambda_1
   54ms     0.1%   interaction_monad.monad._lambda_9
   54ms     0.1%   tactic.interactive.concat_tags._lambda_5
   53ms     0.1%   tactic.apply
   53ms     0.1%   tactic.apply_core
   37ms     0.1%   tactic.interactive.exact
   29ms     0.0%   tactic.refine
   20ms     0.0%   tactic.exact
    1ms     0.0%   tactic.i_to_expr_for_apply
    1ms     0.0%   tactic.get_goals

lemma zeta_primitive_root :
  is_primitive_root (zeta n K : ring_of_integers (cyclotomic_field n K)) n :=
begin
  suffices : is_primitive_root
    (algebra_map (ring_of_integers $ cyclotomic_field n K) (cyclotomic_field n K)
      ((zeta n K) : ring_of_integers $ cyclotomic_field n K)) n,
  { refine this.of_map_of_injective _,
    apply @no_zero_smul_divisors.algebra_map_injective _ _ _ _ _ _ _,
    { -- nontrivial (cyclotomic_field n K)
      exact local_ring.to_nontrivial
    },
    {
      -- no_zero_smul_divisors ↥(ring_of_integers (cyclotomic_field n K)) (cyclotomic_field n K)
      apply_instance -- slow
    },
  },
  exact zeta'_primitive_root n _ _
end

Yakov Pechersky (Dec 27 2021 at 01:16):

However, on a naked goal that is seemingly the same, it takes <1s:

example (n : ℕ+) (K : Type u)
  [field K]
  [fact (((n : ℕ) : K) ≠ 0)] :
  no_zero_smul_divisors ↥(ring_of_integers (cyclotomic_field n K))
    (cyclotomic_field n K) :=
begin
  apply_instance
end

elaboration: tactic execution took 542ms
num. allocated objects:  24
num. allocated closures: 65
  542ms   100.0%   _interaction._lambda_2
  542ms   100.0%   tactic.step
  542ms   100.0%   _interaction
  542ms   100.0%   tactic.istep
  542ms   100.0%   tactic.with_ast
  542ms   100.0%   tactic.istep._lambda_1
  542ms   100.0%   tactic.apply_instance
  542ms   100.0%   scope_trace
  541ms    99.8%   tactic.mk_instance
    1ms     0.2%   tactic.exact

Yakov Pechersky (Dec 27 2021 at 01:16):

So maybe there's something hidden in the pp.all, I'll check that.

Yakov Pechersky (Dec 27 2021 at 01:41):

Here is the difference that makes it slower. This part makes it fast:

             (@ring_of_integers (@cyclotomic_field n K _inst_4)
                (@cyclotomic_field.field n K _inst_4)).module_left))) :=

but this one makes it slow:

             (@algebra.to_module
                ↥(@ring_of_integers (@cyclotomic_field n K _inst_4)
                     (@cyclotomic_field.field n K _inst_4))
                (@cyclotomic_field n K _inst_4)
                (@comm_ring.to_comm_semiring
                   ↥(@ring_of_integers (@cyclotomic_field n K _inst_4)
                        (@cyclotomic_field.field n K _inst_4))
                   (@ring_of_integers (@cyclotomic_field n K _inst_4)
                      (@cyclotomic_field.field n K _inst_4)).to_comm_ring)
                (@ring.to_semiring (@cyclotomic_field n K _inst_4)
                   (@division_ring.to_ring (@cyclotomic_field n K _inst_4)
                      (@field.to_division_ring (@cyclotomic_field n K _inst_4)
                         (@cyclotomic_field.field n K _inst_4))))
                (@ring_of_integers (@cyclotomic_field n K _inst_4)
                   (@cyclotomic_field.field n K _inst_4)).to_algebra)))) :=

Yakov Pechersky (Dec 27 2021 at 01:43):

inside smul_with_zero.to_has_scalar

Yakov Pechersky (Dec 27 2021 at 01:58):

So I don't know why that particular module definition makes it slow, but that's the smallest quantum of difference I could find that led to the slowdown.

Yakov Pechersky (Dec 27 2021 at 01:59):

-- fast

Yakov Pechersky (Dec 27 2021 at 02:00):

--slow

Eric Rodriguez (Dec 27 2021 at 04:38):

The lack of typechecking originally is worrying, but I think in unrelated to my problem; if we specialize of_map_of_injective to comm_ring \to field (like what's used in the lemma) it still typechecks, but the proof fails:

code

the reason it doesn't typecheck seems to be something weird about ring.to_semiring; I'm not too sure what it is but that seems to be the only diff obvious to a difftool.

Eric Rodriguez (Dec 27 2021 at 04:41):

also, if you exact the right instance, it doesn't seem to take too long on the second one, so it's not some sort of heavy refl

Eric Rodriguez (Dec 27 2021 at 04:52):

the trace.class_instances log for the slow example seems to consist of mainly lines looking like this (~240K of them):

[class_instances] cached failure for @algebra ↥(@ring_of_integers (@cyclotomic_field n K _inst_4) (@cyclotomic_field.field n K _inst_4)) K
  (@comm_ring.to_comm_semiring
     ↥(@ring_of_integers (@cyclotomic_field n K _inst_4) (@cyclotomic_field.field n K _inst_4))
     (@ring_of_integers (@cyclotomic_field n K _inst_4) (@cyclotomic_field.field n K _inst_4)).to_comm_ring)
  (@ring.to_semiring K (@division_ring.to_ring K (@field.to_division_ring K _inst_4)))

Weirdly, none of these say failed is_def_eq, which is the usual error message I see for these sorts of traces the few times I've seen them, except at the very, very end of the repetition. The fact that it looped for so long and yet terminated... mysteries of computers. Then it fails a couple more times and only then it finds the right instance.

Eric Rodriguez (Dec 27 2021 at 04:52):

Thanks so much for looking at this, Yakov. I'm going to sleep on it and hopefully some idea as to what's going on appears, because this is mysterious...

Anne Baanen (Dec 27 2021 at 10:04):

The repeated inference of the same(?) instance looks like this issue: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/odd.20repeated.20type.20class.20search

Last updated: Dec 20 2023 at 11:08 UTC