Unexpected occurence of recursive function

Stream: general

[Henrik Böving]

Hey, I'm currently trying to define a tree data structure and do some algorithms on it:

inductive tree
| tip : tree
| node : list tree -> tree

open list

namespace tree

def count_nodes : tree → ℕ
| tip := 1
| (node children) := (foldl (+) 0 (map count_nodes children)) + 1


def count_edges : tree → ℕ
| tip := 0
| (node children) := (length children) + (foldl (+) 0 (map count_edges children))

end tree

(I just did it without data for now for simplicity sake) I got two questions regarding this code:

1. I'd expect there is some sort of sum function that does what i am trying to achieve with foldl (+) 0 list but I didn't manage to find it right away, is there one?
2. On both of these functions lean is giving me an error "unexpected occurence of recursive function" but I'm not quite sure what would be unexpected here? Both of these functions look quite normal to me.

[Yury G. Kudryashov]

My guess: the problem is that list is an inductive and Lean can't figure out that one of the trees in this list can't be the original tree.

[Henrik Böving]

If that was the case how do you think I could tell the type system about this?

[Yury G. Kudryashov]

You can avoid list. I don't know about other options. This doesn't mean that they don't exist.

[Ryan Lahfa]

Lean cannot guess that that recursive calls have an argument which is smaller than the initial one, therefore it will not allow this definition.

Changing list to something else might help, a better way is to show to Lean that it is indeed valid by providing a measure of the size of arguments.

The depthness of your trees would be such a measure.

[Ryan Lahfa]

Reading this might help: https://leanprover-community.github.io/extras/well_founded_recursion.html

[Henrik Böving]

I already thought about the well founded recursion part as well, but no matter where in the function I look it sadly doesn't give me a goal to prove the well foundedness of my relation so I wouldn't really know where to start with that as well if I dont have a goal.

[Yakov Pechersky]

It's on that page, the section at https://leanprover-community.github.io/extras/well_founded_recursion.html#using_well_founded-rel_tac

[Ryan Lahfa]

Henrik Böving said:

I already thought about the well founded recursion part as well, but no matter where in the function I look it sadly doesn't give me a goal to prove the well foundedness of my relation so I wouldn't really know where to start with that as well if I dont have a goal.

Otherwise, you might try to define the function using the well_founded API first: https://leanprover-community.github.io/mathlib_docs/init/wf.html#well_founded

[Yakov Pechersky]

After your equation compiler definition, you can provide hints to the compiler that the terms on the RHS are shrinking. Or if you have a tactic that does that proof you can provide that as well

[Mario Carneiro]

This is a nested inductive type, which should be avoided because lean generates the wrong recursor for it. I would suggest using a simple inductive type, either by using binary trees if that's an option or by explicitly constructing the list:

inductive tree' : bool → Type
| tip : tree' tt
| node : tree' ff → tree' tt
| nil : tree' ff
| cons : tree' tt → tree' ff → tree' ff
def tree := tree' tt

Here tree' tt is list tree and tree' ff is tree

[Henrik Böving]

So you are more or less simulating the mutual inductive type lean generates out of this nested inductive type with the bool argument right? Would just writing out the mutual inductive type be a nice option as well?

[Mario Carneiro]

Unfortunately mutual inductive types have a similar caveat as nested inductives

[Mario Carneiro]

Both mutual and nested inductives don't actually exist in the kernel, so the lean front end is just doing this compilation for you, and this doesn't interact very well with the equation compiler for writing recursive definitions because it was a late addition

[Henrik Böving]

So basically I'm working at a rather rough edge of lean if I use these types, alright. I'm gonna try and adopt your tree type instead and see how it goes then, thank you!