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

[David Renshaw]

Mario Carneiro said:

David Renshaw 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!

It currently has zero polish and is not really intended for external consumption, but here it is: https://github.com/dwrensha/lean4lean/tree/reduce-cmd

[Eric Rodriguez]

do you guys think it's worth writing an RFC/issue requesting Acc/one constructor Props's recursors to be expanded eagerly in the kernel?

[David Renshaw]

It started to get rather ugly when I made it so that it returns a trace even when the reduction throws an exception.

[David Renshaw]

Mario Carneiro said:

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

Sounds good to me, as long as the cost isn't: "now writing a third-party typechecker is much more difficult".

[Joachim Breitner]

Mario Carneiro said:

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

I’m out of my depth here, so this is more about me learning more…

If I understand you correctly, it would be great if a definition like this

def WellFounded.apply' {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (x : α) : Acc r x :=
  Acc.intro x (fun y _ => wf.apply' y)

would unfold as such in the kernel, so that recursive definitions can recurse on that one (rather than wf.apply which could lead to complex proofs).

But of course that definition isn’t accepted, because it’s recursive. One could try to write a function that traverses the “Acc tree” and replace all proofs by a “short expression”, maybe like this

def WellFounded.apply' {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (x : α) : Acc r x :=
  Acc.rec (fun x _ _ => Acc.intro x (fun y _h => wf.apply y)) (wf.apply x)

but that just moves the issue around: To see these nicerAcc.intro constructors, the kernel would have to unfold this proof, and we still end up with the large proofs from wf.apply.

Is that correct so far?

[Mario Carneiro]

Yes. My idea behind making WellFounded.apply' work would be to make it magic in the kernel, it would perform that reduction instead of the real one when coming across that particular constant

[Mario Carneiro]

Note that this does not involve any new definitional equalities, because WellFounded.apply' is a proof

[Mario Carneiro]

The natural definition which would have the right properties here is:

opaque WellFounded.apply' {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (x : α) : Acc r x :=
  wf.apply x

theorem WellFounded.apply'_iota {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (x : α) :
  wf.apply' x = Acc.intro x (fun y _ => wf.apply' y) := rfl

[Mario Carneiro]

making it opaque ensures that apply' is exposed when we want it to be and does not have any unexpected reductions, and then apply'_iota is a built in reduction rule

[Mario Carneiro]

note: you would have to turn this reduction off in #reduce I think, or else it would trivially loop

[David Renshaw]

I posted a website with an example kernel reduction trace (minus3 7) here: https://dwrensha.github.io/kernel-reduction-explosion/ . (Warning: the data payload is > 75MB.)

[Mario Carneiro]

yeah, debugging these traces is fun and blows up vscode a lot

[Mario Carneiro]

I also have a half baked logging branch of lean4lean but the one you demoed looks a lot better than mine

[David Renshaw]

The raw json for this trace is 16MB. The syntax highlighting is what makes it really heavy. (I'm using pygments.)

[Arthur Paulino]

I just want to acknowledge that this is the best video about Lean 4 in terms of production quality I've seen so far :exploding_head:
Good dynamics, audio capture, frame rate, font size, editing etc :pinched:

[Joachim Breitner]

I agree, great video. Good speed, too :-)

Small technical comment: Proof erasure is not why the IR code for well-founded recursion doesn’t blow up. The actual reason is that there is a fork in the Expr pipeline. The definitions are first elaborated to PreDefinition, which can be recursive.
The path towards the compiler forrks here, and IR, IR interpreter and compiler then simply process recursive definitions. This is also why partial or unsafe recursive definitions work in #eval.
The other path goes towards the kernel, and the (recursive) PreDefinitions are then elaborated some more into non-recursive definitions using .brec or WellFounded.fix etc.

[David Renshaw]

Interesting! I wonder whether there is a way to cause any kind of proof-term reduction to happen during an #eval...

[David Renshaw]

It would be fun to see an example where #eval is slow but the compiled native code is fast.

[Kyle Miller]

My understanding is that #eval t puts t through the compiler pipeline to create IR, and then this IR is evaluated by a virtual machine. By that point, there are no proofs.

