move Std.Range to Std.Legacy.Range

Author: datokrat

src/Init/Data/Range/Basic.lean

@@ -10,7 +10,7 @@ public import Init.Omega
 
 public section
 
-namespace Std
+namespace Std.Legacy
 -- We put `Range` in `Init` because we want the notation `[i:j]`  without importing `Std`
 -- We don't put `Range` in the top-level namespace to avoid collisions with user defined types
 structure Range where
@@ -74,15 +74,17 @@ macro_rules
   | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range })
 
 end Range
-end Std
+end Std.Legacy
 
-theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2.1
+@[deprecated "use the new range notation `a...b` instead of `[a:b]` and `Std.Rco.lt_upper_of_mem`" (since := "2025-12-01")]
+theorem Membership.mem.upper {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : i < r.stop := h.2.1
 
-theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1
+@[deprecated "use the new range notation `a...b` instead of `[a:b]` and `Std.Rco.lower_le_of_mem`" (since := "2025-12-01")]
+theorem Membership.mem.lower {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : r.start ≤ i := h.1
 
-theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2
+theorem Membership.mem.step {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2
 
-theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
+theorem Membership.get_elem_helper {i n : Nat} {r : Std.Legacy.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
     i < n := h₂ ▸ h₁.2.1
 
 macro_rules

src/Init/Data/Range/Lemmas.lean

@@ -15,12 +15,12 @@ public import Init.Data.Nat.Div.Lemmas
 public section
 
 /-!
-# Lemmas about `Std.Range`
+# Lemmas about `Std.Legacy.Range`
 
-We provide lemmas rewriting for loops over `Std.Range` in terms of `List.range'`.
+We provide lemmas rewriting for loops over `Std.Legacy.Range` in terms of `List.range'`.
 -/
 
-namespace Std.Range
+namespace Std.Legacy.Range
 
 /-- Generalization of `mem_of_mem_range'` used in `forIn'_loop_eq_forIn'_range'` below. -/
 private theorem mem_of_mem_range'_aux {r : Range} {a : Nat} (w₁ : (i - r.start) % r.step = 0)
@@ -37,7 +37,7 @@ theorem mem_of_mem_range' {r : Range} (h : x ∈ List.range' r.start r.size r.st
   unfold size at h
   apply mem_of_mem_range'_aux (by simp) (by simp) h
 
-private theorem size_eq (r : Std.Range) (h : i < r.stop) :
+private theorem size_eq (r : Range) (h : i < r.stop) :
     (r.stop - i + r.step - 1) / r.step =
       (r.stop - (i + r.step) + r.step - 1) / r.step + 1 := by
   have w := r.step_pos
@@ -57,7 +57,7 @@ private theorem size_eq (r : Std.Range) (h : i < r.stop) :
       rw [Nat.div_eq_iff] <;> omega
     omega
 
-private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
+private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) :
     forIn'.loop r f init i w₁ w₂ =
       forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init
@@ -75,20 +75,20 @@ private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
       rw [Nat.div_eq_iff] <;> omega
     simp [this]
 
-@[simp] theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
+@[simp] theorem forIn'_eq_forIn'_range' [Monad m] (r : Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
     forIn' r init f =
       forIn' (List.range' r.start r.size r.step) init (fun a h => f a (mem_of_mem_range' h)) := by
   conv => lhs; simp only [forIn', Range.forIn']
   simp only [size]
   rw [forIn'_loop_eq_forIn'_range']
 
-@[simp] theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+@[simp] theorem forIn_eq_forIn_range' [Monad m] (r : Range)
     (init : β) (f : Nat → β → m (ForInStep β)) :
     forIn r init f = forIn (List.range' r.start r.size r.step) init f := by
   simp only [forIn, forIn'_eq_forIn'_range']
 
-private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+private theorem forM_loop_eq_forM_range' [Monad m] (r : Range) (f : Nat → m PUnit) :
     forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f := by
   have w := r.step_pos
   rw [forM.loop]
@@ -101,8 +101,8 @@ private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat →
       rw [Nat.div_eq_iff] <;> omega
     simp [this]
 
-@[simp] theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+@[simp] theorem forM_eq_forM_range' [Monad m] (r : Range) (f : Nat → m PUnit) :
     forM r f = forM (List.range' r.start r.size r.step) f := by
   simp only [forM, Range.forM, forM_loop_eq_forM_range', size]
 
-end Std.Range
+end Std.Legacy.Range

src/Init/Data/Stream.lean

@@ -82,7 +82,7 @@ instance : ToStream (Subarray α) (Subarray α) where
 instance : ToStream String Substring.Raw where
   toStream s := s.toRawSubstring
 
-instance : ToStream Std.Range Std.Range where
+instance : ToStream Std.Legacy.Range Std.Legacy.Range where
   toStream r := r
 
 instance [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β) where
@@ -108,7 +108,7 @@ instance : Stream (Subarray α) α where
     else
       none
 
-instance : Stream Std.Range Nat where
+instance : Stream Std.Legacy.Range Nat where
   next? r :=
     if r.start < r.stop then
       some (r.start, { r with start := r.start + r.step })

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1291,9 +1291,9 @@ def delabPProdMk : Delab := delabPProdMkCore ``PProd.mk
 @[builtin_delab app.MProd.mk]
 def delabMProdMk : Delab := delabPProdMkCore ``MProd.mk
 
-@[builtin_delab app.Std.Range.mk]
+@[builtin_delab app.Std.Legacy.Range.mk]
 def delabRange : Delab := whenPPOption getPPNotation do
-  -- Std.Range.mk : (start : Nat) → (stop : Nat) → (step : Nat) → 0 < step → Std.Range
+  -- Std.Legacy.Range.mk : (start : Nat) → (stop : Nat) → (step : Nat) → 0 < step → Std.Legacy.Range
   guard <| (← getExpr).getAppNumArgs == 4
   -- `none` if the start is `0`
   let start? ← withNaryArg 0 do

src/Std/Do/Triple/SpecLemmas.lean

@@ -24,12 +24,12 @@ public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 This module contains Hoare triple specifications for some functions in Core.
 -/
 
-namespace Std.Range
+namespace Std.Legacy.Range
 
-abbrev toList (r : Std.Range) : List Nat :=
+abbrev toList (r : Std.Legacy.Range) : List Nat :=
   List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
 
-end Std.Range
+end Std.Legacy.Range
 
 namespace List
 
@@ -718,23 +718,23 @@ theorem Spec.foldlM_list_const_inv
 @[spec]
 theorem Spec.forIn'_range {β : Type u} {m : Type u → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
-    {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
+    {xs : Std.Legacy.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
     (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
       Triple
-        (f cur (by simp [Std.Range.mem_of_mem_range', h]) b)
+        (f cur (by simp [Std.Legacy.Range.mem_of_mem_range', h]) b)
         (inv.1 (⟨pref, cur::suff, h.symm⟩, b))
         (fun r => match r with
           | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
           | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) :
     Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by
-  simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1]
+  simp only [Std.Legacy.Range.forIn'_eq_forIn'_range', Std.Legacy.Range.size, Std.Legacy.Range.size.eq_1]
   apply Spec.forIn'_list inv (fun c hcur b => step c hcur b)
 
 @[spec]
 theorem Spec.forIn_range {β : Type u} {m : Type u → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
-    {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
+    {xs : Std.Legacy.Range} {init : β} {f : Nat → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
     (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
       Triple
@@ -744,7 +744,7 @@ theorem Spec.forIn_range {β : Type u} {m : Type u → Type v} {ps : PostShape}
           | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
           | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) :
     Triple (forIn xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by
-  simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
+  simp only [Std.Legacy.Range.forIn_eq_forIn_range', Std.Legacy.Range.size]
   apply Spec.forIn_list inv step
 
 open Std.PRange in

tests/lean/run/delabStdRange.lean

@@ -1,40 +1,40 @@
 /-!
-# Tests for delaborators for Std.Range and Std.PRange
+# Tests for delaborators for Std.Legacy.Range and Std.PRange
 -/
 
 /-!
-## Tests for `Std.Range`
+## Tests for `Std.Legacy.Range`
 -/
 
 /-!
 Default lower bound and step
 -/
-/-- info: [:10] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 0 10 1 (by grind)
+/-- info: [:10] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 0 10 1 (by grind)
 
 /-!
 Default step
 -/
-/-- info: [5:10] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 5 10 1 (by grind)
+/-- info: [5:10] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 5 10 1 (by grind)
 
 /-!
 Default lower bound
 -/
-/-- info: [:10:2] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 0 10 2 (by grind)
+/-- info: [:10:2] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 0 10 2 (by grind)
 
 /-!
 No defaults
 -/
-/-- info: [5:10:2] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 5 10 2 (by grind)
+/-- info: [5:10:2] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 5 10 2 (by grind)
 
 /-!
 Disable notation
 -/
-/-- info: { stop := 10, step_pos := _check._proof_1 } : Std.Range -/
-#guard_msgs in set_option pp.notation false in #check Std.Range.mk 0 10 1 (by grind)
+/-- info: { stop := 10, step_pos := _check._proof_1 } : Std.Legacy.Range -/
+#guard_msgs in set_option pp.notation false in #check Std.Legacy.Range.mk 0 10 1 (by grind)
 
 /-!
 ## Tests for `Std.PRange`

tests/lean/run/grind_lint_std_misc.lean

@@ -4,4 +4,4 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 /-! Check remaining Std sub-namespaces: -/
 
 #guard_msgs in
-#grind_lint check (min := 20) in Std.Do Std.Range Std.Tactic
+#grind_lint check (min := 20) in Std.Do Std.Legacy.Range Std.Tactic