termination_by proof

Stream: lean4

[Henrik Böving]

Given this declaration:

inductive Foo where
| text : String → Foo
| element : Array Foo → Foo

namespace Foo

def textLength : Foo → Nat
| text s => s.length
| element children =>
  let lengths := children.map textLength
  lengths.foldl Nat.add 0

end Foo

How can I proof textLength terminating? I'm guessing it would be related to the fact that I'm always unwrapping one element per recursive call but I'm not sure how i can express this.

[Chris B]

You should be able to use the SizeOf instances for Foo and Array, but this particular use of a nested inductive might not be ready; if you feign having a termination proof, you still get unexpected occurrence of recursive application Foo.textLength.

[Henrik Böving]

It shall be a partial in this case!

[Chris B]

Something like this will be good for the eventual well-founded docs though, this pattern is pretty common.

[Henrik Böving]

Yeah that's why I though it might just work^^ I'd love to help on the well founded docs but I don't really have a full picture on how it works myself yet

[Alexander Bentkamp]

I think the main issue is that the recursive call to textLength appears unapplied in your definition. Here is a definition that avoids that:

mutual
  def textLength : Foo → Nat
    | text s => s.length
    | element xs =>
      have _ : sizeOf xs < 1 + sizeOf xs := sorry
      textLengthArr xs
  def textLengthArr : Array Foo → Nat
    | {data := []} => 0
    | {data := x :: xs} =>
      have _ : sizeOf x < 1 + (1 + sizeOf x + sizeOf xs) := sorry
      have _ : 1 + sizeOf xs < 1 + (1 + sizeOf x + sizeOf xs) := sorry
      textLength x + textLengthArr {data := xs}
end
termination_by _ f => SizeOf.sizeOf f

The sorrys should be doable although they certainly make me wish we had linarith already :D