opaque recursion definitions break mergeSort decidability

Stream: lean4

[Tristan Figueroa-Reid]

I decided on Finset.sort which broke in the recent Lean 4.19 update. This is an MRE of the issue:

example : ([1] : List Nat).mergeSort (· ≤ ·) = [1] := by
  unfold List.mergeSort
  decide +kernel

/-
tactic 'decide' failed for proposition
  ([1].mergeSort fun x1 x2 => decide (x1 ≤ x2)) = [1]
since its 'Decidable' instance
  instDecidableEqList ([1].mergeSort fun x1 x2 => decide (x1 ≤ x2)) [1]
did not reduce to 'isTrue' or 'isFalse'.

Reduction got stuck at the 'Decidable' instance
  ([1].mergeSort fun x1 x2 => decide (x1 ≤ x2)).hasDecEq [1]
-/
example : ([1] : List Nat).mergeSort (· ≤ ·) = [1] := by
  decide +kernel

[Eric Wieser]

In the past I think the suggestion was to keep these functions defined in a way that is reducible, and then use csimp to link them to their irreducible optimized versions.

[Eric Wieser]

I think src#List.mergeSort hasn't changed, but the rules for reducibility have

[Tristan Figueroa-Reid]

Eric Wieser said:

In the past I think the suggestion was to keep these functions defined in a way that is reducible, and then use csimp to link them to their irreducible optimized versions.

I do believe that mergeSort already has a irreducible optimized version linked by csimp

[Tristan Figueroa-Reid]

I believe the rules for reducibility changed (which broke this well-founded definition of List.mergeSort) changed in #5182.

[Tristan Figueroa-Reid]

I don't know much of anything regarding reducibility with csimp, but given that List.mergeSort already has a csimp-linked tail-recursive definition, would it make sense to mark it as semireducible?

[Tristan Figueroa-Reid]

Actually, should decide follow csimp marked theorems?

[Eric Wieser]

I don't think that would be useful, the runtime-optimal version is less likely to reduce well

[Eric Wieser]

And following them in reverse would also not be very useful, because the runtime version should never appear in any theorem statements

[Joachim Breitner]

Copying from a discussion with @Bhavik Mehta right now

Oof, is there really no way of making it temporarily semireducible after the fact for decide?

Yes, and after having tiptoed around this issue for a while I believe that reducing proofs in the kernel (as it necessary for well-founded recursion) is just too big of a footgun to be allowed. It may have worked ok in a number of cases so far, but every so often it goes horribly wrong (kernel heartbeat timeout, hard to debug).
Also with the upcoming module system we really want proofs to be irrelevant, so that they can be omitted from interface files, maybe even omitted from downloaded olean etc.
So the conclusion is that well-founded recursion should only be used when you really only care about the classical existence of a function with that specification, and never when you want to get any kind of useful defeqs.

So conversely, if you have a function that you want to have useful defeqs, then don't use well-founded recursion. One way is to use a helper definition that is built to reduce nicely, e.g. using fuel, like I did here: https://github.com/leanprover/lean4/pull/7558

This should be possible for any function that's currently defined by wf recursion with a single Nat measure.

We could even consider having a termination_by fuel … variant that uses that construction internally.

(I don’t know how well this fares when reducing larger inputs, because I assume that although it won’t reduce proofs, the kernel will still construct a large proof for the fuel argument, so it may not scale to large number of recursions either.)

Another alternative is not to use decide, but rewriting, when doing the proof. But I understand that our rewriting tractics (simp, rw) are not great for the use case of “do cbv normalization by rewriting” yet. I did some steps in that direction in https://github.com/leanprover/lean4/pull/5977, but it wasn't quite convincing yet.

I agree that this is all a bit unsatisfactory until we are weaned off reducing wf proofs…

This is orthogonal, but I don't actually understand why reducing defs which use wfrec needs reduction of proofs at all?

Defs using well-founded recursion use WellFounded.fix which is essentially structural recursion on the Acc predicate, and to reduce these definitions by more than one step, the proof of Acc x y needs to be reduce to the Acc.intro constructor. Depending how your well-founded definition is defined, this may involve reducing Nat.le or stuff like that, and can be very expensive, exponential even.

You can kick the can down the road by identifying all affected functions, define them as semireducible, and then right afterwards use attribute [irreducible] foo. This gives you the old behavior and you don’t need to fix all at once.