The difference between #eval and native compilation is that this IR isn't translated to C and then compiled.

[Mario Carneiro]

David Renshaw said:

It would be fun to see an example where #eval is slow but the compiled native code is fast.

One case where this happens is when using naive recursive algorithms, because #eval and the compiler do exactly what you say here while the kernel uses brecOn which is "accidentally" a memoizing computation.

def fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fib n + fib (n + 1)

#reduce fib 30 -- fast
#eval fib 30   -- slow

[Mario Carneiro]

er, I guess that's not exactly what you asked for, since you compared #eval to native code, not to kernel computation

[David Renshaw]

right, I expect the native code for that to be slow too

[Mario Carneiro]

well it's not that hard to find examples where #eval is slower than compiled C code, this is the normal case. But maybe you mean asymptotically?

[David Renshaw]

yeah, like how Nat.digits takes O(n^2) time with #reduce, but O(log(n)) time with #eval.

[David Renshaw]

I do remember seeing that fib example in TPIL4: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html#structural-recursion-and-induction

[Mario Carneiro]

do get a difference there it would have to be a low level optimization. The interpreter is supposed to have the same general performance profile as the compiler, but the compiler also involves some additional optimization passes (some in lean, some in clang/LLVM) and some of them change the asymptotic behavior of the code

[David Renshaw]

The interpreter is supposed to have the same general performance profile as the compiler

Cool, then I think the diagrams in my video still make sense, even if as a minor oversimplification. :sweat_smile:

[Joachim Breitner]

Yes, absolutely! I didn’t mean to say that it’s wrong in any serious sense.

[Mario Carneiro]

Here's an example:

partial def foo (i b : UInt64) : UInt64 :=
  if i == 0 then b else foo (i - 1) (b + 1)

#eval foo 10000000 0

def main (args : List String): IO Unit := do
  let x ← IO.getNumHeartbeats
  let n := args.getD 0 "10000000" |>.toNat!
  println! foo n.toUInt64 0

I was able to confirm by disassembling the binary that foo is compiled to a nonrecursive function, def foo i b := i + b, but lean misses this optimization so #eval is linear time while lake exe test NNN is constant time

[David Renshaw]

nice

[Johan Commelin]

@David Renshaw Thanks a lot for making that video! Very instructive and entertaining!

[Newell Jensen]

Yes, well done @David Renshaw

[David Renshaw]

What I'm curious about now is: how do other dependently-typed languages, like Coq and Agda, handle this kind of situation? Do they support well-founded recursion interacting with definitional equality any better than Lean currently does?

[Mario Carneiro]

I think they don't really have well founded recursion in lean's sense

[Eric Rodriguez]

These languages have decidable type-checking, right? So they should just be able to unfold an Acc.rec application eagerly, without having to unfold it into (Acc.intro ...).rec?

[Mario Carneiro]

