chore: require 0 < Range.step (#6391)

This PR requires that the step size in `Std.Range` is positive, to avoid
ill-specified behaviour.

src/Init/Data/Range.lean

@@ -14,6 +14,7 @@ structure Range where
   start : Nat := 0
   stop  : Nat
   step  : Nat := 1
+  step_pos : 0 < step
 
 instance : Membership Nat Range where
   mem r i := r.start ≤ i ∧ i < r.stop ∧ (i - r.start) % r.step = 0
@@ -24,36 +25,33 @@ universe u v
 @[inline] protected def forIn' [Monad m] (range : Range) (init : β)
     (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop (b : β) (i : Nat)
-      (hs : (i - range.start) % range.step = 0) (hl : range.start ≤ i := by omega)
-      (w : 0 < range.step := by omega) : m β := do
+      (hs : (i - range.start) % range.step = 0) (hl : range.start ≤ i := by omega) : m β := do
     if h : i < range.stop then
       match (← f i ⟨hl, by omega, hs⟩ b) with
       | .done b  => pure b
       | .yield b =>
+        have := range.step_pos
         loop b (i + range.step) (by rwa [Nat.add_comm, Nat.add_sub_assoc hl, Nat.add_mod_left])
     else
       pure b
-  if h : range.step = 0 then
-    return init
-  else
-    loop init range.start (by simp)
+  have := range.step_pos
+  loop init range.start (by simp)
 
 instance : ForIn' m Range Nat inferInstance where
   forIn' := Range.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
 
 @[inline] protected def forM [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit :=
-  let rec @[specialize] loop (i : Nat) (h : 0 < range.step) : m PUnit := do
-    if h' : i < range.stop then
+  let rec @[specialize] loop (i : Nat): m PUnit := do
+    if i < range.stop then
       f i
-      loop (i + range.step) h
+      have := range.step_pos
+      loop (i + range.step)
     else
       pure ⟨⟩
-  if h : range.step = 0 then
-    return ⟨⟩
-  else
-    loop range.start (by omega)
+  have := range.step_pos
+  loop range.start
 
 instance : ForM m Range Nat where
   forM := Range.forM
@@ -64,10 +62,10 @@ syntax:max "[" withoutPosition(":" term ":" term) "]" : term
 syntax:max "[" withoutPosition(term ":" term ":" term) "]" : term
 
 macro_rules
-  | `([ : $stop]) => `({ stop := $stop : Range })
-  | `([ $start : $stop ]) => `({ start := $start, stop := $stop : Range })
-  | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step : Range })
-  | `([ : $stop : $step ]) => `({ stop := $stop, step := $step : Range })
+  | `([ : $stop]) => `({ stop := $stop, step_pos := Nat.zero_lt_one : Range })
+  | `([ $start : $stop ]) => `({ start := $start, stop := $stop, step_pos := Nat.zero_lt_one : Range })
+  | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step, step_pos := by decide : Range })
+  | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range })
 
 end Range
 end Std

src/Lean/Compiler/LCNF/Util.lean

@@ -56,7 +56,7 @@ def getCasesInfo? (declName : Name) : CoreM (Option CasesInfo) := do
   let arity        := numParams + 1 /- motive -/ + val.numIndices + 1 /- major -/ + val.numCtors
   let discrPos     := numParams + 1 /- motive -/ + val.numIndices
   -- We view indices as discriminants
-  let altsRange    := { start := discrPos + 1,  stop := arity }
+  let altsRange    := [discrPos + 1:arity]
   let altNumParams ← val.ctors.toArray.mapM fun ctor => do
     let .ctorInfo ctorVal ← getConstInfo ctor | unreachable!
     return ctorVal.numFields

src/Lean/Meta/Match/MatcherInfo.lean

@@ -43,13 +43,13 @@ def MatcherInfo.getFirstDiscrPos (info : MatcherInfo) : Nat :=
   info.numParams + 1
 
 def MatcherInfo.getDiscrRange (info : MatcherInfo) : Std.Range :=
-  { start := info.getFirstDiscrPos, stop := info.getFirstDiscrPos + info.numDiscrs }
+  [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs]
 
 def MatcherInfo.getFirstAltPos (info : MatcherInfo) : Nat :=
   info.numParams + 1 + info.numDiscrs
 
 def MatcherInfo.getAltRange (info : MatcherInfo) : Std.Range :=
-  { start := info.getFirstAltPos, stop := info.getFirstAltPos + info.numAlts }
+  [info.getFirstAltPos : info.getFirstAltPos + info.numAlts]
 
 def MatcherInfo.getMotivePos (info : MatcherInfo) : Nat :=
   info.numParams