In-place writes on Int64Array

Writes through slices, and folds that write each element back in place.

Writes through slices

@[inline]

def ScalarArray.Int64Array.Slice.set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s := by get_elem_tactic) : Int64Array.Slice

Replaces the element at index i of the slice, counted from the start of the slice, in the underlying array. The array is updated in place when neither it nor the slice is shared, so a slice taken from an array that is no longer used writes into that array. s.array gives back the whole array afterwards.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ScalarArray.Int64Array.Slice.array_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) : (s.set i v h).array = s.array.set (s.start + i) v ⋯

@[simp]

theorem ScalarArray.Int64Array.Slice.start_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) : (s.set i v h).start = s.start

@[simp]

theorem ScalarArray.Int64Array.Slice.stop_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) : (s.set i v h).stop = s.stop

@[simp]

theorem ScalarArray.Int64Array.Slice.size_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) : Std.Slice.size (s.set i v h) = Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.Slice.getElem_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) (j : Nat) (hj : j < Std.Slice.size (s.set i v h)) : (s.set i v h)[j] = if i = j then v else s[j]

@[simp]

theorem ScalarArray.Int64Array.Slice.copy_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) : (s.set i v h).copy = s.copy.set i v ⋯

@[inline]

def ScalarArray.Int64Array.Slice.set! (s : Int64Array.Slice) (i : Nat) (v : Int64) : Int64Array.Slice

Replaces the element at index i of the slice in the underlying array, like set. If i is out of bounds, the slice is returned unmodified.

Equations

• s.set! i v = if h : i < Std.Slice.size s then s.set i v h else s

theorem ScalarArray.Int64Array.Slice.set!_eq (s : Int64Array.Slice) (i : Nat) (v : Int64) : s.set! i v = if h : i < Std.Slice.size s then s.set i v h else s

@[simp]

theorem ScalarArray.Int64Array.Slice.set!_eq_set (s : Int64Array.Slice) (i : Nat) (v : Int64) (h : i < Std.Slice.size s) : s.set! i v = s.set i v h

@[inline]

def ScalarArray.Int64Array.Slice.modify (s : Int64Array.Slice) (i : Nat) (f : Int64 → Int64) : Int64Array.Slice

Applies f to the element at index i of the slice, in place like set. If i is out of bounds, the slice is returned unmodified.

Equations

• s.modify i f = if h : i < Std.Slice.size s then s.set i (f s[i]) h else s

theorem ScalarArray.Int64Array.Slice.modify_eq (s : Int64Array.Slice) (i : Nat) (f : Int64 → Int64) : s.modify i f = if h : i < Std.Slice.size s then s.set i (f s[i]) h else s

@[simp]

theorem ScalarArray.Int64Array.Slice.start_modify (s : Int64Array.Slice) (i : Nat) (f : Int64 → Int64) : (s.modify i f).start = s.start

@[simp]

theorem ScalarArray.Int64Array.Slice.stop_modify (s : Int64Array.Slice) (i : Nat) (f : Int64 → Int64) : (s.modify i f).stop = s.stop

@[simp]

theorem ScalarArray.Int64Array.Slice.size_modify (s : Int64Array.Slice) (i : Nat) (f : Int64 → Int64) : Std.Slice.size (s.modify i f) = Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.Slice.getElem_modify (s : Int64Array.Slice) (i : Nat) (f : Int64 → Int64) (j : Nat) (hj : j < Std.Slice.size (s.modify i f)) : (s.modify i f)[j] = have hj' := ⋯; if i = j then f s[j] else s[j]

@[inline]

def ScalarArray.Int64Array.Slice.swap (s : Int64Array.Slice) (i j : Nat) (hi : i < Std.Slice.size s := by get_elem_tactic) (hj : j < Std.Slice.size s := by get_elem_tactic) : Int64Array.Slice

Swaps the elements at indices i and j of the slice, in place like set.

Equations

