@[never_extract]

def outOfBounds {α : Sort u_1} [Inhabited α] : α

Equations

• outOfBounds = panicWithPosWithDecl "Init.GetElem" "outOfBounds" 15 2 "index out of bounds"

theorem outOfBounds_eq_default {α : Sort u_1} [Inhabited α] : outOfBounds = default

class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) : Type (max (max u v) w)

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.

• getElem (xs : coll) (i : idx) (h : valid xs i) : elem

  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.

  Conventions for notations in identifiers:

  • The recommended spelling of xs[i] in identifiers is getElem.

  • The recommended spelling of xs[i]'h in identifiers is getElem.

def «term__[_]» : Lean.TrailingParserDescr

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.

Conventions for notations in identifiers:

• The recommended spelling of xs[i] in identifiers is getElem.

Equations

• One or more equations did not get rendered due to their size.

def «term__[_]'_» : Lean.TrailingParserDescr

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.

Conventions for notations in identifiers:

• The recommended spelling of xs[i]'h in identifiers is getElem.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev decidableGetElem? {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem

Helper function for implementation of GetElem?.getElem?.

Equations

• decidableGetElem? xs i = if h : valid xs i then some xs[i] else none

class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid : Type (max (max u v) w)

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.

• getElem (xs : coll) (i : idx) (h : valid xs i) : elem
• getElem? : coll → idx → Option elem

  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.

  Conventions for notations in identifiers:

  • The recommended spelling of xs[i]? in identifiers is getElem?.
• getElem! [Inhabited elem] (xs : coll) (i : idx) : 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.

  Conventions for notations in identifiers:

  • The recommended spelling of xs[i]! in identifiers is getElem!.

def «term__[_]_?» : Lean.TrailingParserDescr

The syntax arr[i]? gets the i'th element of the collection arr or returns none if i is out of bounds.

Conventions for notations in identifiers:

• The recommended spelling of xs[i]? in identifiers is getElem?.

Equations

• One or more equations did not get rendered due to their size.

def «term__[_]_!» : Lean.TrailingParserDescr

The syntax arr[i]! gets the i'th element of the collection arr and panics i is out of bounds.

Conventions for notations in identifiers:

