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 .elem
ends 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