• s.swap i j hi hj = (s.set i s[j] hi).set j s[i] ⋯

theorem ScalarArray.Int64Array.Slice.swap_eq (s : Int64Array.Slice) (i j : Nat) (hi : i < Std.Slice.size s) (hj : j < Std.Slice.size s) : s.swap i j hi hj = (s.set i s[j] hi).set j s[i] ⋯

@[simp]

theorem ScalarArray.Int64Array.Slice.start_swap (s : Int64Array.Slice) (i j : Nat) (hi : i < Std.Slice.size s) (hj : j < Std.Slice.size s) : (s.swap i j hi hj).start = s.start

@[simp]

theorem ScalarArray.Int64Array.Slice.stop_swap (s : Int64Array.Slice) (i j : Nat) (hi : i < Std.Slice.size s) (hj : j < Std.Slice.size s) : (s.swap i j hi hj).stop = s.stop

@[simp]

theorem ScalarArray.Int64Array.Slice.size_swap (s : Int64Array.Slice) (i j : Nat) (hi : i < Std.Slice.size s) (hj : j < Std.Slice.size s) : Std.Slice.size (s.swap i j hi hj) = Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.Slice.getElem_swap (s : Int64Array.Slice) (i j : Nat) (hi : i < Std.Slice.size s) (hj : j < Std.Slice.size s) (k : Nat) (hk : k < Std.Slice.size (s.swap i j hi hj)) : (s.swap i j hi hj)[k] = if j = k then s[i] else if i = k then s[j] else s[k]

@[irreducible]

def ScalarArray.Int64Array.Slice.reverse.loop (s : Int64Array.Slice) (i j : Nat) (hj : j < Std.Slice.size s) : Int64Array.Slice

The loop of reverse: swaps the elements at i and j, then moves both towards the middle.

Equations

• ScalarArray.Int64Array.Slice.reverse.loop s i j hj = if h : i < j then ScalarArray.Int64Array.Slice.reverse.loop (s.swap i j ⋯ hj) (i + 1) (j - 1) ⋯ else s

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.Slice.reverseImpl]

def ScalarArray.Int64Array.Slice.reverse (s : Int64Array.Slice) : Int64Array.Slice

Reverses the order of the elements of the slice, in place like set. The array is made exclusive once, before the loop, which then stores without checks.

Equations

• s.reverse = if h : 0 < Std.Slice.size s then ScalarArray.Int64Array.Slice.reverse.loop s 0 (Std.Slice.size s - 1) ⋯ else s

@[simp]

theorem ScalarArray.Int64Array.Slice.start_reverse (s : Int64Array.Slice) : s.reverse.start = s.start

@[simp]

theorem ScalarArray.Int64Array.Slice.stop_reverse (s : Int64Array.Slice) : s.reverse.stop = s.stop

@[simp]

theorem ScalarArray.Int64Array.Slice.size_reverse (s : Int64Array.Slice) : Std.Slice.size s.reverse = Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.Slice.getElem_reverse (s : Int64Array.Slice) (i : Nat) (h : i < Std.Slice.size s.reverse) : s.reverse[i] = s[Std.Slice.size s - 1 - i]

@[simp]

theorem ScalarArray.Int64Array.Slice.toList_copy_reverse (s : Int64Array.Slice) : s.reverse.copy.toList = s.copy.toList.reverse

In-place folds over slices

@[irreducible]

def ScalarArray.Int64Array.Slice.foldlInPlace.loop {β : Type v} (n : Nat) (f : (k : USize) → k.toNat < n → Int64 → β → Int64 × β) (s : Int64Array.Slice) (hs : Std.Slice.size s = n) (k : Nat) (b : β) : Int64Array.Slice × β

The loop of foldlInPlace, over Nat indices.

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.Slice.foldlInPlaceImpl]

def ScalarArray.Int64Array.Slice.foldlInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : Int64Array.Slice × β

