doc-next-gen

Init.GetElem

Module docstring

{"### getElem? "}

outOfBounds definition
[Inhabited α] : α
Full source 
@[never_extract]
def outOfBounds [Inhabited α] : α :=
  panic! "index out of bounds"
Out of bounds error value
Informal description
The term `outOfBounds` is a placeholder value of type `α` (where `α` is an inhabited type) that is returned when an index is out of bounds during array access. It is defined to panic with the message "index out of bounds" when evaluated.
outOfBounds_eq_default theorem
[Inhabited α] : (outOfBounds : α) = default
Full source 
theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
Out-of-bounds error equals default value
Informal description
For any inhabited type $\alpha$, the out-of-bounds error value `outOfBounds` is equal to the default value of $\alpha$.
GetElem structure
(coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop))
Full source 
/--
The classes `GetElem` and `GetElem?` implement lookup notation,
specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.

Both classes are indexed by types `coll`, `idx`, and `elem` which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation `valid` determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.

For example, an instance for arrays looks like
`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
holds, which is true when `i` is less than the size of the array. `Array`
additionally supports indexing with `USize` instead of `Nat`.
In either case, because the bounds are checked at compile time,
no runtime check is required.

Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
`GetElem coll idx elem valid` and uses this to infer the type of the return
value `elem` and side condition `valid` required to ensure `xs[i]` yields
a valid value of type `elem`. The tactic `get_elem_tactic` is
invoked to prove validity automatically. The `xs[i]'p` notation uses the
proof `p` to satisfy the validity condition.
If the proof `p` is long, it is often easier to place the
proof in the context using `have`, because `get_elem_tactic` tries
`assumption`.


The proof side-condition `valid xs i` is automatically dispatched by the
`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
`get_elem_tactic_trivial` using `macro_rules`.

`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
an `Option elem`, with `none` signalling that the value isn't present, and
the latter returns `elem` but panics if the value isn't there, returning
`default : elem` based on the `Inhabited elem` instance.
These are provided by the `GetElem?` class, for which there is a default instance
generated from a `GetElem` class as long as `valid xs i` is always decidable.

Important instances include:
  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
    side goal `i < l.length`.

-/
class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
              (valid : outParam (coll → idx → Prop)) where
  /--
  The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
  are proof side conditions to the application, they will be automatically
  inferred by the `get_elem_tactic` tactic.
  -/
  getElem (xs : coll) (i : idx) (h : valid xs i) : elem
