proving termination of simple function over recursive type

Stream: new members

[chris477]

Hi!
I'm trying to implement some simple functions over a recursive data type but am not able to prove that the terminate.
Here is a minimal example:

structure G where
  offset : ℕ
  recursive : List (G × G)

def G.sum (g : G) : ℕ :=
  g.recursive.foldl (fun acc (g1, g2) => acc + g1.sum + g2.sum) g.offset

Or am I looking at this the wrong way and such structures can actually be self-containing?
Thank you for your help!

[Aaron Liu]

I would suggest some structural recursion

[Aaron Liu]

That means you will have to write out the foldl

[Robin Arnez]

This works:

structure G where
  offset : Nat
  recursive : List (G × G)

def G.sum (g : G) : Nat :=
  match g with
  | { recursive, .. } =>
    recursive.foldl (fun acc gs =>
      match _ : gs with
      | (g1, g2) => acc + g1.sum + g2.sum) g.offset
decreasing_by all_goals grind [→ List.sizeOf_lt_of_mem, Prod.mk.sizeOf_spec, G.mk.sizeOf_spec]

[chris477]

Oh nice, thanks a lot! Although this is all a bit combersome. Since I don't strictly need recursion, maybe I'll limit the recursion depth or something.

[Robin Arnez]

If you don't intend to prove anything about it you can also simply tag it as a partial def

[Robin Arnez]

and keep the original definition without needing to prove termination

[chris477]

This might sound weird, but in my application, the recursion depth is probably not much more than 5, so does it make sense to bake the depth into the data type similar to

structure G (depth : Nat) where
  offset : Nat
  recursive : List (G (depth - 1) × G (depth - 1))

Of course it does not work like that since depth - 1 is not valid for all numbers in Nat, is there something similar that could work?

I'm still a bit baffled that something like a function returning the recursion depth is not obviously terminating for lean.

[Aaron Liu]

chris477 said:

I'm still a bit baffled that something like a function returning the recursion depth is not obviously terminating for lean.

Nothing is "obviously" terminating, there's just a lot of automation set up to try to prove termination in different ways, and this is a case that the automation fails.