It works sometimes (for example, for technical reasons one unfolding is actually free), and when it works it’s annoyingly useful. But it shot a few legs, so we’d really like to pretend it never worked at all :-)

[Mario Carneiro]

If we really actually make Acc reduction not work, maybe we can finally actually fix the core reason why lean has undecidable typechecking and rip this out of the kernel?

[Edward van de Meent]

(what is Acc reduction?) i should read :see_no_evil:

[Aaron Liu]

Mario Carneiro said:

If we really actually make Acc reduction not work, maybe we can finally actually fix the core reason why lean has undecidable typechecking and rip this out of the kernel?

Why

[Joachim Breitner]

Mario Carneiro said:

If we really actually make Acc reduction not work, maybe we can finally actually fix the core reason why lean has undecidable typechecking and rip this out of the kernel?

Just to avoid confusion, what precisely is “this”?

(I can’t answer your question, but maybe we can at least make it an option by eventually removing all uses of reducible wf rec.)

[Mario Carneiro]

I'm thinking to change the inductive schema so that types like Acc do not have an iota rule, but possibly give you an iota axiom instead

[Mario Carneiro]

which is hopefully enough to prove WellFounded.fix

[Joachim Breitner]

While we are at it: What do you think of https://github.com/leanprover/lean4/issues/5234, @Mario Carneiro ?
Summary: When the measure of wf-recursion is just one Nat (not lexicographic, not a different order), use a Nat-specific fix-point operator that is a drop-in replacement for WellFounded.fix, but implemented by using Nat.rec on fuel that’s initialized by the measure.

It seems that this would be simple to implement, would let decide work for many (but not all) wf-rec function, and would avoid most (bot not all) “reduction bombs” because for neutral arguments, the intial fuel is neutral and reduction gets stuck, as it should.

[Mario Carneiro]

I don't see why to specialize on Nat here, you can do the same thing for any inductive type

[Mario Carneiro]

I'm sad about the general direction, it's making well founded recursion turn into a big bugaboo and discouraging people from using it

[Joachim Breitner]

I’m not particularly happy either (besides that this will make proofs even more irrelevant, which is great for the upcoming module system, smaller olean, less recompilation, and that we hopefully get rid of this sometimes hard-to-debug “reduction bombs”)

[Mario Carneiro]

I definitely think proofs should be irrelevant but I don't see why that means wf recursion has to suck

[Mario Carneiro]

this should never have been implemented by reducing proofs in the first place

[Joachim Breitner]

Mario Carneiro said:

I don't see why to specialize on Nat here, you can do the same thing for any inductive type

Can you? Maybe with an inductive type where the < relation that’s picked up by WellFoundedRelation contains the subterm-relation, unless I am missing something. Do you have concrete examples in mind?

[Mario Carneiro]

I was thinking you would not use a well founded relation at all, you would just use the subterm relation on an inductive type

[Joachim Breitner]

Mario Carneiro said:

this should never have been implemented by reducing proofs in the first place

What are the alternatives? We once discussed a world where Acc.rec reduces always, without looking at theAcc proof, but doesn’t that make the problem of the kernel reducing things ad infinitum even worse?

[Mario Carneiro]

you could reduce only closed terms

[Mario Carneiro]

I think we should kind of set Acc aside, because we actually care more about WellFounded (they are equivalent in strength) and WellFounded doesn't have the issue of a monotonically increasing proof term during reduction

[Mario Carneiro]

I think we're just reinventing fix + match here, we should just check what Rocq does

[Joachim Breitner]

Rocq has an in-kernel termination checker (the “guardedness checker”), AFAIR

[Mario Carneiro]

yeah but that's sort of separate from this

[Mario Carneiro]

the question is more about when reduction happens

[Joachim Breitner]

Mario Carneiro said:

I think we should kind of set Acc aside, because we actually care more about WellFounded (they are equivalent in strength) and WellFounded doesn't have the issue of a monotonically increasing proof term during reduction

I’m sorry, but I think you have to spell this out some more for me. Is there another definition of WellFounded that doesn’t go through Acc and allows for recursion somehow?

[Mario Carneiro]

I think the definition of WellFounded is an implementation detail, it could be built in axiomatic

[Aaron Liu]

Mario Carneiro said:

I think the definition of WellFounded is an implementation detail, it could be built in axiomatic

How?

[Mario Carneiro]