Coq at least is much more careful to use "binary nats" (i.e. docs#Num) for kernel computation, which is to say that they don't handle it any better and the libraries worked around it

[Mario Carneiro]

that said, Coq's kernel is much better than lean's for doing heavy reduction

[Mario Carneiro]

@Eric Rodriguez I don't understand what you mean by that, or what that has to do with decidable typechecking

[Mario Carneiro]

I think the short answer is that Acc would not be in Prop in Coq/Agda

[Mario Carneiro]

so you would still be reducing it to Acc.intro but it wouldn't be a "proof" you are reducing

[David Renshaw]

... so I suppose one would be less justified in trying to implement of the kinds of optimizations discussed above (swap in a different value for the Acc)

[Mario Carneiro]

yes, that wouldn't work for acc-in-type

[Mario Carneiro]

well it might hold up to propositional equality

[Eric Rodriguez]

Mario Carneiro said:

Eric Rodriguez I don't understand what you mean by that, or what that has to do with decidable typechecking

my understanding of this issue is that even though Acc.rec doesn't actually "need" to be reduced to (Acc.intro ...).rec in order to be unfolded (because there is no data, just a proposition is true), Lean's kernel does so because (a) it needs to do it for all other types, and (b) it causes issues with decidability in type-checking if this short-circuiting is done. However, I assumed as these other languages have decidable type-checking, they'd be justified in taking this shortcut; I guess your argument about turing machines from your thesis then works verbatim to make their type-checking uncomputable, however

[Mario Carneiro]

However, I assumed as these other languages have decidable type-checking, they'd be justified in taking this shortcut

They have decidable type-checking because they do not take the shortcut

[Mario Carneiro]

(Lean also doesn't take the shortcut but that makes lean's typechecker not complete. But the theory allows it to do so)

[Mario Carneiro]

even though Acc.rec doesn't actually "need" to be reduced to (Acc.intro ...).rec in order to be unfolded (because there is no data, just a proposition is true), Lean's kernel does so because (a) it needs to do it for all other types, and (b) it causes issues with decidability in type-checking if this short-circuiting is done.

It's also not quite as simple as this, you need the Acc.intro term because it has the data you need to continue the computation (the arguments to the Acc.intro are remixed with the arguments to Acc.rec in the iota rule)

[Eric Rodriguez]

noncomputable def test.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
    {a : α} (h : (y : α) → r y a → Acc r y) : (Acc.intro a h).rec m = m a h _ := rfl

this rule being something like this (I was struggling to make the general version typecheck, so I stole this from Acc.ndrec), right? ohh, do you need a?

[Eric Rodriguez]

wait no, a should be there already. the underscore is still something I don't understand

[Mario Carneiro]

you need h

[Mario Carneiro]

the underscore is another Acc.rec application

[Eric Rodriguez]

but h is a prop; can't we do some magic and say it exists because we have the term of Acc? proofs are irrelevant anyways

[Mario Carneiro]

yes, that's Acc.inv

[Mario Carneiro]

well, it's not magic, it's an explicit term

[Mario Carneiro]

you need to actually put something there and if you put something bigger than what you started with then things can get out of hand

[Eric Rodriguez]

right, I see! I think I fully understand the situation and why this kernel-rewrite rule is needed. Is anything similar done anywhere else in the kernel?

[Mario Carneiro]

this is just the regular iota rule for inductives

[Mario Carneiro]

it's just weird in this case because you don't actually have to use it, there are additional defeq side channels in Prop

[Mario Carneiro]

the kernel doesn't really do anything special here, and that's kind of the problem

[Eric Rodriguez]

no I mean I understood your proposed solution now, I was wondering if there's precedent for such solutions

[Mario Carneiro]

Well eta for structures is kind of similar?

[Mario Carneiro]

when faced with T.casesOn t f you reduce it to f t.1 t.2 t.3 instead of first computing t to a constructor (or rather, trying this if you get stuck computing t)

[Joachim Breitner]

Could the kernel for all values of sort Prop drop the actual terms, just keeping their types (and maybe the set of free variables) around? Together with an eta rule like above for, Acc reduction would not lead to large terms, I assume, as the h.inv term work be erased like this. But what would break?

[Mario Carneiro]

You can't reduce that, obviously, so anything that reduces proofs won't work anymore

[Mario Carneiro]

Apparently Coq does essentially this, they eagerly replace checked proof terms with a proof irrelevance marker to avoid having to re-typecheck it

[Joachim Breitner]

When do you have to reduce a (already type checked) proof?

[Eric Rodriguez]

In this case, to turn an Acc.rec call into an (Acc.intro _).rec call, so that the iota rule can then apply to reduce the rec

[Mario Carneiro]

Joachim Breitner said:

When do you have to reduce a (already type checked) proof?

In the situations that have come up here: when it's an inductive type and you need to head normalize it

[Joachim Breitner]

What happens if you consider “proof erased” the normal form?

[Mario Carneiro]

then terms become stuck

[Mario Carneiro]

If you have a recursor with a stuck term in the major premise then it will also be stuck

[Mario Carneiro]

which is why it is specifically large eliminating props which cause problems since they have recursors that produce values which we want to reduce

[Joachim Breitner]

I guess it's these large eliminating props that confuse me. They are eliminating into Type, so the kernel has to reduce them for type checking, but they are not eliminating into, say, Nat, so the compiler can have proof irrelevance, is that right?

But I'm still a bit confused how eliminating props into anything but prop goes together with proof irrelevance. What would be an example where a prop needs to be eliminated and it's value matters?

[Mario Carneiro]

No, by eliminating into Type I mean the motive argument has a type like motive : T -> Sort u and if you take motive := fun _ => Nat then the recursor is being used to produce a Nat

[Mario Carneiro]

So you are doing recursion on proofs to produce a value in Nat

[Mario Carneiro]

The rules for large eliminating props are essentially to restrict to cases where the value "doesn't matter", and while it is true in some sense - you can reconstruct the arguments from the type in other ways - this is only true up to equality, it does not follow the reduction itself. It's like adding a simp lemma pointed the wrong direction, while it's still a true statement you might have broken other properties of the reduction system like confluence or termination. And without that, what even is the point of using definitional equality in the first place? Just make it an extensional type theory already

[Joachim Breitner]

Just make it an extensional type theory already

I guess my thinking is still very much extensionally influenced :-)

