deep recursion

Stream: new members

[Richard Copley]

I get a "(kernel) deep recursion detected" error, in the last def in this code:

import Mathlib.Data.Int.Basic
import Mathlib.Tactic.NormNum

def prop0 (x : ℤ) := x ≠ 0
def prop1 (x : ℤ) := x.natAbs / 2 ^ (Nat.size (x.natAbs) - 24) * 2 ^ (Nat.size (x.natAbs) - 24) = x.natAbs

inductive float where
  | normal (val : {x : ℤ // prop0 x ∧ prop1 x})

-- Can construct a `float` from the value `(2 ^ 23 : ℤ)`:

theorem has_prop0 : prop0 (2 ^ 23) := by
  unfold prop0
  simp

theorem has_prop1 : prop1 (2 ^ 23) := by
  unfold prop1
  rewrite [(by rfl : (2 ^ 23 : ℤ).natAbs = 2 ^ 23)]
  rewrite [Nat.size_pow]
  norm_num

def x₀ : float := float.normal ⟨2 ^ 23, has_prop0, has_prop1⟩

-- Cannot construct from same value if the proof of `prop1 val` is inlined:

def x₁ : float :=
--  ~~ error: "(kernel) deep recursion detected"
  let val : ℤ := 2 ^ 23
  have h₀ : prop0 val := has_prop0
  have h₁ : prop1 val := by
    unfold prop1
    rewrite [(by rfl : val.natAbs = 2 ^ 23)]
    rewrite [Nat.size_pow]
    norm_num
  float.normal ⟨val, h₀, h₁⟩

Why does this happen? Is there a well-known way to avoid it? If not, can you give me any hints on how to get more details about the recursion from Lean, for debugging?

[Kevin Buzzard]

Using rfl and large numbers is dangerous. Changing it to this

    rewrite [(by norm_num : val.natAbs = 2 ^ 23)]

works.

[Richard Copley]

Perfect, thanks.