Deep recursion in mathlib but not in lean core

Stream: mathlib4

[Jeremy Tan]

In #31315 I need to prove a power tower inequality. To avoid deep recursion @Joachim Breitner suggested in lean4#11713 the following code:

theorem tower_inequality : 2010 ^ 2010 ^ 2010 ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ 11 := by
  calc
    _ ≤ 2 ^ (11 * 2010 ^ 2010) := by
      generalize h : 2010 ^ 2010 = p
      rw [Nat.pow_mul, Nat.pow_le_pow_iff_left <| Nat.ne_of_gt (by subst h; apply Nat.pow_pos (by decide))]
    _ ≤ _ := Nat.pow_le_pow_right Nat.zero_lt_two ?_
  calc
    _ ≤ 2 ^ (4 + 11 * 2010) := by
      generalize h : 2010 = p
      rw [Nat.pow_add, Nat.pow_mul]
      exact Nat.mul_le_mul (by decide) (Nat.pow_le_pow_left (by subst h; decide) _)
    _ ≤ _ := Nat.pow_le_pow_right Nat.zero_lt_two ?_
  calc
    _ ≤ 2 ^ 2 ^ 2 ^ 2 := by decide
    _ ≤ _ := by
      iterate 3 apply Nat.pow_le_pow_right Nat.zero_lt_two
      decide

It works – in isolation. When I paste this into my file in #31315 the (kernel) deep recursion detected error reappears.

As I note in lean4#11713, if I import Mathlib.Algebra.Group.Nat.Defs the deep recursion error appears, but not if I import Mathlib.Algebra.Group.Defs (the former file's sole import is the latter file).

What do I do?

[Joachim Breitner]

(The last lean4 PR number has a typo)

[Jeremy Tan]

Joachim Breitner said:

(The last lean4 PR number has a typo)

:squared_ok:

[Joachim Breitner]

This is weird. Does it help to replace ^ with Nat.pow, to avoid type class resolution? Maybe the

instance instCommMonoid : CommMonoid ℕ where

makes a difference?

You could copy your theorem into import Mathlib.Algebra.Group.Nat.Defs and move it up command by command in that file to find out more.

[Joachim Breitner]

Yes, instance instCommMonoid : CommMonoid ℕ where makes a difference somehow

[Joachim Breitner]

And somehow

--- a/Mathlib/Algebra/Group/Nat/Defs.lean
+++ b/Mathlib/Algebra/Group/Nat/Defs.lean
@@ -46,10 +46,29 @@ instance instCommMonoid : CommMonoid ℕ where
   one_mul := Nat.one_mul
   mul_one := Nat.mul_one
   mul_comm := Nat.mul_comm
-  npow m n := n ^ m
+  npow m n := Nat.pow n m
   npow_zero := Nat.pow_zero
   npow_succ _ _ := rfl

fixes it

[Joachim Breitner]

Also, before the instance:

(@HPow.hPow Nat Nat Nat (@instHPow Nat Nat (@instPowNat Nat instNatPowNat))

after the instance:

(@HPow.hPow Nat Nat Nat (@instHPow Nat Nat (@Monoid.toNatPow Nat (@CommMonoid.toMonoid Nat instCommMonoid)))

This doesn't look like a good instance synthesis decision.

[Joachim Breitner]

:bulb: Ah, and probably somewhere lean now needs to prove that these two are defeq, and in the process starts evaluating large numbers.

[Jeremy Tan]

Joachim Breitner said:

And somehow

-  npow m n := n ^ m
+  npow m n := Nat.pow n m

fixes it

I don't know if this is a good fix or not

[Robin Arnez]

Can you not just omit that line?

[Robin Arnez]

Oh right no that's different

[Robin Arnez]

Well it seems like we use Nat.add above in the same file so using Nat.pow directly doesn't seem too far fetched

[Tomaz Mascarenhas]

Does something like

theorem tower_inequality (m1 m2 : Nat) (hm1 : m1 = 2010) (hm2 : m2 = 11) : 2010 ^ 2010 ^ m1 ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ m2 := by ...

helps?

I had a similar problem once and I remember using this to be able to avoid the kernel to crash

[Jeremy Tan]

Tomaz Mascarenhas said:

Does something like

theorem tower_inequality (m1 m2 : Nat) (hm1 : m1 = 2010) (hm2 : m2 = 11) : 2010 ^ 2010 ^ m1 ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ m2 := by ...

helps?

I had a similar problem once and I remember using this to be able to avoid the kernel to crash

YES, it works. I have pushed it to #31315, and it now looks ready to be merged