That is, WellFounded is a primitive axiomatic constructor and so is WellFounded.fix and it has magic computation rules provided by the kernel. Whether it gets these computation rules because it's built in or because it has a definition that works out that way doesn't really matter for things built on top

[Mario Carneiro]

My point is that WellFounded.fix has better definitional reduction rules than Acc.rec does because Acc needs to manipulate a proof term in every step of the recursion

[Edward van de Meent]

ok, but then will we be able to create instances for WellFounded?

[Mario Carneiro]

sure, it can have a constructor that looks like WellFounded.mk too

[Mario Carneiro]

I'm saying to separate the API from the implementation

[Edward van de Meent]

i guess that makes sense

[Mario Carneiro]

the API of WellFounded includes WellFounded.mk and WellFounded.fix and possibly a defeq that looks like WellFounded.fix_eq, so it's worth talking about what kind of API here and what kind of restrictions on fix_eq give desirable behaviors for things on top

[Mario Carneiro]

and if at the end of that it turns out it can be defined in terms of something more basic, great, but if not, it can still be a built in primitive supplied by the kernel

[Mario Carneiro]

Acc is already super special and complicates the inductive schema for a case which has essentially only one practical application

[Mario Carneiro]

I would definitely trade having a simpler schema in exchange for needing another magic special type like Quot

[Edward van de Meent]

does making WellFounded internal/axiomatic let us make sure something like Acc can't be created, though?

[Mario Carneiro]

yeah, we would ban types like it and/or make them have crappy defeqs

[Aaron Liu]

Edward van de Meent said:

does making WellFounded internal/axiomatic let us make sure something like Acc can't be created, though?

You can do something like saying the subtype of stuff less than x is well-founded

[Mario Carneiro]

if it wasn't for Acc -> WellFounded -> every wf rec definition ever, we wouldn't care about Acc at all

[Aaron Liu]

Mario Carneiro said:

if it wasn't for Acc -> WellFounded -> every wf rec definition ever, we wouldn't care about Acc at all

We have this one file file#SetTheory/Ordinal/Rank

[Mario Carneiro]

Also, keep in mind that "Acc in Type" is one way of neutering Acc by making it act like a regular inductive

[Mario Carneiro]

and in the presence of the axiom of choice you can go back and forth with something that has the type of the current Acc

[Mario Carneiro]

so I think that rank file would be fine

[Edward van de Meent]

what is special about current Acc? as far as i can tell it's really just a normal inductive, so i don't get how you would even begin to ban "inductives like it"

[Mario Carneiro]

It's a large eliminating subsingleton type

[Edward van de Meent]

it's large eliminating!?

[Mario Carneiro]

it's the only large eliminating recursive inductive type in lean

[Edward van de Meent]

ah, i missed that bit

[Edward van de Meent]

so you don't even get to define something like Acc in lean as-is? that clears it up a bunch

[Mario Carneiro]

Equality is also a large eliminating inductive, but it's not recursive

[Mario Carneiro]

No, you can define something like Acc

[Mario Carneiro]

because it's not actually special cased

[Mario Carneiro]

but there is an additional clause in the inductive schema which allows "Acc and things like it" but in practice that means just Acc

[Mario Carneiro]

in fact, there is a proof in #leantt that Acc is universal for such types

[Mario Carneiro]

Edward van de Meent said:

it's large eliminating!?

It has to be large eliminating or else one can't define functions by well founded recursion, only prove theorems by well founded induction

[Joachim Breitner]

Mario Carneiro said:

Equality is also a large eliminating inductive, but it's not recursive

Any interesting large eliminating inductives besides these two? Or put differently: If we didn’t need Acc, could Eq be the only large eliminating inductive?

[Mario Carneiro]

And is also large eliminating

[Mario Carneiro]

but it's not interesting

[Mario Carneiro]

True and False too

[Mario Carneiro]

only recursive large eliminating types are really problematic though

[Mario Carneiro]

Eq is semi-problematic :)

[Aaron Liu]

False, Eq, and Acc are interesting

[Aaron Liu]

With True you can't do anything with its large elimination and with And you can just use the projections

[Mario Carneiro]

False's large elimination is quite important but it usually is harmless from a type theory perspective because it has no iota rule (since it has no constructors to have iota rules for)

[Aaron Liu]

Mario Carneiro said:

False's large elimination is quite important but it usually is harmless from a type theory perspective because it has no iota rule (since it has no constructors to have iota rules for)

