Strong recursor

Stream: Is there code for X?

[Terence Tao]

Hi, I am wondering if there is a recursor that can construct a function f on the natural numbers obeying a given recursion $f(n) = F(f(0), \dots, f(n-1))$ for a given function F. More precisely, I would like

theorem Nat.strong_rec {X : ℕ → Type*} (F: ∀ n, (∀ i:Fin n, X i) → X n)  :
  ∃ (f: ∀ i, X i), ∀ n, f n = F n (fun i ↦ f ↑i) := by sorry

I am aware of docs#Nat.strongRec' but am struggling to apply it to this situation. I think I can cobble together a very long construction here in which I first show inductively that I can build a function f on Fin n for each n obeying the required properties, and which is consistent as one goes from n to n+1, and then extract the diagonal, but surely there is a better way?

[Aaron Liu]

import Mathlib

theorem Nat.strong_rec {X : ℕ → Type*} (F : ∀ n, (∀ i:Fin n, X i) → X n)  :
    ∃ (f : ∀ i, X i), ∀ n, f n = F n (fun i ↦ f i) :=
  ⟨Nat.strongRec fun n ih => F n fun i => ih i.val i.isLt,
    Nat.strongRec_eq fun n ih => F n fun i => ih i.val i.isLt⟩

[Aaron Liu]

Can we deprecate docs#Nat.strongRec' ? It's just a copy of docs#Nat.strongRec with worse argument names.

[Terence Tao]

Ah, I had failed to appreciate what docs#Nat.strongRec (or docs#Nat.strongRec') was actually doing. Thanks!

[Terence Tao]

It's remarkable to me that the elaborator can even verify that the definition for Nat.strongRec provably terminates

[Joachim Breitner]

When your theorems or definitions are recursive in an interesting way, it's often easier to write them as actually recursive declarations, and then do the termination argument separately (if lean doesn't figure it out itself anyways), using termination_by and decreasing_by, than to find a suitable induction to invoke.

[Joachim Breitner]

And if you have a definition defined that way, you might enjoy ”functional induction” (the fun_induction tactic) when proving properties of that definition.

[suhr]

Terence Tao said:

It's remarkable to me that the elaborator can even verify that the definition for Nat.strongRec provably terminates

I can see how it does it (infer the termination condition from usage and than prove it by assumption), but it's indeed pretty cool.

[Junyan Xu]

Joachim Breitner said:

When your theorems or definitions are recursive in an interesting way, it's often easier to write them as actually recursive declarations, and then do the termination argument separately (if lean doesn't figure it out itself anyways), using termination_by and decreasing_by, than to find a suitable induction to invoke.

You don't get nice kernel reduction with that, which can be achieved with this version of Nat.strongRec.

[Robin Arnez]

Junyan Xu schrieb:

You don't get nice kernel reduction with that

There is lean4#7965 :-) I'd love to see this merged in some form but there are still some things to figure out about this

[Joachim Breitner]

And that one would only give you nice reduction behavior for closed terms (by decide), not necessary for open terms (what you want when you use these definitions within types).