Well-founded recursion on Nat

Stream: lean4

[Dan Velleman]

The following used to work:

import Mathlib

@[semireducible]
def mygcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := Nat.mod_lt a (Nat.succ_pos n)
      mygcd (n + 1) (a % (n + 1))
  termination_by b

example (a n : Nat) : mygcd a (n + 1) = mygcd (n + 1) (a % (n + 1)) := by rfl

Then a change was made so that definitions by well-founded recursion couldn't be marked as semireducible, and it stopped working. Now, in v4.27.0, it is once again possible to mark a definition by well-founded recursion as semireducible if the termination measure has type Nat. So the @[semireducible] in the example above works again. But rfl doesn't work to prove the example, even though it used to. Anyone know why?

[Aaron Liu]

See lean4#7965. Since it's not a definitional equality rfl doesn't work.

[Dan Velleman]

Well, my question was, why isn't it a definitional equality? In v4.19.0 it was.

I guess this is related to the comment from @Joachim Breitner in lean4#7965 about a couple of mathlib proofs that were broken by this change. I guess for some reason the new fix function makes things that used to be defeq no longer defeq?

[Robin Arnez]

Well, it's a compromise. If you compare the following two lines on the earlier and the later version:

example (a n : Nat) : mygcd a (n + 1) = mygcd (n + 1) (a % (n + 1)) := by rfl
example : mygcd 6765 10946 = 1 := by rfl

you'll see that in earlier versions, the first one worked but the second one failed. In newer versions, the first one fails but the second one succeeds pretty quickly, and is still reasonably fast (~a second) for

Absurdly long example

@[semireducible]
def mygcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := Nat.mod_lt a (Nat.succ_pos n)
      mygcd (n + 1) (a % (n + 1))
  termination_by b

example : mygcd 3878968454388325633701916308325905312082127714646245106160597214895550139044037097010822916462210669479293452858882973813483102008954982940361430156911478938364216563944106910214505634133706558656238254656700712525929903854933813928836378347518908762970712033337052923107693008518093849801803847813996748881765554653788291644268912980384613778969021502293082475666346224923071883324803280375039130352903304505842701147635242270210934637699104006714174883298422891491273104054328753298044273676822977244987749874555691907703880637046832794811358973739993110106219308149018570815397854379195305617510761053075688783766033667355445258844886241619210553457493675897849027988234351023599844663934853256411952221859563060475364645470760330902420806382584929156452876291575759142343809142302917491088984155209854432486594079793571316841692868039545309545388698114665082066862897420639323438488465240988742395873801976993820317174208932265468879364002630797780058759129671389634214252579116872755600360311370547754724604639987588046985178408674382863125 6276302800488957086035253108349684055478528702736457439025824448927937256811663264475883711527806250329984690249846819800648580083040107584710332687596562185073640422286799239932615797105974710857095487342820351307477141875012176874307156016229965832589137779724973854362777629878229505500260477136108363709090010421536915488632339240756987974122598603591920306874926755600361865354330444681915154695741851960071089944015319300128574107662757054790648152751366475529121877212785489665101733755898580317984402963873738187000120737824193162011399200547424034440836239726275765901190914513013217132050988064832024783370583789324109052449717186857327239783000020791777804503930439875068662687670678802914269784817022567088069496231111407908953313902398529655056082228598715882365779469902465675715699187225655878240668599547496218159297881601061923195562143932693324644219266564617042934227893371179832389642895285401263875342640468017378925921483580111278055044254198382265567395946431803304304326865077742925818757370691726168228648841319231470626 = 1 := rfl

Note: these are the 5000th and 5001st fibonacci number each, so it will actually take 5000 steps to calculate but it has no problem with it!

[Robin Arnez]

If you want to know in which sense it's different, it's something along the lines of

mygcd a (n + 1) = something a (n + 1) (n + 1) = something (n + 1) (a % (n + 1)) n
  ≠ something (n + 1) (a % (n + 1)) (a % (n + 1)) = mygcd (n + 1) (a % (n + 1))

where the last argument to this mystery function is something called "fuel" that decreases by one each iteration instead of by however a % (n + 1) decreases.

[Dan Velleman]

Thanks, that helps.

[Junyan Xu]

So it seems the number of reduction steps the kernel take doesn't actually depend on the fuel measure (b in termination_by b)? Looking at lean#7965 I see that Nat.fix is defined in terms of go which unfolds to Nat.rec _ _ (fuel + 1) but fuel has 1046 digits in this case, so since the kernel doesn't timeout it can't possibly be reducing Nat.rec, so it somehow reduced mygcd a (n+1) directly to mygcd (n + 1) (a % (n + 1))? Does anyone know how exactly this works (this is not WellFounded.fix but Nat.rec)? Was it already so in Lean 3 (or was there already a corresponding feature in Lean 3)? I guess it wasn't needed because we're freely reducing WellFounded.fix back then.

[Robin Arnez]

Well, let's take something like Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) fuel n, i.e. Nat.log2. Even if we use an absurdly large number as fuel, say 1000000000, what happens is the following:

1. Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 1000000000 3 reduces to (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999999 (Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999999) 3
2. Beta reduction comes into play: if 3 < 2 then 0 else Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999999 (3 / 2) + 1. Now the rec call is buried in the if
3. Some kind of reducing decidable instances later, the if is reduced to: Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999999 (3 / 2) + 1 and then to Nat.succ (Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999999 (3 / 2))
4. Now reduce another time: Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999999 (3 / 2) reduces to if 3 / 2 < 2 then 0 else Nat.rec (fun _ ih n => if n < 2 then 0 else ih (n / 2) + 1) 999999998 (3 / 2 / 2)
5. Now the condition is false but the rec is in another branch, so we just reduce to 0. With the Nat.succ around it, we end up with Nat.log2 3 = Nat.succ 0 = 1.

So, the kernel doesn't reduce Nat.rec all at once but step by step and the recursive call only happens once reduction reaches it. Thus, how deep Nat.rec is reduced is bounded by the fuel but not necessarily exactly the fuel.