structural recursion cannot be used

Stream: lean4

[Kyle Miller]

How can I show that nodes terminates in the following example?

inductive Foo
| a : Foo → Foo
| b : String × Foo → Foo
| c : Foo

namespace Foo

def nodes : Foo → Nat
| a x => x.nodes + 1
| b _ => 1
| c => 1
/-
fail to show termination for
  Foo.nodes
with errors
structural recursion cannot be used

'termination_by' modifier missing
-/

end Foo

[Kyle Miller]

Changing it to the following, Lean's able to see that the function terminates, but in what I'm actually doing, b has a List (String × Foo) instead.

inductive Foo
| a : Foo → Foo
| b : String → Foo → Foo
| c : Foo

namespace Foo

def nodes : Foo → Nat
| a x => x.nodes + 1
| b _ _ => 1
| c => 1

end Foo

[Mario Carneiro]

You should try termination_by

[Kyle Miller]

Mario Carneiro said:

You should try termination_by

... Yes, I read the error message and I messed around with it for a bit, looking up uses of termination_by in the lean4 repository, but I couldn't see how to use it for this.

[Mario Carneiro]

worst case scenario I believe you can use the Foo recursor directly, but hopefully the autogenerated sizeof instance works

[Kyle Miller]

Thanks for the sizeOf pointer.

Is there a simpler way to write this than what I did below? (Are there plans to make writing recursive functions like this easier?)

inductive Foo
| a : Foo → Foo
| b : String × Foo → Foo
| c : Foo

namespace Foo

def nodes (f : Foo) : Nat :=
  match f with
  | a x =>
    have : sizeOf x < 1 + sizeOf x := by
      rw [Nat.add_comm]
      apply Nat.le_refl
    x.nodes + 1
  | b _ => 1
  | c => 1
termination_by _ => sizeOf f

end Foo