Struggling with termination over "nested" recursion

Stream: lean4

[Valentin Robert]

I am trying to write a recursive function over a datatype that contains a list of itself. I'm almost there, but I can't get my proof done:

inductive KVTree (K V : Type) where
  | KVLeaf : Bool → KVTree K V
  | KVNode : List (K × KVTree K V) → KVTree K V → KVTree K V

def sizeOfListElement (l : List T) (e : T) : sizeOf e < sizeOf l := by
  simp
  cases l
  simp
  simp
  apply Nat.lt_add_right
  simp

def interpretKVTree [BEq K] : KVTree K V → K → Bool
  | .KVLeaf b => fun _ => b
  | .KVNode kvs default => fun k =>
    match H : List.find? (fun (k', _) => k == k') kvs with
    | none => interpretKVTree default k
    | some (fst, v) => interpretKVTree v k
termination_by kv => sizeOf kv
decreasing_by

  simp
  apply Nat.lt_add_right
  trivial

  simp
  apply Nat.lt_add_right
  apply Nat.lt_add_left
  apply Nat.lt_trans (m := sizeOf (fst, v))
  simp
  apply sizeOfListElement (e := (fst, v)) (l := kvs)

The error:

tactic 'apply' failed, could not unify the type of `sizeOfListElement kvs (fst, v)`
  @sizeOf (K × KVTree K V) (instSizeOfDefault (K × KVTree K V)) (fst, v) < sizeOf kvs
with the goal
  @sizeOf (K × KVTree K V) (Prod._sizeOf_inst K (KVTree K V)) (fst, v) < sizeOf kvs

suggests that the problem is the inference of the SizeOf instance picks a different instance for my current theorem (instSizeOfDefault (K × KVTree K V)) versus when I invoke my sizeOfListElement lemma (Prod.sizeOf_inst K (KVTree K V)).

How would I go about forcing the two to use the same instance?

Or alternatively, is there a way to get my function working with much less work on my part?

[Joachim Breitner]

This default SizeOf instance certainly is a footgun. I wonder what breaks if we do without.

Anyways, your sozeOfListElement looks fishy: the size of any element is less than the size of any list, even totally unrelated ones?

[Robin Arnez]

You forgot a [SizeOf T] assumption is sizeOfListElement. Otherwise, you can do:

def interpretKVTree [BEq K] : KVTree K V → K → Bool
  | .KVLeaf b => fun _ => b
  | .KVNode kvs default => fun k =>
    match _ : List.find? (fun (k', _) => k == k') kvs with
    | none => interpretKVTree default k
    | some (_, v) => interpretKVTree v k
termination_by kv => sizeOf kv
decreasing_by all_goals grind [→ List.sizeOf_lt_of_mem, = Prod.mk.sizeOf_spec, = KVTree.KVNode.sizeOf_spec]

[Robin Arnez]

(List.sizeOf_lt_of_mem is your sizeOfListElement)