Collection Indexing with Validity Predicate
Informal description
The structure `GetElem` implements lookup notation `xs[i]` for collections, where `xs` is a collection of type `coll`, `i` is an index of type `idx`, and the lookup returns an element of type `elem`. The predicate `valid : coll → idx → Prop` ensures that the index is valid for the collection, guaranteeing that the lookup will succeed. For example, given an array `arr : Array α` and an index `i : Nat`, `arr[i]` returns an element of type `α` if `i < arr.size` holds. The validity condition is automatically verified by the `get_elem_tactic` tactic.
term__[_]'_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc getElem]
syntax term noWs "[" withoutPosition(term) "]'" term:max : term
Safe element access with optional return
Informal description
The syntax `t[i]'?` represents a safe element access operation that returns an optional value, where `t` is a collection, `i` is an index, and the operation returns `some e` if the index is valid or `none` otherwise.
decidableGetElem? abbrev
[GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem
Full source 
/-- Helper function for implementation of `GetElem?.getElem?`. -/
abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
    Option elem :=
  if h : valid xs i then some xs[i] else none
Decidable Safe Element Access with Optional Result
Informal description
Given a collection `xs` of type `coll`, an index `i` of type `idx`, and a validity predicate `valid : coll → idx → Prop` that is decidable, the function `decidableGetElem?` returns an optional element of type `elem`. It returns `some e` if the index `i` is valid for the collection `xs` (i.e., `valid xs i` holds), and `none` otherwise.
GetElem? structure
(coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid
Full source 
@[inherit_doc GetElem]
class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
  /--
  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
  if it is present (and wraps it in `some`), and otherwise returns `none`.
  -/
  getElem? : coll → idx → Option elem

  /--
  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
  if it is present, and otherwise panics at runtime and returns the `default` term
  from `Inhabited elem`.
  -/
  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
    match getElem? xs i with | some e => e | none => outOfBounds
Optional Indexed Element Access
Informal description
The structure `GetElem?` extends `GetElem` and represents a type class for indexed access to elements of a collection `coll` with index type `idx` and element type `elem`, where the access is guarded by a validity predicate `valid`. This allows for safe element retrieval with an optional result, typically used when the validity of the index is not statically known.
instGetElem?OfGetElemOfDecidable instance
[GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] : GetElem? coll idx elem valid
Full source 
instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
    GetElem? coll idx elem valid where
  getElem? xs i := decidableGetElem? xs i
Optional Element Access via Decidable Validity Predicate
Informal description
For any collection type `coll` with index type `idx` and element type `elem`, equipped with a decidable validity predicate `valid : coll → idx → Prop`, there exists an instance of `GetElem?` that allows safe optional element access. This means that for any collection `xs : coll` and index `i : idx`, the lookup `xs[i]?` will return `some e` if `valid xs i` holds (i.e., the index is valid), and `none` otherwise.
getElem_congr theorem
[GetElem coll idx elem valid] {c d : coll} (h : c = d) {i j : idx} (h' : i = j) (w : valid c i) : c[i] = d[j]'(h' ▸ h ▸ w)
Full source 
theorem getElem_congr [GetElem coll idx elem valid] {c d : coll} (h : c = d)
    {i j : idx} (h' : i = j) (w : valid c i) : c[i] = d[j]'(h' ▸ h ▸ w) := by
  cases h; cases h'; rfl
Congruence of Indexed Access under Equality of Collections and Indices
Informal description
Let `coll` be a type with a `GetElem` instance, where `idx` is the index type and `elem` is the element type, with a validity predicate `valid : coll → idx → Prop`. For any collections `c, d : coll` such that `c = d`, and any indices `i, j : idx` such that `i = j`, if the validity condition `valid c i` holds, then the elements `c[i]` and `d[j]` are equal.
getElem_congr_coll theorem
[GetElem coll idx elem valid] {c d : coll} {i : idx} {w : valid c i} (h : c = d) : c[i] = d[i]'(h ▸ w)
Full source 
theorem getElem_congr_coll [GetElem coll idx elem valid] {c d : coll} {i : idx} {w : valid c i}
    (h : c = d) : c[i] = d[i]'(h ▸ w) := by
  cases h; rfl
Congruence of Indexed Access under Equality of Collections
Informal description
Let `coll` be a type with a `GetElem` instance, where `idx` is the index type and `elem` is the element type, with a validity predicate `valid : coll → idx → Prop`. For any collections `c, d : coll` such that `c = d`, and any index `i : idx` where `valid c i` holds, the elements `c[i]` and `d[i]` are equal.
getElem_congr_idx theorem
[GetElem coll idx elem valid] {c : coll} {i j : idx} {w : valid c i} (h' : i = j) : c[i] = c[j]'(h' ▸ w)
Full source 
theorem getElem_congr_idx [GetElem coll idx elem valid] {c : coll} {i j : idx} {w : valid c i}
    (h' : i = j) : c[i] = c[j]'(h' ▸ w) := by
  cases h'; rfl
Congruence of Indexed Access under Equality of Indices
Informal description
Let `coll` be a type with a `GetElem` instance, where `idx` is the index type, `elem` is the element type, and `valid : coll → idx → Prop` is a validity predicate. For any collection `c : coll` and indices `i, j : idx` such that `i = j` and `valid c i` holds, the elements `c[i]` and `c[j]` are equal.
LawfulGetElem structure
(cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom]
Full source 
/--
Lawful `GetElem?` instances (which extend `GetElem`) are those for which the potentially-failing
`GetElem?.getElem?` and `GetElem?.getElem!` operators succeed when the validity predicate is
satisfied, and fail when it is not.
-/
class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
   (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where

  /-- `GetElem?.getElem?` succeeds when the validity predicate is satisfied and fails otherwise. -/
  getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
      c[i]? = if h : dom c i then some (c[i]'h) else none := by
    intros
    try simp only [getElem?] <;> congr

  /-- `GetElem?.getElem!` succeeds and fails when `GetElem.getElem?` succeeds and fails. -/
  getElem!_def [Inhabited elem] (c : cont) (i : idx) :
      c[i]! = match c[i]? with | some e => e | none => default := by
    intros
    simp only [getElem!, getElem?, outOfBounds_eq_default]
Lawful Indexed Element Access
Informal description
The structure `LawfulGetElem` represents a type class for collections with indexed element access where the operations `getElem?` and `getElem!` behave as expected: they succeed when the index is valid (according to the predicate `dom`) and fail otherwise. This ensures that the potentially-failing operations are lawful with respect to the validity predicate.
instLawfulGetElem instance
[GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] : LawfulGetElem coll idx elem valid
Full source 
instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
    LawfulGetElem coll idx elem valid where
Lawful Optional Element Access for Collections with Decidable Validity
Informal description
For any collection type `coll` with index type `idx` and element type `elem`, equipped with a decidable validity predicate `valid : coll → idx → Prop`, there exists a lawful instance of `GetElem?`. This ensures that the operations `getElem?` and `getElem!` behave as expected: they succeed when the index is valid (i.e., `valid xs i` holds) and fail otherwise.
getElem?_pos theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h)
Full source 
theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
  have : Decidable (dom c i) := .isTrue h
  rw [getElem?_def]
  exact dif_pos h
Optional Access Yields Element on Valid Index: $c[i]? = \text{some}(c[i])$ when $\text{dom}(c, i)$ holds
Informal description
For a collection $c$ with index type $\text{idx}$ and element type $\text{elem}$, equipped with a validity predicate $\text{dom}$ on indices, if $\text{GetElem?}$ and $\text{LawfulGetElem}$ instances exist, then for any index $i$ that satisfies $\text{dom}(c, i)$, the optional access operation $c[i]?$ returns $\text{some}(c[i])$, where $c[i]$ is the element at index $i$ in $c$.
getElem?_neg theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none
Full source 
theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
  have : Decidable (dom c i) := .isFalse h
  rw [getElem?_def]
  exact dif_neg h
Optional Access Yields None on Invalid Index: $c[i]? = \text{none}$ when $\text{dom}(c, i)$ fails
Informal description
For a collection $c$ with index type $\text{idx}$ and element type $\text{elem}$, equipped with a validity predicate $\text{dom}$ on indices, if $\text{GetElem?}$ and $\text{LawfulGetElem}$ instances exist, then for any index $i$ that does not satisfy $\text{dom}(c, i)$, the optional access operation $c[i]?$ returns $\text{none}$.
getElem!_pos theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : dom c i) : c[i]! = c[i]'h
Full source 
theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
    c[i]! = c[i]'h := by
  have : Decidable (dom c i) := .isTrue h
  simp [getElem!_def, getElem?_def, h]
Forced Access Yields Element on Valid Index: $c[i]! = c[i]$ when $\text{dom}(c, i)$ holds
Informal description
For a collection $c$ with index type $\text{idx}$ and element type $\text{elem}$, equipped with a validity predicate $\text{dom}$ on indices, if $\text{GetElem?}$ and $\text{LawfulGetElem}$ instances exist and $\text{elem}$ is inhabited, then for any index $i$ that satisfies $\text{dom}(c, i)$, the forced access operation $c[i]!$ returns the element $c[i]$ (with validity proof $h$).
getElem!_neg theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default
Full source 
theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
  have : Decidable (dom c i) := .isFalse h
  simp [getElem!_def, getElem?_def, h]
Forced Access Yields Default on Invalid Index: `c[i]! = default` when `¬dom c i`
Informal description
For a collection `c` with index type `idx` and element type `elem`, equipped with a validity predicate `dom` on indices, if `GetElem?` and `LawfulGetElem` instances exist and `elem` is inhabited, then for any index `i` that does not satisfy `dom c i`, the forced access operation `c[i]!` returns the default value of type `elem`.
get_getElem? theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] (h) : c[i]?.get h = c[i]'(by simp only [getElem?_def] at h; split at h <;> simp_all)
Full source 
@[simp] theorem get_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) [Decidable (dom c i)] (h) :
    c[i]?.get h = c[i]'(by simp only [getElem?_def] at h; split at h <;> simp_all) := by
  simp only [getElem?_def] at h ⊢
  split <;> simp_all
Equality of Optional and Lawful Indexed Access: `c[i]?.get h = c[i]'`
Informal description
For a collection `c` of type `cont` with index type `idx` and element type `elem`, where `dom` is a validity predicate for indices, if `GetElem?` and `LawfulGetElem` instances exist and the decidability of `dom c i` is provided, then for any proof `h` that `c[i]?` is not `none`, the value obtained from `c[i]?.get h` is equal to the value obtained from the lawful indexed access `c[i]'` (with the validity proof derived from `h`).
getElem?_eq_none_iff theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i
Full source 
@[simp] theorem getElem?_eq_none_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?c[i]? = none ↔ ¬dom c i := by
  simp only [getElem?_def]
  split <;> simp_all
Optional Access Yields `none` if and only if Index is Invalid: `c[i]? = none ↔ ¬dom c i`
Informal description
For a collection `c` with index type `idx` and element type `elem`, equipped with a validity predicate `dom` on indices, if `GetElem?` and `LawfulGetElem` instances exist and the decidability of `dom c i` is provided, then the optional indexed access `c[i]?` returns `none` if and only if the index `i` is not valid for the collection `c` (i.e., `¬dom c i`).
getElem?_eq_none abbrev
Full source 
@[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
abbrev getElem?_eq_none := @getElem?_eq_none_iff
Optional Element Access Yields `none` if and only if Index is Invalid
Informal description
For a collection `c` with index type `idx` and element type `elem`, equipped with a validity predicate `dom` on indices, if `GetElem?` and `LawfulGetElem` instances exist and the decidability of `dom c i` is provided, then the optional indexed access `c[i]?` returns `none` if and only if the index `i` is not valid for the collection `c` (i.e., `¬dom c i`).
isNone_getElem? abbrev
Full source 
@[deprecated getElem?_eq_none (since := "2024-12-11")]
abbrev isNone_getElem? := @getElem?_eq_none_iff
Optional Access Yields `none` if and only if Index is Invalid: `c[i]? = none ↔ ¬dom c i`
Informal description
For a collection `c` with index type `idx` and element type `elem`, equipped with a validity predicate `dom` on indices, if `GetElem?` and `LawfulGetElem` instances exist and the decidability of `dom c i` is provided, then the optional indexed access `c[i]?` returns `none` if and only if the index `i` is not valid for the collection `c` (i.e., `¬dom c i`).
isSome_getElem? theorem
[GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i
Full source 
@[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by
  simp only [getElem?_def]
  split <;> simp_all
Optional Element Access Yields Some if and only if Index is Valid
Informal description
For a collection `c` with index type `idx` and element type `elem`, where `dom` is a validity predicate for indices, and given a decidable instance for `dom c i`, the optional element access `c[i]?` has `isSome` equal to `dom c i`. In other words, `c[i]?` returns `some` value if and only if the index `i` is valid for the collection `c` according to `dom`.
Fin.instGetElemFinVal instance
[GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i
Full source 
instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
  getElem xs i h := getElem xs i.1 h
Finite Indexing for Collections with Natural Number Indices
Informal description
For any collection type `cont` with a `GetElem` instance for natural number indices, there is a corresponding `GetElem` instance for finite type indices `Fin n`. Specifically, if `xs : cont` and `i : Fin n`, then `xs[i]` returns an element of type `elem` provided that the underlying validity predicate `dom xs i` holds.
Fin.instGetElem?FinVal instance
[GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i
Full source 
instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
  getElem? xs i := getElem? xs i.val
  getElem! xs i := getElem! xs i.val
Optional Element Access for Finite Indices
Informal description
For any collection type `cont` with a `GetElem?` instance for natural number indices, there is a corresponding `GetElem?` instance for finite type indices `Fin n`. Specifically, if `xs : cont` and `i : Fin n`, then `xs[i]?` returns an optional element of type `elem` provided that the underlying validity predicate `dom xs i` holds.
Fin.instLawfulGetElemValOfNat instance
[GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] : LawfulGetElem cont (Fin n) elem fun xs i => dom xs i
Full source 
instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
      LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
  getElem?_def _c _i _d := h.getElem?_def ..
  getElem!_def _c _i := h.getElem!_def ..
Lawful Element Access for Finite Indices
Informal description
For any collection type `cont` with a lawful `GetElem?` instance for natural number indices, there is a corresponding lawful `GetElem?` instance for finite type indices `Fin n`. This ensures that the operations `getElem?` and `getElem!` behave as expected when using finite indices, provided the underlying validity predicate `dom` holds for the natural number representation of the index.
Fin.getElem_fin theorem
[GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) : a[i] = a[i.1]
Full source 
@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
    a[i] = a[i.1] := rfl
Element Access Equality for Finite Indices: $a[i] = a[i.1]$
Informal description
For a collection `a` of type `Cont` with an instance of `GetElem?` for natural number indices, and for a finite index `i : Fin n` such that the validity predicate `Dom a i` holds, the element access `a[i]` is equal to `a[i.1]`, where `i.1` is the underlying natural number of the finite index `i`.
Fin.getElem?_fin theorem
[h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]?
Full source 
@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := by rfl
Equality of Optional Element Access for Finite Indices: $a[i]? = a[i.1]?$
Informal description
For a collection `a` of type `Cont` with an instance of `GetElem?` for natural number indices, and for a finite index `i : Fin n`, the optional element access `a[i]?` is equal to `a[i.1]?`, where `i.1` is the underlying natural number of the finite index `i`.
Fin.getElem!_fin theorem
[GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]!
Full source 
@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
Equality of Non-Optional Element Access for Finite Indices: $a[i]! = a[i.1]!$
Informal description
For a collection `a` of type `Cont` with an instance of `GetElem?` for natural number indices, and for a finite index `i : Fin n`, the non-optional element access `a[i]!` (assuming `Elem` is inhabited) is equal to `a[i.1]!`, where `i.1` is the underlying natural number of the finite index `i`.
List.instGetElemNatLtLength instance
: GetElem (List α) Nat α fun as i => i < as.length
Full source 
instance : GetElem (List α) Nat α fun as i => i < as.length where
  getElem as i h := as.get ⟨i, h⟩
List Indexing with Validity Condition
Informal description
For any list `as` of type `List α` and natural number index `i`, the lookup operation `as[i]` returns an element of type `α` when `i` is a valid index for the list (i.e., when `i < as.length`).
List.getElem_cons_zero theorem
(a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a
Full source 
@[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
  rfl
First Element of Cons List is Head: $(a :: as)[0] = a$
Informal description
For any element $a$ of type $\alpha$ and list $as$ of type $\text{List } \alpha$, if $0$ is a valid index for the list $a :: as$ (i.e., $0 < \text{length}(a :: as)$), then the element at index $0$ of $a :: as$ is equal to $a$.
List.getElem_cons_succ theorem
(a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i + 1) h = getElem as i (Nat.lt_of_succ_lt_succ h)
Full source 
@[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
  rfl
Successor Index in Cons List: $(a :: as)[i + 1] = as[i]$
Informal description
For any element $a$ of type $\alpha$, list $as$ of type $\text{List } \alpha$, and natural number index $i$ such that $i + 1 < \text{length}(a :: as)$, the element at index $i + 1$ of the list $a :: as$ is equal to the element at index $i$ of the list $as$. That is, $(a :: as)[i + 1] = as[i]$.
List.getElem_mem theorem
: ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
Full source 
@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'hl[n]'h ∈ l
  | _ :: _, 0, _ => .head ..
  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
List Element Membership: $l[n] \in l$ when $n < \text{length}(l)$
Informal description
For any list $l$ of type $\text{List } \alpha$ and natural number index $n$ such that $n < \text{length}(l)$, the element $l[n]$ is a member of the list $l$.
List.getElem_cons_drop_succ_eq_drop theorem
{as : List α} {i : Nat} (h : i < as.length) : as[i] :: as.drop (i + 1) = as.drop i
Full source 
theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
    as[i]as[i] :: as.drop (i+1) = as.drop i :=
  match as, i with
  | _::_, 0   => rfl
  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) (Nat.add_one_lt_add_one_iff.mp h)
List Element and Drop Equivalence
Informal description
For any list `as` of type `List α` and natural number index `i` such that `i < as.length`, the element at position `i` in `as` followed by the list obtained by dropping the first `i + 1` elements of `as` is equal to the list obtained by dropping the first `i` elements of `as`. In other words, $as[i] :: \text{drop}(as, i + 1) = \text{drop}(as, i)$.
List.get_drop_eq_drop abbrev
Full source 
@[deprecated getElem_cons_drop_succ_eq_drop (since := "2024-11-05")]
abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
List Element Equals Head of Dropped List
Informal description
For any list `as` of type `List α` and natural number index `i` such that `i < as.length`, the element at position `i` in `as` is equal to the head of the list obtained by dropping the first `i` elements of `as`. In other words, $as[i] = (\text{drop}(as, i)).head$.
List.instGetElem?NatLtLength instance
: GetElem? (List α) Nat α fun as i => i < as.length
Full source 
/-- This instance overrides the default implementation of `a[i]?` via `decidableGetElem?`,
giving better definitional equalities. -/
instance : GetElem? (List α) Nat α fun as i => i < as.length where
  getElem? as i := as.get?Internal i
  getElem! as i := as.get!Internal i
Optional List Indexing with Validity Check
Informal description
For any list `as` of type `List α` and natural number index `i`, the optional lookup operation `as[i]?` returns an element of type `α` when `i` is a valid index for the list (i.e., when `i < as.length`), and returns `none` otherwise. This instance provides a more efficient implementation than the default `decidableGetElem?`.
List.get?Internal_eq_getElem? theorem
{l : List α} {i : Nat} : l.get?Internal i = l[i]?
Full source 
@[simp] theorem get?Internal_eq_getElem? {l : List α} {i : Nat} :
    l.get?Internal i = l[i]? := rfl
Equivalence of Internal and Optional Indexing Operations for Lists
Informal description
For any list $l$ of type $\text{List } \alpha$ and natural number index $i$, the internal lookup function $\text{get?Internal}$ applied to $l$ and $i$ is equal to the optional indexing operation $l[i]?$.
List.get!Internal_eq_getElem! theorem
[Inhabited α] {l : List α} {i : Nat} : l.get!Internal i = l[i]!
Full source 
@[simp] theorem get!Internal_eq_getElem! [Inhabited α] {l : List α} {i : Nat} :
    l.get!Internal i = l[i]! := rfl
Equivalence of Internal and Indexing Operations for Lists with Default Values
Informal description
For any inhabited type $\alpha$, list $l$ of type $\text{List } \alpha$, and natural number index $i$, the internal function $\text{get!Internal}$ applied to $l$ and $i$ is equal to the element obtained by the indexing operation $l[i]!$ (which returns the $i$-th element of $l$ or a default value if $i$ is out of bounds).
List.getElem?_eq_getElem theorem
{l : List α} {i} (h : i < l.length) : l[i]? = some l[i]
Full source 
@[simp] theorem getElem?_eq_getElem {l : List α} {i} (h : i < l.length) :
    l[i]? = some l[i] := by
  induction l generalizing i with
  | nil => cases h
  | cons a l ih =>
    cases i with
    | zero => rfl
    | succ i => exact ih ..
Optional List Indexing Yields Some Element for Valid Indices
Informal description
For any list $l$ of type $\text{List}\,\alpha$ and natural number index $i$ such that $i < \text{length}\,l$, the optional indexing operation $l[i]?$ returns $\text{some}\,l[i]$, where $l[i]$ is the $i$-th element of $l$.
List.getElem?_eq_none_iff theorem
: l[i]? = none ↔ length l ≤ i
Full source 
@[simp] theorem getElem?_eq_none_iff : l[i]?l[i]? = none ↔ length l ≤ i :=
  match l with
  | [] => by simp; rfl
  | _ :: l => by
    cases i with
    | zero => simp
    | succ i =>
      simp only [length_cons, Nat.add_le_add_iff_right]
      exact getElem?_eq_none_iff (l := l) (i := i)
Optional List Indexing Yields None for Out-of-Bounds Indices
Informal description
For any list $l$ of type $\text{List}\,\alpha$ and natural number index $i$, the optional indexing operation $l[i]?$ returns $\text{none}$ if and only if the length of $l$ is less than or equal to $i$.
List.none_eq_getElem?_iff theorem
{l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i
Full source 
@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : nonenone = l[i]? ↔ length l ≤ i := by
  simp [eq_comm (a := none)]
Equivalence of None and Optional List Indexing
Informal description
For any list $l$ of type $\text{List}\,\alpha$ and natural number index $i$, the equality $\text{none} = l[i]?$ holds if and only if the length of $l$ is less than or equal to $i$.
List.getElem?_eq_none theorem
(h : length l ≤ i) : l[i]? = none
Full source 
theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
Optional List Indexing Yields None for Out-of-Bounds Indices
Informal description
For any list $l$ and natural number index $i$, if the length of $l$ is less than or equal to $i$, then the optional indexing operation $l[i]?$ returns `none`.
List.instLawfulGetElemNatLtLength instance
: LawfulGetElem (List α) Nat α fun as i => i < as.length
Full source 
instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
  getElem?_def as i h := by
    split <;> simp_all
  getElem!_def as i := by
    induction as generalizing i with
    | nil => rfl
    | cons a as ih =>
      cases i with
      | zero => rfl
      | succ i => simpa using ih i
Lawful Indexed Access for Lists with Natural Number Indices
Informal description
For any list `as` of type `List α` and natural number index `i`, the indexed element access operation `as[i]` is lawful when `i` is a valid index (i.e., `i < as.length`). This means the operation behaves as expected: it successfully returns the element at index `i` when the index is valid and fails otherwise.
Array.instGetElemNatLtSize instance
: GetElem (Array α) Nat α fun xs i => i < xs.size
Full source 
instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
  getElem xs i h := xs.getInternal i h
Array Indexing with Bounds Check
Informal description
For any array `xs` of type `Array α` and natural number index `i`, the notation `xs[i]` returns an element of type `α` provided that `i` is less than the size of `xs`. This instance implements the array indexing operation with a validity condition ensuring the index is within bounds.
Array.instGetElem?NatLtSize instance
: GetElem? (Array α) Nat α fun xs i => i < xs.size
Full source 
instance : GetElem? (Array α) Nat α fun xs i => i < xs.size where
  getElem? xs i := decidableGetElem? xs i
  getElem! xs i := xs.get!Internal i
Optional Array Indexing with Bounds Check
Informal description
For any array `xs` of type `Array α` and natural number index `i`, the notation `xs[i]?` returns an optional element of type `α`. It returns `some xs[i]` if `i` is a valid index (i.e., `i < xs.size`), and `none` otherwise.
Array.instLawfulGetElemNatLtSize instance
: LawfulGetElem (Array α) Nat α fun xs i => i < xs.size
Full source 
instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
  getElem?_def xs i h := by
    simp only [getElem?, decidableGetElem?]
    split <;> rfl
  getElem!_def xs i := by
    simp only [getElem!, getElem?, decidableGetElem?, get!Internal, getD, getElem]
    split <;> rfl
Lawful Array Indexing with Bounds Check
Informal description
For any array `xs` of type `Array α` and natural number index `i`, the indexing operation `xs[i]` is lawful, meaning it satisfies the expected properties when `i` is a valid index (i.e., `i < xs.size`). This includes consistency with the internal array access functions and proper behavior with respect to bounds checking.
Array.getInternal_eq_getElem theorem
(a : Array α) (i : Nat) (h) : a.getInternal i h = a[i]
Full source 
@[simp] theorem getInternal_eq_getElem (a : Array α) (i : Nat) (h) :
    a.getInternal i h = a[i] := rfl
Equivalence of Internal Array Access and Indexing Notation
Informal description
For any array `a` of type `Array α`, natural number index `i`, and proof `h` that `i` is within bounds, the internal array access function `a.getInternal i h` is equal to the array indexing notation `a[i]`.
Array.get!Internal_eq_getElem! theorem
[Inhabited α] (a : Array α) (i : Nat) : a.get!Internal i = a[i]!
Full source 
@[simp] theorem get!Internal_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) :
    a.get!Internal i = a[i]! := by
  simp only [get!Internal, getD, getInternal_eq_getElem, getElem!_def]
  split <;> simp_all [getElem?_pos, getElem?_neg]
Equivalence of Internal Array Access and Panicking Indexing Notation
Informal description
For any inhabited type $\alpha$, array $a$ of type $\text{Array }\alpha$, and natural number index $i$, the internal array access function $\text{get!Internal}$ is equal to the array indexing notation $a[i]!$.
Lean.Syntax.instGetElemNatTrue instance
: GetElem Syntax Nat Syntax fun _ _ => True
Full source 
instance : GetElem Syntax Nat Syntax fun _ _ => True where
  getElem stx i _ := stx.getArg i
Syntax Tree Indexing with Natural Numbers
Informal description
For any syntax tree `s` of type `Syntax` and natural number index `i`, the lookup operation `s[i]` is always valid and returns another syntax tree. The validity predicate is trivially true for all inputs, meaning any natural number index can be used to access elements in a syntax tree.