chore: deprecate List.iota (leanprover#6708)

This PR deprecates `List.iota`, which we make no essential use of. `iota
n` can be replaced with `(range' 1 n).reverse`. The verification lemmas
for `range'` already have better coverage than those for `iota`.
Any downstream projects using it (I am not aware of any) are encouraged
to adopt it.

Author: kim-em

src/Init/Data/List/Basic.lean

@@ -1520,11 +1520,14 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
 `O(n)`. `iota n` is the numbers from `1` to `n` inclusive, in decreasing order.
 * `iota 5 = [5, 4, 3, 2, 1]`
 -/
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 def iota : Nat → List Nat
   | 0       => []
   | m@(n+1) => m :: iota n
 
+set_option linter.deprecated false in
 @[simp] theorem iota_zero : iota 0 = [] := rfl
+set_option linter.deprecated false in
 @[simp] theorem iota_succ : iota (i+1) = (i+1) :: iota i := rfl
 
 /-! ### enumFrom -/
@@ -1848,12 +1851,14 @@ def unzipTR (l : List (α × β)) : List α × List β :=
 /-! ### iota -/
 
 /-- Tail-recursive version of `List.iota`. -/
+@[deprecated "Use `List.range' 1 n` instead of `iota n`." (since := "2025-01-20")]
 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 []
 
+set_option linter.deprecated false in
 @[csimp]
 theorem iota_eq_iotaTR : @iota = @iotaTR :=
   have aux (n : Nat) (r : List Nat) : iotaTR.go n r = r.reverse ++ iota n := by

src/Init/Data/List/Nat/Range.lean

@@ -195,24 +195,32 @@ theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n -
 
 /-! ### iota -/
 
+section
+set_option linter.deprecated false
+
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)
   | 0 => rfl
   | n + 1 => by simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm]
 
-@[simp] theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range']
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range']
 
-@[simp] theorem iota_eq_nil {n : Nat} : iota n = [] ↔ n = 0 := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem iota_eq_nil {n : Nat} : iota n = [] ↔ n = 0 := by
   cases n <;> simp
 
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem iota_ne_nil {n : Nat} : iota n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp]
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
 theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 0 < m ∧ m ≤ n := by
   simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ]
   omega
 
-@[simp] theorem iota_inj : iota n = iota n' ↔ n = n' := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem iota_inj : iota n = iota n' ↔ n = n' := by
   constructor
   · intro h
     have h' := congrArg List.length h
