structural recursion instead of well founded

Stream: mathlib4

[Yakov Pechersky]

We recently had a change to make Nat.digits structurally recursive, which likely has some computational (kernel? VM?) benefit: #25864

But this seems to me to be clunky -- I thought the point of the equation compiler and inference on how a recursive call works was meant to provide sugar and assistance for not having to be so explicit.

What is the overall expectation for recursive functions and how "optimized" (under whatever fitness function) we would like them to be? Do we prefer ease of statement, ease of proof, ease of API lemma, ease of decide support, ease of norm_num? Where do we record these decisions outside of PR discussions?

[David Renshaw]

A while back I made a video discussing the awkwardness that well-founded recursion brings to this function: https://www.youtube.com/watch?v=FOt-GsiNJmU .
Since then, however, a bunch of improvements have landed in core Lean, and my feeling is that switching to a fuel parameter here is not an improvement.

[David Renshaw]

Today we can do (as a stripped down example):

def decimalDigits : Nat → List Nat
| 0 => []
| n + 1 => (n + 1) % 10 :: decimalDigits ((n + 1) / 10)
-- decreasing_by clause no longer needed!

example : decimalDigits 1234567 = [7,6,5,4,3,2,1] := by
  simp [decimalDigits] -- this works now!

[David Renshaw]

I opened mathlib4#30246

[David Renshaw]

The simp in my example above started working in v4.6.0. I suspect that's due to the introduction of simprocs.

[Markus Himmel]

As Aaron points out, with structural recursion the function can be evaluated in the kernel (using decide or rfl). One reason why #25864 seemed reasonable to me was that the comment on digitsAux specifically mentions wanting specific definitional properties. This seems odd on a function defined using well-founded recursion, as such a function does not have any definitional properties.

The function doesn't seem entirely unreasonable as a candidate for something to evaluate in the kernel as the modulo and division operations are optimized. I don't know if @Aaron Liu had any specific applications of using decide on an expression involving Nat.digits in mind.

[David Renshaw]

Relatedly, I opened #30248 deleting the vestigial norm_digits code in that file.

[Yakov Pechersky]

Would it be possible for Nat equation compiler functions to have a sugar to rely on fuel instead of wf?

[Aaron Liu]

sometimes you don't want fuel

[Aaron Liu]

sometimes you want some other equation compilation

[Aaron Liu]

like if you have a function in two arguments (n,m) such that the recursive calls are from (n+1,a) to (n,b) and from (n,m+1) to (n,m) then you can compile that to be structurally recursive

[Aaron Liu]

this is what I'm talking about

Aaron Liu said:

This is what I usually do to convert these termination by product lex kind of functions from well founded recursion into structural recursion

def merge (xs ys : List Nat) : List Nat :=
  match xs with
  | [] => ys
  | x :: xs => go x xs ys fun ys => merge xs ys
where
  go (x : Nat) (xs ys : List Nat) (k : List Nat → List Nat) :=
    match ys with
    | [] => x :: xs
    | y :: ys =>
      if x ≤ y then
        x :: k (y :: ys)
      else
        y :: go x xs ys k

[Bhavik Mehta]

Aaron Liu said:

sometimes you don't want fuel

My reading of Yakov's message is that the default is unchanged, but we have a way of writing "use fuel" for a given function. eg you could write termination_by fuelif you want it to use fuel instead of wf.

[Aaron Liu]

oh yeah that would be great

[Joachim Breitner]

Like https://github.com/leanprover/lean4/pull/7965 you mean?

[Bhavik Mehta]

Yeah, with configurability as suggested in the thread.

[Yakov Pechersky]

That's a great experiment, Joachim, much along the lines I was thinking of. I am not concerned about the proofs breaking, it was ubliley that those particular constructions cared about the rfl aspect of the declarations at hand.

[Yakov Pechersky]

