Termination for Rewrite Validity Proof

Stream: Program verification

[Jesse Slater]

(Apologies, this is an MWE but it is long nonetheless)
I have a DSL for computations on vectors, and a definition of a rewrite on an AST which comes bundled with a proof that the rewrite preserves semantics when applied at the root. I have a function which takes a rewrite and an AST and returns the list of all possible resulting ASTs generated by applying the rewrite to the original AST once. I am having trouble with termination in the proof that this code is correct.

My issue is in the append function, and I think it is related to the fact that the type of the append constructor contains addition. The correlate constructor also takes two inductive parameters, but it's part of the termination proof goes through.

import Mathlib

inductive VecExpr : Nat → Type
  | const :
    (Fin n → Nat) → VecExpr n
  | append :
    VecExpr l → VecExpr r → VecExpr (l + r)
  | correlate :
    VecExpr n → VecExpr m → VecExpr n

def VecExpr.eval : (VecExpr n) → (Fin n → Nat) := sorry --omitted

abbrev VecExpr.rewrites_to (expr expr' : VecExpr n) := expr.eval = expr'.eval

structure Rewrite where
  apply_at_root : (VecExpr n) → Option (VecExpr n)
  rewrite_valid
    (rule_applies : apply_at_root expr = some expr') :
    expr.rewrites_to expr'

def Rewrite.apply_everywhere
  (r : Rewrite ) (expr : VecExpr n)
  : List (VecExpr n) :=
  let app_rec : List (VecExpr n) :=
    match expr with
    | .const _ => []
    | .append expr' expr'' =>
      (r.apply_everywhere expr').map (.append · expr'')
      ++ (r.apply_everywhere expr'').map (.append expr' ·)
    | .correlate expr' expr'' =>
      (r.apply_everywhere expr').map (.correlate · expr'')
      ++ (r.apply_everywhere expr'').map (.correlate expr' ·)
  if let some expr' := r.apply_at_root expr
  then expr' :: app_rec
  else app_rec

theorem Append.rewrite_case_left
  {expr expr' : VecExpr l} {expr'': VecExpr r} (rewrite : expr.rewrites_to expr')
  : (expr.append expr'').rewrites_to (expr'.append expr'') := sorry --omitted

theorem Append.rewrite_case_right
  {expr : VecExpr l} {expr' expr'': VecExpr r} (rewrite : expr'.rewrites_to expr'')
  : (expr.append expr').rewrites_to (expr.append expr'') := sorry --omitted

theorem Correlate.rewrite_case_left
  {expr expr' : VecExpr l} {expr'': VecExpr r} (rewrite : expr.rewrites_to expr')
  : (expr.correlate expr'').rewrites_to (expr'.correlate expr'') := sorry --omitted

theorem Correlate.rewrite_case_right
  {expr : VecExpr l} {expr' expr'': VecExpr r} (rewrite : expr'.rewrites_to expr'')
  : (expr.correlate expr').rewrites_to (expr.correlate expr'') := sorry --omitted

theorem Rewrite.apply_everywhere_valid
  (r : Rewrite) {expr expr' : VecExpr n} (mem : expr' ∈ r.apply_everywhere expr)
  : expr.rewrites_to expr' := by
  unfold apply_everywhere at mem
  split at mem
  <;> split at mem
  <;> simp_all only [imp_false, List.mem_cons, List.mem_append, List.mem_map]
  <;> cases mem
  case h_1.h_1.inl head_rewritten eq =>
      obtain rfl := eq
      exact r.rewrite_valid head_rewritten
  case h_1.h_1.inr mem =>
      simp_all only [List.not_mem_nil]
  case h_2.h_1.inl head_rewritten eq =>
      obtain rfl := eq
      exact r.rewrite_valid head_rewritten
  case h_2.h_1.inr mem =>
      cases mem
      <;> (rename_i ex; rcases ex with ⟨_, mem', rfl⟩)
      · exact Append.rewrite_case_left (r.apply_everywhere_valid mem')
      · exact Append.rewrite_case_right (r.apply_everywhere_valid mem')
  case h_2.h_2.inl ex =>
      rcases ex with ⟨_, mem', rfl⟩
      exact Append.rewrite_case_left (r.apply_everywhere_valid mem')
  case h_2.h_2.inr ex =>
      rcases ex with ⟨_, mem', rfl⟩
      exact Append.rewrite_case_right (r.apply_everywhere_valid mem')
  case h_3.h_1.inl head_rewritten eq =>
      obtain rfl := eq
      exact r.rewrite_valid head_rewritten
  case h_3.h_1.inr mem =>
      cases mem
      <;> (rename_i ex; rcases ex with ⟨_, mem', rfl⟩)
      · exact Correlate.rewrite_case_left (r.apply_everywhere_valid mem')
      · exact Correlate.rewrite_case_right (r.apply_everywhere_valid mem')
  case h_3.h_2.inl ex =>
      rcases ex with ⟨_, mem', rfl⟩
      exact Correlate.rewrite_case_left (r.apply_everywhere_valid mem')
  case h_3.h_2.inr ex =>
      rcases ex with ⟨_, mem', rfl⟩
      exact Correlate.rewrite_case_right (r.apply_everywhere_valid mem')
  termination_by sizeOf expr'
  decreasing_by
    all_goals rename_i eq
    any_goals rw [← eq]
    any_goals simp_wf
    any_goals omega