Slow definition

Stream: general

[Sebastien Gouezel]

I have a little riddle, from the file exterior_algebra. Consider the following two definitions:

import linear_algebra.exterior_algebra

variables (R : Type*) [comm_semiring R]
variables (M : Type*) [add_comm_monoid M] [semimodule R M]

set_option profiler true

def foo1 {S : Type*} [comm_ring S] [semimodule S M] : semiring (exterior_algebra S M) :=
let i : semiring (tensor_algebra S M) := infer_instance in
@ring_quot.semiring (tensor_algebra S M) i (exterior_algebra.rel S M)

def foo2 {S : Type*} [comm_ring S] [semimodule S M] : ring (exterior_algebra S M) :=
let i : ring (tensor_algebra S M) := infer_instance in
@ring_quot.ring (tensor_algebra S M) i (exterior_algebra.rel S M)

Here foo1 elaborates in 18ms on my computer, and foo2 in 18s. So a ratio of 1 to 1000...

[Eric Wieser]

This one was a mystery to me too

[Eric Wieser]

I was kinda fed up with not having a ring structure at all, and had such a hard time adding one that I lost interest in making it fast too!

[Eric Wieser]

src#exterior_algebra.ring has a few more lets than that, doesn't it?

[Sebastien Gouezel]

I noticed it because it gets even slower in #7084

[Sebastien Gouezel]

Eric Wieser said:

src#exterior_algebra.ring has a few more lets than that, doesn't it?

No, I copied the exact definition.

[Eric Wieser]

I thought that might be where this was going

[Eric Wieser]

Does #7084 change ring_quot (docs#ring_quot.semiring?) to add a non-auto_param nsmul?

[Eric Wieser]

I just noticed that ring_quot.ring uses the automatic has_sub - I'll see if changing that makes things better.

[Sebastien Gouezel]

It didn't initially, although it does now on my local branch (because there is also an algebra instance below, so to kill the potential diamond one needs to add the nsmul field). But it becomes too slow even without adding it.

[Sebastien Gouezel]

I found a way to speed up things, but I don't understand what's going on. The current ring structure on a quotient is:

instance {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
{ neg           := quot.map (λ a, -a)
    rel.neg,
  add_left_neg  := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _), },
  .. (ring_quot.semiring r) }

With this definition, my test example foo2 takes 18s to compile. If I change it to

instance {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
{ add           := quot.map₂ (+) rel.add_right rel.add_left,
  add_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (add_assoc _ _ _), },
  zero          := quot.mk _ 0,
  zero_add      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (zero_add _), },
  add_zero      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_zero _), },
  add_comm      := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (add_comm _ _), },
  mul           := quot.map₂ (*) rel.mul_right rel.mul_left,
  mul_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (mul_assoc _ _ _), },
  one           := quot.mk _ 1,
  one_mul       := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (one_mul _), },
  mul_one       := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (mul_one _), },
  left_distrib  := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (left_distrib _ _ _), },
  right_distrib := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (right_distrib _ _ _), },
  neg           := quot.map (λ a, -a) rel.neg,
  add_left_neg  := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _) } }

(So, doing everything by hand instead of referring to the semiring structure), then this goes down to 8s.

If I trim it down to

instance {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
{ add           := quot.map₂ (+) rel.add_right rel.add_left,
  zero          := quot.mk _ 0,
  mul           := quot.map₂ (*) rel.mul_right rel.mul_left,
  one           := quot.mk _ 1,
  neg           := quot.map (λ a, -a) rel.neg,
  add_left_neg  := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _) },
  .. (ring_quot.semiring r) }

(Keeping only the data fields, and leaving the Prop fields to the semiring structure), this goes up again to 21s.

So the content of Prop-fields matters, which I don't get. And all this is to be compared to the 18ms for the semiring version.

TLDR: I don't understand anything to the inner workings of structure elaboration. Any advice on how to make things right / good practice rule would be most welcome!

[Eric Wieser]

Eric Wieser said:

I just noticed that ring_quot.ring uses the automatic has_sub - I'll see if changing that makes things better.

Done in #7112, although I didn't end up profiling it because the behavior seemed like something we'd want anyway

[Sebastien Gouezel]

I had done profiling, and it doesn't make any difference. Unfortunately, the speedup I mentioned earlier in the discussion is not enough for #7084, which is therefore stuck for now :-(

