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

Fold nested mapAccumrs into one

@[simp]

theorem List.Vector.mapAccumr_mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (f₁ : β → σ₁ → σ₁ × γ) (f₂ : α → σ₂ → σ₂ × β) : mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ = have m := mapAccumr (fun (x : α) (s : σ₁ × σ₂) => have r₂ := f₂ x s.2; have r₁ := f₁ r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.mapAccumr_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {n : ℕ} (xs : Vector α n) (f₁ : β → σ₁ → σ₁ × γ) {s : σ₁} (f₂ : α → β) : mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun (x : α) (s : σ₁) => f₁ (f₂ x) s) xs s

@[simp]

theorem List.Vector.map_mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₂ : Type u_7} {n : ℕ} (xs : Vector α n) (f₂ : α → σ₂ → σ₂ × β) {s : σ₂} (f₁ : β → γ) : map f₁ (mapAccumr f₂ xs s).2 = (mapAccumr (fun (x : α) (s : σ₂) => have r := f₂ x s; (r.1, f₁ r.2)) xs s).2

@[simp]

theorem List.Vector.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : Vector α n) (f₁ : β → γ) (f₂ : α → β) : map f₁ (map f₂ xs) = map (fun (x : α) => f₁ (f₂ x)) xs

theorem List.Vector.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : Vector α n) {p : α → Prop} (f₁ : β → γ) (f₂ : (a : α) → p a → β) (H : ∀ (x : α), x ∈ xs.toList → p x) : map f₁ (pmap f₂ xs H) = pmap (fun (x : α) (hx : p x) => f₁ (f₂ x hx)) xs H

theorem List.Vector.pmap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : Vector α n) {p : β → Prop} (f₁ : (b : β) → p b → γ) (f₂ : α → β) (H : ∀ (x : β), x ∈ (map f₂ xs).toList → p x) : pmap f₁ (map f₂ xs) H = pmap (fun (x : α) (hx : p (f₂ x)) => f₁ (f₂ x) hx) xs ⋯

@[simp]

theorem List.Vector.mapAccumr₂_mapAccumr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : γ → β → σ₁ → σ₁ × ζ) (f₂ : α → σ₂ → σ₂ × γ) : mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => have r₂ := f₂ x s.2; have r₁ := f₁ r₂.2 y s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.map₂_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : ℕ} (xs : Vector α n) (ys : Vector β n) (f₁ : γ → β → ζ) (f₂ : α → γ) : map₂ f₁ (map f₂ xs) ys = map₂ (fun (x : α) (y : β) => f₁ (f₂ x) y) xs ys

@[simp]

theorem List.Vector.mapAccumr₂_mapAccumr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : α → γ → σ₁ → σ₁ × ζ) (f₂ : β → σ₂ → σ₂ × γ) : mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => have r₂ := f₂ y s.2; have r₁ := f₁ x r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.map₂_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : ℕ} (xs : Vector α n) (ys : Vector β n) (f₁ : α → γ → ζ) (f₂ : β → γ) : map₂ f₁ xs (map f₂ ys) = map₂ (fun (x : α) (y : β) => f₁ x (f₂ y)) xs ys

@[simp]

theorem List.Vector.mapAccumr_mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : γ → σ₁ → σ₁ × ζ) (f₂ : α → β → σ₂ → σ₂ × γ) : mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => have r₂ := f₂ x y s.2; have r₁ := f₁ r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.map_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : ℕ} (xs : Vector α n) (ys : Vector β n) (f₁ : γ → ζ) (f₂ : α → β → γ) : map f₁ (map₂ f₂ xs ys) = map₂ (fun (x : α) (y : β) => f₁ (f₂ x y)) xs ys

@[simp]

theorem List.Vector.mapAccumr₂_mapAccumr₂_left_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : γ → α → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) : mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 xs s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) => match x_1 with | (s₁, s₂) => have r₂ := f₂ x y s₂; have r₁ := f₁ r₂.2 x s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.mapAccumr₂_mapAccumr₂_left_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : γ → β → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) : mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 ys s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) => match x_1 with | (s₁, s₂) => have r₂ := f₂ x y s₂; have r₁ := f₁ r₂.2 y s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.mapAccumr₂_mapAccumr₂_right_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : α → γ → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) : mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).2 s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) => match x_1 with | (s₁, s₂) => have r₂ := f₂ x y s₂; have r₁ := f₁ x r₂.2 s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)

@[simp]

theorem List.Vector.mapAccumr₂_mapAccumr₂_right_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂} (xs : Vector α n) (ys : Vector β n) (f₁ : β → γ → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) : mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).2 s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) => match x_1 with | (s₁, s₂) => have r₂ := f₂ x y s₂; have 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 List.Vector.mapAccumr_bisim {α : Type u_1} {β : Type u_2} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : Vector α n} {f₁ : α → σ₁ → σ₁ × β} {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁ → σ₂ → Prop) (h₀ : R s₁ s₂) (hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) : R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

