@[never_extract]

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

Equations

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

theorem outOfBounds_eq_default {α : Type 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) → 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.

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.

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.

@[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) → 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.

• getElem! : [inst : Inhabited elem] → coll → 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.

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.

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

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

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

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} {h : valid c i} (h' : c = d) : c[i] = d[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 : coll} {i j : idx} {h : 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

• getElem?_def : ∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i then some c[i] else none
• getElem!_def : ∀ [inst : Inhabited elem] (c : cont) (i : idx), c[i]! = match c[i]? with | some e => e | none => default

theorem 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

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]

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

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]

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 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]?.isNone = true) = ¬dom c i

@[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 = GetElem?.mk (fun (xs : cont) (i : Fin n) => xs[↑i]?) fun [Inhabited elem] (xs : cont) (i : Fin n) => xs[↑i]!

theorem 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

@[reducible, inline, deprecated List.getElem_cons_zero]

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

Equations

• @List.cons_getElem_zero = @List.getElem_cons_zero

@[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]

@[reducible, inline, deprecated List.getElem_cons_succ]

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

Equations

• @List.cons_getElem_succ = @List.getElem_cons_succ

@[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] :: List.drop (i + 1) as = List.drop i as

@[reducible, inline, deprecated List.getElem_cons_drop_succ_eq_drop]

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

Equations

• @List.get_drop_eq_drop = @List.getElem_cons_drop_succ_eq_drop

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

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