[Sebastien Gouezel]

I'm wondering if the solution here would not be to make more things irreducible: here the exterior algebra is a quotient of the tensor algebra, which itself is already a complicated quotient, so if Lean tries to unfold anything in exterior algebras the terms are astronomically big right away, which is probably not reasonable (and essentially pointless). Thoughts, anyone?

[Sebastien Gouezel]

(by "irreducible", I mean use structures just like in the definition of reals, not mark things irreducible after the fact).

[Eric Wieser]

Note that originally things were marked irreducible and that actually broke typeclass search

[Kevin Buzzard]

(So, doing everything by hand instead of referring to the semiring structure), then this goes down to 8s.

This makes no difference for me. On my desktop it takes around 9 seconds to elaborate foo2 below, and if I uncomment all the comments then it still takes around 9 seconds.

import linear_algebra.exterior_algebra
import algebra.ring_quot

variables (R : Type*) [comm_semiring R]
variables (M : Type*) [add_comm_monoid M] [semimodule R M]

set_option profiler true

def foo1 {S : Type*} [comm_ring S] [semimodule S M] : semiring (exterior_algebra S M) :=
let i : semiring (tensor_algebra S M) := infer_instance in
@ring_quot.semiring (tensor_algebra S M) i (exterior_algebra.rel S M)

universe u₁

open ring_quot

-- local attribute [-instance] ring_quot.ring

-- instance inst37 {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
-- { add           := quot.map₂ (+) rel.add_right rel.add_left,
--   add_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (add_assoc _ _ _), },
--   zero          := quot.mk _ 0,
--   zero_add      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (zero_add _), },
--   add_zero      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_zero _), },
--   add_comm      := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (add_comm _ _), },
--   mul           := quot.map₂ (*) rel.mul_right rel.mul_left,
--   mul_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (mul_assoc _ _ _), },
--   one           := quot.mk _ 1,
--   one_mul       := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (one_mul _), },
--   mul_one       := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (mul_one _), },
--   left_distrib  := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (left_distrib _ _ _), },
--   right_distrib := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (right_distrib _ _ _), },
--   neg           := quot.map (λ a, -a) rel.neg,
--   add_left_neg  := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _) } }

def foo2 {S : Type*} [comm_ring S] [semimodule S M] : ring (exterior_algebra S M) :=
let i : ring (tensor_algebra S M) := infer_instance in
@ring_quot.ring (tensor_algebra S M) i (exterior_algebra.rel S M)

[Kevin Buzzard]

Oh in fact if I just make ring_quot.ring not an instance then it still takes 9 seconds -- in my set-up it doesn't seem to be using ring_quot.ring at all (this is on a relatively recent master -- are you doing something else?)

[Sebastien Gouezel]

You need to do this in the original file, before tensor_product is defined.

[Kevin Buzzard]

Got it!

[Eric Wieser]

Did you actually mean tensor_product and not tensor_algebra?

[Kevin Buzzard]

It's a universe issue.

import linear_algebra.exterior_algebra

variables (R : Type*) [comm_semiring R]
variables (M : Type*) [add_comm_monoid M] [semimodule R M]

set_option profiler true

def foo1 {S : Type*} [comm_ring S] [semimodule S M] : semiring (exterior_algebra S M) :=
let i : semiring (tensor_algebra S M) := infer_instance in
@ring_quot.semiring (tensor_algebra S M) i (exterior_algebra.rel S M)

-- Change {S : Type*} to {S : Type}
-- 455 ms
def foo2 {S : Type} [comm_ring S] [semimodule S M] : ring (exterior_algebra S M) :=
let i : ring (tensor_algebra S M) := infer_instance in
@ring_quot.ring (tensor_algebra S M) i (exterior_algebra.rel S M)

[Eric Wieser]

What if you put {S : Type*} in a separate variables declaration?

[Kevin Buzzard]

import linear_algebra.exterior_algebra

universes u v w
variables (R : Type u) [comm_semiring R]
variables (M : Type v) [add_comm_monoid M] [semimodule R M]

set_option profiler true

def foo1 {S : Type w} [comm_ring S] [semimodule S M] : semiring (exterior_algebra S M) :=
let i : semiring (tensor_algebra S M) := infer_instance in
@ring_quot.semiring (tensor_algebra S M) i (exterior_algebra.rel S M)

