indirect recursion check

Stream: new members

[Scott Olson]

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]

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]

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

[Simon Hudon]

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

[Scott Olson]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

so you wouldn't have that first parameter in foo

[Simon Hudon]

What Mario said

[Simon Hudon]

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]

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]

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

[Scott Olson]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

I would need a more concrete example to demonstrate

[Scott Olson]

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