Lemmas about Int32Array

Lemmas about arrays and slices, stated in terms of the model Array Int32 and List Int32.

Arrays

@[simp]

theorem ScalarArray.Int32Array.size_mk (a : Array Int32) : (mk a).size = a.size

theorem ScalarArray.Int32Array.size_eq_toArray_size (a : Int32Array) : a.size = a.toArray.size

@[simp]

theorem ScalarArray.Int32Array.size_toArray (a : Int32Array) : a.toArray.size = a.size

@[simp]

theorem ScalarArray.Int32Array.size_uset (a : Int32Array) (i : USize) (v : Int32) (h : i.toNat < a.size) : (a.uset i v h).size = a.size

@[simp]

theorem ScalarArray.Int32Array.size_set (a : Int32Array) (i : Nat) (v : Int32) (h : i < a.size) : (a.set i v h).size = a.size

@[simp]

theorem ScalarArray.Int32Array.size_push (a : Int32Array) (v : Int32) : (a.push v).size = a.size + 1

@[simp]

theorem ScalarArray.Int32Array.toArray_append (a b : Int32Array) : (a ++ b).toArray = a.toArray ++ b.toArray

@[simp]

theorem ScalarArray.Int32Array.size_append (a b : Int32Array) : (a ++ b).size = a.size + b.size

theorem ScalarArray.Int32Array.ext {a b : Int32Array} (h : a.toArray = b.toArray) : a = b

theorem ScalarArray.Int32Array.ext_iff {a b : Int32Array} : a = b ↔ a.toArray = b.toArray

@[simp]

theorem ScalarArray.Int32Array.toArray_inj {a b : Int32Array} : a.toArray = b.toArray ↔ a = b

@[simp]

theorem ScalarArray.Int32Array.getElem_mk (a : Array Int32) (i : Nat) (h : i < (mk a).size) : (mk a)[i] = a[i]

theorem ScalarArray.Int32Array.getElem_eq_getElem_toArray (a : Int32Array) (i : Nat) (h : i < a.size) : a[i] = a.toArray[i]

@[simp]

theorem ScalarArray.Int32Array.getElem_toArray (a : Int32Array) (i : Nat) (h : i < a.toArray.size) : a.toArray[i] = a[i]

theorem ScalarArray.Int32Array.ext_getElem {a b : Int32Array} (h₁ : a.size = b.size) (h₂ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a[i] = b[i]) : a = b

@[simp]

theorem ScalarArray.Int32Array.getElem_usize (a : Int32Array) (i : USize) (h : i.toNat < a.size) : a[i] = a[i.toNat]

@[simp]

theorem ScalarArray.Int32Array.toArray_uset (a : Int32Array) (i : USize) (v : Int32) (h : i.toNat < a.size) : (a.uset i v h).toArray = a.toArray.set i.toNat v ⋯

@[simp]

theorem ScalarArray.Int32Array.toArray_set (a : Int32Array) (i : Nat) (v : Int32) (h : i < a.size) : (a.set i v h).toArray = a.toArray.set i v ⋯

@[simp]

theorem ScalarArray.Int32Array.toArray_push (a : Int32Array) (v : Int32) : (a.push v).toArray = a.toArray.push v

@[simp]

theorem ScalarArray.Int32Array.toArray_pop (a : Int32Array) : a.pop.toArray = a.toArray.pop

@[simp]

theorem ScalarArray.Int32Array.toArray_extract (a : Int32Array) (start stop : Nat) : (a.extract start stop).toArray = a.toArray.extract start stop

@[simp]

theorem ScalarArray.Int32Array.toArray_replicate (n : Nat) (v : Int32) : (replicate n v).toArray = Array.replicate n v

@[simp]

theorem ScalarArray.Int32Array.toArray_ofFn {n : Nat} (f : Fin n → Int32) : (ofFn f).toArray = Array.ofFn f

@[simp]

theorem ScalarArray.Int32Array.toArray_empty : empty.toArray = #[]

@[simp]

theorem ScalarArray.Int32Array.size_pop (a : Int32Array) : a.pop.size = a.size - 1

@[simp]

