unexpected occurrence of recursive function

Stream: general

[Keeley Hoek]

The following snippet does not compile: unexpected occurrence of recursive function

def height : ℕ → ℕ
| 0 := 0
| (n + 1) := id height n

I am very disturbed!

[Neil Strickland]

Did you mean id height n (which is (id height) n, of course) or id (height n)? I am not surprised that the former fails.

[Keeley Hoek]

I mean't the former---why is it expected that it fails?

[Reid Barton]

It wouldn't be so great if you instead had id' height n where id' f n := f (n+1)

[Reid Barton]

So basically you're asking Lean to reduce the right hand side before attempting to determine whether it is syntactically a valid recursive call

[Keeley Hoek]

Sure, but normally when this happens we get could not prove recursive application is decreasing well-founded relation (or something like that I'm just remembering), and instead this time it seems like lean just goes "nope not even trying this time".

[Reid Barton]

Well because you don't even have an application of height

[Keeley Hoek]

aha! ok. Thanks! :)

[Yakov Pechersky]

What's the right way to phrase a recursive show function like this one? I get a unexpected occurrence of recursive function error

import data.buffer.parser.basic

inductive tree
| leaf (s : string)
| branch (s : string) (l : list tree)

open tree

def tree.show : tree → list string
| (leaf   s)   := [s]
| (branch s l) := [s] ++ l.bind tree.show

[Yakov Pechersky]

Or is this an issue of a nested inductive?

[Yakov Pechersky]

I guess this is what is preferred:

import data.buffer.parser.basic

inductive tree
| leaf : string → tree
| branch : string → tree → tree → tree

open tree

def tree.show : tree → list string
| (leaf   s)       := [s]
| (branch s hd tl) := [s] ++ hd.show ++ tl.show

[Greg Price]

TPIL says that Lean supports type definitions like the one you originally wrote:
https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

I don't know what that error means, though.

[Yakov Pechersky]

I'm going to try lean4 later to see if it fares better here

[Greg Price]

Ah, there's also some perhaps helpful information in the previous history of this topic:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unexpected.20occurrence.20of.20recursive.20function/near/167937423
(Which I happened to notice above this just now.)

[Greg Price]

In your example, I think the point is then that when Lean is looking at the definition of tree.show, it doesn't know that list.bind is itself a well-behaved recursive function that's compatible with the recursion you're doing here -- so it can't prove the recursion terminates

[Greg Price]

So one way you could resolve that is like so:

import data.buffer.parser.basic

inductive tree
| leaf (s : string)
| branch (s : string) (l : list tree)

open tree

mutual def tree.show, tree.show_list
with tree.show : tree → list string
| (leaf   s)   := [s]
| (branch s l) := [s] ++ tree.show_list l
with tree.show_list : list tree → list string
|  []      := []
| (h :: t) := tree.show h ++ tree.show_list t

#eval (branch "a" [leaf "b", leaf "c"]).show -- ["a", "b", "c"]

Basically inlining list.bind as part of a mutual recursion.

[Greg Price]

You may also be able to do it while using list.bind itself, if you can exhibit an appropriate well-founded relation. I haven't tried that feature of Lean, and I'm not sure if it's possible to apply in this situation.

[Yakov Pechersky]

Mario has suggested to unravel mutual inductives into a plain inductive, and warns against nested inductives here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nested.20recursion . Also, definitions based on wf aren't as compute friendly, so while this doesn't matter so much here, I do want to find a way to not have to rely on a wf proof.

[Greg Price]

Ah, I see:

Mario Carneiro said:

nested inductives are not really supported in lean, they are compiled (badly) to inductive types. It's better to roll your own inductive type if you want the right recursion principle

Good to know, then.

[Greg Price]

Later in the same thread Mario suggests another solution, if just running this code is what you're interested in and not proving theorems about it: you could use meta def for the function and then write the recursion however you like.

[Yakov Pechersky]

Right. I followed the second solution regarding unfolding. Since it's a simple type, I think it will be okay to have it unraveled (with an additional nil constructor). For reference, here is my lean4 attempt:

inductive tree
| leaf (s : String)
| branch (s : String) (l : List tree)

open tree

def tree.show (t : tree) : List String :=
  loop t
where
  loop := fun
    | leaf s      => [s]
    | branch s xs => [s] ++ xs.bind loop


-- fail to show termination for
--   show.loop
-- with errors
-- structural recursion cannot be used

-- well founded recursion has not been implemented yet

[Mario Carneiro]

I think this definition is more likely to work:

mutual
def tree.show : tree → List String
| leaf s      => [s]
| branch s xs => [s] ++ show_list xs

def tree.show_list : List tree → List String
| [] => []
| (t :: ts) => «show» t ++ show_list ts
end

but "mutual structural recursion" is not implemented yet