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 Mathlib.Vector.mapAccumr_mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : } {s₁ : σ₁} {s₂ : σ₂} (xs : Mathlib.Vector α n) (f₁ : βσ₁σ₁ × γ) (f₂ : ασ₂σ₂ × β) :
Mathlib.Vector.mapAccumr f₁ (Mathlib.Vector.mapAccumr f₂ xs s₂).2 s₁ = let m := Mathlib.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 Mathlib.Vector.mapAccumr_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {n : } (xs : Mathlib.Vector α n) (f₁ : βσ₁σ₁ × γ) {s : σ₁} (f₂ : αβ) :
Mathlib.Vector.mapAccumr f₁ (Mathlib.Vector.map f₂ xs) s = Mathlib.Vector.mapAccumr (fun (x : α) (s : σ₁) => f₁ (f₂ x) s) xs s
@[simp]
theorem Mathlib.Vector.map_mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₂ : Type u_7} {n : } (xs : Mathlib.Vector α n) (f₂ : ασ₂σ₂ × β) {s : σ₂} (f₁ : βγ) :
Mathlib.Vector.map f₁ (Mathlib.Vector.mapAccumr f₂ xs s).2 = (Mathlib.Vector.mapAccumr (fun (x : α) (s : σ₂) => let r := f₂ x s; (r.1, f₁ r.2)) xs s).2
@[simp]
theorem Mathlib.Vector.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (xs : Mathlib.Vector α n) (f₁ : βγ) (f₂ : αβ) :
Mathlib.Vector.map f₁ (Mathlib.Vector.map f₂ xs) = Mathlib.Vector.map (fun (x : α) => f₁ (f₂ x)) xs
@[simp]
theorem Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : γβσ₁σ₁ × ζ) (f₂ : ασ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr₂ f₁ (Mathlib.Vector.mapAccumr f₂ xs s₂).2 ys s₁ = let m := Mathlib.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 Mathlib.Vector.map₂_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : } (xs : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : γβζ) (f₂ : αγ) :
Mathlib.Vector.map₂ f₁ (Mathlib.Vector.map f₂ xs) ys = Mathlib.Vector.map₂ (fun (x : α) (y : β) => f₁ (f₂ x) y) xs ys
@[simp]
theorem Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : αγσ₁σ₁ × ζ) (f₂ : βσ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr₂ f₁ xs (Mathlib.Vector.mapAccumr f₂ ys s₂).2 s₁ = let m := Mathlib.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 Mathlib.Vector.map₂_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : } (xs : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : αγζ) (f₂ : βγ) :
Mathlib.Vector.map₂ f₁ xs (Mathlib.Vector.map f₂ ys) = Mathlib.Vector.map₂ (fun (x : α) (y : β) => f₁ x (f₂ y)) xs ys
@[simp]
theorem Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : γσ₁σ₁ × ζ) (f₂ : αβσ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr f₁ (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ = let m := Mathlib.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 Mathlib.Vector.map_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : } (xs : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : γζ) (f₂ : αβγ) :
Mathlib.Vector.map f₁ (Mathlib.Vector.map₂ f₂ xs ys) = Mathlib.Vector.map₂ (fun (x : α) (y : β) => f₁ (f₂ x y)) xs ys
@[simp]
theorem Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : γασ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr₂ f₁ (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 xs s₁ = let m := Mathlib.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 Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : γβσ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr₂ f₁ (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 ys s₁ = let m := Mathlib.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 Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : αγσ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr₂ f₁ xs (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ = let m := Mathlib.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 Mathlib.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 : Mathlib.Vector α n) (ys : Mathlib.Vector β n) (f₁ : βγσ₁σ₁ × φ) (f₂ : αβσ₂σ₂ × γ) :
Mathlib.Vector.mapAccumr₂ f₁ ys (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ = let m := Mathlib.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 Mathlib.Vector.mapAccumr_bisim {α : Type u_1} {β : Type u_2} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : } {xs : Mathlib.Vector α n} {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 (Mathlib.Vector.mapAccumr f₁ xs s₁).1 (Mathlib.Vector.mapAccumr f₂ xs s₂).1 (Mathlib.Vector.mapAccumr f₁ xs s₁).2 = (Mathlib.Vector.mapAccumr f₂ xs s₂).2
theorem Mathlib.Vector.mapAccumr_bisim_tail {α : Type u_1} {β : Type u_2} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : } {xs : Mathlib.Vector α n} {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) :
(Mathlib.Vector.mapAccumr f₁ xs s₁).2 = (Mathlib.Vector.mapAccumr f₂ xs s₂).2
theorem Mathlib.Vector.mapAccumr₂_bisim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : } {xs : Mathlib.Vector α n} {ys : Mathlib.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 (Mathlib.Vector.mapAccumr₂ f₁ xs ys s₁).1 (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).1 (Mathlib.Vector.mapAccumr₂ f₁ xs ys s₁).2 = (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2
theorem Mathlib.Vector.mapAccumr₂_bisim_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : } {xs : Mathlib.Vector α n} {ys : Mathlib.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) :
(Mathlib.Vector.mapAccumr₂ f₁ xs ys s₁).2 = (Mathlib.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 Mathlib.Vector.map_eq_mapAccumr {α : Type u_1} {β : Type u_2} {n : } {xs : Mathlib.Vector α n} {f : αβ} :
Mathlib.Vector.map f xs = (Mathlib.Vector.mapAccumr (fun (x : α) (x_1 : Unit) => ((), f x)) xs ()).2
theorem Mathlib.Vector.mapAccumr_eq_map {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : } {xs : Mathlib.Vector α n} {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) :
(Mathlib.Vector.mapAccumr f xs s₀).2 = Mathlib.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 Mathlib.Vector.map₂_eq_mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} {f : αβγ} :
Mathlib.Vector.map₂ f xs ys = (Mathlib.Vector.mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) => ((), f x y)) xs ys ()).2
theorem Mathlib.Vector.mapAccumr₂_eq_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : } {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} {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) :
(Mathlib.Vector.mapAccumr₂ f xs ys s₀).2 = Mathlib.Vector.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 Mathlib.Vector.mapAccumr_eq_map_of_constant_state {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : } {xs : Mathlib.Vector α n} (f : ασσ × β) (s : σ) (h : ∀ (a : α), (f a s).1 = s) :
Mathlib.Vector.mapAccumr f xs s = (s, Mathlib.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 Mathlib.Vector.mapAccumr₂_eq_map₂_of_constant_state {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : } {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} (f : αβσσ × γ) (s : σ) (h : ∀ (a : α) (b : β), (f a b s).1 = s) :
Mathlib.Vector.mapAccumr₂ f xs ys s = (s, Mathlib.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 Mathlib.Vector.mapAccumr_eq_map_of_unused_state {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : } {xs : Mathlib.Vector α n} (f : ασσ × β) (s : σ) (h : ∀ (a : α) (s s' : σ), (f a s).2 = (f a s').2) :
(Mathlib.Vector.mapAccumr f xs s).2 = Mathlib.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 Mathlib.Vector.mapAccumr₂_eq_map₂_of_unused_state {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : } {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} (f : αβσσ × γ) (s : σ) (h : ∀ (a : α) (b : β) (s s' : σ), (f a b s).2 = (f a b s').2) :
(Mathlib.Vector.mapAccumr₂ f xs ys s).2 = Mathlib.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 Mathlib.Vector.mapAccumr_redundant_pair {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : } {s : σ} {xs : Mathlib.Vector α n} (f : ασ × σ(σ × σ) × β) (h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2) :
(Mathlib.Vector.mapAccumr f xs (s, s)).2 = (Mathlib.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 Mathlib.Vector.mapAccumr₂_redundant_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : } {s : σ} {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} (f : αβσ × σ(σ × σ) × γ) (h : ∀ (x : α) (y : β) (s : σ), let s' := (f x y (s, s)).1; s'.1 = s'.2) :
(Mathlib.Vector.mapAccumr₂ f xs ys (s, s)).2 = (Mathlib.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 Mathlib.Vector.mapAccumr₂_unused_input_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : } {s : σ} {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} [Inhabited α] (f : αβσσ × γ) (h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s) :
Mathlib.Vector.mapAccumr₂ f xs ys s = Mathlib.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 Mathlib.Vector.mapAccumr₂_unused_input_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : } {s : σ} {xs : Mathlib.Vector α n} {ys : Mathlib.Vector β n} [Inhabited β] (f : αβσσ × γ) (h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s) :
Mathlib.Vector.mapAccumr₂ f xs ys s = Mathlib.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 Mathlib.Vector.map₂_comm {α : Type u_1} {β : Type u_2} {n : } (xs : Mathlib.Vector α n) (ys : Mathlib.Vector α n) (f : ααβ) (comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) :
theorem Mathlib.Vector.mapAccumr₂_comm {α : Type u_1} {γ : Type u_3} {σ : Type u_5} {n : } {s : σ} (xs : Mathlib.Vector α n) (ys : Mathlib.Vector α n) (f : αασσ × γ) (comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s) :

Argument Flipping #

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