From 86328bcb9f587b7c54db8ecb61eb00d025469dd2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 16 Feb 2022 11:25:46 -0800
Subject: [PATCH] feat: tail recursive `List.iota` and `[csimp]` theorem

---
 src/Init/Data/List/Basic.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 1e0c40708f..5b825b4e76 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -310,6 +310,20 @@ def iota : Nat → List Nat
   | 0       => []
   | m@(n+1) => m :: iota n
 
+def iotaTR (n : Nat) : List Nat :=
+  let rec go : Nat → List Nat → List Nat
+    | 0, r => r.reverse
+    | m@(n+1), r => go n (m::r)
+  go n []
+
+@[csimp]
+theorem iota_eq_iotaTR : @iota = @iotaTR :=
+  have aux (n : Nat) (r : List Nat) : iotaTR.go n r = r.reverse ++ iota n := by
+    induction n generalizing r with
+    | zero => simp [iota, iotaTR.go]
+    | succ n ih => simp [iota, iotaTR.go, ih, append_assoc]
+  funext fun n => by simp [iotaTR, aux]
+
 def enumFrom : Nat → List α → List (Nat × α)
   | n, [] => nil
   | n, x :: xs   => (n, x) :: enumFrom (n + 1) xs