What does iota rule do (why is not having one harmless)?

[Mario Carneiro]

T.rec F (T.constructor x) = F x

[Mario Carneiro]

you have one of those for every constructor of an inductive type, so for False there are no rules

[Aaron Liu]

Is having these "harmful" then?

[Mario Carneiro]

it's what makes the theory interesting

[Mario Carneiro]

where "interesting" may go as far as "soundness is an open question"

[Mario Carneiro]

but it's not like we don't want to be able to make definitions by recursion on Nat

[Mario Carneiro]

Here's a proof (using AC) that it is possible to construct WellFounded.fix using a small-eliminating Acc:

import Mathlib.Logic.Unique

inductive SmallAcc {α} (r : α → α → Prop) : α → Prop
  | mk x : Unit → (∀ y, r y x → SmallAcc r y) → SmallAcc r x

def WellFounded' {α} (r : α → α → Prop) := ∀ x, SmallAcc r x

inductive FixOut {α} {C : α → Sort _} {r : α → α → Prop}
    (F : (x : α) → ((y : α) → r y x → C y) → C x) : ∀ x, C x → Prop
  | mk x f : (∀ y h, FixOut F y (f y h)) → FixOut F x (F x f)

theorem SmallAcc.fix_exists {α} {C : α → Sort _} {r : α → α → Prop}
    (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (hwf : SmallAcc r x) :
    ∃ y : C x, FixOut F x y :=
  hwf.rec fun _ _ _ IH =>
    ⟨F _ fun y h => (IH y h).choose, ⟨_, _, fun y h => (IH y h).choose_spec⟩⟩

noncomputable def WellFounded'.fix {α} {C : α → Sort _} {r : α → α → Prop}
    (hwf : WellFounded' r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x :=
  (SmallAcc.fix_exists F x (hwf x)).choose

theorem WellFounded'.fix_eq {α} {C : α → Sort _} {r : α → α → Prop}
    (hwf : WellFounded' r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) :
    fix hwf F x = F x (fun y _ => fix hwf F y) := by
  suffices ∀ y y', FixOut F x y → FixOut F x y' → y = y' from
    this _ _ (SmallAcc.fix_exists F x (hwf x)).choose_spec
      ⟨_, _, fun y _ => (SmallAcc.fix_exists F y (hwf y)).choose_spec⟩
  intro y y' H1 H2
  induction H1 with
  | _ x f h IH =>
    let ⟨_, f', h'⟩ := H2
    congr; ext; exact IH _ _ _ (h' ..)

[Aaron Liu]

No computation makes it slightly disappointing

[Mario Carneiro]

the point is that if one is willing to give up computation then we don't need this kind of inductive at all

[Mario Carneiro]

plus the compiler can of course support computation of this function anyway

[Mario Carneiro]

I don't think it's possible to get a version that computes in the kernel without kernel magic (either Acc-like types or primitive WellFounded.fix)

[Aaron Liu]

What would be the consequences of using a type-valued Acc?

[Mario Carneiro]

You would be able to define fix easily, but WellFounded would no longer be a Prop, and also the proof of well foundedness would not be erased

[Mario Carneiro]

If you make WellFounded a prop using Nonempty then you need the axiom of choice to define fix and you end up with something similar to the above

[Mario Carneiro]

It's possible you could make it work if we had erasure annotations and used them on well foundedness arguments

[Mario Carneiro]

which TBH sounds less scary than the alternatives that involve kernel magic

[Edward van de Meent]

so if i understand correctly, you're proposing to get rid of this rule:
image.png
and make WellFounded a built-in exception?

[Edward van de Meent]

(the image is from #leantt , i added the box)

[Mario Carneiro]

WellFounded isn't exactly an exception to this rule, since it's not an inductive type of this kind at all (it's a structure wrapping Acc)

[Edward van de Meent]

ah, that's fair

[Joachim Breitner]

Mario Carneiro said:

the proof of well foundedness would not be erased

Does that matter? At least if you refer to erasure in compiled code, because the compiler works on the recursive PreDefinition and doesn’t even see the kernel-facing construction we are discussing here. And the kernel doesn’t erase proofs, does it?

[Mario Carneiro]

Ah, I suppose that's true

[Mario Carneiro]

hm... let's try it and see what breaks?

[Joachim Breitner]

Making Acc a Type would allow simplifying the type theory, but not help with the other issues (slow reduction of Acc terms, for example), would it?

[Edward van de Meent]

it might force users to write better-reducing "proofs" though

[Edward van de Meent]

i.e. not use tactics

[Mario Carneiro]

I think it would mean that defeq would work reliably

[Mario Carneiro]

well foundedness proofs would have a similar status to Decidable proofs, you would want to avoid using rw except in the proof arguments

[Joachim Breitner]

I see – are saying we need WF proofs to be more carefully crafted, and that’s more likely to happen in Type

[Mario Carneiro]

Note that a (Type-valued) proof of well foundedness still contains a lot of proofs in it because the r argument is still a prop

[Mario Carneiro]

and unlike "reducing proofs", we can clearly separate out the spine of the WF proof from the side proofs showing individual relations hold

[Joachim Breitner]

Right, that’s my worry still

[Mario Carneiro]

you would not need to do anything special to tell lean to reduce the WF argument but not the side proofs

[Mario Carneiro]

I think it makes a difference in this setting whether you are doing well founded recursion over a relation or its transitive closure. Doing recursion on the transitive closure should be more efficient

[Mario Carneiro]

I'm trying it out now, and there is an issue: Acc in Type is a subsingleton but not definitionally so (because we don't have eta for "recursive structures" and that sounds scary), which means that fix_eq is not a defeq because it uses two different derivations for the well foundedness proof on each side of the equality

[Aaron Liu]

What if we add a rule that elements of a structurally subsingleton type are definitional equal?

[Aaron Liu]

Structural eta already does a lot of this, recursive types like Acc are sort of an exception now

[Mario Carneiro]

it could work

[Mario Carneiro]

I think it reintroduces the issue that makes Acc bad though

[Mario Carneiro]

you can use definitional equality to swap out constructors in an inconsistent context and so typing is undecidable

[Mario Carneiro]

I guess that's the whole point, WellFounded.fix_eq (which ignores its proof argument) can't be a defeq without implicating undecidability of typechecking

[Mario Carneiro]

note that Acc.fixF works just fine

[Edward van de Meent]

docs#Acc.fixF :looking:

[Edward van de Meent]

:man_shrugging:

[Mario Carneiro]

docs#WellFounded.fixF

[Mario Carneiro]

But actually, I think it doesn't matter that fix_eq isn't a defeq. It's already not a defeq. The question is whether it computes on closed terms, and I believe it should

[Bhavik Mehta]

So conversely, if you have a function that you want to have useful defeqs, then don't use well-founded recursion

I have made this change for Nat.xgcd here: #24514

[Aaron Liu]

Should we make everything come with fuel?

[Bhavik Mehta]

That's my conclusion from Joachim's message

[Antoine Chambert-Loir]

Do you have a link to how fuel should be used, or is it enough to guess from what @Bhavik Mehta did in #24514?

[François G. Dorais]

Fuel only works if you have an explicit upper bound on the number of recursion steps needed, so it is not a fully general replacement.

[Eric Wieser]

For mergeSort, this is easy enough to prove as n^2, right?

[François G. Dorais]

Yes, the problematic cases are much more complex.

[Antoine Chambert-Loir]

and for the list of prime factors which interests me, it's at most Nat.log 2 n, so that's ok for me too…

[Bhavik Mehta]

I had adapted it from Joachim's change to Nat.div in core, so that example could also be helpful.

[Mario Carneiro]

There is an almost fully general version, if you allow fuel to be an element of any inductive type, since at that point it basically becomes a version of Acc in type

[Junyan Xu]

In #30169 I redefine xgcd using a "reducible" version of Nat.strongRec, which uses Nat.rec instead of Acc.rec/WellFounded.fix. I changed the mathlib version, but maybe it's better to change batteries version and deduplicate the mathlib version. The changes for xgcd are pretty clean, without the need of private lemmas, though I do need some private def/lemma to prove my strongRec' reduces as expected. You could nest strongRec' with other recursors to work with lexicographic orders involving Nat.
My original motivation is to make Nat.binaryRec reducible (for exponentiation by doubling), but I realized strongRec' still requires linear (not logarithmic) complexity to evaluate a closed term. So this is a case where using fuel is really useful. But I wonder whether the kernel compute the fuel (Nat.log2 in this case) in logarithmic time? It should be the case if it uses GMP.

[Bhavik Mehta]

How does it compare to #24514, which also makes xgcd reducible?

[Junyan Xu]

The changes for xgcd are pretty clean, without the need of private lemmas

[Bhavik Mehta]

I was specifically thinking about the speed of reduction here, rather than the number of private lemmas.

[Junyan Xu]

I think our definitions (and lean#7558) boil down to the same thing, so I'm not expect much difference in performance, though I also don't know how to test.
Unexpectedly my definition is breaking norm_num (reporting Stack overflow detected. Aborting.), and the following tests

theorem ex61 : Nat.gcd (553105253 * 776531401) (553105253 * 920419823) = 553105253 := by norm_num1
theorem ex62 : Nat.gcd (2^1000 - 1) (2^1001 - 1) = 1 := by norm_num1
theorem ex62' : Nat.gcd (2^1001 - 1) (2^1000 - 1) = 1 := by norm_num1
theorem ex63 : Nat.gcd (2^500 - 1) (2^510 - 1) = 2^10 - 1 := by norm_num1
theorem ex64 : Int.gcd (1 - 2^500) (2^510 - 1) = 2^10 - 1 := by norm_num1
theorem ex64' : Int.gcd (1 - 2^500) (2^510 - 1) + 1 = 2^10 := by norm_num1

needs to be replaced by

set_option exponentiation.threshold 1001
theorem ex62 : Nat.gcd (2^1000 - 1) (2^1001 - 1) = 1 := rfl
theorem ex62' : Nat.gcd (2^1001 - 1) (2^1000 - 1) = 1 := rfl
theorem ex63 : Nat.gcd (2^500 - 1) (2^510 - 1) = 2^10 - 1 := rfl
set_option maxRecDepth 4000
theorem ex64 : Int.gcd (1 - 2^500) (2^510 - 1) = 2^10 - 1 := rfl
theorem ex64' : Int.gcd (1 - 2^500) (2^510 - 1) + 1 = 2^10 := rfl

[Aaron Liu]

That sounds like a thing that happens in complied code

[Aaron Liu]

We can just fix that with a csimp lemma

[Mario Carneiro]

when norm_num breaks like that that usually means there is a type error in the proof forcing something bad to be unfolded

[Aaron Liu]

These are big numbers

[Mario Carneiro]

yes, but norm_num should still generate good proofs

[Aaron Liu]

It was a stack overflow

[Mario Carneiro]

in fact it should probably just be deferring to kernel checking in this case because it's Nat.gcd

[Aaron Liu]

Sounds like a problem with the generation not with the proof

[Mario Carneiro]

the definition of xgcd should not be unfolded by norm_num, if it is that's a bug

[Aaron Liu]

What's the code that does norm num gcd

[Mario Carneiro]

unfortunately norm_num has the problem that many of the subproofs are actually true by rfl, it's just not a good idea to prove them that way

[Mario Carneiro]

so when something goes wrong it doesn't break, it just gets really slow or overflows

[Aaron Liu]

Oh that might be a kernel problem now that I think about it

[Mario Carneiro]

It's possible that norm_num is still doing gcd "manually", not sure it has been updated for all the new kernel accelerated functions

[Mario Carneiro]

it seems to be so

[Mario Carneiro]

I think that only helps for gcd itself though, if you want the other parts of xgcd you still need to use the old code, I don't think there is some clever algebra that will give you the coefficients using only gcd

[Aaron Liu]

docs#Tactic.NormNum.proveNatGCD

[Aaron Liu]

now I'm back to thinking that this is not a kernel problem

[Aaron Liu]

it should probably be fixed if you write a @[csimp] lemma for Nat.xgcdAux

[Mario Carneiro]

the code does call Nat.xgcdAux in meta code

[Mario Carneiro]

so if that function is written badly then it will overflow in #eval

[Aaron Liu]

yes I claim that that's what's stack overflowing

[Mario Carneiro]

I think the call to strongRec builds up a huge stack of closures which overflows when it is called

[Mario Carneiro]

I think strongRec' is the one that needs a csimp lemma

[Aaron Liu]

oh yeah that works too

[Junyan Xu]

Thanks! I'm csimping strongRec' to strongRec in #30181. strongRec is irreducible so it's not gonna overflow, right?

[Aaron Liu]

strongRec being irreducible is actually irrelevant

[Junyan Xu]

#30181 passed CI and !bench reported a speedup, while #30169 is still stuck at "test mathlib" after 2h 46m passed.
image.png

The speedup is probably spurious, as #30144 (benched against the same base commit 3da1779) reports an almost identical speedup despite having diffs disjoint from #30181.

[Aaron Liu]

hmmm

[Aaron Liu]

maybe still do that @[csimp] lemma for Nat.xgcdAux and just make it do the original implementation

[Aaron Liu]

or make strongRec be @[specialize] maybe that will work

[Junyan Xu]

#30181 works and is awaiting review.
I've closed #30169, not deleting the branch yet for forensic purposes. (maybe the CI run and/or the machine has crashed.)

[Junyan Xu]

In #30144 I changed Nat.binaryRec to use Nat.rec with docs#Nat.log2 as fuel. But this breaks the following test

def Nat.popcountTR (n : Nat) : Nat :=
  n.binaryRec (·) (fun b _ f x ↦ f (x + b.toNat)) 0

/-- info: 1 -/
#guard_msgs in
#eval Nat.popcountTR (2 ^ 20240)

with error

info: stderr:
libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)
interpreter stacktrace:
#1 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_2._boxed
#2 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_0
#3 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_0._boxed
#4 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_2
#5 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_2._boxed
#6 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_0
#7 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_0._boxed
#8 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_2
...
#8306 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_0
#8307 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_0._boxed
#8308 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_2
#8309 Nat.binaryRec._at_.Nat.popcountTR.spec_0._lam_2._boxed
#8310 Nat.binaryRec._at_.Nat.popcountTR.spec_0
#8311 Nat.popcountTR
#8312 _eval._closed_1
#8313 _eval._closed_2
#8314 _eval._closed_3
#8315 _eval
error: Lean exited with code 134

Anyone knows how to fix?

[Aaron Liu]

csimp it

[Junyan Xu]

#eval also uses csimp? Yes indeed ...
I also tried

set_option exponentiation.threshold 20240
set_option maxRecDepth 15838
theorem x : Nat.popcountTR (2 ^ 20240) = 1 := rfl

which triggers "maximum recursion depth has been reached"; if I change maxRecDepth to 15839 then "Stack overflow detected. Aborting." Is stack size adjustable?

[Junyan Xu]

It seems that csimp only supports constants now, so I need to keep the original binaryRec and csimp my new version to it?

[Junyan Xu]

It turns out

set_option exponentiation.threshold 20240
set_option maxRecDepth 15842
theorem x : Nat.log2 (2 ^ 20240) = 20240 := rfl

is sufficient to overflow the stack. #eval Nat.log2 (2 ^ 20240) is okay though.

[Junyan Xu]

This is interesting: with the current state of #30144, #eval Nat.popcountTR (2 ^ 2075) is okay while #eval Nat.popcountTR (2 ^ 2076) crashes Lean. But if I change binaryRecAux from abbrev to def, then I need to go up to #eval Nat.popcountTR (2 ^ 4186) to crash Lean.

[Aaron Liu]

probably inlining?

[Aaron Liu]

abbrev makes it reducible and inline

[Junyan Xu]

Following the PR #17897 by @Yuyang Zhao that introduced the test, I tried to add @[specialize] to def binaryRecAux, but this decreases the crash threshold from 4186 to 4152. Any idea what's going on?

[Junyan Xu]

Adding inline or specialize to abbrev binaryRecAux has no effect.

[Aaron Liu]

I have no idea why

[Junyan Xu]

Adding inline to def binaryRecAux decreases the crash threshold to 2076, same as abbrev.

[Mario Carneiro]

this indicates that it's not tail recursing either way

[Junyan Xu]

Thanks for the inputs, problem solved by using specialize on both binaryRecAux and binaryRec AND using the equation compiler instead of Nat.rec for binaryRecAux!

[Junyan Xu]

What would happen if we remove @[irreducible] from docs#Rat.add /sub/mul/inv? They're in lean4 repo so harder to test. The above two PRs enable kernel reduction of elliptic curve nsmul over fields of prime order, and I'd like the same over the rationals.

[Bhavik Mehta]

Junyan Xu said:

The above two PRs enable kernel reduction of elliptic curve nsmul over fields of prime order, and I'd like the same over the rationals.

curiously enough, this was my motivation for my PR too :)

[Junyan Xu]

Good to know! I only started thinking about this after the post #general > Problems with elliptic curves @ 💬.

[Bhavik Mehta]

You might like to discuss with @Andrew Yang, who has more thoughts and more code on this :)