wfParam propagation through lets

[nomeata]

David gave me this example:

structure Tree where
  children : List Tree

/--
error: failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
t c : Tree
⊢ sizeOf c < sizeOf t
-/
#guard_msgs in  
def Tree.depth (t : Tree) : Nat :=
  let children := t.children
  let depths := children.map fun c => Tree.depth c
  match depths.max? with
  | some d => d+1
  | none => 0
termination_by t

This shows that wfParam propagation is incomplete; it should float a wfParam from the definition of children to the occurrences. Should be doable.

Versions

Lean 4.18.0-nightly-2025-02-11

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.