Replaces each element of the slice while threading an accumulator, in place like set: for each k < s.size, from 0 up, the element x at index k of the slice becomes the first component of f k hk x b, whose second component is the next accumulator. Returns the new slice and the last accumulator.

The array is made exclusive once, before the loop, which then stores without checks, where each set checks at every write. f only sees the elements, never the array, which is what makes skipping the checks safe. The proof hk : k.toNat < s.size lets f read other arrays with uget.

Equations

• s.foldlInPlace init f = ScalarArray.Int64Array.Slice.foldlInPlace.loop (Std.Slice.size s) f s ⋯ 0 init

@[simp]

theorem ScalarArray.Int64Array.Slice.start_foldlInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : (s.foldlInPlace init f).fst.start = s.start

@[simp]

theorem ScalarArray.Int64Array.Slice.stop_foldlInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : (s.foldlInPlace init f).fst.stop = s.stop

@[simp]

theorem ScalarArray.Int64Array.Slice.size_foldlInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : Std.Slice.size (s.foldlInPlace init f).fst = Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.Slice.size_array_foldlInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : (s.foldlInPlace init f).fst.array.size = s.array.size

theorem ScalarArray.Int64Array.Slice.getElem?_array_foldlInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) (i : Nat) (hi : i < s.start ∨ s.stop ≤ i) : (s.foldlInPlace init f).fst.array[i]? = s.array[i]?

foldlInPlace leaves the elements of the array outside the slice unchanged.

theorem ScalarArray.Int64Array.Slice.foldlInPlace_eq_foldl_finRange {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : ((s.foldlInPlace init f).fst.copy.toList, (s.foldlInPlace init f).snd) = List.foldl (fun (acc : List Int64 × β) (i : Fin (Std.Slice.size s)) => have p := f (↑i).toUSize ⋯ s[i] acc.snd; (acc.fst ++ [p.fst], p.snd)) ([], init) (List.finRange (Std.Slice.size s))

foldlInPlace as a pure left fold over the indices of the slice: the new elements of the slice and the last accumulator, in one statement. The Then form follows by foldlInPlaceThen_eq.

def ScalarArray.Int64Array.Slice.foldrInPlace.loop {β : Type v} (n : Nat) (f : (k : USize) → k.toNat < n → Int64 → β → Int64 × β) (s : Int64Array.Slice) (hs : Std.Slice.size s = n) (k : Nat) : k ≤ n → β → Int64Array.Slice × β

The loop of foldrInPlace, over Nat indices, from k - 1 down to 0.

Equations

• ScalarArray.Int64Array.Slice.foldrInPlace.loop n f s hs 0 x_3 x = (s, x)
• ScalarArray.Int64Array.Slice.foldrInPlace.loop n f s hs k.succ hk x = ScalarArray.Int64Array.Slice.foldrInPlace.loop n f (s.set k (f k.toUSize ⋯ s[k] x).fst ⋯) ⋯ k ⋯ (f k.toUSize ⋯ s[k] x).snd

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.Slice.foldrInPlaceImpl]

def ScalarArray.Int64Array.Slice.foldrInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : Int64Array.Slice × β

Replaces each element of the slice while threading an accumulator, like foldlInPlace but from the last element to the first: for each k < s.size, from s.size - 1 down to 0, the element x at index k of the slice becomes the first component of f k hk x b, whose second component is the next accumulator. Returns the new slice and the last accumulator.

The array is made exclusive once, before the loop, which then stores without checks.

Equations

• s.foldrInPlace init f = ScalarArray.Int64Array.Slice.foldrInPlace.loop (Std.Slice.size s) f s ⋯ (Std.Slice.size s) ⋯ init

@[simp]

theorem ScalarArray.Int64Array.Slice.start_foldrInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : (s.foldrInPlace init f).fst.start = s.start

@[simp]

theorem ScalarArray.Int64Array.Slice.stop_foldrInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : (s.foldrInPlace init f).fst.stop = s.stop

@[simp]