Separately, I am asking if it would be possible for us to record the desirata for why we might prefer wf or fuel or some other construction (like Yury's tail recursive factorial in #28766).

[Bhavik Mehta]

My impression is that (when both are possible) wf can be more readable and sometimes easier to prove things about, whereas fuel will reduce better in the kernel and have better defeq lemmas

[Joachim Breitner]

Bhavik Mehta schrieb:

My impression is that (when both are possible) wf can be more readable and sometimes easier to prove things about, whereas fuel will reduce better in the kernel and have better defeq lemmas

Well, with lean4#7965, you’d get the same proving experience (same equational theorems, same functional induction theorem) as with wfrec, it really only changes the fixpoint combinatior that matters for for the kernel.

Ah, but you mean for when we don't have that… yeah, good question then :-)

[Kyle Miller]

Something I noticed today is that if you eliminate the recursion in

def decimalDigits : Nat → List Nat
  | 0 => []
  | n + 1 => (n + 1) % 10 :: decimalDigits ((n + 1) / 10)

using a similar principle to how the structural recursion compiler works, then you get kernel reduction, without any need for fuel.

The first piece is a utility function for working with Nat.below. We only need a non-dependent version in this case, but the dependent version doesn't appear to block reduction despite using a rewrite.

-- Getting elements from non-dependent `Nat.below`.
def Nat.below.get' {α : Sort _} {n : Nat}
    (f : Nat.below (motive := fun _ => α) n) (i : Nat) (h : i < n) :
    α :=
  match n, f with
  | 0, PUnit.unit => absurd h (Nat.not_lt_zero i)
  | n' + 1, PProd.mk v f' =>
    if hi : i = n' then
      v
    else
      Nat.below.get' f' i (by omega)

Then with this we can mimic how structural recursion on the Nat argument would work, using Nat.brecOn manually:

noncomputable def decimalDigits' : Nat → List Nat :=
fun x =>
  Nat.brecOn (motive := fun _ => List Nat) x fun x f =>
    (match x with
      | 0 => []
      | n + 1 =>
        let r := Nat.below.get' (n := n + 1) f ((n + 1) / 10) (by omega)
        (n + 1) % 10 :: r)

and observe that rfl succeeds:

example : decimalDigits 12 = [2, 1] := by rfl -- fails
example : decimalDigits' 12 = [2, 1] := by rfl -- succeeds

It's possible to get rid of the if by indexing from the reverse direction. Here's the dependent version of that — I wonder if it's possible to eliminate the rewrite?

def Nat.below.getR {motive : Nat → Sort _} {n : Nat}
    (f : Nat.below (motive := motive) n) (i : Nat) (h : i < n) :
    motive (n - (i + 1)) :=
  match n, i with
  | 0, _ => absurd h (Nat.not_lt_zero _)
  | n' + 1, 0 => f.1
  | n' + 1, i' + 1 =>
    have : n' + 1 - (i' + 1 + 1) = n' - (i' + 1) := Nat.succ_sub_succ n' (i' + 1)
    this ▸ Nat.below.getR f.2 i' (by omega)

noncomputable def decimalDigits' : Nat → List Nat :=
fun x =>
  Nat.brecOn (motive := fun _ => List Nat) x fun x f =>
    (match x with
      | 0 => []
      | n + 1 =>
        let r :=
          Nat.below.getR (motive := fun _ => List Nat) (n := n + 1)
            f (n - (n + 1) / 10) (by omega)
        (n + 1) % 10 :: r)

example : decimalDigits' 122 = [2, 2, 1] := by rfl -- succeeds

It seems like it's not so bad to prove the equation lemmas, but as you'd expect they're not just by rfl.

Equation lemmas:

