Unexpected occurence of recursive funtion

Stream: general

[Minchao Wu]

Hi friends, I'm wondering what's the right way to let Lean accept recursive calls with list.map?
For example:

def bar : ℕ → ℕ
| 0     := 0
| (n+1) := list.length $ list.map bar [n, n, n]

Lean is not happy with the above one.

[Chris Hughes]

This works for this example. In general I think you pretty cannot do recursive calls with list.map and you have to find some different way of defining the function.

def bar : ℕ → ℕ
| 0     := 0
| (n+1) := list.length $ [bar n, bar n, bar n]

[Minchao Wu]

Yes, your solution definitely works. But I am curious about why it cannot be done with maps.

[Chris Hughes]

It might be possible, but it's not easy. The equation compiler knows your function is well-founded if the recursive call applies it to a nat less than n + 1. Here your function bar is not actually applied to anything, so it cannot prove it is well founded.

[Minchao Wu]

That's true. Usually if Lean cannot prove well-foundedness then it throws a different error asking me for a proof, but for this one it just gives up. I guess the reason is exactly that bar is not applied to anything as you said.

[Chris Hughes]

I found a way

import data.list.basic
def bar : ℕ → ℕ
| 0     := 0
| (n+1) := list.length
  (list.pmap (λ m (hm : m < n + 1), bar m) [n, n, n]
  (by simp [nat.lt_succ_self]))

[Minchao Wu]

Great, this looks like a general solution. Thanks!