From 9d55d7bf9e6dee2e61c9812c966239b0eccd135e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Apr 2022 18:38:55 -0700
Subject: [PATCH] feat: add helper tactic for applying `List.sizeOf_lt_of_mem`
 in termination proofs

---
 src/Init/Data/List/BasicAux.lean |  9 +++++++++
 tests/lean/run/forInRangeWF.lean | 14 ++++++++++++++
 2 files changed, 23 insertions(+)

diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 1877c76a46..a7a4451166 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -121,6 +121,15 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
   | head => simp_arith
   | tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
 
+macro "sizeOf_list_dec" : tactic =>
+  `(first
+    | apply sizeOf_lt_of_mem; assumption; done
+    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+      case' h => assumption
+      simp_arith)
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
+
 theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs := by
   induction as with
   | nil => assumption
diff --git a/tests/lean/run/forInRangeWF.lean b/tests/lean/run/forInRangeWF.lean
index 34adf9bd67..5070e8a8e6 100644
--- a/tests/lean/run/forInRangeWF.lean
+++ b/tests/lean/run/forInRangeWF.lean
@@ -8,3 +8,17 @@ def Expr.size (e : Expr) : Nat := Id.run do
     for h : i in [: args.size] do
       sz := sz + size (args.get ⟨i, h.upper⟩)
     return sz
+
+namespace Ex2
+inductive Expr where
+  | app (f : String) (args : List Expr)
+
+def Expr.size (e : Expr) : Nat := Id.run do
+  match e with
+  | app f args =>
+    let mut sz := 1
+    for h : arg in args do
+      sz := sz + size arg
+    return sz
+
+end Ex2