protected abbrev Nat.brecOn' {motive : Nat → Sort _} (t : Nat)
    (F : (t : Nat) → Nat.below (motive := motive) t → motive t) :
    Nat.below (motive := motive) (t + 1) :=
  Nat.rec (motive := fun t => motive t ×' Nat.below t) ⟨F Nat.zero PUnit.unit, PUnit.unit⟩ (fun n n_ih => ⟨F n.succ n_ih, n_ih⟩) t

theorem Nat.below.get'_brecOn' {α : Sort _} (t : Nat)
    (F : (t : Nat) → Nat.below (motive := fun _ => α) t → α) (i : Nat) (h : i ≤ t) :
    Nat.below.get' (n := t + 1) (Nat.brecOn' (motive := fun _ => α) t F) i (by omega)
      = Nat.brecOn (motive := fun _ => α) i F := by
  induction t generalizing i with
  | zero =>
    simp only [le_zero_eq] at h
    subst_vars
    rfl
  | succ t ih =>
    conv =>
      lhs
      simp [Nat.brecOn']
      unfold Nat.below.get'
    split
    · subst_vars
      rfl
    · have := ih i (by omega)
      rw [this]

theorem decimalDigits'.def' (n : Nat) :
    decimalDigits' n =
      match n with
      | 0 => []
      | n + 1 => (n + 1) % 10 :: decimalDigits' ((n + 1) / 10) := by
  refine Nat.strongRecOn n (fun n ih => ?_)
  cases n with
  | zero => rfl
  | succ n =>
    conv =>
      lhs
      delta decimalDigits'
    simp only [List.cons.injEq, true_and]
    exact Nat.below.get'_brecOn' (α := List Nat) n (fun x f =>
      (match x with
        | 0 => []
        | n + 1 =>
          let r := Nat.below.get' (n := n + 1) f ((n + 1) / 10) (by omega)
          (n + 1) % 10 :: r)) ((n + 1) / 10) (by omega)

example : decimalDigits' 0 = [] := rfl
example (n : Nat) :
    decimalDigits' (n + 1) = (n + 1) % 10 :: decimalDigits' ((n + 1) / 10) := by
  apply decimalDigits'.def'

[Aaron Liu]

we could redefine Nat.sub to eliminate the rewrite

[Aaron Liu]

actually at this point is it any better than structural strong recursion

@[elab_as_elim]
def Nat.strongRec {motive : Nat → Sort u} (ind : ∀ n, (∀ m < n, motive m) → motive n)
    (n : Nat) : motive n :=
  go n n (Nat.le_refl n)
where
  go (n : Nat) (m : Nat) (hm : m ≤ n) : motive m :=
    match n with
    | 0 => ind m fun k hk => False.elim (Nat.not_lt_zero k (Nat.lt_of_lt_of_le hk hm))
    | n + 1 =>
      if hmn : m = n + 1 then
        ind m fun k hk => go n k (Nat.le_of_lt_add_one (lt_of_lt_of_eq hk hmn))
      else
        go n m (Nat.le_of_lt_add_one (Nat.lt_of_le_of_ne hm hmn))

def decimalDigits : Nat → List Nat :=
  Nat.strongRec fun n ih =>
    match n with
    | 0 => []
    | n + 1 => (n + 1) % 10 :: ih ((n + 1) / 10) (Nat.div_lt_self (Nat.add_one_pos n) (by decide))

example : decimalDigits 122 = [2, 2, 1] := by rfl -- succeeds

[Kyle Miller]

The Nat.brecOn system is already essentially strong structural recursion on Nat. The missing ingredient is being able to index into the Nat.below structure. I was looking at this because I was wondering if I could replace Nat.strongRec with Nat.brecOn in a systematic way, to understand whether or not Lean's structural recursion module could handle this sort of well-founded recursion (at least in theory).

It's not clear it's useful for other types though. For example, with List you're allowed to recurse on any tail of a list, not any list of a smaller size.

It's also not clear that it's that different from having a gas parameter, except that that the theorem that increasing the gas argument doesn't change the result looks like it can be done just once, with Nat.below.get'_brecOn'.