Keeley Hoek (Jun 12 2019 at 11:27):
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 (Jun 12 2019 at 11:33):
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 (Jun 12 2019 at 11:36):
I mean't the former---why is it expected that it fails?
Reid Barton (Jun 12 2019 at 11:37):
It wouldn't be so great if you instead had
id' height n where
id' f n := f (n+1)
Reid Barton (Jun 12 2019 at 11:38):
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 (Jun 12 2019 at 11:39):
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 (Jun 12 2019 at 11:39):
Well because you don't even have an application of
Keeley Hoek (Jun 12 2019 at 11:40):
aha! ok. Thanks! :)
Yakov Pechersky (Apr 01 2021 at 01:39):
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 (Apr 01 2021 at 01:42):
Or is this an issue of a nested inductive?
Yakov Pechersky (Apr 01 2021 at 01:45):
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 (Apr 01 2021 at 02:37):
TPIL says that Lean supports type definitions like the one you originally wrote:
I don't know what that error means, though.
Yakov Pechersky (Apr 01 2021 at 02:51):
I'm going to try lean4 later to see if it fares better here
Greg Price (Apr 01 2021 at 04:00):
Ah, there's also some perhaps helpful information in the previous history of this topic:
(Which I happened to notice above this just now.)
Greg Price (Apr 01 2021 at 04:00):
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 (Apr 01 2021 at 04:08):
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"]
list.bind as part of a mutual recursion.
Greg Price (Apr 01 2021 at 04:13):
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 (Apr 01 2021 at 04:28):
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 (Apr 01 2021 at 04:31):
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 (Apr 01 2021 at 04:32):
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 (Apr 01 2021 at 04:36):
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 (Apr 01 2021 at 08:21):
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
Last updated: May 15 2021 at 02:11 UTC