whnf blowup in Nat.digits

Stream: mathlib4

[David Renshaw]

Pertaining to Archive/Imo/Imo1962Q1.lean, which is one of the broken files in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/request.20for.20help.20with.20failure.20in.20Archive/near/399646876:

import Mathlib.Data.Nat.Digits

set_option trace.Meta.whnf true in
example : Nat.digits 10 15 = [5, 1] := by
  norm_num -- succceds, but with more than 24600 lines of whnf traces

The sheer size of that trace output makes me suspicious.

[David Renshaw]

lots of stuff like

[Meta.whnf] match decEq ((14 + 1) % (8 + 2)) 5 with
    | isTrue hab =>
      match
        List.hasDecEq
          ((fun y a ↦
              Acc.rec
                (fun x₁ h ih ↦
                  (fun a a_1 ↦
                      (match (motive :=
                          (x : ℕ) →
                            ((y : ℕ) → (invImage (fun a ↦ sizeOf a) instWellFoundedRelation).1 y x → List ℕ) → List ℕ)
                          a with
                        | 0 => fun x ↦ []
                        | Nat.succ n => fun x ↦ (n + 1) % (8 + 2) :: x ((n + 1) / (8 + 2)) _)
                        a_1)
                    x₁ ih)
                _)
            ((14 + 1) / (8 + 2)) _)
          [1] with
      | isTrue habs => isTrue _
      | isFalse nabs => isFalse _
    | isFalse nab => isFalse _

[David Renshaw]

Anyone have any ideas about how I might drill down on this further?

[David Renshaw]

Or maybe this isn't actually suspicious, and I'm barking up the wrong tree?

[Mario Carneiro]

it's because norm_num doesn't implement Nat.digits

[David Renshaw]

Do we need to implement a norm_digits tactic?

[David Renshaw]

norm_num currently can't output a value of list type.

[David Renshaw]

it's because norm_num doesn't implement Nat.digits

right, so this is falling back on simp where the mathlib3 version had some tailored norm_num logic.
I guess all that extra whnf form work has to do with simp trying to figure out what steps to take?

[Mario Carneiro]

simp called decide and decide is doing the whnf work

[Mario Carneiro]

I'm currently working on a new tactic that will be much more general than norm_num and can potentially evaluate Nat.digits without a custom implementation, but I can also look into a smaller addition to norm_num to allow it to do reductions in other types

[Mario Carneiro]

#8100 implements norm_num framework support for inductive types

[David Renshaw]

At a high level, I'm still confused about why we need to write special tactic code to reduce functions like Nat.digits. The function is already defined in a perfectly computational way, and #eval has no trouble with it.

[Jireh Loreaux]

(I think) it's because kernel reduction is currently inefficient, but IIUC, this is one of the things Joachim is going to be working on.

[Joachim Breitner]

Hopefully, but maybe not at first, so don’t hold your breath.

[David Renshaw]

Simpler setup, with no norm_num:

import Mathlib.Data.Nat.Digits

set_option trace.Meta.whnf true in
example : Nat.digits 10 25 = [5, 2] := rfl
-- more than 50,000 lines of Meta.whnf traces

[Sebastian Ullrich]

It's only 13ms in total though, no? (with just trace.profiler, which adds its own overhead)

[David Renshaw]

sure, it's fast without the trace

[David Renshaw]

but it hits the maxRecDepth quickly if I make the inputs larger

[David Renshaw]

import Mathlib.Data.Nat.Digits

example : Nat.digits 10 1256 = [6, 5, 2, 1] := rfl
-- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

[David Renshaw]

Maybe some reduction function in the Lean core is supposed to be tail recursive, but isn't?

[David Renshaw]

Am I being unreasonable for expecting to be able to normalize Nat.digits 10 1256 by rfl? It seems like it should not be a very big computation.

[Kyle Miller]

I have a guess that it's due to how the decreasing_by is being compiled for the kernel -- doesn't this mean that it computes Nat.digits 10 for all numbers up to 1256 and then selects this last value?

[Kyle Miller]

Here's another implementation that recurses on a gas variable instead, and it can handle big numbers fine:

def Nat.digitsAux (gas : Nat) (b : Nat) (n : Nat) : List Nat :=
  match gas with
  | 0 => []
  | gas' + 1 =>
    let q := n / b
    if q < n then
      n % b :: Nat.digitsAux gas' b q
    else
      []