theorem ScalarArray.Int32Array.size_extract (a : Int32Array) (start stop : Nat) : (a.extract start stop).size = min stop a.size - start

@[simp]

theorem ScalarArray.Int32Array.size_replicate (n : Nat) (v : Int32) : (replicate n v).size = n

@[simp]

theorem ScalarArray.Int32Array.size_ofFn {n : Nat} (f : Fin n → Int32) : (ofFn f).size = n

@[simp]

theorem ScalarArray.Int32Array.size_empty : empty.size = 0

@[simp]

theorem ScalarArray.Int32Array.getElem_set (a : Int32Array) (i : Nat) (v : Int32) (h : i < a.size) (j : Nat) (hj : j < (a.set i v h).size) : (a.set i v h)[j] = if i = j then v else a[j]

@[simp]

theorem ScalarArray.Int32Array.getElem_push (a : Int32Array) (v : Int32) (i : Nat) (h : i < (a.push v).size) : (a.push v)[i] = if h' : i < a.size then a[i] else v

@[simp]

theorem ScalarArray.Int32Array.getElem_pop (a : Int32Array) (i : Nat) (h : i < a.pop.size) : a.pop[i] = a[i]

@[simp]

theorem ScalarArray.Int32Array.toArray_popWhile (p : Int32 → Bool) (a : Int32Array) : (popWhile p a).toArray = Array.popWhile p a.toArray

@[simp]

theorem ScalarArray.Int32Array.getElem_append (a b : Int32Array) (i : Nat) (h : i < (a ++ b).size) : (a ++ b)[i] = if h' : i < a.size then a[i] else b[i - a.size]

@[simp]

theorem ScalarArray.Int32Array.getElem_extract (a : Int32Array) (start stop i : Nat) (h : i < (a.extract start stop).size) : (a.extract start stop)[i] = a[start + i]

@[simp]

theorem ScalarArray.Int32Array.getElem_replicate (n : Nat) (v : Int32) (i : Nat) (h : i < (replicate n v).size) : (replicate n v)[i] = v

@[simp]

theorem ScalarArray.Int32Array.getElem_ofFn {n : Nat} (f : Fin n → Int32) (i : Nat) (h : i < (ofFn f).size) : (ofFn f)[i] = f ⟨i, ⋯⟩

theorem ScalarArray.Int32Array.foldl_eq_foldl_toArray {β : Type v} (f : β → Int32 → β) (init : β) (a : Int32Array) : foldl f init a = Array.foldl f init a.toArray

theorem ScalarArray.Int32Array.foldr_eq_foldr_toArray {β : Type v} (f : Int32 → β → β) (init : β) (a : Int32Array) : foldr f init a = Array.foldr f init a.toArray

@[simp]

theorem ScalarArray.Int32Array.toList_toArray (a : Int32Array) : a.toArray.toList = a.toList

@[simp]

theorem ScalarArray.Int32Array.emptyc_eq_empty : ∅ = empty

@[simp]

theorem ScalarArray.Int32Array.emptyWithCapacity_eq_empty (c : Nat) : emptyWithCapacity c = empty

theorem ScalarArray.Int32Array.size_eq_zero_iff {a : Int32Array} : a.size = 0 ↔ a = empty

@[simp]

theorem ScalarArray.Int32Array.toArray_set! (a : Int32Array) (i : Nat) (v : Int32) : (a.set! i v).toArray = a.toArray.set! i v

@[simp]

theorem ScalarArray.Int32Array.size_set! (a : Int32Array) (i : Nat) (v : Int32) : (a.set! i v).size = a.size

theorem ScalarArray.Int32Array.getElem!_eq_getElem!_toArray (a : Int32Array) (i : Nat) : a[i]! = a.toArray[i]!

@[simp]

theorem ScalarArray.Int32Array.toArray_ofList (l : List Int32) : (ofList l).toArray = l.toArray

@[simp]

theorem ScalarArray.Int32Array.size_ofList (l : List Int32) : (ofList l).size = l.length

@[simp]

theorem ScalarArray.Int32Array.getElem_ofList (l : List Int32) (i : Nat) (h : i < (ofList l).size) : (ofList l)[i] = l[i]