• The recommended spelling of xs[i]! in identifiers is getElem!.

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance instGetElem?OfGetElemOfDecidable {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [GetElem coll idx elem valid] [(xs : coll) → (i : idx) → Decidable (valid xs i)] : GetElem? coll idx elem valid

Equations

• instGetElem?OfGetElemOfDecidable = { toGetElem := inst✝¹, getElem? := fun (xs : coll) (i : idx) => decidableGetElem? xs i }

theorem getElem_congr {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [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]

theorem getElem_congr_coll {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [GetElem coll idx elem valid] {c d : coll} {i : idx} {w : valid c i} (h : c = d) : c[i] = d[i]

theorem getElem_congr_idx {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [GetElem coll idx elem valid] {c : coll} {i j : idx} {w : valid c i} (h' : i = j) : c[i] = c[j]

class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop

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.

• getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = if h : dom c i then some c[i] else none

  GetElem?.getElem? succeeds when the validity predicate is satisfied and fails otherwise.

• getElem!_def [Inhabited elem] (c : cont) (i : idx) : c[i]! = match c[i]? with | some e => e | none => default

  GetElem?.getElem! succeeds and fails when GetElem.getElem? succeeds and fails.

@[instance 100]

instance instLawfulGetElem {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [GetElem coll idx elem valid] [(xs : coll) → (i : idx) → Decidable (valid xs i)] : LawfulGetElem coll idx elem valid

@[simp]

theorem getElem?_pos {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : dom c i) : c[i]? = some c[i]

@[simp]

theorem getElem?_neg {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none

@[simp]

theorem getElem!_pos {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : dom c i) : c[i]! = c[i]

@[simp]

theorem getElem!_neg {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default

@[simp]

theorem get_getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] (h : c[i]?.isSome = true) : c[i]?.get h = c[i]

@[simp]

theorem getElem?_eq_none_iff {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i

@[simp]

theorem none_eq_getElem?_iff {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : none = c[i]? ↔ ¬dom c i

theorem of_getElem?_eq_some {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : dom c i

theorem getElem?_eq_some_iff {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] : c[i]? = some e ↔ ∃ (h : dom c i), c[i] = e

theorem some_eq_getElem?_iff {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] : some e = c[i]? ↔ ∃ (h : dom c i), c[i] = e

theorem getElem_of_getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : ∃ (h : dom c i), c[i] = e

@[simp]

theorem some_getElem_eq_getElem?_iff {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i) : some c[i] = c[i]? ↔ True

@[simp]

theorem getElem?_eq_some_getElem_iff {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i) : c[i]? = some c[i] ↔ True

@[reducible, inline, deprecated getElem?_eq_none_iff (since := "2025-02-17")]

abbrev getElem?_eq_none {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i

Equations

• @getElem?_eq_none = @getElem?_eq_none_iff

@[reducible, inline, deprecated getElem?_eq_none (since := "2024-12-11")]

abbrev isNone_getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i

Equations

• @isNone_getElem? = @getElem?_eq_none_iff

@[simp]

theorem isSome_getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : (c[i]?.isSome = true) = dom c i

instance Fin.instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs ↑i

Equations

• Fin.instGetElemFinVal = { getElem := fun (xs : cont) (i : Fin n) (h : dom xs ↑i) => xs[↑i] }

instance Fin.instGetElem?FinVal {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs ↑i

Equations

• Fin.instGetElem?FinVal = { toGetElem := Fin.instGetElemFinVal, getElem? := fun (xs : cont) (i : Fin n) => xs[↑i]?, getElem! := fun [Inhabited elem] (xs : cont) (i : Fin n) => xs[↑i]! }

instance Fin.instLawfulGetElemValOfNat {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] : LawfulGetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs ↑i

@[simp]

theorem Fin.getElem_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a ↑i) : a[i] = a[↑i]

@[simp]

theorem Fin.getElem?_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {n : Nat} [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[↑i]?

@[simp]

theorem Fin.getElem!_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {n : Nat} [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[↑i]!

instance List.instGetElemNatLtLength {α : Type u_1} : GetElem (List α) Nat α fun (as : List α) (i : Nat) => i < as.length

Equations

• List.instGetElemNatLtLength = { getElem := fun (as : List α) (i : Nat) (h : i < as.length) => as.get ⟨i, h⟩ }

@[simp]

theorem List.getElem_cons_zero {α : Type u_1} (a : α) (as : List α) (h : 0 < (a :: as).length) : (a :: as)[0] = a

@[simp]

theorem List.getElem_cons_succ {α : Type u_1} (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : (a :: as)[i + 1] = as[i]

@[simp]

theorem List.getElem_mem {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) : l[n] ∈ l

theorem List.getElem_cons_drop_succ_eq_drop {α : Type u_1} {as : List α} {i : Nat} (h : i < as.length) : as[i] :: drop (i + 1) as = drop i as

getElem?

instance List.instGetElem?NatLtLength {α : Type u_1} : GetElem? (List α) Nat α fun (as : List α) (i : Nat) => i < as.length

This instance overrides the default implementation of a[i]? via decidableGetElem?, giving better definitional equalities.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem List.get?Internal_eq_getElem? {α : Type u_1} {l : List α} {i : Nat} : List.get?Internal✝ l i = l[i]?

@[simp]

theorem List.get!Internal_eq_getElem! {α : Type u_1} [Inhabited α] {l : List α} {i : Nat} : List.get!Internal✝ l i = l[i]!

theorem List.getElem?_eq_getElem {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) : l[i]? = some l[i]

theorem List.getElem?_eq_none_iff {α✝ : Type u_1} {l : List α✝} {i : Nat} : l[i]? = none ↔ l.length ≤ i

theorem List.none_eq_getElem?_iff {α : Type u_1} {l : List α} {i : Nat} : none = l[i]? ↔ l.length ≤ i

theorem List.getElem?_eq_none {α✝ : Type u_1} {l : List α✝} {i : Nat} (h : l.length ≤ i) : l[i]? = none

instance List.instLawfulGetElemNatLtLength {α : Type u_1} : LawfulGetElem (List α) Nat α fun (as : List α) (i : Nat) => i < as.length

instance Array.instGetElemNatLtSize {α : Type u_1} : GetElem (Array α) Nat α fun (xs : Array α) (i : Nat) => i < xs.size

Equations

• Array.instGetElemNatLtSize = { getElem := fun (xs : Array α) (i : Nat) (h : i < xs.size) => xs.getInternal i h }

instance Array.instGetElem?NatLtSize {α : Type u_1} : GetElem? (Array α) Nat α fun (xs : Array α) (i : Nat) => i < xs.size

Equations

• One or more equations did not get rendered due to their size.

instance Array.instLawfulGetElemNatLtSize {α : Type u_1} : LawfulGetElem (Array α) Nat α fun (xs : Array α) (i : Nat) => i < xs.size

@[simp]

theorem Array.getInternal_eq_getElem {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) : a.getInternal i h = a[i]

@[simp]

theorem Array.get!Internal_eq_getElem! {α : Type u_1} [Inhabited α] (a : Array α) (i : Nat) : a.get!Internal i = a[i]!

instance Lean.Syntax.instGetElemNatTrue : GetElem Syntax Nat Syntax fun (x : Syntax) (x : Nat) => True

Equations

• Lean.Syntax.instGetElemNatTrue = { getElem := fun (stx : Lean.Syntax) (i : Nat) (x : True) => stx.getArg i }