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₂).snd s₁ = let m :=
Vector.mapAccumr
(fun x s =>
let r₂ := f₂ x s.snd;
let r₁ := f₁ r₂.snd s.fst;
((r₁.fst, r₂.fst), r₁.snd))
xs (s₁, s₂);
(m.fst.fst, m.snd)
@[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).snd = (Vector.mapAccumr
(fun x s =>
let r := f₂ x s;
(r.fst, f₁ r.snd))
xs s).snd
@[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₂).snd ys s₁ = let m :=
Vector.mapAccumr₂
(fun x y s =>
let r₂ := f₂ x s.snd;
let r₁ := f₁ r₂.snd y s.fst;
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂);
(m.fst.fst, m.snd)
@[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₂).snd s₁ = let m :=
Vector.mapAccumr₂
(fun x y s =>
let r₂ := f₂ y s.snd;
let r₁ := f₁ x r₂.snd s.fst;
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂);
(m.fst.fst, m.snd)
@[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₂).snd s₁ = let m :=
Vector.mapAccumr₂
(fun x y s =>
let r₂ := f₂ x y s.snd;
let r₁ := f₁ r₂.snd s.fst;
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂);
(m.fst.fst, m.snd)
@[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₂).snd 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₂.snd x s₁;
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂);
(m.fst.fst, m.snd)
@[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₂).snd 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₂.snd y s₁;
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂);
(m.fst.fst, m.snd)
@[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₂).snd 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₂.snd s₁;
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂);
(m.fst.fst, m.snd)
@[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₂).snd 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₂.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
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).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd)
:
R (Vector.mapAccumr f₁ xs s₁).fst (Vector.mapAccumr f₂ xs s₂).fst ∧ (Vector.mapAccumr f₁ xs s₁).snd = (Vector.mapAccumr f₂ xs s₂).snd
theorem
Vector.mapAccumr_bisim_tail
{α : Type u_2}
{n : ℕ}
{xs : Vector α n}
{σ₁ : Type}
{β : Type u_1}
{σ₂ : Type}
{f₁ : α → σ₁ → σ₁ × β}
{f₂ : α → σ₂ → σ₂ × β}
{s₁ : σ₁}
{s₂ : σ₂}
(h : ∃ R, 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)
:
(Vector.mapAccumr f₁ xs s₁).snd = (Vector.mapAccumr f₂ xs s₂).snd
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).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd)
:
R (Vector.mapAccumr₂ f₁ xs ys s₁).fst (Vector.mapAccumr₂ f₂ xs ys s₂).fst ∧ (Vector.mapAccumr₂ f₁ xs ys s₁).snd = (Vector.mapAccumr₂ f₂ xs ys s₂).snd
theorem
Vector.mapAccumr₂_bisim_tail
{α : Type}
{n : ℕ}
{xs : Vector α n}
{β : Type}
{σ₁ : Type}
{γ : Type}
{σ₂ : Type}
{ys : Vector β n}
{f₁ : α → β → σ₁ → σ₁ × γ}
{f₂ : α → β → σ₂ → σ₂ × γ}
{s₁ : σ₁}
{s₂ : σ₂}
(h : ∃ R,
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)
:
(Vector.mapAccumr₂ f₁ xs ys s₁).snd = (Vector.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
Vector.map_eq_mapAccumr
{α : Type u_2}
{n : ℕ}
{xs : Vector α n}
:
∀ {α : Type u_1} {f : α → α}, Vector.map f xs = (Vector.mapAccumr (fun x x_1 => ((), f x)) xs ()).snd
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 ∈ S → (f a s).fst ∈ S)
(out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd)
:
(Vector.mapAccumr f xs s₀).snd = Vector.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
Vector.map₂_eq_mapAccumr₂
{α : Type}
{n : ℕ}
{β : Type}
{xs : Vector α n}
{ys : Vector β n}
:
∀ {α : Type} {f : α → β → α}, Vector.map₂ f xs ys = (Vector.mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).snd
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 ∈ 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)
:
(Vector.mapAccumr₂ f xs ys s₀).snd = Vector.map₂ (fun x x_1 => (f x x_1 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
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).fst = s)
:
Vector.mapAccumr f xs s = (s, Vector.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
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).fst = s)
:
Vector.mapAccumr₂ f xs ys s = (s, Vector.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
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).snd = (f a s').snd)
:
(Vector.mapAccumr f xs s).snd = Vector.map (fun x => (f x s).snd) 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).snd = (f a b s').snd)
:
(Vector.mapAccumr₂ f xs ys s).snd = Vector.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
Vector.mapAccumr_redundant_pair
{α : Type u_2}
{n : ℕ}
{β : Type u_1}
{xs : Vector α n}
{σ : Type}
{s : σ}
(f : α → σ × σ → (σ × σ) × β)
(h : ∀ (x : α) (s : σ), (f x (s, s)).fst.fst = (f x (s, s)).fst.snd)
:
(Vector.mapAccumr f xs (s, s)).snd = (Vector.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
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)).fst;
s'.fst = s'.snd)
:
(Vector.mapAccumr₂ f xs ys (s, s)).snd = (Vector.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
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