chore: further cleanup of index variable naming in List (leanprover#6963

)

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

@@ -16,6 +16,8 @@ These are in a separate file from most of the list lemmas
 as they required importing more lemmas about natural numbers, and use `omega`.
 -/
 
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -170,7 +172,7 @@ theorem take_one {l : List α} : l.take 1 = l.head?.toList := by
 
 theorem take_eq_append_getElem_of_pos {i} {l : List α} (h₁ : 0 < i) (h₂ : i < l.length) : l.take i = l.take (i - 1) ++ [l[i - 1]] :=
   match i, h₁ with
-  | i + 1, _ => take_succ_eq_append_getElem (n := i) (by omega)
+  | i + 1, _ => take_succ_eq_append_getElem (by omega)
 
 theorem dropLast_take {i : Nat} {l : List α} (h : i < l.length) :
     (l.take i).dropLast = l.take (i - 1) := by

src/Init/Data/List/TakeDrop.lean

@@ -10,6 +10,8 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.take` and `List.drop`.
 -/
 
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -20,19 +22,19 @@ Further results on `List.take` and `List.drop`, which rely on stronger automatio
 are given in `Init.Data.List.TakeDrop`.
 -/
 
-theorem take_cons {l : List α} (h : 0 < n) : take n (a :: l) = a :: take (n - 1) l := by
-  cases n with
+theorem take_cons {l : List α} (h : 0 < i) : take i (a :: l) = a :: take (i - 1) l := by
+  cases i with
   | zero => exact absurd h (Nat.lt_irrefl _)
-  | succ n => rfl
+  | succ i => rfl
 
 @[simp]
 theorem drop_one : ∀ l : List α, drop 1 l = tail l
   | [] | _ :: _ => rfl
 
-@[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
+@[simp] theorem take_append_drop : ∀ (i : Nat) (l : List α), take i l ++ drop i l = l
   | 0, _ => rfl
   | _+1, [] => rfl
-  | n+1, x :: xs => congrArg (cons x) <| take_append_drop n xs
+  | i+1, x :: xs => congrArg (cons x) <| take_append_drop i xs
 
 @[simp] theorem length_drop : ∀ (i : Nat) (l : List α), length (drop i l) = length l - i
   | 0, _ => rfl
@@ -44,14 +46,14 @@ theorem drop_one : ∀ l : List α, drop 1 l = tail l
 theorem drop_of_length_le {l : List α} (h : l.length ≤ i) : drop i l = [] :=
   length_eq_zero.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
 
-theorem length_lt_of_drop_ne_nil {l : List α} {n} (h : drop n l ≠ []) : n < l.length :=
+theorem length_lt_of_drop_ne_nil {l : List α} {i} (h : drop i l ≠ []) : i < l.length :=
   gt_of_not_le (mt drop_of_length_le h)
 
 theorem take_of_length_le {l : List α} (h : l.length ≤ i) : take i l = l := by
   have := take_append_drop i l
   rw [drop_of_length_le h, append_nil] at this; exact this
 
-theorem lt_length_of_take_ne_self {l : List α} {n} (h : l.take n ≠ l) : n < l.length :=
+theorem lt_length_of_take_ne_self {l : List α} {i} (h : l.take i ≠ l) : i < l.length :=
   gt_of_not_le (mt take_of_length_le h)
 
 @[deprecated drop_of_length_le (since := "2024-07-07")] abbrev drop_length_le := @drop_of_length_le
@@ -67,66 +69,66 @@ theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
   | _::_, 0, _ => rfl
   | _::_, i+1, h => getElem_cons_drop _ i (Nat.add_one_lt_add_one_iff.mp h)
 
-theorem drop_eq_getElem_cons {n} {l : List α} (h : n < l.length) : drop n l = l[n] :: drop (n + 1) l :=
-  (getElem_cons_drop _ n h).symm
+theorem drop_eq_getElem_cons {i} {l : List α} (h : i < l.length) : drop i l = l[i] :: drop (i + 1) l :=
+  (getElem_cons_drop _ i h).symm
 
 @[simp]
-theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by
-  induction n generalizing l m with
+theorem getElem?_take_of_lt {l : List α} {i j : Nat} (h : i < j) : (l.take j)[i]? = l[i]? := by
+  induction j generalizing l i with
   | zero =>
-    exact absurd h (Nat.not_lt_of_le m.zero_le)
-  | succ _ hn =>
+    exact absurd h (Nat.not_lt_of_le i.zero_le)
+  | succ _ hj =>
     cases l with
     | nil => simp only [take_nil]
     | cons hd tl =>
-      cases m
+      cases i
       · simp
-      · simpa using hn (Nat.lt_of_succ_lt_succ h)
+      · simpa using hj (Nat.lt_of_succ_lt_succ h)
 
-theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
+theorem getElem?_take_of_succ {l : List α} {i : Nat} : (l.take (i + 1))[i]? = l[i]? := by simp
 
-@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
-  | m, [] => by simp
+@[simp] theorem drop_drop (i : Nat) : ∀ (j) (l : List α), drop i (drop j l) = drop (j + i) l
+  | j, [] => by simp
   | 0, l => by simp
-  | m + 1, a :: l =>
+  | j + 1, a :: l =>
     calc
-      drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
-      _ = drop (m + n) l := drop_drop n m l
-      _ = drop ((m + 1) + n) (a :: l) := by rw [Nat.add_right_comm]; rfl
+      drop i (drop (j + 1) (a :: l)) = drop i (drop j l) := rfl
+      _ = drop (j + i) l := drop_drop i j l
+      _ = drop ((j + 1) + i) (a :: l) := by rw [Nat.add_right_comm]; rfl
 
 theorem drop_add_one_eq_tail_drop (l : List α) : l.drop (i + 1) = (l.drop i).tail := by
   rw [← drop_drop, drop_one]
 
-theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
-  | 0, _, _ => by simp
+theorem take_drop : ∀ (i j : Nat) (l : List α), take i (drop j l) = drop j (take (j + i) l)
+  | _, 0, _ => by simp
   | _, _, [] => by simp
-  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
+  | _, _+1, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
 @[simp]
-theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by
-  induction l generalizing n with
+theorem tail_drop (l : List α) (i : Nat) : (l.drop i).tail = l.drop (i + 1) := by
+  induction l generalizing i with
   | nil => simp
   | cons hd tl hl =>
-    cases n
+    cases i
     · simp
     · simp [hl]
 
 @[simp]
-theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by
+theorem drop_tail (l : List α) (i : Nat) : l.tail.drop i = l.drop (i + 1) := by
   rw [Nat.add_comm, ← drop_drop, drop_one]
 
 @[simp]
-theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by
+theorem drop_eq_nil_iff {l : List α} {i : Nat} : l.drop i = [] ↔ l.length ≤ i := by
   refine ⟨fun h => ?_, drop_eq_nil_of_le⟩
-  induction k generalizing l with
+  induction i generalizing l with
   | zero =>
     simp only [drop] at h
     simp [h]
-  | succ k hk =>
+  | succ i hi =>
     cases l
     · simp
     · simp only [drop] at h
-      simpa [Nat.succ_le_succ_iff] using hk h
+      simpa [Nat.succ_le_succ_iff] using hi h
 
 @[deprecated drop_eq_nil_iff (since := "2024-09-10")] abbrev drop_eq_nil_iff_le := @drop_eq_nil_iff
 
@@ -146,33 +148,33 @@ theorem take_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.take i =
 theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h : as.take i ≠ []) : as ≠ [] :=
   mt take_eq_nil_of_eq_nil h
 
-theorem set_take {l : List α} {n m : Nat} {a : α} :
-    (l.set m a).take n = (l.take n).set m a := by
-  induction n generalizing l m with
+theorem set_take {l : List α} {i j : Nat} {a : α} :
+    (l.set j a).take i = (l.take i).set j a := by
+  induction i generalizing l j with
   | zero => simp
-  | succ _ hn =>
+  | succ _ hi =>
     cases l with
     | nil => simp
-    | cons hd tl => cases m <;> simp_all
+    | cons hd tl => cases j <;> simp_all
 
-theorem drop_set {l : List α} {n m : Nat} {a : α} :
-    (l.set m a).drop n = if m < n then l.drop n else (l.drop n).set (m - n) a := by
-  induction n generalizing l m with
+theorem drop_set {l : List α} {i j : Nat} {a : α} :
+    (l.set j a).drop i = if j < i then l.drop i else (l.drop i).set (j - i) a := by
+  induction i generalizing l j with
   | zero => simp
-  | succ _ hn =>
+  | succ _ hi =>
     cases l with
     | nil => simp
     | cons hd tl =>
-      cases m
+      cases j
       · simp_all
-      · simp only [hn, set_cons_succ, drop_succ_cons, succ_lt_succ_iff]
+      · simp only [hi, set_cons_succ, drop_succ_cons, succ_lt_succ_iff]
         congr 2
         exact (Nat.add_sub_add_right ..).symm
 
-theorem set_drop {l : List α} {n m : Nat} {a : α} :
-    (l.drop n).set m a = (l.set (n + m) a).drop n := by
-  rw [drop_set, if_neg, add_sub_self_left n m]
-  exact (Nat.not_lt).2 (le_add_right n m)
+theorem set_drop {l : List α} {i j : Nat} {a : α} :
+    (l.drop i).set j a = (l.set (i + j) a).drop i := by
+  rw [drop_set, if_neg, add_sub_self_left]
+  exact (Nat.not_lt).2 (le_add_right ..)
 
 theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
     (l.take i).concat l[i] = l.take (i+1) :=
@@ -183,7 +185,7 @@ theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
     (l.take i) ++ [l[i]] = l.take (i+1) := by
   simpa using take_concat_get l i h
 
-theorem take_succ_eq_append_getElem {n} {l : List α} (h : n < l.length) : l.take (n + 1) = l.take n ++ [l[n]] :=
+theorem take_succ_eq_append_getElem {i} {l : List α} (h : i < l.length) : l.take (i + 1) = l.take i ++ [l[i]] :=
   (take_append_getElem _ _ h).symm
 
 @[simp] theorem take_append_getLast (l : List α) (h : l ≠ []) :
@@ -204,40 +206,40 @@ theorem take_succ_eq_append_getElem {n} {l : List α} (h : n < l.length) : l.tak
 theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl
 
 @[deprecated take_of_length_le (since := "2024-07-25")]
-theorem take_all_of_le {n} {l : List α} (h : length l ≤ n) : take n l = l :=
+theorem take_all_of_le {l : List α} {i} (h : length l ≤ i) : take i l = l :=
   take_of_length_le h
 
 theorem drop_left : ∀ l₁ l₂ : List α, drop (length l₁) (l₁ ++ l₂) = l₂
   | [], _ => rfl
   | _ :: l₁, l₂ => drop_left l₁ l₂
 
 @[simp]
-theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l₁ ++ l₂) = l₂ := by
+theorem drop_left' {l₁ l₂ : List α} {i} (h : length l₁ = i) : drop i (l₁ ++ l₂) = l₂ := by
   rw [← h]; apply drop_left
 
 theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
   | [], _ => rfl
   | a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
 
 @[simp]
-theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
+theorem take_left' {l₁ l₂ : List α} {i} (h : length l₁ = i) : take i (l₁ ++ l₂) = l₁ := by
   rw [← h]; apply take_left
 
-theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.toList := by
-  induction l generalizing n with
+theorem take_succ {l : List α} {i : Nat} : l.take (i + 1) = l.take i ++ l[i]?.toList := by
+  induction l generalizing i with
   | nil =>
     simp only [take_nil, Option.toList, getElem?_nil, append_nil]
   | cons hd tl hl =>
-    cases n
+    cases i
     · simp only [take, Option.toList, getElem?_cons_zero, nil_append]
     · simp only [take, hl, getElem?_cons_succ, cons_append]
 
 @[deprecated "Deprecated without replacement." (since := "2024-07-25")]
-theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l := by
-  induction l generalizing n with
+theorem drop_sizeOf_le [SizeOf α] (l : List α) (i : Nat) : sizeOf (l.drop i) ≤ sizeOf l := by
+  induction l generalizing i with
   | nil => rw [drop_nil]; apply Nat.le_refl
   | cons _ _ lih =>
-    induction n with
+    induction i with
     | zero => apply Nat.le_refl
     | succ n =>
       exact Trans.trans (lih _) (Nat.le_add_left _ _)
@@ -428,12 +430,12 @@ theorem dropWhile_replicate (p : α → Bool) :
   simp only [dropWhile_replicate_eq_filter_not, filter_replicate]
   split <;> simp_all
 
-theorem take_takeWhile {l : List α} (p : α → Bool) n :
-    (l.takeWhile p).take n = (l.take n).takeWhile p := by
-  induction l generalizing n with
+theorem take_takeWhile {l : List α} (p : α → Bool) i :
+    (l.takeWhile p).take i = (l.take i).takeWhile p := by
+  induction l generalizing i with
   | nil => simp
   | cons x xs ih =>
-    by_cases h : p x <;> cases n <;> simp [takeWhile_cons, h, ih, take_succ_cons]
+    by_cases h : p x <;> cases i <;> simp [takeWhile_cons, h, ih, take_succ_cons]
 
 @[simp] theorem all_takeWhile {l : List α} : (l.takeWhile p).all p = true := by
   induction l with
@@ -460,7 +462,7 @@ theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool
 
 /-! ### splitAt -/
 
-@[simp] theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n) := by
+@[simp] theorem splitAt_eq (i : Nat) (l : List α) : splitAt i l = (l.take i, l.drop i) := by
   rw [splitAt, splitAt_go, reverse_nil, nil_append]
   split <;> simp_all [take_of_length_le, drop_of_length_le]
 

src/Init/Data/List/ToArray.lean

@@ -15,6 +15,8 @@ import Init.Data.Array.Lex.Basic
 We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
 
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace Array
 
 @[simp] theorem toList_set (a : Array α) (i x h) :
@@ -566,21 +568,15 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
     simp only [append_assoc, cons_append]
     rw [insertIdx_loop_toArray _ _ _ _ (by omega)]
     simp only [swap_toArray, w, append_assoc, cons_append, mk.injEq]
-    rw [List.take_set_of_le _ _ (by omega)]
-    rw [List.drop_eq_getElem_cons (n := j) (by simpa)]
-    rw [List.getElem_set_self]
-    rw [List.drop_set_of_lt _ _ (by omega)]
-    rw [List.drop_set_of_lt _ _ (by omega)]
-    rw [List.getElem_set_ne (by omega)]
-    rw [List.getElem_set_self]
-    rw [List.take_set_of_le (j := j - 1) _ _ (by omega)]
-    rw [List.take_set_of_le (j := j - 1) _ _ (by omega)]
-    rw [List.take_eq_append_getElem_of_pos (i := j) (l := l) (by omega) hj]
-    rw [List.drop_append_of_le_length (by simp; omega)]
+    rw [take_set_of_le _ _ (by omega), drop_eq_getElem_cons (i := j) (by simpa), getElem_set_self,
+      drop_set_of_lt _ _ (by omega), drop_set_of_lt _ _ (by omega), getElem_set_ne (by omega),
+      getElem_set_self, take_set_of_le (j := j - 1) _ _ (by omega),
+      take_set_of_le (j := j - 1) _ _ (by omega), take_eq_append_getElem_of_pos (by omega) hj,
+      drop_append_of_le_length (by simp; omega)]
     simp only [append_assoc, cons_append, nil_append, append_cancel_right_eq]
     cases i with
     | zero => simp
-    | succ i => rw [List.take_set_of_le _ _ (by omega)]
+    | succ i => rw [take_set_of_le _ _ (by omega)]
   · simp only [Nat.not_lt] at h'
     have : i = j := by omega
     subst this

src/Lean/Linter/List.lean

@@ -59,7 +59,8 @@ are `i`, `j`, or `k`.
 -/
 def indexLinter : Linter
   where run := withSetOptionIn fun stx => do
-    unless Linter.getLinterValue linter.indexVariables (← getOptions) do return
+    -- We intentionally do not use `getLinterValue` here, as we do *not* want to opt in to `linter.all`.
+    unless (← getOptions).get linter.indexVariables.name false do return
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do