How to prove termination of nested list

Stream: lean4

[Rikiya Kashiwagi]

The function below fails to prove termination at loop of line 5

inductive NestedList : Type
  | nl : List NestedList → NestedList

def loop : NestedList → NestedList
  | .nl lss => .nl (List.map loop lss)
termination_by lss => sizeOf lss

The error message says:

lss : List NestedList
a✝ : NestedList
⊢ sizeOf a✝ < 1 + sizeOf lss

but where does a✝ come from?
Since we don't know it, it seems termination proof is impossible for this function. or we cannot prove this kind of termination problem using sizeOf?

[Edward van de Meent]

it comes from the unfolding of List.map

[Edward van de Meent]

in the literal context where it applies loop , lean doesn't know that a was orignally a member of lss. using lss.attach.map (fun ⟨a,_⟩ => loop a) might fix this

[Edward van de Meent]

(what that does is add the hypothesis a \in lss to the context of the term loop a)

[Rikiya Kashiwagi]

Thanks, it worked.
I hope that somehow the error message will imply such a solution in the future.

[Kim Morrison]

We're thinking about it! (Even some ideas so you don't need to write the attach in the first place.)