Integer indexing into lists

w[i]? for i : ℤ: the entry of w at i when 0 ≤ i < w.length, and none otherwise. This is the GetElem? instance a list has as a two-sided family padded with blanks, so position arithmetic across the left edge is ordinary ℤ arithmetic rather than a case split on ℕ subtraction. The instance is lawful, so the generic getElem?_pos, getElem?_neg, and getElem?_eq_some_iff apply; the lemmas here bridge to the ℕ index.

Main results

• List.getElem?_int_of_nonneg, List.getElem?_int_of_neg, List.getElem?_natCast: the two cases of the instance and the ℕ specialization.
• List.getElem?_int_eq_none_iff: an entry is blank exactly outside [0, w.length).
• List.ext_getElem?_int and List.ext_take_getElem?_int: extensionality for a list and its prefixes from agreement of integer-indexed entries.
• List.getElem?_int_append_left and List.getElem?_int_take_of_lt: the integer mirrors of List.getElem?_append_left and List.getElem?_take_of_lt.

@[instance_reducible]

instance List.instGetElem?Int {α : Type u_1} : GetElem? (List α) ℤ α fun (w : List α) (i : ℤ) => 0 ≤ i ∧ i < ↑w.length

Equations

• List.instGetElem?Int = { getElem := fun (w : List α) (i : ℤ) (h : 0 ≤ i ∧ i < ↑w.length) => w[i.toNat], getElem? := fun (w : List α) (i : ℤ) => if 0 ≤ i then w[i.toNat]? else none }

instance List.instLawfulGetElemIntAndLeOfNatLtCastLength_linglib {α : Type u_1} : LawfulGetElem (List α) ℤ α fun (w : List α) (i : ℤ) => 0 ≤ i ∧ i < ↑w.length

theorem List.getElem_int {α : Type u_1} {w : List α} {i : ℤ} (h : 0 ≤ i ∧ i < ↑w.length) : w[i] = w[i.toNat]

theorem List.getElem?_int {α : Type u_1} {w : List α} {i : ℤ} : w[i]? = if 0 ≤ i then w[i.toNat]? else none

theorem List.getElem?_int_of_nonneg {α : Type u_1} {w : List α} {i : ℤ} (h : 0 ≤ i) : w[i]? = w[i.toNat]?

theorem List.getElem?_int_of_neg {α : Type u_1} {w : List α} {i : ℤ} (h : i < 0) : w[i]? = none

@[simp]

theorem List.getElem?_natCast {α : Type u_1} (w : List α) (n : ℕ) : w[↑n]? = w[n]?

@[simp]

theorem List.getElem?_int_nil {α : Type u_1} {i : ℤ} : [][i]? = none

theorem List.getElem?_int_eq_none_iff {α : Type u_1} {w : List α} {i : ℤ} : w[i]? = none ↔ i < 0 ∨ ↑w.length ≤ i

theorem List.ext_getElem?_int {α : Type u_1} {w y : List α} (h : ∀ (j : ℤ), j ≤ ↑w.length → y[j]? = w[j]?) : y = w

Agreement of integer-indexed entries up to the length of w forces equality.

theorem List.ext_take_getElem?_int {α : Type u_1} {w y : List α} {c : ℕ} (h : ∀ (j : ℤ), j < ↑c → y[j]? = w[j]?) : take c y = take c w

Agreement of integer-indexed entries below c transfers prefixes of length c.

theorem List.getElem?_int_append_left {α : Type u_1} {u v : List α} {i : ℤ} (h : i < ↑u.length) : (u ++ v)[i]? = u[i]?

theorem List.getElem?_int_take_of_lt {α : Type u_1} {w : List α} {i : ℤ} {c : ℕ} (h : i < ↑c) : (take c w)[i]? = w[i]?