theorem ScalarArray.Int64Array.Slice.size_foldrInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : Std.Slice.size (s.foldrInPlace init f).fst = Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.Slice.size_array_foldrInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : (s.foldrInPlace init f).fst.array.size = s.array.size

theorem ScalarArray.Int64Array.Slice.getElem?_array_foldrInPlace {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) (i : Nat) (hi : i < s.start ∨ s.stop ≤ i) : (s.foldrInPlace init f).fst.array[i]? = s.array[i]?

foldrInPlace leaves the elements of the array outside the slice unchanged.

theorem ScalarArray.Int64Array.Slice.foldrInPlace_eq_foldr_finRange {β : Type v} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) : ((s.foldrInPlace init f).fst.copy.toList, (s.foldrInPlace init f).snd) = List.foldr (fun (i : Fin (Std.Slice.size s)) (acc : List Int64 × β) => have p := f (↑i).toUSize ⋯ s[i] acc.snd; (p.fst :: acc.fst, p.snd)) ([], init) (List.finRange (Std.Slice.size s))

foldrInPlace as a pure right fold over the indices of the slice: the new elements of the slice and the last accumulator, in one statement. The Then form follows by foldrInPlaceThen_eq.

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.Slice.foldlInPlaceThenImpl]

def ScalarArray.Int64Array.Slice.foldlInPlaceThen {β : Type v} {γ : Type w} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) (g : Int64Array.Slice → β → γ) : γ

foldlInPlace followed by g on the new slice and the last accumulator, which the loop calls itself where foldlInPlace returns them as a pair. The pair is a heap object, allocated once per call, which shows when the fold runs over short slices many times; when g consumes the accumulator, for example by writing it into the slice, no pair is allocated at all. foldlInPlace is the case g := Prod.mk.

Equations

• s.foldlInPlaceThen init f g = g (s.foldlInPlace init f).fst (s.foldlInPlace init f).snd

@[simp]

theorem ScalarArray.Int64Array.Slice.foldlInPlaceThen_eq {β : Type v} {γ : Type w} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) (g : Int64Array.Slice → β → γ) : s.foldlInPlaceThen init f g = g (s.foldlInPlace init f).fst (s.foldlInPlace init f).snd

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.Slice.foldrInPlaceThenImpl]

def ScalarArray.Int64Array.Slice.foldrInPlaceThen {β : Type v} {γ : Type w} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) (g : Int64Array.Slice → β → γ) : γ

foldrInPlace followed by g on the new slice and the last accumulator, which the loop calls itself where foldrInPlace returns them as a pair. When g consumes the accumulator, no pair is allocated. foldrInPlace is the case g := Prod.mk.

Equations

• s.foldrInPlaceThen init f g = g (s.foldrInPlace init f).fst (s.foldrInPlace init f).snd

@[simp]

theorem ScalarArray.Int64Array.Slice.foldrInPlaceThen_eq {β : Type v} {γ : Type w} (s : Int64Array.Slice) (init : β) (f : (k : USize) → k.toNat < Std.Slice.size s → Int64 → β → Int64 × β) (g : Int64Array.Slice → β → γ) : s.foldrInPlaceThen init f g = g (s.foldrInPlace init f).fst (s.foldrInPlace init f).snd

Folding over windows of one array

@[irreducible]

def ScalarArray.Int64Array.foldlInPlace2.loop {β : Type v} (xs ys rs len : Nat) (f : (j : USize) → j.toNat < len → Int64 → Int64 → β → Int64 × β) (a : Int64Array) (hx : xs + len ≤ a.size) (hy : ys + len ≤ a.size) (hr : rs + len ≤ a.size) (j : Nat) (b : β) : Int64Array × β

The loop of foldlInPlace2, over Nat offsets and indices.

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldlInPlace2Impl]