def Nat.digits (b : Nat) (n : Nat) : List Nat :=
  match b with
  | 0 =>
    match n with
    | 0 => []
    | _ => [n]
  | 1 => List.replicate n 1
  | _ => Nat.digitsAux n b n


example : Nat.digits 10 1234567890 = [0, 9, 8, 7, 6, 5, 4, 3, 2, 1] := rfl

[Kyle Miller]

You can remove the gas variable and Lean can still see it terminates, but then that example hits max recursion depth.

def Nat.digitsAux (b : Nat) (n : Nat) : List Nat :=
  let q := n / b
  if q < n then
    n % b :: Nat.digitsAux b q
  else
    []

def Nat.digits (b : Nat) (n : Nat) : List Nat :=
  match b with
  | 0 =>
    match n with
    | 0 => []
    | _ => [n]
  | 1 => List.replicate n 1
  | _ => Nat.digitsAux b n


example : Nat.digits 10 1234567890 = [0, 9, 8, 7, 6, 5, 4, 3, 2, 1] := rfl -- maximum recursion depth has been reached

[Joachim Breitner]

With gas, it’s using structural recursion, without it’s using well-founded recursion. I thought the latter doesn't even reduce definionally, but it seems the kernel can somehow evaluate it, but obviously much slower. I wonder (blind guess) if the kernel is explicitly constructing the Acc predicate provided by WellFoundedRelation for the argument number?

[David Renshaw]

I thought this was an interesting topic, so I investigated a bit more deeply and I made a video explaining what I learned: https://www.youtube.com/watch?v=FOt-GsiNJmU

[Eric Rodriguez]

Thanks for the really interesting video David! It led to a very naive question for me - why does the kernel have to expand and typecheck the proof of docs#Nat.lt_wfRel out at all?

[David Renshaw]

My understanding is:

1. WellFounded is only used to kick things off. Once the recursion gets going, it's all in terms of Acc
2. If the recursion is at value n and needs to step to value m, then it has an Acc n and needs to use it to get an Acc m. I think it's that conversion where all the proof reduction happens.
3. This all seems kind of silly, because we have an ambient WellFounded floating around in the typeclass system, so it feels like we ought to be able to ask it directly for an Acc m, rather than reducing our existing proof term.

[David Renshaw]

I want to emphasize that my understanding is only hazy, and I love it if someone who's more of an expert on these things could explain better.

[David Renshaw]

To take a step back, though: Acc.rec is where the recursion is coming from. It accepts an argument of type Acc, and for its reduction rule to fire, that argument must be normalized to a form Acc.intro ....

[Eric Rodriguez]

It seems to me that the fact that docs#WellFoundedRelation is in Sort is the cause of all this

[Eric Rodriguez]

