Zulip Chat Archive

Stream: new members

Topic: Why the following requires partial?


Luis Enrique Muñoz Martín (Jul 28 2024 at 10:14):

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 (Jul 28 2024 at 11:06):

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 (Jul 28 2024 at 11:06):

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

Yury G. Kudryashov (Jul 28 2024 at 11:09):

BTW, this doesn't work either:

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

Luis Enrique Muñoz Martín (Jul 28 2024 at 11:49):

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 (Jul 28 2024 at 11:56):

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

Yury G. Kudryashov (Jul 28 2024 at 12:27):

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

Edward van de Meent (Jul 28 2024 at 12:33):

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 (Jul 28 2024 at 12:35):

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 (Jul 28 2024 at 12:41):

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

Edward van de Meent (Jul 28 2024 at 12:43):

use a termination_by clause

Luis Enrique Muñoz Martín (Jul 28 2024 at 18:17):

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

Mario Carneiro (Jul 28 2024 at 18:27):

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

Last updated: May 02 2025 at 03:31 UTC