## Stream: new members

### Topic: indirect recursion check

#### Scott Olson (Sep 27 2018 at 01:03):

A while ago I was porting some code from Coq to Lean and it was going very well, but there was one definition that reduces to something like this:

def foo (f : ℕ → bool) (n : ℕ) : bool :=
f n

def bar : ℕ → bool
| 0     := true
| (n+1) := foo bar n


I get "unexpected occurrence of recursive function" on bar. Is there any way to make this kind of definition work, and prove termination? I'm actually kind of surprised it worked in Coq in the first place...

#### Scott Olson (Sep 27 2018 at 01:04):

Effectively, you need to prove that foo only calls bar with something smaller than n+1, which it does in this case. Maybe it's technically possible, but the equation compiler in particular doesn't support it?

#### Simon Hudon (Sep 27 2018 at 02:45):

It this example, you can inline foo but I assume that's not an option with what you're working on ...

#### Simon Hudon (Sep 27 2018 at 02:47):

Otherwise, you can make foo and bar into mutually recursive functions

#### Scott Olson (Sep 27 2018 at 03:43):

It is possible but inconvenient to inline foo in the real code. It turned out more convenient to use a different approach to defining bar entirely.

When I try a mutually recursive approach, I still get the same "unexpected occurrence of recursive function" error (which comes from the pattern compiler, I assume):

mutual def foo, bar
with foo : (ℕ → bool) → ℕ → bool
| f n := f n
with bar : ℕ → bool
| 0     := true
| (n+1) := foo bar n


#### Scott Olson (Sep 27 2018 at 03:46):

When I find the time, I'll look up the original Coq example again for comparison.

#### Mario Carneiro (Sep 27 2018 at 03:48):

the idea is to define bar and foo bar by mutual recursion

#### Mario Carneiro (Sep 27 2018 at 03:48):

so you wouldn't have that first parameter in foo

What Mario said

#### Simon Hudon (Sep 27 2018 at 03:59):

So that would look like:

mutual def foo, bar
with foo : ℕ → bool
| n := bar n -- this will be trouble because n doesn't decrease
with bar : ℕ → bool
| 0     := true
| (n+1) := foo n


#### Scott Olson (Sep 27 2018 at 03:59):

Hmm, I suspect I still haven't fully understood, but here's my latest attempt:

-- (To be clear this is elsewhere, can't be changed, inconvenient to inline.)
def foo (f : ℕ → bool) (n : ℕ) : bool := f n

mutual def foo_bar, bar
with foo_bar : ℕ → bool
| n := foo bar n
with bar : ℕ → bool
| 0     := true
| (n+1) := foo_bar n


Which has the same "unexpected occurrence of recursive function" message.

#### Mario Carneiro (Sep 27 2018 at 04:00):

that is trouble, because you need to know that foo doesn't look at future values of bar

#### Scott Olson (Sep 27 2018 at 04:01):

Yeah, it's definitely fair for Lean to reject it. I think I'll come back to this thread when I've found the Coq example to compare with

#### Mario Carneiro (Sep 27 2018 at 04:02):

One option, used with things like list.map, is to use a theorem like map_congr to acquire an assumption that is needed for the recursion, or use a partial function like list.pmap

#### Scott Olson (Sep 27 2018 at 04:03):

I think the difference is Coq allowed the code with an explicit termination proof, whereas Lean's equation compiler won't even touch it

#### Scott Olson (Sep 27 2018 at 04:03):

Unlike simpler examples where you just need to prove something is decreasing

#### Mario Carneiro (Sep 27 2018 at 04:03):

lean allows explicit termination proofs, but you have to thread the proof through in a kind of awkward way

#### Mario Carneiro (Sep 27 2018 at 04:04):

I would need a more concrete example to demonstrate

#### Scott Olson (Sep 27 2018 at 04:05):

I've got to head out for now but I'll come back to this with more details

Last updated: May 14 2021 at 13:24 UTC