-- 455 ms
def foo2 {S : Type w} [comm_ring S] [semimodule S M] : ring (exterior_algebra S M) :=
let i : ring (tensor_algebra S M) := infer_instance in
@ring_quot.ring (tensor_algebra S M) i (exterior_algebra.rel S M)

This is also instant. It's {Type*} v {Type u} again.

[Kevin Buzzard]

import linear_algebra.exterior_algebra

variables (R : Type*) [comm_semiring R]
variables (M : Type*) [add_comm_monoid M] [semimodule R M]
variable {S : Type*}

set_option profiler true

def foo1 [comm_ring S] [semimodule S M] : semiring (exterior_algebra S M) :=
let i : semiring (tensor_algebra S M) := infer_instance in
@ring_quot.semiring (tensor_algebra S M) i (exterior_algebra.rel S M)

-- 484ms
def foo2 [comm_ring S] [semimodule S M] : ring (exterior_algebra S M) :=
let i : ring (tensor_algebra S M) := infer_instance in
@ring_quot.ring (tensor_algebra S M) i (exterior_algebra.rel S M)

As Eric suggests: if you strip it out it's quick even with Type*.

[Eric Wieser]

This is annoying, because I constantly run into universe issues where someone wrote Type u and mean Type something_other_than_u because guessing the universe variables already in the lemma was a pain for them.

In the past I've ended up stripping out universe variables entirely and replacing things with Type*. Only now we find that introduces subtler problems...

[Damiano Testa]

I have not encountered this issue much, but the first time it came for me was also in linear algebra. Could there be something specific to the linear algebra part of the library that makes these issues more prominent?

[Kevin Buzzard]

I think this was why universes were causing problems with some previous linear algebra thread:

universes u v w
-- this is the type of `flip`
#check Π {α : Type u} {β : Type v} {φ : Type w}, (α → β → φ) → β → α → φ
-- Type (max (u+1) (v+1) (w+1) (max u v w) v u w)

This type can be simplified, but you can't run the simplifier on universe levels :-)

[Damiano Testa]

Indeed, it was flip! Maybe it is the fact of having 3 interlaced Types that causes problems?

[Kevin Buzzard]

My instinct, probably not the correct one but it's what I tell students, is that whilst it's important to stay universe polymorphic, can you really imagine a situation where you have your ring in one universe and your module in another one? Put everything into one universe! And then of course people want to do modules over $\Z$ and they realise they have to do everything in Type.

[Damiano Testa]

... which is fine as it might even be inconsistent to have more than Type! :upside_down:

[Kevin Buzzard]

Here is the non-diamond which I think is causing the issue:

import linear_algebra.exterior_algebra

universes u v w
variables (R : Type*) [comm_semiring R]
variables (M : Type*) [add_comm_monoid M] [semimodule R M]

set_option profiler true

-- 10 seconds
def foo {S : Type*} [comm_ring S] [semimodule S M] :
  @tensor_algebra.semiring S (@comm_ring.to_comm_semiring S _inst_4) M _inst_2 _inst_5 =
  @ring.to_semiring (@tensor_algebra S (@comm_ring.to_comm_semiring S _inst_4) M _inst_2 _inst_5) (@tensor_algebra.ring M _inst_2 S _inst_4 _inst_5)
:= rfl

-- 1/2 second
def bar {S : Type w} [comm_ring S] [semimodule S M] :
  @tensor_algebra.semiring S (@comm_ring.to_comm_semiring S _inst_4) M _inst_2 _inst_5 =
  @ring.to_semiring (@tensor_algebra S (@comm_ring.to_comm_semiring S _inst_4) M _inst_2 _inst_5) (@tensor_algebra.ring M _inst_2 S _inst_4 _inst_5)
:= rfl

(foo and bar are the same apart from {S : Type*} changed to {S : Type w})

[Eric Wieser]

What does foo infer for the *?

[Kevin Buzzard]

{S : Type u_2}

[Sebastien Gouezel]

Thanks a lot for debugging this and noticing it was a universe issue! In the meantime, I have made this quotient ring construction irreducible, which I think is a good idea in any case because it hides some irrelevant complexity.

[Kevin Buzzard]