@[simp]

theorem ScalarArray.Int32Array.toList_ofList (l : List Int32) : (ofList l).toList = l

@[simp]

theorem ScalarArray.Int32Array.ofList_toList (a : Int32Array) : ofList a.toList = a

@[simp]

theorem ScalarArray.Int32Array.ensureExclusive_eq (a : Int32Array) : a.ensureExclusive = a

@[simp]

theorem ScalarArray.Int32Array.ensureCapacity_eq (a : Int32Array) (n : Nat) : a.ensureCapacity n = a

@[simp]

theorem ScalarArray.Int32Array.ensureExclusiveWithCapacity_eq (a : Int32Array) (n : Nat) : a.ensureExclusiveWithCapacity n = a

@[simp]

theorem ScalarArray.Int32Array.markLinear_eq (a : Int32Array) : a.markLinear = a

@[simp]

theorem ScalarArray.Int32Array.propagateMark_eq (a b : Int32Array) : a.propagateMark b = b

@[simp]

theorem ScalarArray.Int32Array.append_empty (a : Int32Array) : a ++ empty = a

@[simp]

theorem ScalarArray.Int32Array.empty_append (a : Int32Array) : empty ++ a = a

theorem ScalarArray.Int32Array.append_assoc (a b c : Int32Array) : a ++ b ++ c = a ++ (b ++ c)

@[simp]

theorem ScalarArray.Int32Array.append_eq_empty_iff {a b : Int32Array} : a ++ b = empty ↔ a = empty ∧ b = empty

@[simp]

theorem ScalarArray.Int32Array.append_right_inj (a : Int32Array) {b c : Int32Array} : a ++ b = a ++ c ↔ b = c

@[simp]

theorem ScalarArray.Int32Array.append_left_inj {a b : Int32Array} (c : Int32Array) : a ++ c = b ++ c ↔ a = b

theorem ScalarArray.Int32Array.getElem_append_left {a b : Int32Array} {i : Nat} (h : i < a.size) : (a ++ b)[i] = a[i]

