Lemmas about USizeArray

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

Arrays

@[simp]

theorem ScalarArray.USizeArray.size_mk (a : Array USize) : (mk a).size = a.size

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.size_push (a : USizeArray) (v : USize) : (a.push v).size = a.size + 1

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem ScalarArray.USizeArray.ext_getElem {a b : USizeArray} (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.USizeArray.getElem_usize (a : USizeArray) (i : USize) (h : i.toNat < a.size) : a[i] = a[i.toNat]

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toArray_push (a : USizeArray) (v : USize) : (a.push v).toArray = a.toArray.push v

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toArray_replicate (n : Nat) (v : USize) : (replicate n v).toArray = Array.replicate n v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.size_replicate (n : Nat) (v : USize) : (replicate n v).size = n

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.getElem_set (a : USizeArray) (i : Nat) (v : USize) (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.USizeArray.getElem_push (a : USizeArray) (v : USize) (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.USizeArray.getElem_pop (a : USizeArray) (i : Nat) (h : i < a.pop.size) : a.pop[i] = a[i]

@[simp]

theorem ScalarArray.USizeArray.toArray_popWhile (p : USize → Bool) (a : USizeArray) : (popWhile p a).toArray = Array.popWhile p a.toArray

@[simp]

theorem ScalarArray.USizeArray.getElem_append (a b : USizeArray) (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.USizeArray.getElem_extract (a : USizeArray) (start stop i : Nat) (h : i < (a.extract start stop).size) : (a.extract start stop)[i] = a[start + i]

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.emptyc_eq_empty : ∅ = empty

@[simp]

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

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

@[simp]

theorem ScalarArray.USizeArray.toArray_set! (a : USizeArray) (i : Nat) (v : USize) : (a.set! i v).toArray = a.toArray.set! i v

@[simp]

theorem ScalarArray.USizeArray.size_set! (a : USizeArray) (i : Nat) (v : USize) : (a.set! i v).size = a.size

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

@[simp]

theorem ScalarArray.USizeArray.toArray_ofList (l : List USize) : (ofList l).toArray = l.toArray

@[simp]

theorem ScalarArray.USizeArray.size_ofList (l : List USize) : (ofList l).size = l.length

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toList_ofList (l : List USize) : (ofList l).toList = l

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toArray_copySlice (src : USizeArray) (srcOff : Nat) (dest : USizeArray) (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.USizeArray.copySlice_eq_append (src : USizeArray) (srcOff : Nat) (dest : USizeArray) (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.USizeArray.toList_mk (a : Array USize) : (mk a).toList = a.toList

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toList_push (a : USizeArray) (v : USize) : (a.push v).toList = a.toList ++ [v]

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toList_set! (a : USizeArray) (i : Nat) (v : USize) : (a.set! i v).toList = a.toList.set i v

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toList_replicate (n : Nat) (v : USize) : (replicate n v).toList = List.replicate n v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.toList_copySlice (src : USizeArray) (srcOff : Nat) (dest : USizeArray) (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.USizeArray.get_eq_getElem (a : USizeArray) (i : Nat) (h : i < a.size) : a.get i h = a[i]

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Last element

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.back?_push (a : USizeArray) (v : USize) : (a.push v).back? = some v

@[simp]

theorem ScalarArray.USizeArray.back!_push (a : USizeArray) (v : USize) : (a.push v).back! = v

@[simp]

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

Writes

@[simp]

theorem ScalarArray.USizeArray.getElem_uset (a : USizeArray) (i v : USize) (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.USizeArray.getElem_set! (a : USizeArray) (i : Nat) (v : USize) (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.USizeArray.getElem?_set! (a : USizeArray) (i : Nat) (v : USize) (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.USizeArray.size_popWhile_le (p : USize → Bool) (a : USizeArray) : (popWhile p a).size ≤ a.size

@[simp]

theorem ScalarArray.USizeArray.size_copySlice (src : USizeArray) (srcOff : Nat) (dest : USizeArray) (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.USizeArray.getElem_copySlice (src : USizeArray) (srcOff : Nat) (dest : USizeArray) (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.USizeArray.toNat_usize_of_lt (a : USizeArray) (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.USizeArray.lt_usize_iff (a : USizeArray) (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.USizeArray.any_toList (a : USizeArray) (p : USize → Bool) : a.toList.any p = a.any p

@[simp]

theorem ScalarArray.USizeArray.all_toList (a : USizeArray) (p : USize → Bool) : a.toList.all p = a.all p

@[simp]

theorem ScalarArray.USizeArray.contains_toList (a : USizeArray) (v : USize) : a.toList.contains v = a.contains v

@[simp]

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

@[simp]

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

@[simp]

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

theorem ScalarArray.USizeArray.findIdx?_eq (a : USizeArray) (p : USize → 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.USizeArray.findIdx?_toList (a : USizeArray) (p : USize → Bool) : List.findIdx? p a.toList = a.findIdx? p

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Membership

theorem ScalarArray.USizeArray.mem_def {x : USize} {a : USizeArray} : x ∈ a ↔ x ∈ a.toArray

@[simp]

theorem ScalarArray.USizeArray.mem_toArray {x : USize} {a : USizeArray} : x ∈ a.toArray ↔ x ∈ a

@[simp]

theorem ScalarArray.USizeArray.mem_mk {x : USize} {xs : Array USize} : x ∈ mk xs ↔ x ∈ xs

@[simp]

theorem ScalarArray.USizeArray.mem_toList {x : USize} {a : USizeArray} : x ∈ a.toList ↔ x ∈ a

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

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

@[simp]

theorem ScalarArray.USizeArray.not_mem_empty (x : USize) : ¬x ∈ empty

@[simp]

theorem ScalarArray.USizeArray.mem_push {x v : USize} {a : USizeArray} : x ∈ a.push v ↔ x ∈ a ∨ x = v

@[simp]

theorem ScalarArray.USizeArray.mem_append {x : USize} {a b : USizeArray} : x ∈ a ++ b ↔ x ∈ a ∨ x ∈ b

Collecting iterators

@[simp]

theorem Std.Iter.toList_toUSizeArray {α : Type} [Iterator α Id USize] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] (it : Iter USize) : it.toUSizeArray.toList = it.toList

Slices

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.copy_toSlice (a : USizeArray) (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.USizeArray.array_toSlice (a : USizeArray) (start stop : Nat) : (a.toSlice start stop).array = a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.Slice.getElem_slice (s : USizeArray.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.USizeArray.Slice.copy_slice (s : USizeArray.Slice) (start stop : Nat) : (s.slice start stop).copy = s.copy.extract start stop

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem ScalarArray.USizeArray.Slice.foldr_eq_foldr_toList_copy {β : Type v} (f : USize → β → β) (init : β) (s : USizeArray.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.USizeArray.Slice.size_empty : Std.Slice.size Slice.empty = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.Slice.toUSizeSlice_iter (s : USizeArray.Slice) : (Std.Slice.iter s).toUSizeSlice = s

@[simp]

theorem Std.Iter.iter_toUSizeSlice (it : Iter USize) : Slice.iter it.toUSizeSlice = it

theorem Std.Iter.toList_eq_toList_toUSizeSlice (it : Iter USize) : it.toList = Slice.toList it.toUSizeSlice

@[simp]

theorem ScalarArray.USizeArray.Slice.toUSizeArray_iter (s : USizeArray.Slice) : (Std.Slice.iter s).toUSizeArray = s.copy

@[simp]

theorem ScalarArray.USizeArray.toUSizeArray_iter (a : USizeArray) : a.iter.toUSizeArray = a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ScalarArray.USizeArray.Slice.any_eq_any_copy (s : USizeArray.Slice) (p : USize → Bool) : s.any p = s.copy.any p

@[simp]

theorem ScalarArray.USizeArray.Slice.all_eq_all_copy (s : USizeArray.Slice) (p : USize → Bool) : s.all p = s.copy.all p

@[simp]

theorem ScalarArray.USizeArray.Slice.contains_eq_contains_copy (s : USizeArray.Slice) (v : USize) : s.contains v = s.copy.contains v

@[simp]

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

@[simp]

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

@[simp]

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

Membership in slices

@[simp]

theorem ScalarArray.USizeArray.Slice.mem_iff_mem_copy {x : USize} {s : USizeArray.Slice} : x ∈ s ↔ x ∈ s.copy

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

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

Slice equality

@[simp]

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