@@ -221,6 +229,7 @@ theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 0 < m ∧ m ≤ n := by
   · rintro rfl
     simp
 
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem iota_eq_cons_iff : iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n - 1) := by
   simp [iota_eq_reverse_range']
   simp [range'_eq_append_iff, reverse_eq_iff]
@@ -234,6 +243,7 @@ theorem iota_eq_cons_iff : iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n
     rw [eq_comm, range'_eq_singleton]
     omega
 
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem iota_eq_append_iff : iota n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = iota k := by
   simp only [iota_eq_reverse_range']
   rw [reverse_eq_append_iff]
@@ -245,42 +255,52 @@ theorem iota_eq_append_iff : iota n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (rang
   · rintro ⟨k, h, rfl, rfl⟩
     exact ⟨k, by simp; omega⟩
 
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem pairwise_gt_iota (n : Nat) : Pairwise (· > ·) (iota n) := by
   simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range' 1 n
 
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem nodup_iota (n : Nat) : Nodup (iota n) :=
   (pairwise_gt_iota n).imp Nat.ne_of_gt
 
-@[simp] theorem head?_iota (n : Nat) : (iota n).head? = if n = 0 then none else some n := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem head?_iota (n : Nat) : (iota n).head? = if n = 0 then none else some n := by
   cases n <;> simp
 
-@[simp] theorem head_iota (n : Nat) (h) : (iota n).head h = n := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem head_iota (n : Nat) (h) : (iota n).head h = n := by
   cases n with
   | zero => simp at h
   | succ n => simp
 
-@[simp] theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by
   cases n <;> simp
 
-@[simp] theorem reverse_iota : reverse (iota n) = range' 1 n := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem reverse_iota : reverse (iota n) = range' 1 n := by
   induction n with
   | zero => simp
   | succ n ih =>
     rw [iota_succ, reverse_cons, ih, range'_1_concat, Nat.add_comm]
 
-@[simp] theorem getLast?_iota (n : Nat) : (iota n).getLast? = if n = 0 then none else some 1 := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem getLast?_iota (n : Nat) : (iota n).getLast? = if n = 0 then none else some 1 := by
   rw [getLast?_eq_head?_reverse]
   simp [head?_range']
 
-@[simp] theorem getLast_iota (n : Nat) (h) : (iota n).getLast h = 1 := by
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem getLast_iota (n : Nat) (h) : (iota n).getLast h = 1 := by
   rw [getLast_eq_head_reverse]
   simp
 
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
 theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
     (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i := by
   simp
 
-@[simp] theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
+@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
+theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by
   rw [find?_eq_some_iff_append]
   simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
@@ -317,6 +337,8 @@ theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
       · omega
       · omega
 
+end
+
 /-! ### enumFrom -/
 
 @[simp]

src/Lean/Language/Basic.lean

@@ -185,7 +185,7 @@ language server.
 -/
 def withAlwaysResolvedPromises [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] [Inhabited α]
     (count : Nat) (act : Array (IO.Promise α) → m Unit) : m Unit := do
-  let ps ← List.iota count |>.toArray.mapM fun _ => IO.Promise.new
+  let ps ← Array.range count |>.mapM fun _ => IO.Promise.new
   try
     act ps
   finally

tests/bench/mergeSort/Bench.lean

@@ -5,14 +5,14 @@ def main (args : List String) : IO Unit := do
   let some arg := args[0]? | throw <| IO.userError s!"specify length of test data in multiples of 10^{k}"
   let some i := arg.toNat? | throw <| IO.userError s!"specify length of test data in multiples of 10^{k}"
   let n := i * (10^k)
-  let i₁ := List.iota n
+  let i₁ := (List.range' 1 n).reverse
   let i₂ := List.range n
   let i₃ ← (List.range n).mapM (fun _ => IO.rand 0 1000)
-  let i₄ := (List.range (i * (10^(k-3)))).bind (fun k => (k * 1000 + 1) :: (k * 1000) :: List.range' (k * 1000 + 2) 998)
+  let i₄ := (List.range (i * (10^(k-3)))).flatMap (fun k => (k * 1000 + 1) :: (k * 1000) :: List.range' (k * 1000 + 2) 998)
   let start ← IO.monoMsNow
-  let o₁ := (mergeSortTR₂ (· ≤ ·) i₁).length == n
-  let o₂ := (mergeSortTR₂ (· ≤ ·) i₂).length == n
-  let o₃ := (mergeSortTR₂ (· ≤ ·) i₃).length == n
-  let o₄ := (mergeSortTR₂ (· ≤ ·) i₄).length == n
+  let o₁ := (mergeSortTR₂ i₁).length == n
+  let o₂ := (mergeSortTR₂ i₂).length == n
+  let o₃ := (mergeSortTR₂ i₃).length == n
+  let o₄ := (mergeSortTR₂ i₄).length == n
   IO.println (((← IO.monoMsNow) - start)/4)
   IO.Process.exit (if o₁ && o₂ && o₃ && o₄ then 0 else 1)

tests/lean/derivingHashable.lean

@@ -6,14 +6,14 @@ structure Foo where
   flag  : Bool
   deriving Hashable
 
-#eval hash <| { name := "Joe", val := List.iota 40, flag := true, inv := by decide : Foo }
+#eval hash <| { name := "Joe", val := (List.range' 1 40).reverse, flag := true, inv := by decide : Foo }
 
 inductive Tree (α : Type) where
   | node : List (Tree α) → Bool → Tree α
   | leaf : α → Tree α
   deriving Hashable
 
-#eval hash <| Tree.node (List.iota 10 |>.map fun i => Tree.node [Tree.leaf i] (i%2==0)) true
+#eval hash <| Tree.node ((List.range' 1 10).reverse |>.map fun i => Tree.node [Tree.leaf i] (i%2==0)) true
 
 inductive StructureLikeInductive where
   | field : Nat -> StructureLikeInductive

tests/lean/run/IO_test.lean

@@ -62,7 +62,7 @@ withFile fn2 Mode.append $ fun h => do
 { h.putStrLn xs₁;
   pure () };
 let ys ← withFile fn2 Mode.read $ fun h => do
-  { let ys ← (List.iota 4).mapM $ fun i => do
+  { let ys ← (List.range 4).mapM $ fun i => do
     { let ln ← h.getLine;
       IO.println i;
       IO.println ∘ repr $ ln;
@@ -80,13 +80,13 @@ info: ⟨[₂,α]⟩⟨[₂,α]⟩
 
 ⟨[₂,α]⟩⟨[₂,α]⟩
 
-4
+0
 "⟨[₂,α]⟩⟨[₂,α]⟩\n"
-3
+1
 "/* Handle.getLine : Handle → IO Unit                     *//*   The line returned by `lean_io_prim_handle_get_line` *//*   is truncated at the first '\\0' character and the    *//*   rest of the line is discarded.                      */\n"
 2
 "⟨[6,8,@]⟩\n"
-1
+3
 "⟨[6,8,@]⟩\n"
 [⟨[₂,α]⟩⟨[₂,α]⟩
 , /* Handle.getLine : Handle → IO Unit                     *//*   The line returned by `lean_io_prim_handle_get_line` *//*   is truncated at the first '\0' character and the    *//*   rest of the line is discarded.                      */

tests/lean/run/derivingRepr.lean

@@ -15,7 +15,7 @@ info: { name := "Joe",
   flag := true }
 -/
 #guard_msgs in
-#eval { name := "Joe", val := List.iota 40, flag := true, inv := by decide : Foo }
+#eval { name := "Joe", val := (List.range' 1 40).reverse, flag := true, inv := by decide : Foo }
 
 inductive Tree (α : Type) where
   | node : List (Tree α) → Bool → Tree α
@@ -37,7 +37,7 @@ info: Tree.node
   true
 -/
 #guard_msgs in
-#eval Tree.node (List.iota 10 |>.map fun i => Tree.node [Tree.leaf i] (i%2==0)) true
+#eval Tree.node ((List.range' 1 10).reverse |>.map fun i => Tree.node [Tree.leaf i] (i%2==0)) true
 
 inductive StructureLikeInductive where
   | field : Nat -> StructureLikeInductive

tests/lean/run/filter.lean

@@ -1 +1 @@
-#guard ((List.iota 1000000).filter (fun x => x % 2 = 1)).length = 500000
+#guard ((List.range 1000000).filter (fun x => x % 2 = 1)).length = 500000

tests/lean/run/forInPArray.lean

@@ -45,31 +45,73 @@ IO.println s!"sum: {sum}"
 return sum
 
 /--
-info: x: 100
-x: 98
-x: 96
-x: 94
-x: 92
-x: 90
-x: 88
-x: 86
-x: 84
-x: 82
-x: 80
-x: 78
-x: 100
-x: 98
-x: 96
-x: 94
-x: 92
-x: 90
-x: 88
-x: 86
-x: 84
-x: 82
-x: 80
-x: 78
-sum: 1068
+info: x: 0
+x: 2
+x: 4
+x: 6
+x: 8
+x: 10
+x: 12
+x: 14
+x: 16
+x: 18
+x: 20
+x: 22
+x: 24
+x: 26
+x: 28
+x: 30
+x: 32
+x: 34
+x: 36
+x: 38
+x: 40
+x: 42
+x: 44
+x: 46
+x: 48
+x: 50
+x: 52
+x: 54
+x: 56
+x: 58
+x: 60
+x: 62
+x: 64
+x: 0
+x: 2
+x: 4
+x: 6
+x: 8
+x: 10
+x: 12
+x: 14
+x: 16
+x: 18
+x: 20
+x: 22
+x: 24
+x: 26
+x: 28
+x: 30
+x: 32
+x: 34
+x: 36
+x: 38
+x: 40
+x: 42
+x: 44
+x: 46
+x: 48
+x: 50
+x: 52
+x: 54
+x: 56
+x: 58
+x: 60
+x: 62
+x: 64
+sum: 1056
 -/
 #guard_msgs in
-#eval check (f1 (List.iota 100).toPArray' 1000) (f2 (List.iota 100).toPArray' 1000)
+#eval check (f1 (List.range 100).toPArray' 1000) (f2 (List.range 100).toPArray' 1000)

tests/lean/run/parray1.lean

@@ -6,10 +6,10 @@ def check [BEq α] (as : List α) : Bool :=
 def tst1 : IO Unit := do
   assert! check [1, 2, 3]
   assert! check ([] : List Nat)
-  assert! check (List.iota 17)
-  assert! check (List.iota 533)
-  assert! check (List.iota 1000)
-  assert! check (List.iota 2600)
+  assert! check (List.range 17)
+  assert! check (List.range 533)
+  assert! check (List.range 1000)
+  assert! check (List.range 2600)
   IO.println "done"
 
 /-- info: done -/

tests/lean/run/task_test2.lean

@@ -8,7 +8,7 @@ n.repeat (fun r =>
 
 def tst (n : Nat) : IO UInt32 :=
 let ys := (List.replicate n 1);
-let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.spawn fun _ => run1 (i+1) n ys);
+let ts : List (Task Nat) := (List.range 10).map (fun i => Task.spawn fun _ => run1 (i+1) n ys);
 let ns : List Nat := ts.map Task.get;
 IO.println (">> " ++ toString ns) *>
 pure 0