Thanks a lot for your diamond-killing! You have put in a lot of work recently with some really technical and messy issues and I am all too happy to help.

[Sebastien Gouezel]

After making things irreducible, foo takes 2 seconds and bartakes 0.5s, so it's better but the universe issues are still in the way.

[Kevin Buzzard]

@Eric Wieser as far as I can see foo and bar are identical even up to universes.

[Kevin Buzzard]

For some reason Lean is spending a long time solving for * in foo, and ultimately deciding that it can be anything.

[Kevin Buzzard]

If someone had told me 5 years ago I'd be working with an analyst on universe issues, I would have been extremely skeptical.

[Eric Wieser]

Kevin Buzzard said:

If someone had told me 5 years ago I'd be working with an analyst on universe issues, I would have been extremely skeptical.

Sounds like you're in a different universe now to the one you thought you were in

[Sebastien Gouezel]

I'm not really an analyst, you know, more of a dynamical systems/probability person. But still in a different universe, yes :-)

[Sebastien Gouezel]

And I've already written a paper relying on the classification of irreducible unitary representations of $SL(2,\R)$, so that almost makes me an automorphic guy also :-)

[Kevin Buzzard]

They're defeq to projective 2-d reps of the Weil group of $\R$ I guess.

[Sebastien Gouezel]

Another weirdness I encountered while fixing the slowness. In the file data.mv_polynomial.equiv, on Line 255, there is

change algebra_map R (mv_polynomial S₁ (mv_polynomial S₂ R)) r with C (C r),

which is already slow, and becomes slower after the refactor. You can replace the change with an equivalent

  have A : algebra_map R (mv_polynomial S₁ (mv_polynomial S₂ R)) r = C (C r) := rfl

which takes 64s on my branch. With := by refl, same thing. With , by refl, it becomes instant (less than 200ms).

[Sebastien Gouezel]

Another weird example.

@[simp] lemma finite_field.char_poly_pow_card {K : Type*} [field K] [fintype K] (M : matrix n n K) :
  char_poly (M ^ (fintype.card K)) = char_poly M :=
begin
  by_cases hn : nonempty n,
  { haveI := hn,
    cases char_p.exists K with p hp, letI := hp,
    rcases finite_field.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩,
    haveI : fact p.prime := ⟨hp⟩,
    dsimp at hk, rw hk at *,
    apply (frobenius_inj (polynomial K) p).iterate k,
    repeat { rw iterate_frobenius, rw ← hk },
    rw ← finite_field.expand_card,
    unfold char_poly, rw [alg_hom.map_det, ← is_monoid_hom.map_pow],
    apply congr_arg det,
    apply mat_poly_equiv.injective, swap, { apply_instance },
    rw [← mat_poly_equiv.coe_alg_hom, alg_hom.map_pow, mat_poly_equiv.coe_alg_hom,
          mat_poly_equiv_char_matrix, hk, sub_pow_char_pow_of_commute, ← C_pow],
    { exact mat_poly_equiv_eq_X_pow_sub_C (p ^ k) M },
    { exact (C M).commute_X } },
  { congr, apply @subsingleton.elim _ (subsingleton_of_empty_left hn) _ _, },
end

takes 30s on mathlib master. If I change the last three lines to

    { exact (id (mat_poly_equiv_eq_X_pow_sub_C (p ^ k) M) : _) },
    { exact (C M).commute_X } },
  { apply congr_arg, apply @subsingleton.elim _ (subsingleton_of_empty_left hn) _ _, },

it goes down to 2s.

This PR is getting me to meet all the corners of mathlib where weird things are going on!

[Sebastien Gouezel]

#7084 is finally building without timeouts. There is an issue with the tests for transport, though, since it can not transport just by itself the nsmul field (or it can not transport the proof that it is equal to the inductive nsmul). Can this be fixed in transport, or should we use another playground for transport tests (or do you think this PR was a bad idea to begin with)? @Scott Morrison , you wrote transport, right?

[Scott Morrison]

Yes. Sorry, it's been a while since I worked on transport. Last year I had a long todo list of further improvements, but I stopped working on it for a while. I'd like to get back to it, but I think for now we should just change the tests to avoid this situation.

[Scott Morrison]

Hmm.. Actually, I guess this fundamentally breaks transport... :-) I'll see how hard a fix would be.

[Scott Morrison]