def ScalarArray.Int64Array.foldlInPlace2 {β : Type v} (a : Int64Array) (xs ys rs len : USize) (hx : xs.toNat + len.toNat ≤ a.size) (hy : ys.toNat + len.toNat ≤ a.size) (hr : rs.toNat + len.toNat ≤ a.size) (init : β) (f : (j : USize) → j.toNat < len.toNat → Int64 → Int64 → β → Int64 × β) : Int64Array × β

Writes the window of len elements at rs from the windows at xs and ys of the same array, in place, threading an accumulator: for each j < len, from 0 up, it reads x := a[xs + j] and y := a[ys + j] from the current array, then stores the first component of f j hj x y b at rs + j, and the second component is the next accumulator. Returns the new array and the last accumulator.

Each step reads after the writes of the earlier steps, so overlapping windows are well defined: with rs = xs + 1, for example, step j reads what step j - 1 wrote. Reading the windows through f rather than through another reference to a keeps a exclusive, which a second reference would not, and then the first write would copy the whole array.

The array is made exclusive once, before the loop, which then reads and stores without checks.

Equations

• a.foldlInPlace2 xs ys rs len hx hy hr init f = ScalarArray.Int64Array.foldlInPlace2.loop xs.toNat ys.toNat rs.toNat len.toNat f a hx hy hr 0 init

@[simp]

theorem ScalarArray.Int64Array.size_foldlInPlace2 {β : Type v} (a : Int64Array) (xs ys rs len : USize) (hx : xs.toNat + len.toNat ≤ a.size) (hy : ys.toNat + len.toNat ≤ a.size) (hr : rs.toNat + len.toNat ≤ a.size) (init : β) (f : (j : USize) → j.toNat < len.toNat → Int64 → Int64 → β → Int64 × β) : (a.foldlInPlace2 xs ys rs len hx hy hr init f).fst.size = a.size

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldlInPlace2ThenImpl]

def ScalarArray.Int64Array.foldlInPlace2Then {β : Type v} {γ : Type w} (a : Int64Array) (xs ys rs len : USize) (hx : xs.toNat + len.toNat ≤ a.size) (hy : ys.toNat + len.toNat ≤ a.size) (hr : rs.toNat + len.toNat ≤ a.size) (init : β) (f : (j : USize) → j.toNat < len.toNat → Int64 → Int64 → β → Int64 × β) (g : (a' : Int64Array) → a'.size = a.size → β → γ) : γ

foldlInPlace2 followed by g on the new array and the last accumulator, which the loop calls itself where foldlInPlace2 returns them as a pair. When g consumes the accumulator, no pair is allocated. g also receives a proof that the size is unchanged, so that it can go on with bounded reads and writes, such as another foldlInPlace2Then.

Equations

• a.foldlInPlace2Then xs ys rs len hx hy hr init f g = g (a.foldlInPlace2 xs ys rs len hx hy hr init f).fst ⋯ (a.foldlInPlace2 xs ys rs len hx hy hr init f).snd

@[simp]

theorem ScalarArray.Int64Array.foldlInPlace2Then_eq {β : Type v} {γ : Type w} (a : Int64Array) (xs ys rs len : USize) (hx : xs.toNat + len.toNat ≤ a.size) (hy : ys.toNat + len.toNat ≤ a.size) (hr : rs.toNat + len.toNat ≤ a.size) (init : β) (f : (j : USize) → j.toNat < len.toNat → Int64 → Int64 → β → Int64 × β) (g : (a' : Int64Array) → a'.size = a.size → β → γ) : a.foldlInPlace2Then xs ys rs len hx hy hr init f g = g (a.foldlInPlace2 xs ys rs len hx hy hr init f).fst ⋯ (a.foldlInPlace2 xs ys rs len hx hy hr init f).snd

In-place folds over a USize range

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldlInPlaceRangeImpl]

def ScalarArray.Int64Array.foldlInPlaceRange {β : Type v} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) : Int64Array × β

