# Documentation

Mathlib.Data.Vector.MapLemmas

This file establishes a set of normalization lemmas for map/mapAccumr operations on vectors

## Fold nested mapAccumrs into one #

@[simp]
theorem Vector.mapAccumr_mapAccumr {α : Type u_3} {n : } {β : Type u_2} {σ₁ : Type} {γ : Type u_1} {σ₂ : Type} (xs : Vector α n) (f₁ : βσ₁σ₁ × γ) (f₂ : ασ₂σ₂ × β) {s₂ : σ₂} {s₁ : σ₁} :
Vector.mapAccumr f₁ (Vector.mapAccumr f₂ xs s₂).snd s₁ = let m := Vector.mapAccumr (fun x s => let r₂ := f₂ x s.snd; let r₁ := f₁ r₂.snd s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.mapAccumr_map {α : Type u_3} {n : } {β : Type u_2} {σ₁ : Type} {γ : Type u_1} (xs : Vector α n) (f₁ : βσ₁σ₁ × γ) {s : σ₁} (f₂ : αβ) :
Vector.mapAccumr f₁ (Vector.map f₂ xs) s = Vector.mapAccumr (fun x s => f₁ (f₂ x) s) xs s
@[simp]
theorem Vector.map_mapAccumr {α : Type u_3} {n : } {β : Type u_2} {γ : Type u_1} {σ₂ : Type} (xs : Vector α n) (f₂ : ασ₂σ₂ × β) {s : σ₂} (f₁ : βγ) :
Vector.map f₁ (Vector.mapAccumr f₂ xs s).snd = (Vector.mapAccumr (fun x s => let r := f₂ x s; (r.fst, f₁ r.snd)) xs s).snd
@[simp]
theorem Vector.map_map {α : Type u_3} {n : } {β : Type u_2} {γ : Type u_1} (xs : Vector α n) (f₁ : βγ) (f₂ : αβ) :
Vector.map f₁ (Vector.map f₂ xs) = Vector.map (fun x => f₁ (f₂ x)) xs
@[simp]
theorem Vector.mapAccumr₂_mapAccumr_left {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {ζ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : γβσ₁σ₁ × ζ) (f₂ : ασ₂σ₂ × γ) :
Vector.mapAccumr₂ f₁ (Vector.mapAccumr f₂ xs s₂).snd ys s₁ = let m := Vector.mapAccumr₂ (fun x y s => let r₂ := f₂ x s.snd; let r₁ := f₁ r₂.snd y s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.map₂_map_left {α : Type u_4} {n : } {β : Type u_3} (xs : Vector α n) (ys : Vector β n) {γ : Type u_1} {ζ : Type u_2} (f₁ : γβζ) (f₂ : αγ) :
Vector.map₂ f₁ (Vector.map f₂ xs) ys = Vector.map₂ (fun x y => f₁ (f₂ x) y) xs ys
@[simp]
theorem Vector.mapAccumr₂_mapAccumr_right {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {ζ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : αγσ₁σ₁ × ζ) (f₂ : βσ₂σ₂ × γ) :
Vector.mapAccumr₂ f₁ xs (Vector.mapAccumr f₂ ys s₂).snd s₁ = let m := Vector.mapAccumr₂ (fun x y s => let r₂ := f₂ y s.snd; let r₁ := f₁ x r₂.snd s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.map₂_map_right {α : Type u_3} {n : } {β : Type u_4} (xs : Vector α n) (ys : Vector β n) {γ : Type u_1} {ζ : Type u_2} (f₁ : αγζ) (f₂ : βγ) :
Vector.map₂ f₁ xs (Vector.map f₂ ys) = Vector.map₂ (fun x y => f₁ x (f₂ y)) xs ys
@[simp]
theorem Vector.mapAccumr_mapAccumr₂ {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {ζ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : γσ₁σ₁ × ζ) (f₂ : αβσ₂σ₂ × γ) :
Vector.mapAccumr f₁ (Vector.mapAccumr₂ f₂ xs ys s₂).snd s₁ = let m := Vector.mapAccumr₂ (fun x y s => let r₂ := f₂ x y s.snd; let r₁ := f₁ r₂.snd s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.map_map₂ {α : Type u_3} {n : } {β : Type u_4} (xs : Vector α n) (ys : Vector β n) {γ : Type u_1} {ζ : Type u_2} (f₁ : γζ) (f₂ : αβγ) :
Vector.map f₁ (Vector.map₂ f₂ xs ys) = Vector.map₂ (fun x y => f₁ (f₂ x y)) xs ys
@[simp]
theorem Vector.mapAccumr₂_mapAccumr₂_left_left {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {φ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : γασ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Vector.mapAccumr₂ f₁ (Vector.mapAccumr₂ f₂ xs ys s₂).snd xs s₁ = let m := Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ r₂.snd x s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.mapAccumr₂_mapAccumr₂_left_right {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {φ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : γβσ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Vector.mapAccumr₂ f₁ (Vector.mapAccumr₂ f₂ xs ys s₂).snd ys s₁ = let m := Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ r₂.snd y s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.mapAccumr₂_mapAccumr₂_right_left {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {φ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : αγσ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Vector.mapAccumr₂ f₁ xs (Vector.mapAccumr₂ f₂ xs ys s₂).snd s₁ = let m := Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ x r₂.snd s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)
@[simp]
theorem Vector.mapAccumr₂_mapAccumr₂_right_right {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {γ : Type} {σ₁ : Type} {φ : Type} {σ₂ : Type} {s₂ : σ₂} {s₁ : σ₁} (f₁ : βγσ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Vector.mapAccumr₂ f₁ ys (Vector.mapAccumr₂ f₂ xs ys s₂).snd s₁ = let m := Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ y r₂.snd s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

## Bisimulations #

We can prove two applications of mapAccumr equal by providing a bisimulation relation that relates the initial states.

That is, by providing a relation R : σ₁ → σ₁ → Prop such that R s₁ s₂ implies that R also relates any pair of states reachable by applying f₁ to s₁ and f₂ to s₂, with any possible input values.

theorem Vector.mapAccumr_bisim {α : Type u_2} {n : } {xs : Vector α n} {σ₁ : Type} {β : Type u_1} {σ₂ : Type} {f₁ : ασ₁σ₁ × β} {f₂ : ασ₂σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁σ₂Prop) (h₀ : R s₁ s₂) (hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s qR (f₁ a s).fst (f₂ a q).fst (f₁ a s).snd = (f₂ a q).snd) :
R (Vector.mapAccumr f₁ xs s₁).fst (Vector.mapAccumr f₂ xs s₂).fst (Vector.mapAccumr f₁ xs s₁).snd = (Vector.mapAccumr f₂ xs s₂).snd
theorem Vector.mapAccumr_bisim_tail {α : Type u_2} {n : } {xs : Vector α n} {σ₁ : Type} {β : Type u_1} {σ₂ : Type} {f₁ : ασ₁σ₁ × β} {f₂ : ασ₂σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (h : R, R s₁ s₂ ∀ {s : σ₁} {q : σ₂} (a : α), R s qR (f₁ a s).fst (f₂ a q).fst (f₁ a s).snd = (f₂ a q).snd) :
(Vector.mapAccumr f₁ xs s₁).snd = (Vector.mapAccumr f₂ xs s₂).snd
theorem Vector.mapAccumr₂_bisim {α : Type} {n : } {xs : Vector α n} {β : Type} {σ₁ : Type} {γ : Type} {σ₂ : Type} {ys : Vector β n} {f₁ : αβσ₁σ₁ × γ} {f₂ : αβσ₂σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁σ₂Prop) (h₀ : R s₁ s₂) (hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s qR (f₁ a b s).fst (f₂ a b q).fst (f₁ a b s).snd = (f₂ a b q).snd) :
R (Vector.mapAccumr₂ f₁ xs ys s₁).fst (Vector.mapAccumr₂ f₂ xs ys s₂).fst (Vector.mapAccumr₂ f₁ xs ys s₁).snd = (Vector.mapAccumr₂ f₂ xs ys s₂).snd
theorem Vector.mapAccumr₂_bisim_tail {α : Type} {n : } {xs : Vector α n} {β : Type} {σ₁ : Type} {γ : Type} {σ₂ : Type} {ys : Vector β n} {f₁ : αβσ₁σ₁ × γ} {f₂ : αβσ₂σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂} (h : R, R s₁ s₂ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s qR (f₁ a b s).fst (f₂ a b q).fst (f₁ a b s).snd = (f₂ a b q).snd) :
(Vector.mapAccumr₂ f₁ xs ys s₁).snd = (Vector.mapAccumr₂ f₂ xs ys s₂).snd

## Redundant state optimization #

The following section are collection of rewrites to simplify, or even get rid, redundant accumulation state

theorem Vector.map_eq_mapAccumr {α : Type u_2} {n : } {xs : Vector α n} :
∀ {α : Type u_1} {f : αα}, Vector.map f xs = (Vector.mapAccumr (fun x x_1 => ((), f x)) xs ()).snd
theorem Vector.mapAccumr_eq_map {α : Type u_2} {n : } {β : Type u_1} {xs : Vector α n} {σ : Type} {f : ασσ × β} {s₀ : σ} (S : Set σ) (h₀ : s₀ S) (closure : ∀ (a : α) (s : σ), s S(f a s).fst S) (out : ∀ (a : α) (s s' : σ), s Ss' S(f a s).snd = (f a s').snd) :
(Vector.mapAccumr f xs s₀).snd = Vector.map (fun x => (f x s₀).snd) xs

If there is a set of states that is closed under f, and such that f produces that same output for all states in this set, then the state is not actually needed. Hence, then we can rewrite mapAccumr into just map

theorem Vector.map₂_eq_mapAccumr₂ {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} :
∀ {α : Type} {f : αβα}, Vector.map₂ f xs ys = (Vector.mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).snd
theorem Vector.mapAccumr₂_eq_map₂ {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} {σ : Type} {γ : Type} {f : αβσσ × γ} {s₀ : σ} (S : Set σ) (h₀ : s₀ S) (closure : ∀ (a : α) (b : β) (s : σ), s S(f a b s).fst S) (out : ∀ (a : α) (b : β) (s s' : σ), s Ss' S(f a b s).snd = (f a b s').snd) :
(Vector.mapAccumr₂ f xs ys s₀).snd = Vector.map₂ (fun x x_1 => (f x x_1 s₀).snd) xs ys

If there is a set of states that is closed under f, and such that f produces that same output for all states in this set, then the state is not actually needed. Hence, then we can rewrite mapAccumr₂ into just map₂

@[simp]
theorem Vector.mapAccumr_eq_map_of_constant_state {α : Type u_2} {n : } {β : Type u_1} {xs : Vector α n} {σ : Type} (f : ασσ × β) (s : σ) (h : ∀ (a : α), (f a s).fst = s) :
Vector.mapAccumr f xs s = (s, Vector.map (fun x => (f x s).snd) xs)

If an accumulation function f, given an initial state s, produces s as its output state for all possible input bits, then the state is redundant and can be optimized out

@[simp]
theorem Vector.mapAccumr₂_eq_map₂_of_constant_state {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} {σ : Type} {γ : Type} (f : αβσσ × γ) (s : σ) (h : ∀ (a : α) (b : β), (f a b s).fst = s) :
Vector.mapAccumr₂ f xs ys s = (s, Vector.map₂ (fun x y => (f x y s).snd) xs ys)

If an accumulation function f, given an initial state s, produces s as its output state for all possible input bits, then the state is redundant and can be optimized out

@[simp]
theorem Vector.mapAccumr_eq_map_of_unused_state {α : Type u_2} {n : } {β : Type u_1} {xs : Vector α n} {σ : Type} (f : ασσ × β) (s : σ) (h : ∀ (a : α) (s s' : σ), (f a s).snd = (f a s').snd) :
(Vector.mapAccumr f xs s).snd = Vector.map (fun x => (f x s).snd) xs

If an accumulation function f, produces the same output bits regardless of accumulation state, then the state is redundant and can be optimized out

@[simp]
theorem Vector.mapAccumr₂_eq_map₂_of_unused_state {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} {σ : Type} {γ : Type} (f : αβσσ × γ) (s : σ) (h : ∀ (a : α) (b : β) (s s' : σ), (f a b s).snd = (f a b s').snd) :
(Vector.mapAccumr₂ f xs ys s).snd = Vector.map₂ (fun x y => (f x y s).snd) xs ys

If an accumulation function f, produces the same output bits regardless of accumulation state, then the state is redundant and can be optimized out

@[simp]
theorem Vector.mapAccumr_redundant_pair {α : Type u_2} {n : } {β : Type u_1} {xs : Vector α n} {σ : Type} {s : σ} (f : ασ × σ(σ × σ) × β) (h : ∀ (x : α) (s : σ), (f x (s, s)).fst.fst = (f x (s, s)).fst.snd) :
(Vector.mapAccumr f xs (s, s)).snd = (Vector.mapAccumr (fun x s => ((f x (s, s)).fst.fst, (f x (s, s)).snd)) xs s).snd

If f takes a pair of states, but always returns the same value for both elements of the pair, then we can simplify to just a single element of state

@[simp]
theorem Vector.mapAccumr₂_redundant_pair {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} {σ : Type} {γ : Type} {s : σ} (f : αβσ × σ(σ × σ) × γ) (h : ∀ (x : α) (y : β) (s : σ), let s' := (f x y (s, s)).fst; s'.fst = s'.snd) :
(Vector.mapAccumr₂ f xs ys (s, s)).snd = (Vector.mapAccumr₂ (fun x y s => ((f x y (s, s)).fst.fst, (f x y (s, s)).snd)) xs ys s).snd

If f takes a pair of states, but always returns the same value for both elements of the pair, then we can simplify to just a single element of state

## Unused input optimizations #

@[simp]
theorem Vector.mapAccumr₂_unused_input_left {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} {σ : Type} {γ : Type} {s : σ} [] (f : αβσσ × γ) (h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s) :
Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr (fun b s => f default b s) ys s

If f returns the same output and next state for every value of it's first argument, then xs : Vector is ignored, and we can rewrite mapAccumr₂ into map

@[simp]
theorem Vector.mapAccumr₂_unused_input_right {α : Type} {n : } {β : Type} {xs : Vector α n} {ys : Vector β n} {σ : Type} {γ : Type} {s : σ} [] (f : αβσσ × γ) (h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s) :
Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr (fun a s => f a default s) xs s

If f returns the same output and next state for every value of it's second argument, then ys : Vector is ignored, and we can rewrite mapAccumr₂ into map

## Commutativity #

theorem Vector.map₂_comm {α : Type u_2} {n : } (xs : Vector α n) (ys : Vector α n) {β : Type u_1} (f : ααβ) (comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) :
Vector.map₂ f xs ys = Vector.map₂ f ys xs
theorem Vector.mapAccumr₂_comm {α : Type} {n : } (xs : Vector α n) (ys : Vector α n) {σ : Type} {γ : Type} {s : σ} (f : αασσ × γ) (comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s) :

## Argument Flipping #

theorem Vector.map₂_flip {α : Type u_2} {n : } {β : Type u_3} (xs : Vector α n) (ys : Vector β n) {γ : Type u_1} (f : αβγ) :
Vector.map₂ f xs ys = Vector.map₂ (flip f) ys xs
theorem Vector.mapAccumr₂_flip {α : Type} {n : } {β : Type} (xs : Vector α n) (ys : Vector β n) {σ : Type} {γ : Type} {s : σ} (f : αβσσ × γ) :