@Sebastien Gouezel, do you know if there is some way to ask refine_struct to make use of optional values? This would solve the problem.

[Scott Morrison]

Ah, it was meant to all along, but #2319 accidentally broke it.

[Scott Morrison]

Okay #7143 will fix this problem. I'd suggest just merging it into #7084.

[Scott Morrison]

Unfortunately #7143 doesn't work at all, so I've marked it WIP, and am hoping for some help from Simon.

[Sebastien Gouezel]

I think I've found a workaround, switching to better requirements for nsmul that should be more in line with what transfer can do.

[Sebastien Gouezel]

I've now changed the definition of add_monoid in #7084. It is now

class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M :=
(nsmul : ℕ → M → M := nsmul_rec)
(nsmul_zero' : ∀ x, nsmul 0 x = 0 . try_refl_tac)
(nsmul_succ' : ∀ (n : ℕ) x, nsmul n.succ x = nsmul n x + x . try_refl_tac)

so, just using addition and multiplication to express the properties one wants of nsmul. This is the kind of thing that transfer should like more, and indeed in the tests transfer has no difficulty transferring a semiring instance with this new definition. Some tests are failing, but just because the definition is not the same so there are more fields to fill. @Scott Morrison , I could fix the tests myself but I am not sure what they are testing, so it is maybe better if you have a look yourself. If you trust me to fix them, tell me and I'll do it!

[Scott Morrison]

You mean transport not transfer, right?

[Scott Morrison]

I'll look now.

[Scott Morrison]

I fixed the tests for equiv_rw, but am a bit stumped by the failure of the test for transport. It works for semiring at the top of the file, but then not at the bottom.

[Scott Morrison]

I've also fixed the tests for refine_struct. transport itself really shouldn't care how many fields there are: it works that out for the structure itself.

[Scott Morrison]

Oh!

[Scott Morrison]

The problem is that the second test for transport is transporting between nat and mynat. When it gets to the npow field, it can't tell the difference between the copies of nat that it is meant to transport to mynat (because they are the carrier type of the semiring), and the copies of nat that are referring to powers, and just be left invariant.

[Scott Morrison]

It's late here, but I will try to think about a good solution to this. Not sure at this point.

[Sebastien Gouezel]

Isn't it just that the test is unfortunate here? Doing the same with $\R$ instead of $\N$ should avoid this issue, right?

[Scott Morrison]

Yes.

[Sebastien Gouezel]

I have fixed the test by using the general semiring.map defined at the top of the file (which is defined for a generic ring and therefore not perturbed by the coincidental fact that our ring is $\N$). I hope it's ok.

[Sebastien Gouezel]

There is another test failing in #7084, for ring_exp (hopefully the last one!)

example (a b : ℚ) : (a * b) ^ 1000000 = (b * a) ^ 1000000 := by ring_exp
-- deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

This is probably due to the fact that I changed the definition of powers (now, x ^ n.succ is definitionally x ^ n * x, while it used to be x * x^n). I don't understand the internals of ring_exp enough to be able to fix this. @Anne Baanen , do you think you could have a look or give me a hint where to look?

[Anne Baanen]

It's not supposed to use defeq to unfold pows, instead applying the pow_p_pf_succ family of lemmas. Those still typecheck, right?

[Anne Baanen]

Would it work to fix the previous commit, or should I wait for the new oleans to be built?

[Sebastien Gouezel]

Fixing the previous commit would be perfect.

[Sebastien Gouezel]

Yes, all the lemmas still typecheck, the problem only shows up in this specific test.

[Sebastien Gouezel]

Strangely enough, the test works if one replaces $\mathbb{Q}$ with $\N$, or a general comm_ring.

[Anne Baanen]

The proof term looks like it typechecks too, so it is the last exact that fails.

[Anne Baanen]

I think it's a general bug that ring_exp happens to expose:

def my_op {α : Type*} [comm_semiring α] : α → α := λ a, a ^ 10000000000
example (a : ℚ) : my_op a = a ^ 100000000000 := rfl -- deep recursion detected at replace

[Anne Baanen]

Nevermind, miscopied the number of 0's

[Anne Baanen]

But overall yes, seems that this is an artifact of bad unfolding of the definition of npow. The following works:

local attribute [irreducible] npow_rec

example (a b : ℚ) : (a * b) ^ 1000000 = (b * a) ^ 1000000 := by ring_exp -- works

[Anne Baanen]

Ah, and changing elaboration order by going from example to lemma breaks the my_op example:

def my_op {α : Type*} [comm_semiring α] : α → α := λ a, a ^ 10000
lemma fooQ (a : ℚ) : my_op a = a ^ 10000 := rfl -- deep recursion detected at replace
lemma fooN (a : ℕ) : my_op a = a ^ 10000 := rfl -- works

local attribute [irreducible] npow_rec

lemma fooQ' (a : ℚ) : my_op a = a ^ 10000 := rfl -- works

[Anne Baanen]

Is there an easy way to suggest to lean "when unifying @npow α inst1 x n =?= @npow α inst2 x n, try unifying inst1 with inst2 before unfolding the whole thing"?

[Anne Baanen]

(I guess making npow_rec irreducible is close enough.)

[Anne Baanen]

Here's my attempt at fixing this by making npow_rec irreducible (doesn't build yet because there are still some uses of reducible npow_rec): https://github.com/leanprover-community/mathlib/commit/7dc0d02c8610d881cd33f1605c3315518484b8fb

If we make npow_rec irreducible, we can't prove its properties anymore by try_refl_tac in the instances. I made a new npow_zero_tac and npow_succ_tac that try to apply the correct definitional lemmas. Unfolding npow_rec in try_refl_tac doesn't work always, since it may appear in a form like div_inv_monoid.npow._default.

[Sebastien Gouezel]

What I don't get is why it didn't show up before. Is it that one definition x^(n+1) = x * x^n is optimized by tail-recursion and the other x^(n+1) = x^n * x is not? If this is the case, I should definitely switch back to the original definition. I'd like to avoid putting npow_rec irreducible, because being able to compute small powers by rfl on $\mathbb{N}$ or $\mathbb{Q}$ seems desirable.

[Anne Baanen]

The issue is not with the definition of npow itself, it's the fact that there are many npow fields available, so to unify some_class_extending_monoid.npow with some_other_class_extending_monoid.npow we need to unfold both sides a couple of times. But if one side has a shorter path to npow_rec than another, it will unfold the definition of npow_rec, actually calculating the outcome.

[Anne Baanen]

So the better comparison is: why doesn't this happen for the (+) operator on ℕ?

[Anne Baanen]

Is it just that npow causes the terms to grow exponentially?

[Sebastien Gouezel]

I think it's really a tail-recursion optimization. Look at the following:

def mypow1 {α : Type*} [comm_semiring α] : ℕ → α → α
| 0 x := 1
| (n+1) x := mypow1 n x * x

def haspow1 : has_pow ℚ ℕ := ⟨λ x n, mypow1 n x⟩
def my_op1 {α : Type*} [comm_semiring α] : α → α := λ a, mypow1 10000 a
lemma foo1 (a : ℚ) : my_op1 a = @has_pow.pow ℚ ℕ haspow1 a 10000  := rfl -- deep recursion detected at replace

def mypow2 {α : Type*} [comm_semiring α] : ℕ → α → α
| 0 x := 1
| (n+1) x := x * mypow2 n x

def haspow2 : has_pow ℚ ℕ := ⟨λ x n, mypow2 n x⟩
def my_op2 {α : Type*} [comm_semiring α] : α → α := λ a, mypow2 10000 a
lemma foo2 (a : ℚ) : my_op2 a = @has_pow.pow ℚ ℕ haspow2 a 10000  := rfl -- works

Exact same definition for both, but one with left multiplication and the other one with right multiplication. One works, the other fails.

[Sebastien Gouezel]

I'll switch back to the other direction, even if it makes some things more painful.

[Sebastien Gouezel]

(And I'll add a comment explaining why it has to be done this way).

[Anne Baanen]

Huh, but the recursive call isn't in tail position for those definitions.

[Sebastien Gouezel]

It might depend on how multiplication is defined, no?

[Anne Baanen]

This is always a "proper" tail-recursive definition, but still fails:

def mypow3 {α : Type*} [comm_semiring α] : ℕ → α → α → α
| 0 x acc := acc
| (n+1) x acc := mypow3 n x (acc * x)

def haspow3 : has_pow ℚ ℕ := ⟨λ x n, mypow3 n x 1⟩
def my_op3 {α : Type*} [comm_semiring α] : α → α := λ a, mypow3 10000 a 1
lemma foo3 (a : ℚ) : my_op3 a = @has_pow.pow ℚ ℕ haspow3 a 10000 := rfl -- deep recursion detected at replace

[Sebastien Gouezel]

Really weird...

[Anne Baanen]

Looking at the set_option trace.type_context.is_def_eq_detail true, for some reason Lean really wants to unfold only the mypow3 on the right hand side:

[type_context.is_def_eq_detail] [2]: a ^ 10000 =?= my_op3 a
[type_context.is_def_eq_detail] unfold right: my_op3
[type_context.is_def_eq_detail] [3]: a ^ 10000 =?= mypow3 10000 a 1
[type_context.is_def_eq_detail] unfold right: mypow3
[type_context.is_def_eq_detail] [4]: a ^ 10000 =?= mypow3 (5000.add (2500.add (1250.add (62
5.add (624.add 0))))) a (1 * a)
[type_context.is_def_eq_detail] unfold right: mypow3
[type_context.is_def_eq_detail] [5]: a ^ 10000 =?= mypow3 (5000.add (2500.add (1250.add (62
5.add (312.add (156.add (78.add (39.add (38.add 0))))))))) a (1 * a * a)
[type_context.is_def_eq_detail] unfold right: mypow3
[type_context.is_def_eq_detail] [6]: a ^ 10000 =?= mypow3 (5000.add (2500.add (1250.add (62
5.add (312.add (156.add (78.add (39.add (19.add (18.add 0)))))))))) a
  (1 * a * a * a)
[type_context.is_def_eq_detail] unfold right: mypow3
[type_context.is_def_eq_detail] [7]: a ^ 10000 =?= mypow3 (5000.add (2500.add (1250.add (62
5.add (312.add (156.add (78.add (39.add (19.add (9.add (8.add 0))))))))))) a
  (1 * a * a * a * a)
[type_context.is_def_eq_detail] unfold right: mypow3
[type_context.is_def_eq_detail] [8]: a ^ 10000 =?= mypow3
  (5000.add
     (2500.add (1250.add (625.add (312.add (156.add (78.add (39.add (19.add (9.add (4.add (
2.add (1.add 0)))))))))))))
  a
  (1 * a * a * a * a * a)
[type_context.is_def_eq_detail] unfold right: mypow3
...

[Anne Baanen]

(From the Lean source: because mypow3 can be delta-reduced, and has_pow.pow cannot?)

[Anne Baanen]

So we actually want non-tail recursive definitions? It looks like, for foo2, they block the delta-reducing:

[type_context.is_def_eq_detail] [2]: a ^ 10000 =?= my_op2 a
[type_context.is_def_eq_detail] unfold right: my_op2
[type_context.is_def_eq_detail] [3]: a ^ 10000 =?= mypow2 10000 a
[type_context.is_def_eq_detail] unfold right: mypow2
[type_context.is_def_eq_detail] [4]: a ^ 10000 =?= a * mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a
[type_context.is_def_eq_detail] [5]: (λ (x : ℚ) (n : ℕ), mypow2 n x) a 10000 =?= distrib.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] after whnf_core: mypow2 10000 a =?= distrib.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] unfold left: mypow2
[type_context.is_def_eq_detail] [6]: a * mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a =?= distrib.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [7]: distrib.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= semiring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [8]: semiring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= comm_semiring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [9]: comm_semiring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= comm_ring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [10]: comm_ring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= euclidean_domain.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [11]: euclidean_domain.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= a * mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a
[type_context.is_def_eq_detail] [12]: a * mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a =?= distrib.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [13]: distrib.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= ring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [14]: ring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= division_ring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [15]: division_ring.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= field.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a)
[type_context.is_def_eq_detail] [16]: field.mul a (mypow2 (5000.add (2500.add (1250.add (625.add (624.add 0))))) a) =?= a.mul (mypow2 (5000.add (2500.add (1250.add (625.add (624.add : ...

[Eric Wieser]

Would an id_delta help? edit: I can't see a way

[Sebastien Gouezel]

I'll just switch to the mypow2 definition, which works fine.

[Eric Wieser]

This is probably worth filing as a github issue since you have a MWE, just so it doesn't get forgotten

[Anne Baanen]

lean#563