Missing property required to prove termination when using decreasing_by

Prerequisites

• [ x] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [x ] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [x ] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Some inductive types have missing properties for proving termination in certain functions . The code below shows two functions defined for an inductive type. Both functions use recursion in the same way, and require manual termination proofs. For some reason, the second function has a missing property which makes it impossible to prove termination.

inductive Typ where
  | int 
  | rcrd (fields : List (Typ × String))

def Typ.size : Typ → Nat
  | .int => 1
  | .rcrd fields => 
    fields.foldl (· + ·.fst.size) 0
decreasing_by
  induction fields
  · grind
  · grind 

def Typ.simplify : Typ → Typ
  | .int => .int
  | .rcrd fields =>
    .rcrd (fields.map (·.map (·.simplify) (id)))
decreasing_by
  induction fields
  · grind
  · -- Impossible due to missing property : x✝ = x✝¹.1

Steps to Reproduce

0. Paste the code above into the lean4 nightly playground

Expected behavior: Possible to prove termination for both functions.

Actual behavior: Missing property for the second function makes termination proof impossible.

Versions

Version: "4.34.0, commit 3259610687883ec1ea48c481aba2469f2f83facf"

Additional Information

This issue is also observed when using Sum instead of Prod in the inductive type. Likewise, the example below might be related and has an interesting solution which unfortunately does not work for the list case:

inductive Typ2 where
  | int 
  | rcrd (hd : Typ2 × String) (fields : List (Typ2 × String))
deriving Inhabited

def Typ2.size : Typ2 → Nat
  | .int => 1
  | .rcrd hd fields => 
    fields.foldl (· + ·.fst.size) hd.fst.size
decreasing_by
  induction fields
  · grind
  · grind 
  grind

def Typ2.simplify : Typ2 → Typ2
  | .int => .int
  | .rcrd hd fields =>
    .rcrd (hd.map (·.simplify) (id)) (fields.map (·.map (·.simplify) (id)))
decreasing_by
  · grind -- Impossible due to missing property : x✝ = hd.1
  · grind -- Impossible due to missing property : x✝ = x✝¹.1

def Typ2.simplify2 : Typ2 → Typ2
  | .int => .int
  | .rcrd ⟨tp, name⟩ fields =>
    .rcrd ⟨tp.simplify2, name⟩ (fields.map (·.map (·.simplify2) (id)))
decreasing_by
  · grind -- Now possible
  · grind -- Impossible due to missing property : x✝ = x✝¹.1

def Typ2.simplify3 : Typ2 → Typ2
  | .int => .int
  | .rcrd ⟨tp, name⟩ fields =>
    .rcrd ⟨tp.simplify3, name⟩ (fields.map (fun ⟨tp, name⟩ => ⟨tp.simplify3, name⟩ ))
decreasing_by
  · grind -- Now possible
  · grind -- Still Impossible due to missing property : tp = x✝.1

def Typ2.simplify4 : Typ2 → Typ2
  | .int => .int
  | .rcrd ⟨tp, name⟩ [] => .rcrd ⟨tp.simplify4, name⟩ []
  | .rcrd hd (⟨tp1,name1⟩::xs) =>
    match (Typ2.rcrd hd xs).simplify4 with
    | .rcrd hd fields => .rcrd hd (⟨tp1.simplify, name1⟩::fields)
    | _ => panic! "Unreachable"
  decreasing_by
  · grind -- Now possible
  · grind -- Now possible

Start by reproducing the minimal Typ.simplify example in the Lean nightly playground, then compare its decreasing_by obligations with Typ.size and the working Typ2 variants. Trace how termination obligations are generated for recursive calls under List.map and product projections. Done means the reported missing equality property is available so the supplied termination proofs succeed.