[Trebor Huang]

Joachim Breitner said:

What happens if you consider “proof erased” the normal form?

Then consider a context with a variable t : False you could then prove any wellfoundedness claims, and since the proof is erased the typechecker would wrongly assume that it is actually wellfounded and fall into a loop

[Joachim Breitner]

Mario Carneiro said:

No, by eliminating into Type I mean the motive argument has a type like motive : T -> Sort u and if you take motive := fun _ => Nat then the recursor is being used to produce a Nat

Ah, but not every prop’s .rec allows such motives, but only those with a single constructor maybe?

Ok, the answer is in “2.6.2 Large elimination” in Mario’s thesis. I should read more and ask less :-)

[Trebor Huang]

If wellfoundedness is a Set instead there would be no problem because the reducer waits until the constructor is revealed before reducing, and if the proof came from a False then it would be forever stuck and no constructor will be revealed

[Joachim Breitner]

Trebor Huang said:

Then consider a context with a variable t : False you could then prove any wellfoundedness claims, and since the proof is erased the typechecker would wrongly assume that it is actually wellfounded and fall into a loop

Yes, agreed, but that’s also true for some of the other alternatives discussed in this thread, like a special reduction rule for Acc or WellFounded.

I guess I am wondering what else breaks :-)

[Trebor Huang]

I think the only three essential case for Prop eliminating into other things are the True type (which is harmless), the Acc type, and the Eq type (which iirc is also harmless if we embrace axiom K).

[Joachim Breitner]

So the reason to keep around proofs terms for proofs of these types (rather than just their type and maybe set of free variables) is termination of open terms and (somehow) confluence. Is that a reasonable summary?

[Eric Rodriguez]

A disparate example, but I think this is again related to WF reduction:

import Mathlib
example : False := by

  let a : ∃ n : ℕ, 3 ≤ n := ⟨3, le_rfl⟩
  let b : ∃ n : ℕ, 3 ≤ n := ⟨10000-1000, by linarith⟩
  let c : ∃ n : ℕ, 3 ≤ n := ⟨67123817236182736182731628371623871623871263817263817236187236182, by norm_num⟩


  have : Nat.find a = 3 := rfl
  --have : Nat.find b = 3 := rfl -- uncomment to get a max recursion depth crash
  have : Nat.find c = 3 := rfl

I thought Nat.find was more immune, as it always goes up "one step at a time". But I guess not

[Eric Rodriguez]