theorem List.Vector.mapAccumr_bisim_tail {α : Type u_1} {β : Type u_2} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : Vector α n} {f₁ : α → σ₁ → σ₁ × β} {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (h : ∃ (R : σ₁ → σ₂ → Prop), R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) : (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

theorem List.Vector.mapAccumr₂_bisim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : Vector α n} {ys : Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ} {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁ → σ₂ → Prop) (h₀ : R s₁ s₂) (hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) : R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

theorem List.Vector.mapAccumr₂_bisim_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : Vector α n} {ys : Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ} {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂} (h : ∃ (R : σ₁ → σ₂ → Prop), R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) : (mapAccumr₂ f₁ xs ys s₁).2 = (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 List.Vector.map_eq_mapAccumr {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector α n} {f : α → β} : map f xs = (mapAccumr (fun (x : α) (x_1 : Unit) => ((), f x)) xs ()).2

theorem List.Vector.mapAccumr_eq_map {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {xs : Vector α n} {f : α → σ → σ × β} {s₀ : σ} (S : Set σ) (h₀ : s₀ ∈ S) (closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S) (out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2) : (mapAccumr f xs s₀).2 = 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 List.Vector.map₂_eq_mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {xs : Vector α n} {ys : Vector β n} {f : α → β → γ} : map₂ f xs ys = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) => ((), f x y)) xs ys ()).2

theorem List.Vector.mapAccumr₂_eq_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {xs : Vector α n} {ys : Vector β n} {f : α → β → σ → σ × γ} {s₀ : σ} (S : Set σ) (h₀ : s₀ ∈ S) (closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S) (out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2) : (mapAccumr₂ f xs ys s₀).2 = map₂ (fun (x1 : α) (x2 : β) => (f x1 x2 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 List.Vector.mapAccumr_eq_map_of_constant_state {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {xs : Vector α n} (f : α → σ → σ × β) (s : σ) (h : ∀ (a : α), (f a s).1 = s) : mapAccumr f xs s = (s, 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 List.Vector.mapAccumr₂_eq_map₂_of_constant_state {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {xs : Vector α n} {ys : Vector β n} (f : α → β → σ → σ × γ) (s : σ) (h : ∀ (a : α) (b : β), (f a b s).1 = s) : mapAccumr₂ f xs ys s = (s, 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 List.Vector.mapAccumr_eq_map_of_unused_state {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {xs : Vector α n} (f : α → σ → σ × β) (f' : α → β) (s : σ) (h : ∀ (a : α) (s : σ), (f a s).2 = f' a) : (mapAccumr f xs s).2 = map f' 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 List.Vector.mapAccumr₂_eq_map₂_of_unused_state {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {xs : Vector α n} {ys : Vector β n} (f : α → β → σ → σ × γ) (f' : α → β → γ) (s : σ) (h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b) : (mapAccumr₂ f xs ys s).2 = 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 List.Vector.mapAccumr_redundant_pair {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {s : σ} {xs : Vector α n} (f : α → σ × σ → (σ × σ) × β) (h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2) : (mapAccumr f xs (s, s)).2 = (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 List.Vector.mapAccumr₂_redundant_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} {xs : Vector α n} {ys : Vector β n} (f : α → β → σ × σ → (σ × σ) × γ) (h : ∀ (x : α) (y : β) (s : σ), have s' := (f x y (s, s)).1; s'.1 = s'.2) : (mapAccumr₂ f xs ys (s, s)).2 = (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 List.Vector.mapAccumr₂_unused_input_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} {xs : Vector α n} {ys : Vector β n} (f : α → β → σ → σ × γ) (f' : β → σ → σ × γ) (h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s) : mapAccumr₂ f xs ys s = mapAccumr f' 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 List.Vector.mapAccumr₂_unused_input_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} {xs : Vector α n} {ys : Vector β n} (f : α → β → σ → σ × γ) (f' : α → σ → σ × γ) (h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s) : mapAccumr₂ f xs ys s = mapAccumr f' 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 List.Vector.map₂_comm {α : Type u_1} {β : Type u_2} {n : ℕ} (xs ys : Vector α n) (f : α → α → β) (comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) : map₂ f xs ys = map₂ f ys xs

theorem List.Vector.mapAccumr₂_comm {α : Type u_1} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} (xs ys : Vector α n) (f : α → α → σ → σ × γ) (comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s) : mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s

Argument Flipping

theorem List.Vector.map₂_flip {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : Vector α n) (ys : Vector β n) (f : α → β → γ) : map₂ f xs ys = map₂ (flip f) ys xs

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