feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs

RELEASES.md

@@ -1,6 +1,22 @@
 Unreleased
 ---------
 
+* Add support for `for h : i in [start:stop] do .. ` where `h : i ∈ [start:stop]`. This feature is useful for proving
+  termination of functions such as:
+```lean
+inductive Expr where
+  | app (f : String) (args : Array Expr)
+
+def Expr.size (e : Expr) : Nat := Id.run do
+  match e with
+  | app f args =>
+    let mut sz := 1
+    for h : i in [: args.size] do
+      -- h.upper : i < args.size
+      sz := sz + size (args.get ⟨i, h.upper⟩)
+    return sz
+```
+
 * Add tactic `case'`. It is similar to `case`, but does not admit the goal on failure.
   For example, the new tactic is useful when writing tactic scripts where we need to use `case'`
   at `first | ... | ...`, and we want to take the next alternative when `case'` fails.

src/Init/Data/Array/Mem.lean

@@ -47,4 +47,11 @@ termination_by aux j _ => as.size - j
   apply Nat.lt_trans (List.sizeOf_get ..)
   simp_arith
 
+macro "array_get_dec" : tactic =>
+  `(first
+    | apply sizeOf_get
+    | apply Nat.lt_trans (sizeOf_get ..); simp_arith)
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
+
 end Array

tests/lean/run/forInRangeWF.lean

@@ -0,0 +1,10 @@
+inductive Expr where
+  | app (f : String) (args : Array Expr)
+
+def Expr.size (e : Expr) : Nat := Id.run do
+  match e with
+  | app f args =>
+    let mut sz := 1
+    for h : i in [: args.size] do
+      sz := sz + size (args.get ⟨i, h.upper⟩)
+    return sz

tests/lean/run/missingSizeOfArrayGetThm.lean

@@ -7,10 +7,6 @@ def Node.FixedBranching (n : Nat) : Node Data → Prop
   | empty => True
   | node children => children.size = n ∧ ∀ i, (children.get i).FixedBranching n
   | leaf _ => True
-decreasing_by
-  simp_wf
-  apply Nat.lt_trans (Array.sizeOf_get ..) -- TODO: remove after we add linarith
-  simp_arith
 
 structure MNode (Data : Type) (m : Nat) where
   node : Node Data