theorem ScalarArray.Int32Array.getElem_append_right {a b : Int32Array} {i : Nat} (h : a.size ≤ i) (h' : i < (a ++ b).size) : (a ++ b)[i] = b[i - a.size]

@[simp]

theorem ScalarArray.Int32Array.extract_same (a : Int32Array) (i : Nat) : a.extract i i = empty

@[simp]

theorem ScalarArray.Int32Array.extract_zero_size (a : Int32Array) : a.extract 0 a.size = a

@[simp]

theorem ScalarArray.Int32Array.extract_eq_empty_iff {a : Int32Array} {i j : Nat} : a.extract i j = empty ↔ min j a.size ≤ i

theorem ScalarArray.Int32Array.extract_extract (a : Int32Array) (i j k l : Nat) : (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j)

theorem ScalarArray.Int32Array.extract_append_extract (a : Int32Array) (i j k : Nat) : a.extract i j ++ a.extract j k = a.extract (min i j) (max j k)

@[simp]

theorem ScalarArray.Int32Array.extract_append_eq_left (a b : Int32Array) : (a ++ b).extract 0 a.size = a

@[simp]

theorem ScalarArray.Int32Array.extract_append_eq_right (a b : Int32Array) : (a ++ b).extract a.size (a.size + b.size) = b

@[simp]

theorem ScalarArray.Int32Array.toArray_copySlice (src : Int32Array) (srcOff : Nat) (dest : Int32Array) (destOff len : Nat) (exact : Bool) : (src.copySlice srcOff dest destOff len exact).toArray = dest.toArray.extract 0 destOff ++ src.toArray.extract srcOff (srcOff + len) ++ dest.toArray.extract (destOff + min len (src.size - srcOff)) dest.size

theorem ScalarArray.Int32Array.copySlice_eq_append (src : Int32Array) (srcOff : Nat) (dest : Int32Array) (destOff len : Nat) (exact : Bool) : src.copySlice srcOff dest destOff len exact = dest.extract 0 destOff ++ src.extract srcOff (srcOff + len) ++ dest.extract (destOff + min len (src.size - srcOff)) dest.size

Lists

@[simp]

theorem ScalarArray.Int32Array.toList_mk (a : Array Int32) : (mk a).toList = a.toList

@[simp]

theorem ScalarArray.Int32Array.length_toList (a : Int32Array) : a.toList.length = a.size

@[simp]

theorem ScalarArray.Int32Array.getElem_toList (a : Int32Array) (i : Nat) (h : i < a.toList.length) : a.toList[i] = a[i]

@[simp]

theorem ScalarArray.Int32Array.getElem?_toList (a : Int32Array) (i : Nat) : a.toList[i]? = a[i]?

@[simp]

theorem ScalarArray.Int32Array.toList_inj {a b : Int32Array} : a.toList = b.toList ↔ a = b

theorem ScalarArray.Int32Array.ext_getElem? {a b : Int32Array} (h : ∀ (i : Nat), a[i]? = b[i]?) : a = b

@[simp]

theorem ScalarArray.Int32Array.toList_empty : empty.toList = []

@[simp]

theorem ScalarArray.Int32Array.toList_push (a : Int32Array) (v : Int32) : (a.push v).toList = a.toList ++ [v]

@[simp]

theorem ScalarArray.Int32Array.toList_pop (a : Int32Array) : a.pop.toList = a.toList.dropLast

@[simp]

theorem ScalarArray.Int32Array.toList_append (a b : Int32Array) : (a ++ b).toList = a.toList ++ b.toList

@[simp]

theorem ScalarArray.Int32Array.toList_set (a : Int32Array) (i : Nat) (v : Int32) (h : i < a.size) : (a.set i v h).toList = a.toList.set i v

@[simp]

theorem ScalarArray.Int32Array.toList_set! (a : Int32Array) (i : Nat) (v : Int32) : (a.set! i v).toList = a.toList.set i v

@[simp]

theorem ScalarArray.Int32Array.toList_extract (a : Int32Array) (start stop : Nat) : (a.extract start stop).toList = a.toList.extract start stop

@[simp]

theorem ScalarArray.Int32Array.toList_replicate (n : Nat) (v : Int32) : (replicate n v).toList = List.replicate n v

@[simp]

theorem ScalarArray.Int32Array.toList_ofFn {n : Nat} (f : Fin n → Int32) : (ofFn f).toList = List.ofFn f

@[simp]

theorem ScalarArray.Int32Array.toList_popWhile (p : Int32 → Bool) (a : Int32Array) : (popWhile p a).toList = (List.dropWhile p a.toList.reverse).reverse

@[simp]

theorem ScalarArray.Int32Array.toList_uset (a : Int32Array) (i : USize) (v : Int32) (h : i.toNat < a.size) : (a.uset i v h).toList = a.toList.set i.toNat v

@[simp]

theorem ScalarArray.Int32Array.toList_copySlice (src : Int32Array) (srcOff : Nat) (dest : Int32Array) (destOff len : Nat) (exact : Bool) : (src.copySlice srcOff dest destOff len exact).toList = dest.toList.extract 0 destOff ++ src.toList.extract srcOff (srcOff + len) ++ dest.toList.extract (destOff + min len (src.size - srcOff)) dest.size

Accessors

@[simp]

theorem ScalarArray.Int32Array.get_eq_getElem (a : Int32Array) (i : Nat) (h : i < a.size) : a.get i h = a[i]

@[simp]

theorem ScalarArray.Int32Array.uget_eq_getElem (a : Int32Array) (i : USize) (h : i.toNat < a.size) : a.uget i h = a[i.toNat]

@[simp]

theorem ScalarArray.Int32Array.get!_eq_getElem! (a : Int32Array) (i : Nat) : a.get! i = a[i]!

@[simp]

theorem ScalarArray.Int32Array.getD_eq_getD_getElem? (a : Int32Array) (i : Nat) (v₀ : Int32) : a.getD i v₀ = a[i]?.getD v₀

@[simp]

theorem ScalarArray.Int32Array.isEmpty_iff {a : Int32Array} : a.isEmpty = true ↔ a = empty

Last element

theorem ScalarArray.Int32Array.back?_eq_getElem? (a : Int32Array) : a.back? = a[a.size - 1]?

theorem ScalarArray.Int32Array.back!_eq_getElem! (a : Int32Array) : a.back! = a[a.size - 1]!

theorem ScalarArray.Int32Array.back_eq_getElem (a : Int32Array) (h : 0 < a.size) : a.back h = a[a.size - 1]

@[simp]

theorem ScalarArray.Int32Array.getLast?_toList (a : Int32Array) : a.toList.getLast? = a.back?

@[simp]

theorem ScalarArray.Int32Array.back?_empty : empty.back? = none

@[simp]

theorem ScalarArray.Int32Array.back?_push (a : Int32Array) (v : Int32) : (a.push v).back? = some v

@[simp]

theorem ScalarArray.Int32Array.back!_push (a : Int32Array) (v : Int32) : (a.push v).back! = v

@[simp]

theorem ScalarArray.Int32Array.back_push (a : Int32Array) (v : Int32) (h : 0 < (a.push v).size) : (a.push v).back h = v

Writes

@[simp]

theorem ScalarArray.Int32Array.getElem_uset (a : Int32Array) (i : USize) (v : Int32) (h : i.toNat < a.size) (j : Nat) (hj : j < (a.uset i v h).size) : (a.uset i v h)[j] = if i.toNat = j then v else a[j]

@[simp]

theorem ScalarArray.Int32Array.getElem_set! (a : Int32Array) (i : Nat) (v : Int32) (j : Nat) (hj : j < (a.set! i v).size) : (a.set! i v)[j] = if i = j then v else a[j]

@[simp]

theorem ScalarArray.Int32Array.getElem?_set! (a : Int32Array) (i : Nat) (v : Int32) (j : Nat) : (a.set! i v)[j]? = if i = j then if i < a.size then some v else none else a[j]?

theorem ScalarArray.Int32Array.size_popWhile_le (p : Int32 → Bool) (a : Int32Array) : (popWhile p a).size ≤ a.size

@[simp]

theorem ScalarArray.Int32Array.size_copySlice (src : Int32Array) (srcOff : Nat) (dest : Int32Array) (destOff len : Nat) (exact : Bool) : (src.copySlice srcOff dest destOff len exact).size = max dest.size (min destOff dest.size + min len (src.size - srcOff))

theorem ScalarArray.Int32Array.getElem_copySlice (src : Int32Array) (srcOff : Nat) (dest : Int32Array) (destOff len : Nat) (exact : Bool) (i : Nat) (h : i < (src.copySlice srcOff dest destOff len exact).size) : (src.copySlice srcOff dest destOff len exact)[i] = if h₁ : i < min destOff dest.size then dest[i] else if h₂ : i - min destOff dest.size < min len (src.size - srcOff) then src[srcOff + (i - min destOff dest.size)] else dest[i]

Machine-word indices

theorem ScalarArray.Int32Array.toNat_usize_of_lt (a : Int32Array) (h : a.size < USize.size) : a.usize.toNat = a.size

usize is the size when the size fits in a USize, which holds for every array in memory. Loops over USize indices take this as a hypothesis, since the model Array has no bound on its size.

theorem ScalarArray.Int32Array.lt_usize_iff (a : Int32Array) (h : a.size < USize.size) {i : USize} : i < a.usize ↔ i.toNat < a.size

The guard i < a.usize of a loop over USize indices bounds the index.

Folds and queries

@[simp]

theorem ScalarArray.Int32Array.any_toList (a : Int32Array) (p : Int32 → Bool) : a.toList.any p = a.any p

@[simp]

theorem ScalarArray.Int32Array.all_toList (a : Int32Array) (p : Int32 → Bool) : a.toList.all p = a.all p

@[simp]

theorem ScalarArray.Int32Array.contains_toList (a : Int32Array) (v : Int32) : a.toList.contains v = a.contains v

@[simp]

theorem ScalarArray.Int32Array.foldl_toList {β : Type v} (f : β → Int32 → β) (init : β) (a : Int32Array) : List.foldl f init a.toList = foldl f init a

@[simp]

theorem ScalarArray.Int32Array.foldr_toList {β : Type v} (f : Int32 → β → β) (init : β) (a : Int32Array) : List.foldr f init a.toList = foldr f init a

@[simp]

theorem ScalarArray.Int32Array.forIn_toList {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (a : Int32Array) (init : β) (f : Int32 → β → m (ForInStep β)) : ForIn.forIn a.toList init f = ForIn.forIn a init f

theorem ScalarArray.Int32Array.findIdx?_eq (a : Int32Array) (p : Int32 → Bool) (start : Nat) : a.findIdx? p start = Option.map (fun (x : Nat) => x + start) (List.findIdx? p (List.drop start a.toList))

@[simp]

theorem ScalarArray.Int32Array.findIdx?_toList (a : Int32Array) (p : Int32 → Bool) : List.findIdx? p a.toList = a.findIdx? p

@[simp]

theorem ScalarArray.Int32Array.map_val_findFinIdx? (a : Int32Array) (p : Int32 → Bool) (start : Nat) : Option.map Fin.val (a.findFinIdx? p start) = a.findIdx? p start

@[simp]

theorem ScalarArray.Int32Array.foldlM_toList {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Int32 → m β) (init : β) (a : Int32Array) : List.foldlM f init a.toList = foldlM f init a

@[simp]

theorem ScalarArray.Int32Array.foldrM_toList {β : Type v} {m : Type v → Type w} [Monad m] (f : Int32 → β → m β) (init : β) (a : Int32Array) : List.foldrM f init a.toList = foldrM f init a

@[simp]

theorem ScalarArray.Int32Array.forM_eq_forM {m : Type v → Type w} [Monad m] (f : Int32 → m PUnit) (a : Int32Array) : forM f a = ForM.forM a f

@[simp]

theorem ScalarArray.Int32Array.forM_toList {m : Type v → Type w} [Monad m] (f : Int32 → m PUnit) (a : Int32Array) : ForM.forM a.toList f = ForM.forM a f

Membership

theorem ScalarArray.Int32Array.mem_def {x : Int32} {a : Int32Array} : x ∈ a ↔ x ∈ a.toArray

@[simp]

theorem ScalarArray.Int32Array.mem_toArray {x : Int32} {a : Int32Array} : x ∈ a.toArray ↔ x ∈ a

@[simp]

theorem ScalarArray.Int32Array.mem_mk {x : Int32} {xs : Array Int32} : x ∈ mk xs ↔ x ∈ xs

@[simp]

theorem ScalarArray.Int32Array.mem_toList {x : Int32} {a : Int32Array} : x ∈ a.toList ↔ x ∈ a

theorem ScalarArray.Int32Array.mem_iff_getElem {x : Int32} {a : Int32Array} : x ∈ a ↔ ∃ (i : Nat), ∃ (h : i < a.size), a[i] = x

theorem ScalarArray.Int32Array.getElem_mem {a : Int32Array} {i : Nat} (h : i < a.size) : a[i] ∈ a

@[simp]

theorem ScalarArray.Int32Array.not_mem_empty (x : Int32) : ¬x ∈ empty

@[simp]

theorem ScalarArray.Int32Array.mem_push {x v : Int32} {a : Int32Array} : x ∈ a.push v ↔ x ∈ a ∨ x = v

@[simp]

theorem ScalarArray.Int32Array.mem_append {x : Int32} {a b : Int32Array} : x ∈ a ++ b ↔ x ∈ a ∨ x ∈ b

Collecting iterators

@[simp]

theorem Std.Iter.toList_toInt32Array {α : Type} [Iterator α Id Int32] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] (it : Iter Int32) : it.toInt32Array.toList = it.toList

Slices

@[simp]

theorem ScalarArray.Int32Array.Slice.size_copy (s : Int32Array.Slice) : s.copy.size = Std.Slice.size s

@[simp]

theorem ScalarArray.Int32Array.Slice.getElem_copy (s : Int32Array.Slice) (i : Nat) (h : i < s.copy.size) : s.copy[i] = s[i]

@[simp]

theorem ScalarArray.Int32Array.copy_toSlice (a : Int32Array) (start stop : Nat) : (a.toSlice start stop).copy = a.extract start stop

Copying the slice from start to stop is the same as extracting those elements.

@[simp]

theorem ScalarArray.Int32Array.array_toSlice (a : Int32Array) (start stop : Nat) : (a.toSlice start stop).array = a

@[simp]

theorem ScalarArray.Int32Array.start_toSlice (a : Int32Array) (start stop : Nat) : (a.toSlice start stop).start = min start (min stop a.size)

@[simp]

theorem ScalarArray.Int32Array.stop_toSlice (a : Int32Array) (start stop : Nat) : (a.toSlice start stop).stop = min stop a.size

@[simp]

theorem ScalarArray.Int32Array.size_toSlice (a : Int32Array) (start stop : Nat) : Std.Slice.size (a.toSlice start stop) = min stop a.size - start

@[simp]

theorem ScalarArray.Int32Array.getElem_toSlice (a : Int32Array) (start stop i : Nat) (h : i < Std.Slice.size (a.toSlice start stop)) : (a.toSlice start stop)[i] = a[start + i]

@[simp]

theorem ScalarArray.Int32Array.Slice.size_slice (s : Int32Array.Slice) (start stop : Nat) : Std.Slice.size (s.slice start stop) = min stop (Std.Slice.size s) - start

@[simp]

theorem ScalarArray.Int32Array.Slice.getElem_slice (s : Int32Array.Slice) (start stop i : Nat) (h : i < Std.Slice.size (s.slice start stop)) : (s.slice start stop)[i] = s[start + i]

@[simp]

theorem ScalarArray.Int32Array.Slice.copy_slice (s : Int32Array.Slice) (start stop : Nat) : (s.slice start stop).copy = s.copy.extract start stop

@[simp]

theorem ScalarArray.Int32Array.Slice.array_popFront (s : Int32Array.Slice) : s.popFront.array = s.array

@[simp]

theorem ScalarArray.Int32Array.Slice.start_popFront (s : Int32Array.Slice) : s.popFront.start = min (s.start + 1) s.stop

@[simp]

theorem ScalarArray.Int32Array.Slice.stop_popFront (s : Int32Array.Slice) : s.popFront.stop = s.stop

@[simp]

theorem ScalarArray.Int32Array.Slice.size_popFront (s : Int32Array.Slice) : Std.Slice.size s.popFront = Std.Slice.size s - 1

@[simp]

theorem ScalarArray.Int32Array.Slice.getElem_popFront (s : Int32Array.Slice) (i : Nat) (h : i < Std.Slice.size s.popFront) : s.popFront[i] = s[i + 1]

theorem ScalarArray.Int32Array.Slice.getD_eq (s : Int32Array.Slice) (i : Nat) (v₀ : Int32) : s.getD i v₀ = if h : i < Std.Slice.size s then s[i] else v₀

theorem ScalarArray.Int32Array.Slice.get!_eq (s : Int32Array.Slice) (i : Nat) : s.get! i = if h : i < Std.Slice.size s then s[i] else default

theorem ScalarArray.Int32Array.Slice.foldr_eq_foldr_toList_copy {β : Type v} (f : Int32 → β → β) (init : β) (s : Int32Array.Slice) : foldr f init s = List.foldr f init s.copy.toList

Folding over a slice is folding over the list of its elements.

Slices as copies

@[simp]

theorem ScalarArray.Int32Array.Slice.size_empty : Std.Slice.size Slice.empty = 0

@[simp]

theorem ScalarArray.Int32Array.Slice.emptyc_eq_empty : ∅ = Slice.empty

@[simp]

theorem ScalarArray.Int32Array.Slice.copy_empty : Slice.empty.copy = empty

@[simp]

theorem ScalarArray.Int32Array.Slice.toList_eq_toList_copy (s : Int32Array.Slice) : Std.Slice.toList s = s.copy.toList

@[simp]

theorem ScalarArray.Int32Array.Slice.toInt32Slice_iter (s : Int32Array.Slice) : (Std.Slice.iter s).toInt32Slice = s

@[simp]

theorem Std.Iter.iter_toInt32Slice (it : Iter Int32) : Slice.iter it.toInt32Slice = it

theorem Std.Iter.toList_eq_toList_toInt32Slice (it : Iter Int32) : it.toList = Slice.toList it.toInt32Slice

@[simp]

theorem ScalarArray.Int32Array.Slice.toInt32Array_iter (s : Int32Array.Slice) : (Std.Slice.iter s).toInt32Array = s.copy

@[simp]

theorem ScalarArray.Int32Array.toInt32Array_iter (a : Int32Array) : a.iter.toInt32Array = a

@[simp]

theorem ScalarArray.Int32Array.Slice.foldl_eq_foldl_copy {β : Type v} (f : β → Int32 → β) (init : β) (s : Int32Array.Slice) : Std.Slice.foldl f init s = foldl f init s.copy

@[simp]

theorem ScalarArray.Int32Array.Slice.foldlM_eq_foldlM_copy {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : β → Int32 → m β) (init : β) (s : Int32Array.Slice) : Std.Slice.foldlM f init s = foldlM f init s.copy

@[simp]

theorem ScalarArray.Int32Array.Slice.forIn_eq_forIn_copy {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (s : Int32Array.Slice) (init : β) (f : Int32 → β → m (ForInStep β)) : ForIn.forIn s init f = ForIn.forIn s.copy init f

@[simp]

theorem ScalarArray.Int32Array.Slice.forM_eq_forM_copy {m : Type v → Type w} [Monad m] [LawfulMonad m] (s : Int32Array.Slice) (f : Int32 → m PUnit) : ForM.forM s f = ForM.forM s.copy f

@[simp]

theorem ScalarArray.Int32Array.Slice.foldr_eq_foldr_copy {β : Type v} (f : Int32 → β → β) (init : β) (s : Int32Array.Slice) : foldr f init s = Int32Array.foldr f init s.copy

@[simp]

theorem ScalarArray.Int32Array.Slice.foldrM_eq_foldrM_copy {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : Int32 → β → m β) (init : β) (s : Int32Array.Slice) : foldrM f init s = Int32Array.foldrM f init s.copy

@[simp]

theorem ScalarArray.Int32Array.Slice.any_eq_any_copy (s : Int32Array.Slice) (p : Int32 → Bool) : s.any p = s.copy.any p

@[simp]

theorem ScalarArray.Int32Array.Slice.all_eq_all_copy (s : Int32Array.Slice) (p : Int32 → Bool) : s.all p = s.copy.all p

@[simp]

theorem ScalarArray.Int32Array.Slice.contains_eq_contains_copy (s : Int32Array.Slice) (v : Int32) : s.contains v = s.copy.contains v

@[simp]

theorem ScalarArray.Int32Array.Slice.find?_eq_find?_toList_copy (s : Int32Array.Slice) (p : Int32 → Bool) : s.find? p = List.find? p s.copy.toList

@[simp]

theorem ScalarArray.Int32Array.Slice.count_eq_countP_toList_copy (s : Int32Array.Slice) (p : Int32 → Bool) : s.count p = List.countP p s.copy.toList

@[simp]

theorem ScalarArray.Int32Array.Slice.findRev?_eq_find?_reverse_toList_copy (s : Int32Array.Slice) (p : Int32 → Bool) : s.findRev? p = List.find? p s.copy.toList.reverse

Membership in slices

@[simp]

theorem ScalarArray.Int32Array.Slice.mem_iff_mem_copy {x : Int32} {s : Int32Array.Slice} : x ∈ s ↔ x ∈ s.copy

theorem ScalarArray.Int32Array.Slice.mem_iff_getElem {x : Int32} {s : Int32Array.Slice} : x ∈ s ↔ ∃ (i : Nat), ∃ (h : i < Std.Slice.size s), s[i] = x

theorem ScalarArray.Int32Array.Slice.getElem_mem {s : Int32Array.Slice} {i : Nat} (h : i < Std.Slice.size s) : s[i] ∈ s

Slice equality

@[simp]

theorem ScalarArray.Int32Array.Slice.beq_eq_beq_copy (s t : Int32Array.Slice) : (s == t) = (s.copy == t.copy)