Init.Data.Range.Basic

Std.Range structure

Full source

structure Range where
  start : Nat := 0
  stop  : Nat
  step  : Nat := 1
  step_pos : 0 < step

Range of natural numbers

Informal description

The structure `Range` represents a range of natural numbers, typically used for iteration or indexing purposes. It supports membership operations (checking if a natural number is in the range) and provides a size operation to determine the number of elements in the range.

Std.instMembershipNatRange instance

: Membership Nat Range

Full source

instance : Membership Nat Range where
  mem r i := r.start ≤ i ∧ i < r.stop ∧ (i - r.start) % r.step = 0

Membership Relation for Natural Numbers in Ranges

Informal description

For any natural number $n$ and range $r$ of natural numbers, the membership relation $n \in r$ holds if and only if $n$ is contained within the range $r$.

Std.Range.size definition

(r : Range) : Nat

Full source

/-- The number of elements in the range. -/
@[simp] def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step

Size of a range of natural numbers

Informal description

For a range `r` of natural numbers with start `r.start`, stop `r.stop`, and step size `r.step`, the size of the range is given by the formula: \[ \text{size}(r) = \left\lfloor \frac{r.\text{stop} - r.\text{start} + r.\text{step} - 1}{r.\text{step}} \right\rfloor \] This computes the number of elements in the range `r`.

Std.Range.forIn' definition

[Monad m] (range : Range) (init : β) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β

Full source

@[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) : 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
  have := range.step_pos
  loop init range.start (by simp)

Monadic iteration over a range with state and early termination

Informal description

Given a monad `m`, a range of natural numbers `range`, an initial state `init : β`, and a function `f` that takes a natural number `i` in the range, a proof that `i` is in the range, and the current state `β`, producing a monadic computation of type `ForInStep β`, the function `Std.Range.forIn'` iterates over the range, applying `f` to each element in sequence. The iteration starts at `range.start` and increments by `range.step` until it exceeds `range.stop`. The function returns the final state after iteration, which may terminate early if `f` returns a `ForInStep.done` value.

Std.Range.instForIn'NatInferInstanceMembership instance

: ForIn' m Range Nat inferInstance

Full source

instance : ForIn' m Range Nat inferInstance where
  forIn' := Range.forIn'

Monadic Iteration with Membership Proofs for Natural Number Ranges

Informal description

For any monad `m`, the type `Range` of natural number ranges supports monadic iteration with membership proofs over its elements. This allows the use of `for h : x in xs` notation where `h` provides a proof that `x` is in the range `xs`.

Std.Range.forM definition

[Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit

Full source

@[inline] protected def forM [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit :=
  let rec @[specialize] loop (i : Nat): m PUnit := do
    if i < range.stop then
      f i
      have := range.step_pos
      loop (i + range.step)
    else
      pure ⟨⟩
  have := range.step_pos
  loop range.start

Monadic iteration over a range of natural numbers

Informal description

Given a monad `m`, a range of natural numbers `range`, and a function `f : ℕ → m PUnit`, the function `Std.Range.forM` iterates over each natural number `i` in the range (starting from `range.start` and incrementing by `range.step` until `i` exceeds `range.stop`), applying `f` to each `i` in sequence. The result is a monadic computation producing the unit value `⟨⟩`.

Std.Range.instForMNat instance

: ForM m Range Nat

Full source

instance : ForM m Range Nat where
  forM := Range.forM

Monadic Iteration over Natural Number Ranges

Informal description

For any monad `m`, the type `Range` of natural number ranges supports monadic iteration over its elements.

Std.Range.term[:_] definition

: Lean.ParserDescr✝

Full source

syntaxsyntax:max "[" withoutPosition(":" term) "]" : term

Range notation `[:a]` (zero-start)

Informal description

The syntax `[:a]` represents a range from `0` to natural number `a`, where `a` is a term that evaluates to a natural number. This is a parser description for range notation in Lean.

Std.Range.term[_:_] definition

: Lean.ParserDescr✝

Full source

syntaxsyntax:max "[" withoutPosition(term ":" term) "]" : term

Range notation parser `[a:b]`

Informal description

The syntax `[a:b]` represents a range from natural number `a` to natural number `b`, where `a` and `b` are terms that evaluate to natural numbers. This is a parser description for range notation in Lean.

Std.Range.term[:_:_] definition

: Lean.ParserDescr✝

Full source

syntaxsyntax:max "[" withoutPosition(":" term ":" term) "]" : term

Range notation `[:a:b]` (zero-start with step size)

Informal description

The syntax `[:a:b]` represents a range from `0` to natural number `a` with step size `b`, where `a` and `b` are terms that evaluate to natural numbers. This is a parser description for range notation in Lean.

Std.Range.term[_:_:_] definition

: Lean.ParserDescr✝

Full source

syntaxsyntax:max "[" withoutPosition(term ":" term ":" term) "]" : term

Range notation with step size `[a:b:c]`

Informal description

The syntax `[a:b:c]` represents a range from natural number `a` to natural number `b` with step size `c`, where `a`, `b`, and `c` are terms that evaluate to natural numbers. This is a parser description for range notation in Lean.

Membership.mem.upper theorem

{i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop

Full source

theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2.1

Upper Bound Property for Natural Number Range Membership

Informal description

For any natural number $i$ and range $r$ of natural numbers, if $i$ is a member of $r$ (denoted $i \in r$), then $i$ is strictly less than the stop value of $r$, i.e., $i < r.\text{stop}$.

Membership.mem.lower theorem

{i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i

Full source

theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1

Lower Bound of Range Membership for Natural Numbers

Informal description

For any natural number $i$ and range $r$ of natural numbers, if $i$ is a member of $r$, then the start of the range $r$ is less than or equal to $i$, i.e., $r.\text{start} \leq i$.

Membership.mem.step theorem

{i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0

Full source

theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2

Divisibility Condition for Range Membership in Natural Numbers

Informal description

For any natural number $i$ and range $r$ of natural numbers, if $i$ is a member of $r$, then the difference $i - r.\text{start}$ is divisible by $r.\text{step}$, i.e., $(i - r.\text{start}) \% r.\text{step} = 0$.

Membership.get_elem_helper theorem

{i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) : i < n

Full source

theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
    i < n := h₂ ▸ h₁.2.1

Range Membership Implies Boundedness: $i \in r \land \text{stop}(r) = n \Rightarrow i < n$

Informal description

For any natural numbers $i$ and $n$, and any range $r$ of natural numbers, if $i$ is a member of $r$ and the stop value of $r$ equals $n$, then $i < n$.