(the size of the number isn't what matters, but the proof term size generated - a raw literal of an enormous size will generate a working example!)

[Eric Rodriguez]

also, it's quite unintuitive that if you use have on the Prop, the reduction gets stuck.

[Eric Rodriguez]

@Mario Carneiro , do you have a core issue in mind you'd like to open or should I try draft one? You'll be far more knowledgeable about what exactly to write.

[Mario Carneiro]

I think it's not that useful to be pursuing kernel performance issues at this time. There are some ideas for speeding up the kernel but they will basically involve rewriting the algorithm. It's not the sort of thing which I think can be addressed by a quick patch

[Eric Rodriguez]

should we at least open the issue to say that there is interest in this?

[David Renshaw]

Even if kernel reduction is not going to change, I'm interested in better understanding it, so that I know how to work around these issues when they come up.

[Mario Carneiro]

The issue in this example is the same as before: Nat.find is defined by well founded recursion, and unlike other examples it really has to be, it's not possible to define Nat.find without Acc-in-prop

[Eric Rodriguez]

I imagined as much :/

[Mario Carneiro]

the only thing that actually decreases here is the proof term

[Mario Carneiro]

There is a workaround though if you really want to pursue this style of proof, which is to write proofs that compute well

[Mario Carneiro]

in fact there are a few of these in the WF.lean file itself

[David Renshaw]

But then why does this work?

import Mathlib

abbrev b : ∃ n : ℕ, 3 ≤ n := ⟨10000-1000, by linarith⟩

-- works
example : Nat.find b = 3 := rfl

[Mario Carneiro]

does it work as a def?

[David Renshaw]

works with either def or abbrev

[Mario Carneiro]

seems likely that the difference in that example has to do with kernel reducibility in some way

[Mario Carneiro]

you should try running it through your kernel reduction viewer to find out

[David Renshaw]

this works too

example : let b : ∃ n : ℕ, 3 ≤ n := ⟨10000-1000, by linarith⟩; Nat.find b = 3 := rfl

[David Renshaw]

right, the reason I was pulling it into a def was to try to run it through the kernel reduction visualizer

[Mario Carneiro]

Oh, it might also not be a kernel issue but an elaborator issue, since the original example involved an unfinished definition

[Eric Rodriguez]

replacing : False with : True and appending trivial doesn't do much

[David Renshaw]

welp, when I try to grab a kernel reduction trace, I get

Messages here (2)
6:20:
unknown identifier 'Nb'
6:0:
unknown metavariable '?_uniq.2866'

Probably a bug in my code.
EDIT: actually, restarting the Lean server made this go away.

[David Renshaw]

I'm interested in understanding the (possible) elaborator issue too.

[Mario Carneiro]

probably a missing withSynthesize in the term elaboration before sending to the kernel

[Mario Carneiro]

The elaborator has a bit more logging, but whnf in particular is not logged as much as you would want

[Mario Carneiro]

I have a #whnf_seq command from a long time ago that does something similar to your reduction viewer for WHNF.lean, but it needs an update and I'm sure you can do better with your version

[Eric Rodriguez]

David Renshaw said:

this works too

example : let b : ∃ n : ℕ, 3 ≤ n := ⟨10000-1000, by linarith⟩; Nat.find b = 3 := rfl

this actually seems to be something - it seems to be a coincidence, and you can make it time out by setting 3 = 500, for example, but that's enough to make the le_rfl example time out too.

[Eric Rodriguez]

(however, this doesn't fix my actual example, so I think this is just some sort of confluence of coincidences)

[David Renshaw]

import Mathlib

example : True := by
  let b : ∃ n : ℕ, 3 ≤ n := ⟨10000-1000, by linarith⟩

  -- works
  have : Nat.find b = 3 := by rfl

  -- maximum recursion depth has been reached
  --have : Nat.find b = 3 := rfl

  exact True.intro

[David Renshaw]

by rfl works, but rfl does not

[David Renshaw]

One idea for dealing with Nat.digits: we could make it an irreducible_def. That seems to enable simp_arith to successfully handle Nat.digits in many cases: #10414

[David Renshaw]

A less invasive alternative: adding a simp_digits macro: #10428

[David Renshaw]

But maybe we don't need a new tactic at all, because norm_num works well on Nat.digits now: #10429

[David Renshaw]

@Joachim Breitner I noticed that lean4#4061 looks potentially relevant to this issue, but also that the "recursion limit" error still happens on the latest Lean. Is that expected?

[Joachim Breitner]

Could it be that that #reduce, well, reduces, even if things are marked as irreducible?

Note that

example : decimalDigits 1234 = [4, 3, 2, 1] := rfl

now fails,

unseal decimalDigits in
example : decimalDigits 1234 = [4, 3, 2, 1] := rfl

has recursion error and

example : decimalDigits 1234 = [4, 3, 2, 1] := by simp [decimalDigits]

works.