Understanding the termination checker for nested recursion

Stream: new members

[Josh Cohen]

Hi, I am trying to understand the behavior and limits of the termination checker when we have a nested recursive type, like a rose tree:

inductive rose (α: Type) : Type where
| leaf : α → rose α
| node: List (rose α) → rose α

I can define a size function exactly as I would expect:

def rose_size (r: rose α) : Nat :=
  match r with
  | .leaf _ => 1
  | .node l => List.sum (List.map rose_size l)

But if I try to write an equality function (purely as an example), Lean cannot prove termination:

def map2 (f: α → β → γ) : List α → List β → List γ
  | x :: xs, y :: ys => f x y :: map2 f xs ys
  | _, _ => []

def rose_eq (eq: α → α → Bool) (r1 r2: rose α) : Bool :=
  match r1, r2 with
  | .leaf x1, .leaf x2 => eq x1 x2
  | .node l1, .node l2 => List.all (map2 (rose_eq eq) l1 l2) id
  | _, _ => false

In this context, I don't understand why Lean treats the use of List.map and map2 differently when it comes to termination. Is there a way to define map2 so that the above typechecks? If so, what is the general rule? I know I can use a nested recursive function, but I am trying to do without to see how Lean's termination checking works.

[Aaron Liu]

the termination checker doesn't know that map2 calls its testing function with elements of the list

[Aaron Liu]

it also doesn't know that List.map calls its function elements from the list, but List.map has a theorem docs#List.map_wfParam which is used in preprocessing to "attach" this information to the list

[Aaron Liu]

map2 does not have such a theorem since you didn't write one

[Aaron Liu]

you can use docs#List.attach to attach the information to your list

[Aaron Liu]

you can also use structural recursion by writing out the map manually and making it mutually recursive with your defintion

[Josh Cohen]

Aaron Liu said:

map2 does not have such a theorem since you didn't write one

Thanks for the pointers, that is helpful. I tried to write a similar theorem for map2:

@[wf_preprocess] theorem map2_wfParam {xs : List α} {ys: List β} {f : α → β → γ} :
    (wfParam xs).map2 f ys = xs.attach.unattach.map2 f ys := by
  simp [wfParam]

But that still doesn't seem the satisfy the termination checker. Is that theorem the one I want?

[Robin Arnez]

You need the theorem defined below as well, docs#List.map_unattach

[Josh Cohen]

Thank you, that worked! So just to clarify, for each such function I want to use in a nested way, I would need the _wfParam lemma (or at least to inline the attach.unattach pattern in the recursive call) and then the _unattach theorem?

[Aaron Liu]

you could also just call it with the attached lists

[Aaron Liu]

like

def rose_eq (eq: α → α → Bool) (r1 r2: rose α) : Bool :=
  match r1, r2 with
  | .leaf x1, .leaf x2 => eq x1 x2
  | .node l1, .node l2 => List.all (map2 (rose_eq eq) l1.attach l2.attach) id
  | _, _ => false

[Josh Cohen]

This gives me an error because rose_eq expects a List a rather than a List of sigma types. Am I missing a coercion somewhere?

[Aaron Liu]

probably I forgot to put a coercion somewhere

[Aaron Liu]

try

def rose_eq (eq: α → α → Bool) (r1 r2: rose α) : Bool :=
  match r1, r2 with
  | .leaf x1, .leaf x2 => eq x1 x2
  | .node l1, .node l2 => List.all
    (map2 (fun x y => rose_eq eq x.1 y.1) l1.attach l2.attach) id
  | _, _ => false

[Josh Cohen]

This version seems to end up back at the original error message. I suppose I would need to add a manual proof obligation that x : { x // x ∈ l1 } implies sizeOf x.val < 1 + sizeOf l1, which shouldn't be too hard (though now that I think about it, I'm not sure how the sizeOf operator is defined).

[Robin Arnez]

Almost, you need (fun ⟨x, _⟩ ⟨y, _⟩ => rose_eq eq x y)