# 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₂).2 s₁ = let m := Vector.mapAccumr (fun (x : α) (s : σ₁ × σ₂) => let r₂ := f₂ x s.2; let r₁ := f₁ r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs (s₁, s₂); (m.1.1, m.2)
@[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).2 = (Vector.mapAccumr (fun (x : α) (s : σ₂) => let r := f₂ x s; (r.1, f₁ r.2)) xs s).2
@[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₂).2 ys s₁ = let m := Vector.mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => let r₂ := f₂ x s.2; let r₁ := f₁ r₂.2 y s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
@[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₂).2 s₁ = let m := Vector.mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => let r₂ := f₂ y s.2; let r₁ := f₁ x r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
@[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₂).2 s₁ = let m := Vector.mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => let r₂ := f₂ x y s.2; let r₁ := f₁ r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
@[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₂).2 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₂.2 x s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
@[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₂).2 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₂.2 y s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
@[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₂).2 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₂.2 s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
@[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₂).2 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₂.2 s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

## 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).1 (f₂ a q).1 (f₁ a s).2 = (f₂ a q).2) :
R (Vector.mapAccumr f₁ xs s₁).1 (Vector.mapAccumr f₂ xs s₂).1 (Vector.mapAccumr f₁ xs s₁).2 = (Vector.mapAccumr f₂ xs s₂).2
theorem Vector.mapAccumr_bisim_tail {α : Type u_2} {n : } {xs : Vector α n} {σ₁ : Type} {β : Type u_1} {σ₂ : Type} {f₁ : ασ₁σ₁ × β} {f₂ : ασ₂σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (h : ∃ (R : σ₁σ₂Prop), R s₁ s₂ ∀ {s : σ₁} {q : σ₂} (a : α), R s qR (f₁ a s).1 (f₂ a q).1 (f₁ a s).2 = (f₂ a q).2) :
(Vector.mapAccumr f₁ xs s₁).2 = (Vector.mapAccumr f₂ xs s₂).2
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).1 (f₂ a b q).1 (f₁ a b s).2 = (f₂ a b q).2) :
R (Vector.mapAccumr₂ f₁ xs ys s₁).1 (Vector.mapAccumr₂ f₂ xs ys s₂).1 (Vector.mapAccumr₂ f₁ xs ys s₁).2 = (Vector.mapAccumr₂ f₂ xs ys s₂).2
theorem Vector.mapAccumr₂_bisim_tail {α : Type} {n : } {xs : Vector α n} {β : Type} {σ₁ : Type} {γ : Type} {σ₂ : Type} {ys : Vector β n} {f₁ : αβσ₁σ₁ × γ} {f₂ : αβσ₂σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂} (h : ∃ (R : σ₁σ₂Prop), R s₁ s₂ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s qR (f₁ a b s).1 (f₂ a b q).1 (f₁ a b s).2 = (f₂ a b q).2) :
(Vector.mapAccumr₂ f₁ xs ys s₁).2 = (Vector.mapAccumr₂ f₂ xs ys s₂).2

## 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} :
∀ {α_1 : Type u_1} {f : αα_1}, Vector.map f xs = (Vector.mapAccumr (fun (x : α) (x_1 : Unit) => ((), f x)) xs ()).2
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 : α), sS, (f a s).1 S) (out : ∀ (a : α) (s s' : σ), s Ss' S(f a s).2 = (f a s').2) :
(Vector.mapAccumr f xs s₀).2 = Vector.map (fun (x : α) => (f x s₀).2) 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} :
∀ {α_1 : Type} {f : αβα_1}, Vector.map₂ f xs ys = (Vector.mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) => ((), f x y)) xs ys ()).2
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 : β), sS, (f a b s).1 S) (out : ∀ (a : α) (b : β) (s s' : σ), s Ss' S(f a b s).2 = (f a b s').2) :
(Vector.mapAccumr₂ f xs ys s₀).2 = Vector.map₂ (fun (x : α) (x_1 : β) => (f x x_1 s₀).2) 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).1 = s) :
Vector.mapAccumr f xs s = (s, Vector.map (fun (x : α) => (f x s).2) 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).1 = s) :
Vector.mapAccumr₂ f xs ys s = (s, Vector.map₂ (fun (x : α) (y : β) => (f x y s).2) 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).2 = (f a s').2) :
(Vector.mapAccumr f xs s).2 = Vector.map (fun (x : α) => (f x s).2) 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).2 = (f a b s').2) :
(Vector.mapAccumr₂ f xs ys s).2 = Vector.map₂ (fun (x : α) (y : β) => (f x y s).2) 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)).1.1 = (f x (s, s)).1.2) :
(Vector.mapAccumr f xs (s, s)).2 = (Vector.mapAccumr (fun (x : α) (s : σ) => ((f x (s, s)).1.1, (f x (s, s)).2)) xs s).2

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)).1; s'.1 = s'.2) :
(Vector.mapAccumr₂ f xs ys (s, s)).2 = (Vector.mapAccumr₂ (fun (x : α) (y : β) (s : σ) => ((f x y (s, s)).1.1, (f x y (s, s)).2)) xs ys s).2

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 : αβσσ × γ) :