unexpected error on #reduce

Stream: lean4

[Asei Inoue]

def foo (x : String) := "hello, " ++ x

#check foo "hello"

#eval foo "hello"

/-
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#reduce foo "hello"

[Asei Inoue]

why this error occurs?

[Kevin Buzzard]

Because Unicode is huge?

[Asei Inoue]

@Kevin Buzzard maybe...?

def square (x : Int) := x * x

-- this does not throw error
#reduce square 19

[Eric Wieser]

Here's a more minimal #mwe:

#reduce Char.ofNat (nat_lit 0) -- fails

[Eric Wieser]

https://github.com/leanprover/lean4/issues/4465

[Henrik Böving]

This is probably because it needs to execute docs#Nat.isValidChar which executes less than with a very wide range of bounds. The decision procedure that's synthesized for this has an efficient extern but no efficient kernel implementation. Unless you can convince core to add native support for reducing docs#Nat.ble in the kernel there is pretty much no chance of this working out.

[Henrik Böving]

Asei Inoue said:

Kevin Buzzard maybe...?

def square (x : Int) := x * x

-- this does not throw error
#reduce square 19

This on the other hand works out because it is backed by Nat.mul which does already have a native kernel implementation

[Mario Carneiro]

Henrik Böving said:

This is probably because it needs to execute docs#Nat.isValidChar which executes less than with a very wide range of bounds. The decision procedure that's synthesized for this has an efficient extern but no efficient kernel implementation. Unless you can convince core to add native support for reducing docs#Nat.ble in the kernel there is pretty much no chance of this working out.

Not exactly. These definitions compute well enough in the kernel, but the problem is that #reduce also reduces proofs, and does not stop until it reaches a normal form. What is the normal form of a proof of 0 <= 0x10FFFF? It's a sequence of 0x10FFFF applications of Nat.le.step, so it's impossible for #reduce not to take that long because the correct output itself is huge.

[Mario Carneiro]

I guess if you apply toNat to the result it will be fast again

[Mario Carneiro]

It's a little more complicated to do this for strings but this works:

def foo (x : String) := "hello, " ++ x

#check foo "hello"

#eval foo "hello"

#reduce (foo "hello").data.map Char.toNat
-- [104, 101, 108, 108, 111, 44, 32, 104, 101, 108, 108, 111]