Type checking time correlates with value in expression

Stream: lean4

[Daniil Kisel]

Type checking this code takes 4.6s and ~1GB mem on my pc:

def f : Bool :=
  let x := (480 : UInt32) |>.toUInt8
  if h: x < 24
    then
      have hh : x.toNat < 24 := h
      true
    else
      false

How can I make it faster and less memory consuming? I don't understand why the value (480) affects type checking time (bigger ~ slower). On 900 it takes 23.3s and 4GB.

[Alex J. Best]

The issue appears to be the have hh line if you comment that the tc is way faster.
Likely this ends up asking the kernel to do too much unfolding, or compute something in an inefficient way by saying that the type of h is defeq to that of hh.
If you replace things with a proof that makes use of tactics rather than defeq, e.g.

by  simpa [x] using h

it works way faster for me

[Daniil Kisel]

If I replace h with by simpa [x] using h it outputs error
"invalid 'simp', proposition expected
UInt8"..

[Alex J. Best]

Oh right the simpa tactic is in Std I guess.
You can use

 by
        simp [x] at h ⊢
        exact h

for a pure lean equivalent

[Daniil Kisel]

I did import Std though

[Kyle Miller]

You're probably using an older version of Lean 4. It was the last couple months where you could do simp [x] with x a local definition.

[Alex J. Best]

import Std
def f : Bool :=
  let x := (900000 : UInt32) |>.toUInt8
  if h: x < 24
    then
      have hh : x.toNat < 24 := by simpa [x] using h
      true
    else
      false

works in the web editor, so I think Kyle must be right

[Daniil Kisel]

I'm on v4.2.0, I'll try with 4.3.0-rc2 now

[Alex J. Best]

If you are on an older version then maybe you can just get rid of the [x] even

[Kyle Miller]

I don't understand why by simp [x]; exact h makes this fast. With no imports, all it's doing is unfolding x.

[Daniil Kisel]

Yes, works in an instant, thanks!

[Alex J. Best]

yeah indeed id h also works instantly :mind_blown:

[Kyle Miller]

Maybe it's somehow tricking it to unfold definitions rather than evaluating them on this particular x...

If you unfold all the definitions, you have

h: { val := Fin.ofNat 480.val.val } < 24
⊢ (Fin.ofNat 480.val.val).val < 24

where the first is a UInt8 less-than.

[Daniil Kisel]

It seems like neither id nor simpa work in the original context, here is another example:

def f (h0 : Char): Unit :=
  let x := h0.val - '0'.val |>.toUInt8
  if h: x < 24
    then
      have hh : x.toNat < 24 := id h -- by simpa [x] using h
      ()
    else
      ()

Replacing h0.val - '0'.val with a constant or with h0.val makes it instant, making h0 constant is the same...

[Alex J. Best]

def f (h0 h1 : Char) : Unit :=
  let x := (h0.val - '0'.val) * 10 + (h1.val - '0'.val) |>.toUInt8
  if h: x < 24
    then
      have hh : x.toNat < 24 := by
        rw [UInt8.toNat]
        exact h
      ()
    else
      ()

works for me

[Daniil Kisel]

Works in the context, thanks again! But why does it loop in the first place, or when I replace rewrite with unfold?

[Mario Carneiro]

Profiler says that most of the time is spent in the kernel typechecker; I'm running it through lean4lean to get some more logging but it seems like Nat.mod is unfolded at some point and thereafter whnf tries to run the underlying WF definition

[Mario Carneiro]

Looks like the issue is that the kernel typechecking goal is

example :
  let x := UInt32.toUInt8 400
  UInt8.toNat x = Nat.mod (UInt32.toNat 400) (255 + 1) := by intro x; rfl

and the heuristic for determining whether to use the Nat.mod kernel accelerated definition is that both sides of the equality have no fvars, including fvars with definitions. So Nat.mod is unfolded instead, and thereafter comes 400 steps and a massive expression at each step