Lemmas about arrays and getElem!

Statements that mention nothing from this development. They were proved here because something in the library needed them, and they are collected in ForMathlib so that they can be contributed upstream, or deleted when Mathlib grows its own.

theorem array_extD {α : Type u_1} [Inhabited α] {a b : Array α} (hs : a.size = b.size) (h : ∀ i < a.size, a[i]! = b[i]!) : a = b

theorem mem_iff_getElemD {a : Array ℕ} {v : ℕ} : v ∈ a ↔ ∃ i < a.size, a[i]! = v

theorem getElemD_mem {a : Array ℕ} {j : ℕ} (h : j < a.size) : a[j]! ∈ a

An in-bounds getElem! is a member.

theorem getElemD_setD {α : Type u_1} [Inhabited α] {a : Array α} {i : ℕ} {x : α} (hi : i < a.size) (k : ℕ) : (a.set! i x)[k]! = if k = i then x else a[k]!

Reading one entry of Array.set!, the only fact about it these proofs need.

theorem getElemD_setD_ne {α : Type u_1} [Inhabited α] {a : Array α} {i : ℕ} {x : α} {k : ℕ} (h : k ≠ i) : (a.set! i x)[k]! = a[k]!

Companion to getElemD_setD for the off-diagonal case, where no bound on i is needed: writing at i never disturbs another index, in bounds or not.

theorem nodup_getElemD_ne {a : Array ℕ} (h : a.toList.Nodup) {i j : ℕ} (hi : i < a.size) (hj : j < a.size) (hij : i ≠ j) : a[i]! ≠ a[j]!

Distinct positions of a duplicate-free array hold distinct values.

theorem nodup_of_getElemD_ne {a : Array ℕ} (h : ∀ (i j : ℕ), i < a.size → j < a.size → i < j → a[i]! ≠ a[j]!) : a.toList.Nodup

An array whose entries at distinct indices differ has no duplicates.

theorem pairwise_getElemD_le {a : Array ℕ} (hp : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) a.toList) {i j : ℕ} (hj : j < a.size) (hij : i ≤ j) : a[i]! ≤ a[j]!

theorem pairwise_getElemD_lt {a : Array ℕ} (hp : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) a.toList) (hnd : a.toList.Nodup) {i j : ℕ} (hj : j < a.size) (hij : i < j) : a[i]! < a[j]!

theorem arr_isEmpty_iff (a : Array ℕ) : a.isEmpty = true ↔ ∀ (x : ℕ), x ∉ a

theorem push_getElemD_eq {α : Type} [Inhabited α] (a : Array α) (v : α) : (a.push v)[a.size]! = v

theorem push_getElemD_lt {α : Type} [Inhabited α] (a : Array α) (v : α) {i : ℕ} (hi : i < a.size) : (a.push v)[i]! = a[i]!

theorem extract_self (a : Array ℕ) : a.extract = a

theorem extract_size {a : Array ℕ} {j : ℕ} (hj : j ≤ a.size) : (a.extract 0 j).size = j

theorem extract_getElemD {a : Array ℕ} {j i : ℕ} (hi : i < j) : (a.extract 0 j)[i]! = a[i]!

theorem push_extract {a : Array ℕ} {v j : ℕ} (hj : j ≤ a.size) : (a.push v).extract 0 j = a.extract 0 j

theorem take_toList_eq {a b : Array ℕ} {j : ℕ} (hja : j ≤ a.size) (hjb : j ≤ b.size) (h : ∀ k < j, a[k]! = b[k]!) : List.take j a.toList = List.take j b.toList

theorem take_getElemD_self {c : Array ℕ} {j i : ℕ} (hi : i < j) (hic : i < c.size) : (List.take j c.toList)[i]! = c[i]!

theorem take_getElemD {a b : Array ℕ} {j : ℕ} (h : List.take j a.toList = List.take j b.toList) {i : ℕ} (hi : i < j) (hia : i < a.size) : a[i]! = b[i]!

theorem replicate_getElemD_false {n w : ℕ} : (Array.replicate n false)[w]! = false