Zulip Chat Archive

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

Simon Hudon (Sep 27 2018 at 03:50):

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: Dec 20 2023 at 11:08 UTC