RFC: Bounded recursion instead of well-founded recursion on Nat

[nomeata]

Motivation

Right now, functions defined by well-founded recursion get compiled to (effectively)

fixBy {α : Sort u} {β : Sort v} [WellFoundedRelation β] (f : α → β)
  {C : α → Sort w} (F : ∀ x, (∀ y, WellFoundedRelation.rel (f y) (f x) → C y) → C x) (x : α) : C x

Internally, this function uses recursion on Acc, and is known to reduce very inefficiently in the kernel, sometimes causing odd errors #2171. We have made these functions irreducible to the meta code (#4061) and am considering also making it irreducible to the kernel (#5192).

However, many recursive functions have a measure function that maps into Nat. These functions do not need the full power of well-founded recursion: That Nat simply indicates an upper bound on the number of recursive calls and can be implemented using the following fuel-based fixpoint combinator:

def Nat.fix (h : α → Nat) {motive : α → Sort u}  (F : (x : α) → ((y : α) → h y < h x → motive y) → motive x) : (x : α) → motive x :=
  let rec go : ∀ (fuel : Nat) (x : α), (h x < fuel) → motive x := Nat.rec 
    (fun _ hfuel => (not_succ_le_zero _ hfuel).elim)
    (fun _ ih x hfuel => F x (fun y hy => ih y (Nat.lt_of_lt_of_le hy (Nat.le_of_lt_add_one hfuel))))
  fun x => go (h x + 1) x (Nat.lt_add_one _)

This is essentially drop-in, so existing features of recursive functions (equational theorems, functional induction) should work as before. But with this fuel-based implementation, kernel reduction works fine.

For example, Nat.sqrt 441 now reduces in 2m instead of 1400ms!

Proposal

So we could let WF.Fix recognize when the termination_by argument indicates a termination argument of type Nat, and then use the different combinator, and not mark the functions as irreducible.

Impact

Some functions would now behave well when reduced by the kernel. This would already help mathlib, which uses such reduction to decide primality of small numbers (see #5192 (comment) for more investigation about this function) and will become much more relevant when more proof-by-reflection happens.

The main downside of this change is that the performance cliff between “reduces nicely” and “don’t expect this to reduce” moves from between structural and wf recursion to an even harder to understand place in the spectrum. In particular, lexicographic termination orders will still behave badly.

I also cannot rule out that for some open terms, the reduction behavior may subtly change? But hopefully nobody is relying on that.

Alternatives

• Do nothing
• Require an explicit opt-in from the user, for less surprises.
• “fix well founded recursion”, as desired by Mario, by not reducing proofs in the kernel in the first place

Implementation note

We don’t actually use the fixBy above yet, but WellFounded.fix, so that refactoring should happen first. #5233 tries to change that, but is stuck due to some technical debt in WF.Fix.

Community Feedback

(none yet)

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[nomeata]

Hmm, here is an observation that I didn’t fully appreciate yet.

Well-founded recursion using WellFounded.fix does sensibly reduce even for open terms – one step deep:

set_option pp.fieldNotation.generalized false
set_option pp.proofs true
set_option pp.deepTerms.threshold 8


-- recursive definition
@[semireducible] def foo : Nat → Nat
 | 0 => 0
 | n+1 => (foo n) + 1
 termination_by n => n

-- this works:
example : foo (n+1) = foo n + 1 := rfl

-- here we see why: the function unrolled once, and now only differs
-- by an `Acc` value, and proof irrelevance kicks in.

/--
info: fun n =>
  Nat.succ
    (Acc.rec (fun x₁ h ih => Nat.rec (fun x => 0) (fun n n_ih => ⋯) x₁ ih)
      ((fun y lt => Eq.ndrec (motive := fun x => ⋯ → ⋯) (fun acx ih => ⋯) rfl (fun y lt => ⋯) fun y a => ⋯)
        ((Nat.rec ⟨⋯ Nat.zero PUnit.unit, PUnit.unit⟩ (fun n n_ih => ⋯) 0).1 n)
        (foo.proof_2 ((Nat.rec ⟨⋯, PUnit.unit⟩ (fun n => ⋯) 0).1 n))))
-/
#guard_msgs in
#reduce fun n => foo (n+1)
/--
info: fun n =>
  Nat.succ (Acc.rec (fun x₁ h ih => Nat.rec (fun x => 0) (fun n n_ih => ⋯) x₁ ih) (WellFounded.apply foo.proof_1 n))
-/
#guard_msgs in
#reduce fun n => foo n + 1

-- But this does not work:
example : foo (n+1+1) = foo n + 2 := rfl

-- Because now the `Acc` term is no constructor, and reduction is stuck:

/--
info: fun n =>
  Nat.succ
    (Acc.rec (fun x₁ h ih => Nat.rec (fun x => 0) (fun n n_ih => ⋯) x₁ ih)
      ((fun y lt => Eq.ndrec (motive := fun x => ⋯ → ⋯) (fun acx ih => ⋯) rfl (fun y lt => ⋯) fun y a => ⋯)
        ((Nat.rec ⟨⋯ Nat.zero PUnit.unit, PUnit.unit⟩ (fun n n_ih => ⋯) 1).1 n)
        (foo.proof_2 ((Nat.rec ⟨⋯, PUnit.unit⟩ (fun n => ⋯) 1).1 n))))
-/
#guard_msgs in
#reduce fun n => foo (n+2)

-- This is all quite fragile: Specializing in the working first example n to m+1 breaks the
-- proof:
example : foo ((m+1)+1) = foo (m+1) + 1 := rfl

So where does the first Acc.intro constructor come from that allows one reduction? Probably from the apply WellFounded.intro here

lean4/src/Init/WF.lean

Lines 175 to 191 in e9e858a

	def lt_wfRel : WellFoundedRelation Nat where
	rel := (· < ·)
	wf := by
	apply WellFounded.intro
	intro n
	induction n with
	| zero =>
	apply Acc.intro 0
	intro _ h
	apply absurd h (Nat.not_lt_zero _)
	| succ n ih =>
	apply Acc.intro (Nat.succ n)
	intro m h
	have : m = n ∨ m < n := Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ h)
	match this with
	| Or.inl e => subst e; assumption
	| Or.inr e => exact Acc.inv ih e

