Zulip Chat Archive

Stream: new members

Topic: indirect recursion check


view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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 ...

view this post on Zulip Simon Hudon (Sep 27 2018 at 02:47):

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

view this post on Zulip 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

view this post on Zulip Scott Olson (Sep 27 2018 at 03:46):

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

view this post on Zulip Mario Carneiro (Sep 27 2018 at 03:48):

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

view this post on Zulip Mario Carneiro (Sep 27 2018 at 03:48):

so you wouldn't have that first parameter in foo

view this post on Zulip Simon Hudon (Sep 27 2018 at 03:50):

What Mario said

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Olson (Sep 27 2018 at 04:03):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 27 2018 at 04:04):

I would need a more concrete example to demonstrate

view this post on Zulip 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