foldlInPlace on the slice a[start.toNat...start.toNat + len.toNat], for bounds that are already USize: returns the new array and the last accumulator. It is specified as that slice fold, so the slice lemmas apply after foldlInPlaceRange_eq. The implementation runs the loop of foldlInPlace on the USize bounds directly, without building the slice, whose Nat bounds cost a conversion on the way in and out of every call.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ScalarArray.Int64Array.foldlInPlaceRange_eq {β : Type v} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) : a.foldlInPlaceRange start len h init f = (((a.toSlice start.toNat (start.toNat + len.toNat)).foldlInPlace init fun (k : USize) (hk : k.toNat < Std.Slice.size (a.toSlice start.toNat (start.toNat + len.toNat))) => f k ⋯).fst.array, ((a.toSlice start.toNat (start.toNat + len.toNat)).foldlInPlace init fun (k : USize) (hk : k.toNat < Std.Slice.size (a.toSlice start.toNat (start.toNat + len.toNat))) => f k ⋯).snd)

@[simp]

theorem ScalarArray.Int64Array.size_foldlInPlaceRange {β : Type v} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) : (a.foldlInPlaceRange start len h init f).fst.size = a.size

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldlInPlaceRangeThenImpl]

def ScalarArray.Int64Array.foldlInPlaceRangeThen {β : Type v} {γ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) (g : (a' : Int64Array) → a'.size = a.size → β → γ) : γ

foldlInPlaceRange followed by g on the new array and the last accumulator, which the loop calls itself where foldlInPlaceRange returns them as a pair, like Slice.foldlInPlaceThen. g also receives a proof that the size is unchanged, like foldlInPlace2Then, so that it can go on with bounded reads and writes.

Equations

• a.foldlInPlaceRangeThen start len h init f g = g (a.foldlInPlaceRange start len h init f).fst ⋯ (a.foldlInPlaceRange start len h init f).snd

@[simp]

theorem ScalarArray.Int64Array.foldlInPlaceRangeThen_eq {β : Type v} {γ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) (g : (a' : Int64Array) → a'.size = a.size → β → γ) : a.foldlInPlaceRangeThen start len h init f g = g (a.foldlInPlaceRange start len h init f).fst ⋯ (a.foldlInPlaceRange start len h init f).snd

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldlInPlaceRangeWith2AccImpl]

def ScalarArray.Int64Array.foldlInPlaceRangeWith2Acc {β₁ : Type v} {β₂ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init₁ : β₁) (init₂ : β₂) (f : (k : USize) → k.toNat < len.toNat → Int64 → β₁ → β₂ → Int64 × β₁ × β₂) : Int64Array × β₁ × β₂

foldlInPlaceRange with two accumulators: returns the new array and the two last accumulators. It is specified as foldlInPlaceRange on the pair of accumulators, so the lemmas about that fold apply after foldlInPlaceRangeWith2Acc_eq. The implementation passes the two accumulators as separate arguments of the loop, where a pair would be allocated at every element and would box scalar accumulators such as UInt64 carries.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ScalarArray.Int64Array.foldlInPlaceRangeWith2Acc_eq {β₁ : Type v} {β₂ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init₁ : β₁) (init₂ : β₂) (f : (k : USize) → k.toNat < len.toNat → Int64 → β₁ → β₂ → Int64 × β₁ × β₂) : a.foldlInPlaceRangeWith2Acc start len h init₁ init₂ f = a.foldlInPlaceRange start len h (init₁, init₂) fun (k : USize) (hk : k.toNat < len.toNat) (x : Int64) (b : β₁ × β₂) => f k hk x b.fst b.snd

@[simp]

theorem ScalarArray.Int64Array.size_foldlInPlaceRangeWith2Acc {β₁ : Type v} {β₂ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init₁ : β₁) (init₂ : β₂) (f : (k : USize) → k.toNat < len.toNat → Int64 → β₁ → β₂ → Int64 × β₁ × β₂) : (a.foldlInPlaceRangeWith2Acc start len h init₁ init₂ f).fst.size = a.size

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldlInPlaceRangeWith2AccThenImpl]