I’m not sure if this behavior of open reduction of well-founded recursion is a badly behaving accident, or an ingenious design. It is relied on in mathlib in at least one instance, namely here:

https://github.com/leanprover-community/mathlib4/blob/74692d179beb8ffc96264f909af763339a2cf8b5/Mathlib/CategoryTheory/Filtered/Small.lean#L77-L85

[nomeata]

While this seems quite nice, I have since learned that we actually expect the lean kernel to eventually reduce Acc.rec without looking at the proofs, obliterating the need for this. Hence closing.

[nomeata]

In #5624 I am exploring a variant of this that maybe helps with any WellFounded relation. I wonder even if it means that some equational lemmas can become defeq this way. Given that currently

Well-founded recursion using WellFounded.fix does sensibly reduce even for open terms – one step deep:

then this would maybe make it reduce sensibly for finite steps deep.

Ah, but it seems that this makes lean just reduce far too much. Too bad.

@[semireducible] def foo : Nat → Nat
 | 0 => 0
 | n+1 => (foo n) + 1
 termination_by n => n


set_option pp.match false
set_option pp.proofs true

#print foo

noncomputable 
def foo2 : Nat → Nat :=
foo.proof_1.fix fun a a_1 =>
  foo.match_1 (fun x => ((y : Nat) → (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y x → Nat) → Nat) a
    (fun a x => 0) (fun n x => x n (foo.proof_2 n) + 1) a_1

example : foo2 (n+1) = foo2 n + 1 := rfl

/--
error: type mismatch
  rfl
has type
  foo2 (n + 1 + 1) = foo2 (n + 1 + 1) : Prop
but is expected to have type
  foo2 (n + 1 + 1) = foo2 n + 2 : Prop
-/
#guard_msgs in
example : foo2 (n+1+1) = foo2 n + 2 := rfl


theorem WellFounded.boost (wf : WellFounded r) : WellFounded r := ⟨go 4611686018427387904⟩
where go : Nat → ∀ x, Acc r x := Nat.rec (fun x => wf.apply x) (fun _ ih x => .intro x (fun y _ => ih y))


noncomputable 
def foo3 : Nat → Nat :=
foo.proof_1.boost.fix fun a a_1 =>
  foo.match_1 (fun x => ((y : Nat) → (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y x → Nat) → Nat) a
    (fun a x => 0) (fun n x => x n (foo.proof_2 n) + 1) a_1

/--
error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
example : foo3 (n+1) = foo3 n + 1 := rfl

/--
error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
example : foo3 (n+1+1) = foo3 n + 2 := rfl