Bootstrapping theorems about arrays

This file contains some theorems about Array and List needed for Std.List.Basic.

@[simp]

theorem Array.mkEmpty_eq (α : Type u_1) (n : Nat) : Array.mkEmpty n = #[]

@[simp]

theorem Array.size_toArray {α : Type u_1} (as : List α) : Array.size (List.toArray as) = List.length as

@[simp]

theorem Array.size_mk {α : Type u_1} (as : List α) : Array.size { data := as } = List.length as

theorem Array.getElem_eq_data_get {α : Type u_1} {i : Nat} (a : Array α) (h : i < Array.size a) : a[i] = List.get a.data { val := i, isLt := h }

theorem Array.foldlM_eq_foldlM_data.aux {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (arr : Array α) (i : Nat) (j : Nat) (H : Array.size arr ≤ i + j) (b : β) : Array.foldlM.loop f arr (Array.size arr) (_ : Array.size arr ≤ Array.size arr) i j b = List.foldlM f b (List.drop j arr.data)

theorem Array.foldlM_eq_foldlM_data {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (arr : Array α) : Array.foldlM f init arr 0 = List.foldlM f init arr.data

theorem Array.foldl_eq_foldl_data {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (arr : Array α) : Array.foldl f init arr 0 = List.foldl f init arr.data

theorem Array.foldrM_eq_reverse_foldlM_data.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (arr : Array α) (init : β) (i : Nat) (h : i ≤ Array.size arr) : List.foldlM (fun (x : β) (y : α) => f y x) init (List.reverse (List.take i arr.data)) = Array.foldrM.fold f arr 0 i h init

theorem Array.foldrM_eq_reverse_foldlM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) : Array.foldrM f init arr (Array.size arr) = List.foldlM (fun (x : β) (y : α) => f y x) init (List.reverse arr.data)

theorem Array.foldrM_eq_foldrM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) : Array.foldrM f init arr (Array.size arr) = List.foldrM f init arr.data

theorem Array.foldr_eq_foldr_data {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) : Array.foldr f init arr (Array.size arr) = List.foldr f init arr.data

@[simp]

theorem Array.push_data {α : Type u_1} (arr : Array α) (a : α) : (Array.push arr a).data = arr.data ++ [a]

theorem Array.foldrM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : Array.foldrM f init (Array.push arr a) (Array.size (Array.push arr a)) = do let init ← f a init Array.foldrM f init arr (Array.size arr)

@[simp]

theorem Array.foldrM_push' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : Array.foldrM f init (Array.push arr a) (Array.size arr + 1) = do let init ← f a init Array.foldrM f init arr (Array.size arr)

theorem Array.foldr_push {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) (a : α) : Array.foldr f init (Array.push arr a) (Array.size (Array.push arr a)) = Array.foldr f (f a init) arr (Array.size arr)

@[simp]

theorem Array.foldr_push' {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) (a : α) : Array.foldr f init (Array.push arr a) (Array.size arr + 1) = Array.foldr f (f a init) arr (Array.size arr)

@[simp]

theorem Array.toListAppend_eq {α : Type u_1} (arr : Array α) (l : List α) : Array.toListAppend arr l = arr.data ++ l

@[simp]

theorem Array.toList_eq {α : Type u_1} (arr : Array α) : Array.toList arr = arr.data

@[inline]

def Array.toListRev {α : Type u_1} (arr : Array α) : List α

A more efficient version of arr.toList.reverse.

Equations

• Array.toListRev arr = Array.foldl (fun (l : List α) (t : α) => t :: l) [] arr 0

@[simp]

theorem Array.toListRev_eq {α : Type u_1} (arr : Array α) : Array.toListRev arr = List.reverse arr.data

theorem Array.SatisfiesM_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → m β} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive i.val b → SatisfiesM (motive (i.val + 1)) (f b as[i])) : SatisfiesM (motive (Array.size as)) (Array.foldlM f init as 0)

theorem Array.SatisfiesM_foldlM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} (motive : Nat → β → Prop) {f : β → α → m β} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive i.val b → SatisfiesM (motive (i.val + 1)) (f b as[i])) {i : Nat} {j : Nat} {b : β} (h₁ : j ≤ Array.size as) (h₂ : Array.size as ≤ i + j) (H : motive j b) : SatisfiesM (motive (Array.size as)) (Array.foldlM.loop f as (Array.size as) (_ : Array.size as ≤ Array.size as) i j b)

theorem Array.foldl_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive i.val b → motive (i.val + 1) (f b as[i])) : motive (Array.size as) (Array.foldl f init as 0)

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

@[simp]

theorem Array.get_push_eq {α : Type u_1} (a : Array α) (x : α) : (Array.push a x)[Array.size a] = x

theorem Array.get_push {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < Array.size (Array.push a x)) : (Array.push a x)[i] = if h : i < Array.size a then a[i] else x

theorem Array.mapM_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : Array.mapM f arr = Array.foldlM (fun (bs : Array β) (a : α) => Array.push bs <$> f a) #[] arr 0

theorem Array.mapM_eq_foldlM.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) (i : Nat) (r : Array β) : Array.mapM.map f arr i r = List.foldlM (fun (bs : Array β) (a : α) => Array.push bs <$> f a) r (List.drop i arr.data)

theorem Array.SatisfiesM_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β) (motive : Nat → Prop) (h0 : motive 0) (p : Fin (Array.size as) → β → Prop) (hs : ∀ (i : Fin (Array.size as)), motive i.val → SatisfiesM (fun (x : β) => p i x ∧ motive (i.val + 1)) (f as[i])) : SatisfiesM (fun (arr : Array β) => motive (Array.size as) ∧ ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } arr[i]) (Array.mapM f as)

