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 q → R (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 q → R (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 q → R (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 q → R (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 : α), ∀ s ∈ S, (f a s).1 ∈ S)
(out : ∀ (a : α) (s s' : σ), s ∈ S → 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 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 : β), ∀ 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)
:
(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 : σ}
[Inhabited α]
(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 : σ}
[Inhabited β]
(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)
:
Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr₂ f ys xs 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 : α → β → σ → σ × γ)
:
Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr₂ (flip f) ys xs s