Better tactics for showing that recursive calls are "decreasing"

The ideal solution must include forward chaining + linear arithmetic.
Here is an example where the builtin tactic in the core fails:

import Mathlib.Data.List.Defs
import Std.Data.List.Basic

open Option

inductive Val where
  | Int (i : Int)
  | Tag (ps : List (String × Val))

def asInt : Val → Option Int
  | .Int i => some i
  | _      => none

inductive Expr where
  | Int (i : Int)
  | Add (es : List Expr)
  | Tag (ps : List (String × Expr))

def interpret : Expr → Option Val
  | .Int i  => some (Val.Int i)
  | .Add es => do -- works with attach
    let vs ← es.attach.mapM (fun ⟨e, _⟩ => interpret e)
    let is ← vs.mapM asInt
    some (Val.Int is.sum)
  | .Tag ps => do -- doesn't work with attach: termination proof fails
    let vs ← ps.attach.mapM (fun ⟨⟨s, e⟩, _⟩ => do let v ← interpret e; some (s, v))
    some (Val.Tag vs)

Here is the a possible workaround.

import Mathlib.Tactic.Linarith
import Mathlib.Data.List.Defs
import Std.Data.List.Basic

open Option

inductive Val where
  | Int (i : Int)
  | Tag (ps : List (String × Val))

def asInt : Val → Option Int
  | .Int i => some i
  | _      => none

inductive Expr where
  | Int (i : Int)
  | Add (es : List Expr)
  | Tag (ps : List (String × Expr))

def interpret : Expr → Option Val
  | .Int i  => some (Val.Int i)
  | .Add es => do -- works with attach
    let vs ← es.attach.mapM (fun ⟨e, _⟩ => interpret e)
    let is ← vs.mapM asInt
    some (Val.Int is.sum)
  | .Tag ps => do -- doesn't work with attach: termination proof fails
    let vs ← ps.attach.mapM (fun ⟨(s, e), h⟩ => do
      have : sizeOf e < 1 + sizeOf ps := by
        have : sizeOf (s, e) < sizeOf ps := by apply List.sizeOf_lt_of_mem; assumption
        have : sizeOf e < sizeOf (s, e) := by simp
        linarith
      let v ← interpret e; some (s, v))
    some (Val.Tag vs)
/-
By including the `termination_by` we ensure Lean will produce an error message saying where it failed to
prove that call is "decreasing". Then, we learn that it failed to prove that `sizeOf e < 1 + sizeOf ps`.
I "fix" the issue by adding a manual proof. We need better automation in the core for proving this kind of example automatically.
-/
termination_by interpret e => e

Reproduce the recursive interpret example, especially the Expr.Tag branch using ps.attach.mapM and termination_by interpret e => e. Start by examining the termination-checking path that handles decreasing recursive calls and the existing forward-chaining or linear-arithmetic support. Done means the original example verifies without the manual sizeOf proof.