From 64cfbc1ae33a7a3167a84678a0d4137eaa618e8f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Apr 2022 18:29:41 -0700
Subject: [PATCH] feat: add helper tactic for applying `sizeOf (a.get i) <
 sizeOf a` automatically in termination proofs

---
 RELEASES.md                                  | 16 ++++++++++++++++
 src/Init/Data/Array/Mem.lean                 |  7 +++++++
 tests/lean/run/forInRangeWF.lean             | 10 ++++++++++
 tests/lean/run/missingSizeOfArrayGetThm.lean |  4 ----
 4 files changed, 33 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/forInRangeWF.lean

diff --git a/RELEASES.md b/RELEASES.md
index 32a2c4eace..faeee0f959 100644
--- a/RELEASES.md
+++ b/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.
diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean
index 8dccc1086c..d17a746fb6 100644
--- a/src/Init/Data/Array/Mem.lean
+++ b/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
diff --git a/tests/lean/run/forInRangeWF.lean b/tests/lean/run/forInRangeWF.lean
new file mode 100644
index 0000000000..34adf9bd67
--- /dev/null
+++ b/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
diff --git a/tests/lean/run/missingSizeOfArrayGetThm.lean b/tests/lean/run/missingSizeOfArrayGetThm.lean
index e518b2ac0d..058e020c0a 100644
--- a/tests/lean/run/missingSizeOfArrayGetThm.lean
+++ b/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