theorem Array.SatisfiesM_mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β) (p : Fin (Array.size as) → β → Prop) (hs : ∀ (i : Fin (Array.size as)), SatisfiesM (p i) (f as[i])) : SatisfiesM (fun (arr : Array β) => ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } arr[i]) (Array.mapM f as)

theorem Array.size_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (as : Array α) : SatisfiesM (fun (arr : Array β) => Array.size arr = Array.size as) (Array.mapM f as)

@[simp]

theorem Array.map_data {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (Array.map f arr).data = List.map f arr.data

@[simp]

theorem Array.size_map {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : Array.size (Array.map f arr) = Array.size arr

@[simp]

theorem Array.getElem_map {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) (i : Nat) (h : i < Array.size (Array.map f arr)) : (Array.map f arr)[i] = f arr[i]

@[simp]

theorem Array.pop_data {α : Type u_1} (arr : Array α) : (Array.pop arr).data = List.dropLast arr.data

@[simp]

theorem Array.append_eq_append {α : Type u_1} (arr : Array α) (arr' : Array α) : Array.append arr arr' = arr ++ arr'

@[simp]

theorem Array.append_data {α : Type u_1} (arr : Array α) (arr' : Array α) : (arr ++ arr').data = arr.data ++ arr'.data

@[simp]

theorem Array.appendList_eq_append {α : Type u_1} (arr : Array α) (l : List α) : Array.appendList arr l = arr ++ l

@[simp]

theorem Array.appendList_data {α : Type u_1} (arr : Array α) (l : List α) : (arr ++ l).data = arr.data ++ l

@[simp]

theorem Array.appendList_nil {α : Type u_1} (arr : Array α) : arr ++ [] = arr

@[simp]

theorem Array.appendList_cons {α : Type u_1} (arr : Array α) (a : α) (l : List α) : arr ++ a :: l = Array.push arr a ++ l

theorem Array.foldl_data_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ (acc : Array β) (a : α), (F acc a).data = acc.data ++ G a) : (List.foldl F acc l).data = acc.data ++ List.bind l G

theorem Array.foldl_data_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (G : α → β) : (List.foldl (fun (acc : Array β) (a : α) => Array.push acc (G a)) acc l).data = acc.data ++ List.map G l

theorem Array.size_uset {α : Type u_1} (a : Array α) (v : α) (i : USize) (h : USize.toNat i < Array.size a) : Array.size (Array.uset a i v h) = Array.size a

theorem Array.anyM_eq_anyM_loop {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat) (stop : Nat) : Array.anyM p as start stop = Array.anyM.loop p as (min stop (Array.size as)) (_ : min stop (Array.size as) ≤ Array.size as) start

theorem Array.anyM_stop_le_start {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat) (stop : Nat) (h : min stop (Array.size as) ≤ start) : Array.anyM p as start stop = pure false

theorem Array.SatisfiesM_anyM {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (start : Nat) (stop : Nat) (hstart : start ≤ min stop (Array.size as)) (tru : Prop) (fal : Nat → Prop) (h0 : fal start) (hp : ∀ (i : Fin (Array.size as)), i.val < stop → fal i.val → SatisfiesM (fun (x : Bool) => bif x then tru else fal (i.val + 1)) (p as[i])) : SatisfiesM (fun (res : Bool) => bif res then tru else fal (min stop (Array.size as))) (Array.anyM p as start stop)

theorem Array.SatisfiesM_anyM.go {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (tru : Prop) (fal : Nat → Prop) {stop : Nat} {j : Nat} (hj' : j ≤ stop) (hstop : stop ≤ Array.size as) (h0 : fal j) (hp : ∀ (i : Fin (Array.size as)), i.val < stop → fal i.val → SatisfiesM (fun (x : Bool) => bif x then tru else fal (i.val + 1)) (p as[i])) : SatisfiesM (fun (res : Bool) => bif res then tru else fal stop) (Array.anyM.loop p as stop hstop j)

theorem Array.SatisfiesM_anyM_iff_exists {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (start : Nat) (stop : Nat) (q : Fin (Array.size as) → Prop) (hp : ∀ (i : Fin (Array.size as)), start ≤ i.val → i.val < stop → SatisfiesM (fun (x : Bool) => x = true ↔ q i) (p as[i])) : SatisfiesM (fun (res : Bool) => res = true ↔ ∃ (i : Fin (Array.size as)), start ≤ i.val ∧ i.val < stop ∧ q i) (Array.anyM p as start stop)

theorem Array.any_iff_exists {α : Type u_1} (p : α → Bool) (as : Array α) (start : Nat) (stop : Nat) : Array.any as p start stop = true ↔ ∃ (i : Fin (Array.size as)), start ≤ i.val ∧ i.val < stop ∧ p as[i] = true

theorem Array.any_eq_true {α : Type u_1} (p : α → Bool) (as : Array α) : Array.any as p 0 = true ↔ ∃ (i : Fin (Array.size as)), p as[i] = true

theorem Array.mem_def {α : Type u_1} (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data

theorem Array.any_def {α : Type u_1} {p : α → Bool} (as : Array α) : Array.any as p 0 = List.any as.data p

theorem Array.contains_def {α : Type u_1} [DecidableEq α] {a : α} {as : Array α} : Array.contains as a = true ↔ a ∈ as

instance Array.instDecidableMemArrayInstMembershipArray {α : Type u_1} [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as)

Equations

• Array.instDecidableMemArrayInstMembershipArray a as = decidable_of_iff (Array.contains as a = true) (_ : Array.contains as a = true ↔ a ∈ as)