(which of course it must be, but if the relation is unbundled as in just docs#WellFounded it should just be able to take the correct steps - theoretically?)

[Eric Rodriguez]

I see, so I just realised - Acc.rec wants a normalised form to be able to actually reduce the recursor. But as a one field Prop structure, there is no actual need for this in reality; but I'm guessing this requires special kernel support, either for Acc specifically or one-constructor Prop structures more generally.

[Eric Rodriguez]

I think some thought has been put into trying to maximise performance: using a very rudimentary testing setup, replacing the definition of Nat.lt_wfRel.wf with alternative options, there's no clear-cut way to make this faster (and indeed, as expected, using sorry to force Lean to not bother reducing the Acc constructors makes #reduce blazing fast)

[Mario Carneiro]

David Renshaw said:

This all seems kind of silly, because we have an ambient WellFounded floating around in the typeclass system, so it feels like we ought to be able to ask it directly for an Acc m, rather than reducing our existing proof term.

The kernel is really myopic, it is in the middle of running whnf on a term and has no idea what is in your context, much less what the typeclass system thinks

[Mario Carneiro]

I have thought about having the kernel use docs#Acc.inv to produce a proof of Acc r m from Acc r n, which would avoid ever having to reduce proofs, but the proofs get larger at every step. If there was some way of mixing a WellFounded fact in there somehow then the proof could be constant size across the recursion, which sounds nice

[Mario Carneiro]

the downside of all these schemes is that they lead to undecidable typechecking, because if you are in an inconsistent context then you can still use whnf on false Acc proofs of termination and loop forever. However this is already a problem with the current system (it's unavoidable as long as Acc is a large-eliminating Prop) which is currently addressed by making Acc only reduce if the proof term reduces to a constructor, so it would get stuck if it was a false hypothesis or axiom. There is a discussion about this in #leantt

[Eric Rodriguez]

Oh, so this is why I couldn't get rfl to work on small terms with my sorried version even when reduce did

[Eric Rodriguez]

Mario Carneiro said:

I have thought about having the kernel use docs#Acc.inv to produce a proof of Acc r m from Acc r n, which would avoid ever having to reduce proofs, but the proofs get larger at every step. If there was some way of mixing a WellFounded fact in there somehow then the proof could be constant size across the recursion, which sounds nice

Isn't this what happens already? The proof of nat wf uses it

[Mario Carneiro]

not sure what you mean

[Mario Carneiro]

what I'm saying is that when you have a term wf : WellFounded R which is opaquified in some way, then we want reducing wf.apply n : Acc R n to a constructor to result in Acc.intro n fun y h => wf.apply y rather than some more complicated (but definitionally equal because of proof irrelevance) term in place of wf.apply y

[Mario Carneiro]

Note that we can't really do this for Acc R n terms directly, because we don't have any easy way to describe Acc R y except in terms of the original h : Acc R n term, so you end up with a more complicated term which uses h on the RHS. Compare:

example {R : T → T → Prop} {wf : WellFounded R} :
    wf.apply n = Acc.intro n fun y _ => wf.apply y := rfl
example {R : T → T → Prop} {h : Acc R n} :
    h = Acc.intro n (fun _ => Acc.inv h) := rfl

[Mario Carneiro]

(imagine these are rewrite rules from left to right applied lazily by whnf)

[Mario Carneiro]

Both of these methods are IMO better than the current approach of unfolding h (which is a proof), exposing lots of implementation details and usually getting stuck on an axiom eventually anyway

[Mario Carneiro]

@David Renshaw I really liked the video, it is very well produced and you explained things well. I was also very interested to see your lean4lean modification for visualizing kernel reduction, I have wanted that for a very long time. You should make it available somewhere!

[Eric Rodriguez]

This seems to have no effect with the rudimentary testing setup linked above, although to my eyes it does seem that it should be far faster to do this. It'd be nice to have David's modification to see the proof terms! I also realised that some of the examples I sent in this file yesterday don't seem to reduce, but for example h_UC uses no axioms so should not be blocked!

[Mario Carneiro]

I'm not sure what you are saying you tried

[Mario Carneiro]

what I described is a change to the kernel reduction algorithm

[Eric Rodriguez]

I just tried inlining the such a definition, which should have a similar enough effect?

[Eric Rodriguez]

Or does stuff get unfolded still

[Mario Carneiro]

which definition?

[Mario Carneiro]

the kernel will unfold definitions when needed, so generally that won't make any difference

[Eric Rodriguez]

My file just contains various different proofs of ∀ (a : ℕ), Acc Nat.lt a to try and understand a bit, so if my understanding wasn't flawed then setting this to Acc.intro n fun y _ => wf.apply y shouldn't be too bad; but now I guess that if you don't have this as a rewrite rule within the kernel then after one layer of peeling you're straight back to the original issue

[Mario Carneiro]

exactly

[Mario Carneiro]

Normally reduction will proceed by first reducing the Acc proof to Acc.intro of something, then stepping the Acc.rec function once, then reducing the user function f until evaluation reaches uses of the IH, and then repeat

[Mario Carneiro]

and the question is whether it is possible to adjust the first step so that the amount of computation needed is minimal and the terms don't grow unnecessarily

[Eric Rodriguez]

I understand that type-theoretically it's bad to have the kernel have even more undecidable type-checking, but is this actually a problem in practice? Practically all that will happen is that we get timeouts during rfl, which we already do in cases where we really would like these statements to reduce anyways, so it seems we're no better off avoiding the issue

[Mario Carneiro]

I tend to agree with that

[Mario Carneiro]

especially since "even more undecidable" is not particularly interesting to type theorists

[Mario Carneiro]

the practical upshot would be that WF definitions compute by rfl just as well as structural recursions, which sounds like a very useful property

[Mario Carneiro]

Note that when I wrote lean4lean I made it structurally terminating by just indiscriminately turning every non-structural recursion into a recursion with 1000 iterations and I could check mathlib just fine

[Mario Carneiro]

So apparently mathlib does not depend on deep recursion in reduction

[Mario Carneiro]

That probably isn't always the case, I'm sure if we had more coq style proofs by reflection we might need to increase the limit in some places

[Eric Rodriguez]

I mean considering how slow this recursion is at the moment (and in Lean3 wasn't it just stuck indiscriminately?) it's not at all surprising to me that Mathlib doesn't seem to use it