Normalization lemmas for map and mapAccumr on vectors

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₂).snd s₁ = have m := mapAccumr (fun (x : α) (s : σ₁ × σ₂) => have r₂ := f₂ x s.snd; have r₁ := f₁ r₂.snd s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs (s₁, s₂); (m.fst.fst, m.snd)

@[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).snd = (mapAccumr (fun (x : α) (s : σ₂) => have r := f₂ x s; (r.fst, f₁ r.snd)) xs s).snd

@[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₂).snd ys s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => have r₂ := f₂ x s.snd; have r₁ := f₁ r₂.snd y s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

@[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₂).snd s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => have r₂ := f₂ y s.snd; have r₁ := f₁ x r₂.snd s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

@[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₂).snd s₁ = have m := mapAccumr₂ (fun (x : α) (y : β) (s : σ₁ × σ₂) => have r₂ := f₂ x y s.snd; have r₁ := f₁ r₂.snd s.fst; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

@[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₂).snd 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₂.snd x s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

@[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₂).snd 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₂.snd y s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

@[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₂).snd 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₂.snd s₁; ((r₁.fst, r₂.fst), r₁.snd)) xs ys (s₁, s₂); (m.fst.fst, m.snd)

@[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₂).snd 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₂.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 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).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd) : R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd

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).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd) : (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd

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).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd) : R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧ (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd

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).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd) : (mapAccumr₂ f₁ xs ys s₁).snd = (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 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 ()).snd

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).fst ∈ S) (out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd) : (mapAccumr f xs s₀).snd = 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 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 ()).snd

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).fst ∈ S) (out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd) : (mapAccumr₂ f xs ys s₀).snd = map₂ (fun (x1 : α) (x2 : β) => (f x1 x2 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 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).fst = s) : mapAccumr f xs s = (s, 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 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).fst = s) : mapAccumr₂ f xs ys s = (s, 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 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).snd = f' a) : (mapAccumr f xs s).snd = 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).snd = f' a b) : (mapAccumr₂ f xs ys s).snd = 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 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)).fst.fst = (f x (s, s)).fst.snd) : (mapAccumr f xs (s, s)).snd = (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 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)).fst; s'.fst = s'.snd) : (mapAccumr₂ f xs ys (s, s)).snd = (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 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 its 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 its 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