def ScalarArray.Int64Array.foldlInPlaceRangeWith2AccThen {β₁ : Type v} {β₂ : Type w} {γ : Type u} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init₁ : β₁) (init₂ : β₂) (f : (k : USize) → k.toNat < len.toNat → Int64 → β₁ → β₂ → Int64 × β₁ × β₂) (g : (a' : Int64Array) → a'.size = a.size → β₁ → β₂ → γ) : γ

foldlInPlaceRangeWith2Acc followed by g on the new array, a proof that its size is unchanged and the two last accumulators, like foldlInPlaceRangeThen.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ScalarArray.Int64Array.foldlInPlaceRangeWith2AccThen_eq {β₁ : Type v} {β₂ : Type w} {γ : Type u} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init₁ : β₁) (init₂ : β₂) (f : (k : USize) → k.toNat < len.toNat → Int64 → β₁ → β₂ → Int64 × β₁ × β₂) (g : (a' : Int64Array) → a'.size = a.size → β₁ → β₂ → γ) : a.foldlInPlaceRangeWith2AccThen start len h init₁ init₂ f g = a.foldlInPlaceRangeThen start len h (init₁, init₂) (fun (k : USize) (hk : k.toNat < len.toNat) (x : Int64) (b : β₁ × β₂) => f k hk x b.fst b.snd) fun (a' : Int64Array) (ha : a'.size = a.size) (b : β₁ × β₂) => g a' ha b.fst b.snd

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldrInPlaceRangeImpl]

def ScalarArray.Int64Array.foldrInPlaceRange {β : Type v} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) : Int64Array × β

foldrInPlace on the slice a[start.toNat...start.toNat + len.toNat], for bounds that are already USize, like foldlInPlaceRange: returns the new array and the last accumulator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ScalarArray.Int64Array.foldrInPlaceRange_eq {β : Type v} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) : a.foldrInPlaceRange start len h init f = (((a.toSlice start.toNat (start.toNat + len.toNat)).foldrInPlace init fun (k : USize) (hk : k.toNat < Std.Slice.size (a.toSlice start.toNat (start.toNat + len.toNat))) => f k ⋯).fst.array, ((a.toSlice start.toNat (start.toNat + len.toNat)).foldrInPlace init fun (k : USize) (hk : k.toNat < Std.Slice.size (a.toSlice start.toNat (start.toNat + len.toNat))) => f k ⋯).snd)

@[simp]

theorem ScalarArray.Int64Array.size_foldrInPlaceRange {β : Type v} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) : (a.foldrInPlaceRange start len h init f).fst.size = a.size

@[implemented_by _private.ScalarArray.Int64.InPlace.0.ScalarArray.Int64Array.foldrInPlaceRangeThenImpl]

def ScalarArray.Int64Array.foldrInPlaceRangeThen {β : Type v} {γ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) (g : (a' : Int64Array) → a'.size = a.size → β → γ) : γ

foldrInPlaceRange followed by g on the new array, a proof that its size is unchanged and the last accumulator, like foldlInPlaceRangeThen.

Equations

• a.foldrInPlaceRangeThen start len h init f g = g (a.foldrInPlaceRange start len h init f).fst ⋯ (a.foldrInPlaceRange start len h init f).snd

@[simp]

theorem ScalarArray.Int64Array.foldrInPlaceRangeThen_eq {β : Type v} {γ : Type w} (a : Int64Array) (start len : USize) (h : start.toNat + len.toNat ≤ a.size) (init : β) (f : (k : USize) → k.toNat < len.toNat → Int64 → β → Int64 × β) (g : (a' : Int64Array) → a'.size = a.size → β → γ) : a.foldrInPlaceRangeThen start len h init f g = g (a.foldrInPlaceRange start len h init f).fst ⋯ (a.foldrInPlaceRange start len h init f).snd