Why the following requires partial?

Stream: new members

[Luis Enrique Muñoz Martín]

Hi, in the following simple example, I don't fully understand why it requires partial:

inductive Foo where
  | elem
  | list (l : List Unit)

partial def Foo.toString : Foo -> String
  | .elem => "e"
  | .list l => .join (.map (fun () => Foo.toString .elem) l)

#eval Foo.toString $ Foo.list [(), (), (), ()]  -- "eeee"

From my understanding calling Foo.toString over .elemends the recursion, and the lists are finite. Why Lean can not determine this always ends?

[Yury G. Kudryashov]

For reference, here are the errors Lean reports without partial:

structural recursion cannot be used:

argument #1 cannot be used for structural recursion
  its type does not have a recursor

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
l: List Unit

[Yury G. Kudryashov]

I don't understand why structural recursion can't be used.

[Yury G. Kudryashov]

BTW, this doesn't work either:

def Foo.toString : Foo -> String
  | .elem => "e"
  | .list _ => Foo.toString .elem

[Luis Enrique Muñoz Martín]

But this, as expected, works:

def Foo.toString : Foo -> String
  | .elem => "e"
  | .list [] =>  ""
  | .list (x :: xs) => Foo.toString .elem

So the problem seems that it's mandatory to match over the list parameter. But it's a pity. Does there exist any workaround for this? Or, each time I use directly a list parameter without matching it, I lose the structural recursion detection?

[Edward van de Meent]

the problem is that lean has trouble proving that sizeOf l is at least 1 for all l : List Unit

[Yury G. Kudryashov]

Why can't it use structural recursion and falls back to the well-founded recursion?

[Edward van de Meent]

you can't use Foo.rec because the structure of the recursion doesn't agree with the structure of your definition, if that's what you mean by "well-founded recursion". you can use structural recursion, but you'll have to help lean proving the fact i mentioned before, possibly by adding a have term to the .list branch

[Edward van de Meent]

to elaborate on the first part:
because the type of Foo.list doesn't have a Foo-dependant argument (i.e. either Foo itself or some m Foo with m a dependent type), using Foo.rec won't allow you to reference the function you're defining.

[Yury G. Kudryashov]

BTW, how can I use a custom measure instead of sizeOf?

[Edward van de Meent]

use a termination_by clause

[Luis Enrique Muñoz Martín]

For a noob in this regard like me. How would the code look like with the above termination_by ?

[Mario Carneiro]

def Foo.toString : Foo -> String
  | .elem => "e"
  | .list l => .join (.map (fun () => Foo.toString .elem) l)
termination_by x => match x with | .elem => 0 | .list _ => 1