chore: complete variable name linting for Vector (#7154)

This commit is contained in:
Kim Morrison 2025-02-20 13:42:50 +11:00 committed by GitHub
parent c86073830f
commit 6a4225bf04
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
19 changed files with 2250 additions and 2164 deletions

View file

@ -239,3 +239,22 @@ If an acronym is typically spelled using mixed case, this mixed spelling may be
Simp sets centered around a conversion function should be called `source_to_target`. For example, a simp set for the `BitVec.toNat` function, which goes from `BitVec` to
`Nat`, should be called `bitvec_to_nat`.
## Variable names
We make the following recommendations for variable names, but without insisting on them:
* Simple hypotheses should be named `h`, `h'`, or using a numerical sequence `h₁`, `h₂`, etc.
* Another common name for a simple hypothesis is `w` (for "witness").
* `List`s should be named `l`, `l'`, `l₁`, etc, or `as`, `bs`, etc.
(Use of `as`, `bs` is encouraged when the lists are of different types, e.g. `as : List α` and `bs : List β`.)
`xs`, `ys`, `zs` are allowed, but it is better if these are reserved for `Array` and `Vector`.
A list of lists may be named `L`.
* `Array`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the arrays are of different types, e.g. `as : Array α` and `bs : Array β`.
An array of arrays may be named `xss`.
* `Vector`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the vectors are of different types, e.g. `as : Vector α n` and `bs : Vector β n`.
A vector of vectors may be named `xss`.
* A common exception for `List` / `Array` / `Vector` is to use `acc` for an accumulator in a recursive function.
* `i`, `j`, `k` are preferred for numerical indices.
Descriptive names such as `start`, `stop`, `lo`, and `hi` are encouraged when they increase readability.
* `n`, `m` are preferred for sizes, e.g. in `Vector α n` or `xs.size = n`.
* `w` is preferred for the width of a `BitVec`.

View file

@ -7,6 +7,9 @@ prelude
import Init.Data.Vector.Lemmas
import Init.Data.Array.Attach
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
/--
@ -17,8 +20,8 @@ to apply `f`.
We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
-/
def pmap {P : α → Prop} (f : ∀ a, P a → β) (l : Vector α n) (H : ∀ a ∈ l, P a) : Vector β n :=
Vector.mk (l.toArray.pmap f (fun a m => H a (by simpa using m))) (by simp)
def pmap {P : α → Prop} (f : ∀ a, P a → β) (xs : Vector α n) (H : ∀ a ∈ xs, P a) : Vector β n :=
Vector.mk (xs.toArray.pmap f (fun a m => H a (by simpa using m))) (by simp)
/--
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
@ -50,37 +53,37 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
(mk xs h).pmap f H = mk (xs.pmap f (by simpa using H)) (by simpa using h) := by
simp [pmap]
@[simp] theorem toArray_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l, P x} :
(l.attachWith P H).toArray = l.toArray.attachWith P (by simpa using H) := by
@[simp] theorem toArray_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs, P x} :
(xs.attachWith P H).toArray = xs.toArray.attachWith P (by simpa using H) := by
simp [attachWith]
@[simp] theorem toArray_attach {α : Type _} {l : Vector α n} :
l.attach.toArray = l.toArray.attachWith (· ∈ l) (by simp) := by
@[simp] theorem toArray_attach {xs : Vector α n} :
xs.attach.toArray = xs.toArray.attachWith (· ∈ xs) (by simp) := by
simp [attach]
@[simp] theorem toArray_pmap {l : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
(l.pmap f H).toArray = l.toArray.pmap f (fun a m => H a (by simpa using m)) := by
@[simp] theorem toArray_pmap {xs : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} :
(xs.pmap f H).toArray = xs.toArray.pmap f (fun a m => H a (by simpa using m)) := by
simp [pmap]
@[simp] theorem toList_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l, P x} :
(l.attachWith P H).toList = l.toList.attachWith P (by simpa using H) := by
@[simp] theorem toList_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs, P x} :
(xs.attachWith P H).toList = xs.toList.attachWith P (by simpa using H) := by
simp [attachWith]
@[simp] theorem toList_attach {α : Type _} {l : Vector α n} :
l.attach.toList = l.toList.attachWith (· ∈ l) (by simp) := by
@[simp] theorem toList_attach {xs : Vector α n} :
xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp) := by
simp [attach]
@[simp] theorem toList_pmap {l : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
(l.pmap f H).toList = l.toList.pmap f (fun a m => H a (by simpa using m)) := by
@[simp] theorem toList_pmap {xs : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} :
(xs.pmap f H).toList = xs.toList.pmap f (fun a m => H a (by simpa using m)) := by
simp [pmap]
/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : Vector α n) (H : ∀ a ∈ l, P a) :
Vector β n := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Vector α n) (H : ∀ a ∈ xs, P a) :
Vector β n := (xs.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
funext α β n p f L h'
rcases L with ⟨L, rfl⟩
funext α β n p f xs h'
rcases xs with ⟨xs, rfl⟩
simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith_eq_pmap, eq_mk]
apply Array.pmap_congr_left
intro a m h₁ h₂
@ -88,9 +91,9 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #v[] (by simp) = #v[] := rfl
@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : Vector α n) (h : ∀ b ∈ l.push a, P b) :
pmap f (l.push a) h =
(pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Vector α n) (h : ∀ b ∈ xs.push a, P b) :
pmap f (xs.push a) h =
(pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
simp [pmap]
@[simp] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
@ -98,121 +101,127 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #v[], P x) : (#v[] : Vector α 0).attachWith P H = #v[] := rfl
@[simp]
theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : Vector α n) (H) :
@pmap _ _ _ p (fun a _ => f a) l H = map f l := by
cases l; simp
theorem pmap_eq_map (p : α → Prop) (f : α → β) (xs : Vector α n) (H) :
@pmap _ _ _ p (fun a _ => f a) xs H = map f xs := by
cases xs; simp
theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : Vector α n) {H₁ H₂}
(h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
rcases l with ⟨l, rfl⟩
theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (xs : Vector α n) {H₁ H₂}
(h : ∀ a ∈ xs, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f xs H₁ = pmap g xs H₂ := by
rcases xs with ⟨xs, rfl⟩
simp only [pmap_mk, eq_mk]
apply Array.pmap_congr_left
simpa using h
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l : Vector α n) (H) :
map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
rcases l with ⟨l, rfl⟩
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (xs : Vector α n) (H) :
map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
rcases xs with ⟨xs, rfl⟩
simp [Array.map_pmap]
theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l : Vector α n) (H) :
pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h) := by
rcases l with ⟨l, rfl⟩
theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (xs : Vector α n) (H) :
pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem _ h) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.pmap_map]
theorem attach_congr {l₁ l₂ : Vector α n} (h : l₁ = l₂) :
l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
theorem attach_congr {xs ys : Vector α n} (h : xs = ys) :
xs.attach = ys.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
subst h
simp
theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h) := by
theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {H : ∀ x ∈ xs, P x} :
xs.attachWith P H = ys.attachWith P fun _ h => H _ (w ▸ h) := by
subst w
simp
@[simp] theorem attach_push {a : α} {l : Vector α n} :
(l.push a).attach =
(l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
rcases l with ⟨l, rfl⟩
@[simp] theorem attach_push {a : α} {xs : Vector α n} :
(xs.push a).attach =
(xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
rcases xs with ⟨xs, rfl⟩
simp [Array.map_attach_eq_pmap]
@[simp] theorem attachWith_push {a : α} {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
(l.push a).attachWith P H =
(l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
rcases l with ⟨l, rfl⟩
@[simp] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
(xs.push a).attachWith P H =
(xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
rcases xs with ⟨xs, rfl⟩
simp
theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l : Vector α n) (H) :
pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
rcases l with ⟨l, rfl⟩
theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (xs : Vector α n) (H) :
pmap f xs H = xs.attach.map fun x => f x.1 (H _ x.2) := by
rcases xs with ⟨xs, rfl⟩
simp only [pmap_mk, Array.pmap_eq_map_attach, attach_mk, map_mk, eq_mk]
rw [Array.map_attach_eq_pmap, Array.map_attachWith]
ext i hi₁ hi₂ <;> simp
@[simp]
theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l : Vector α n) (H) :
pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
cases l
theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (xs : Vector α n) (H) :
pmap (fun a h => ⟨a, f a h⟩) xs H = xs.attachWith q (fun x h => f x (H x h)) := by
rcases xs with ⟨xs, rfl⟩
simp
theorem attach_map_val (l : Vector α n) (f : α → β) :
(l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
cases l
theorem attach_map_val (xs : Vector α n) (f : α → β) :
(xs.attach.map fun (i : {i // i ∈ xs}) => f i) = xs.map f := by
rcases xs with ⟨xs, rfl⟩
simp
@[deprecated attach_map_val (since := "2025-02-17")]
abbrev attach_map_coe := @attach_map_val
theorem attach_map_subtype_val (l : Vector α n) : l.attach.map Subtype.val = l := by
cases l; simp
theorem attach_map_subtype_val (xs : Vector α n) : xs.attach.map Subtype.val = xs := by
rcases xs with ⟨xs, rfl⟩
simp
theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
cases l; simp
theorem attachWith_map_val {p : α → Prop} (f : α → β) (xs : Vector α n) (H : ∀ a ∈ xs, p a) :
((xs.attachWith p H).map fun (i : { i // p i}) => f i) = xs.map f := by
rcases xs with ⟨xs, rfl⟩
simp
@[deprecated attachWith_map_val (since := "2025-02-17")]
abbrev attachWith_map_coe := @attachWith_map_val
theorem attachWith_map_subtype_val {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) :
(l.attachWith p H).map Subtype.val = l := by
cases l; simp
theorem attachWith_map_subtype_val {p : α → Prop} (xs : Vector α n) (H : ∀ a ∈ xs, p a) :
(xs.attachWith p H).map Subtype.val = xs := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp]
theorem mem_attach (l : Vector α n) : ∀ x, x ∈ l.attach
theorem mem_attach (xs : Vector α n) : ∀ x, x ∈ xs.attach
| ⟨a, h⟩ => by
have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
rcases this with ⟨⟨_, _⟩, m, rfl⟩
exact m
@[simp]
theorem mem_attachWith (l : Vector α n) {q : α → Prop} (H) (x : {x // q x}) :
x ∈ l.attachWith q H ↔ x.1 ∈ l := by
rcases l with ⟨l, rfl⟩
theorem mem_attachWith (xs : Vector α n) {q : α → Prop} (H) (x : {x // q x}) :
x ∈ xs.attachWith q H ↔ x.1 ∈ xs := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp]
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H b} :
b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs : Vector α n} {H b} :
b ∈ pmap f xs H ↔ ∃ (a : _) (h : a ∈ xs), f a (H a h) = b := by
simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H} {a} (h : a ∈ l) :
f a (H a h) ∈ pmap f l H := by
theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {xs : Vector α n} {H} {a} (h : a ∈ xs) :
f a (H a h) ∈ pmap f xs H := by
rw [mem_pmap]
exact ⟨a, h, rfl⟩
theorem pmap_eq_self {l : Vector α n} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a}
{f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
cases l; simp [Array.pmap_eq_self]
theorem pmap_eq_self {xs : Vector α n} {p : α → Prop} {hp : ∀ (a : α), a ∈ xs → p a}
{f : (a : α) → p a → α} : xs.pmap f hp = xs ↔ ∀ a (h : a ∈ xs), f a (hp a h) = a := by
rcases xs with ⟨xs, rfl⟩
simp [Array.pmap_eq_self]
@[simp]
theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Vector α n} (h : ∀ a ∈ l, p a) (i : Nat) :
(pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H) := by
cases l; simp
theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {xs : Vector α n} (h : ∀ a ∈ xs, p a) (i : Nat) :
(pmap f xs h)[i]? = Option.pmap f xs[i]? fun x H => h x (mem_of_getElem? H) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp]
theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Vector α n} (h : ∀ a ∈ l, p a) {i : Nat}
theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {xs : Vector α n} (h : ∀ a ∈ xs, p a) {i : Nat}
(hn : i < n) :
(pmap f l h)[i] = f (l[i]) (h _ (by simp)) := by
cases l; simp
(pmap f xs h)[i] = f (xs[i]) (h _ (by simp)) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp]
theorem getElem?_attachWith {xs : Vector α n} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
@ -235,26 +244,27 @@ theorem getElem_attach {xs : Vector α n} {i : Nat} (h : i < n) :
xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
getElem_attachWith h
@[simp] theorem pmap_attach (l : Vector α n) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
pmap f l.attach H =
l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
@[simp] theorem pmap_attach (xs : Vector α n) {p : {x // x ∈ xs} → Prop} (f : ∀ a, p a → β) (H) :
pmap f xs.attach H =
xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
(fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
rcases xs with ⟨xs, rfl⟩
ext <;> simp
@[simp] theorem pmap_attachWith (l : Vector α n) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
pmap f (l.attachWith q H₁) H₂ =
l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
@[simp] theorem pmap_attachWith (xs : Vector α n) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
pmap f (xs.attachWith q H₁) H₂ =
xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
(fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
ext <;> simp
theorem foldl_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
(H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
(l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
theorem foldl_pmap (xs : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
(H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
(xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
rw [pmap_eq_map_attach, foldl_map]
theorem foldr_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
(H : ∀ (a : α), a ∈ l → P a) (g : β → γγ) (x : γ) :
(l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
theorem foldr_pmap (xs : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
(H : ∀ (a : α), a ∈ xs → P a) (g : β → γγ) (x : γ) :
(xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
rw [pmap_eq_map_attach, foldr_map]
/--
@ -267,9 +277,9 @@ Unfortunately this can't be applied by `simp` because of the higher order unific
and even when rewriting we need to specify the function explicitly.
See however `foldl_subtype` below.
-/
theorem foldl_attach (l : Vector α n) (f : β → α → β) (b : β) :
l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
rcases l with ⟨l, rfl⟩
theorem foldl_attach (xs : Vector α n) (f : β → α → β) (b : β) :
xs.attach.foldl (fun acc t => f acc t.1) b = xs.foldl f b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldl_attach]
/--
@ -282,65 +292,65 @@ Unfortunately this can't be applied by `simp` because of the higher order unific
and even when rewriting we need to specify the function explicitly.
See however `foldr_subtype` below.
-/
theorem foldr_attach (l : Vector α n) (f : α → β → β) (b : β) :
l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
rcases l with ⟨l, rfl⟩
theorem foldr_attach (xs : Vector α n) (f : α → β → β) (b : β) :
xs.attach.foldr (fun t acc => f t.1 acc) b = xs.foldr f b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldr_attach]
theorem attach_map {l : Vector α n} (f : α → β) :
(l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
cases l
theorem attach_map {xs : Vector α n} (f : α → β) :
(xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
cases xs
ext <;> simp
theorem attachWith_map {l : Vector α n} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
(l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
theorem attachWith_map {xs : Vector α n} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ xs.map f → P b} :
(xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
fun ⟨x, h⟩ => ⟨f x, h⟩ := by
rcases l with ⟨l, rfl⟩
rcases xs with ⟨xs, rfl⟩
simp [Array.attachWith_map]
@[simp] theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
@[simp] theorem map_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
(f : { x // P x } → β) :
(l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
rcases l with ⟨l, rfl⟩
(xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
rcases xs with ⟨xs, rfl⟩
simp [Array.map_attachWith]
theorem map_attachWith_eq_pmap {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
theorem map_attachWith_eq_pmap {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
(f : { x // P x } → β) :
(l.attachWith P H).map f =
l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
cases l
(xs.attachWith P H).map f =
xs.pmap (fun a (h : a ∈ xs ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
rcases xs with ⟨xs, rfl⟩
ext <;> simp
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
theorem map_attach_eq_pmap {l : Vector α n} (f : { x // x ∈ l } → β) :
l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
cases l
theorem map_attach_eq_pmap {xs : Vector α n} (f : { x // x ∈ xs } → β) :
xs.attach.map f = xs.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
rcases xs with ⟨xs, rfl⟩
ext <;> simp
@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
abbrev map_attach := @map_attach_eq_pmap
theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l : Vector α n) (H₁ H₂) :
pmap f (pmap g l H₁) H₂ =
pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (xs : Vector α n) (H₁ H₂) :
pmap f (pmap g xs H₁) H₂ =
pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
(fun a _ => H₁ a a.2) := by
rcases l with ⟨l, rfl⟩
rcases xs with ⟨xs, rfl⟩
ext <;> simp
@[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ : Vector ι n) (l₂ : Vector ι m)
(h : ∀ a ∈ l₁ ++ l₂, p a) :
(l₁ ++ l₂).pmap f h =
(l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by
cases l₁
cases l₂
@[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (xs : Vector ι n) (ys : Vector ι m)
(h : ∀ a ∈ xs ++ ys, p a) :
(xs ++ ys).pmap f h =
(xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
ys.pmap f fun a ha => h a (mem_append_right xs ha) := by
cases xs
cases ys
simp
theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ : Vector α n) (l₂ : Vector α m)
(h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) :
((l₁ ++ l₂).pmap f fun a ha => (mem_append.1 ha).elim (h₁ a) (h₂ a)) =
l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
pmap_append f l₁ l₂ _
theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (xs : Vector α n) (ys : Vector α m)
(h₁ : ∀ a ∈ xs, p a) (h₂ : ∀ a ∈ ys, p a) :
((xs ++ ys).pmap f fun a ha => (mem_append.1 ha).elim (h₁ a) (h₂ a)) =
xs.pmap f h₁ ++ ys.pmap f h₂ :=
pmap_append f xs ys _
@[simp] theorem attach_append (xs : Vector α n) (ys : Vector α m) :
(xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
@ -408,33 +418,33 @@ theorem back?_attach {xs : Vector α n} :
simp
@[simp]
theorem countP_attach (l : Vector α n) (p : α → Bool) :
l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
cases l
theorem countP_attach (xs : Vector α n) (p : α → Bool) :
xs.attach.countP (fun a : {x // x ∈ xs} => p a) = xs.countP p := by
cases xs
simp [Function.comp_def]
@[simp]
theorem countP_attachWith {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) (q : α → Bool) :
(l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
cases l
theorem countP_attachWith {p : α → Prop} (xs : Vector α n) (H : ∀ a ∈ xs, p a) (q : α → Bool) :
(xs.attachWith p H).countP (fun a : {x // p x} => q a) = xs.countP q := by
cases xs
simp
@[simp]
theorem count_attach [DecidableEq α] (l : Vector α n) (a : {x // x ∈ l}) :
l.attach.count a = l.count ↑a := by
rcases l with ⟨l, rfl⟩
theorem count_attach [DecidableEq α] (xs : Vector α n) (a : {x // x ∈ xs}) :
xs.attach.count a = xs.count ↑a := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp]
theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
(l.attachWith p H).count a = l.count ↑a := by
cases l
theorem count_attachWith [DecidableEq α] {p : α → Prop} (xs : Vector α n) (H : ∀ a ∈ xs, p a) (a : {x // p x}) :
(xs.attachWith p H).count a = xs.count ↑a := by
cases xs
simp
@[simp] theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : Vector α n) (H₁) :
(l.pmap g H₁).countP f =
l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
rcases l with ⟨l, rfl⟩
@[simp] theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (xs : Vector α n) (H₁) :
(xs.pmap g H₁).countP f =
xs.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
rcases xs with ⟨xs, rfl⟩
simp only [pmap_mk, countP_mk, Array.countP_pmap]
simp [Array.countP_eq_size_filter]
@ -442,56 +452,56 @@ theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Vector α n) (H
`Vector.unattach` is the (one-sided) inverse of `Vector.attach`. It is a synonym for `Vector.map Subtype.val`.
We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
functions applied to `l : Vector { x // p x }` which only depend on the value, not the predicate, and rewrite these
in terms of a simpler function applied to `l.unattach`.
We use it by providing a simp lemma `xs.attach.unattach = xs`, and simp lemmas which recognize higher order
functions applied to `xs : Vector { x // p x }` which only depend on the value, not the predicate, and rewrite these
in terms of a simpler function applied to `xs.unattach`.
Further, we provide simp lemmas that push `unattach` inwards.
-/
/--
A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
A synonym for `xs.map (·.val)`. Mostly this should not be needed by users.
It is introduced as in intermediate step by lemmas such as `map_subtype`,
and is ideally subsequently simplified away by `unattach_attach`.
If not, usually the right approach is `simp [Vector.unattach, -Vector.map_subtype]` to unfold.
-/
def unattach {α : Type _} {p : α → Prop} (l : Vector { x // p x } n) : Vector α n := l.map (·.val)
def unattach {α : Type _} {p : α → Prop} (xs : Vector { x // p x } n) : Vector α n := xs.map (·.val)
@[simp] theorem unattach_nil {p : α → Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := rfl
@[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Vector { x // p x } n} :
(l.push a).unattach = l.unattach.push a.1 := by
@[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {xs : Vector { x // p x } n} :
(xs.push a).unattach = xs.unattach.push a.1 := by
simp only [unattach, Vector.map_push]
@[simp] theorem unattach_mk {p : α → Prop} {l : Array { x // p x }} {h : l.size = n} :
(mk l h).unattach = mk l.unattach (by simpa using h) := by
@[simp] theorem unattach_mk {p : α → Prop} {xs : Array { x // p x }} {h : xs.size = n} :
(mk xs h).unattach = mk xs.unattach (by simpa using h) := by
simp [unattach]
@[simp] theorem toArray_unattach {p : α → Prop} {l : Vector { x // p x } n} :
l.unattach.toArray = l.toArray.unattach := by
@[simp] theorem toArray_unattach {p : α → Prop} {xs : Vector { x // p x } n} :
xs.unattach.toArray = xs.toArray.unattach := by
simp [unattach]
@[simp] theorem toList_unattach {p : α → Prop} {l : Array { x // p x }} :
l.unattach.toList = l.toList.unattach := by
@[simp] theorem toList_unattach {p : α → Prop} {xs : Vector { x // p x } n} :
xs.unattach.toList = xs.toList.unattach := by
simp [unattach]
@[simp] theorem unattach_attach {l : Vector α n} : l.attach.unattach = l := by
rcases l with ⟨l, rfl⟩
@[simp] theorem unattach_attach {xs : Vector α n} : xs.attach.unattach = xs := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem unattach_attachWith {p : α → Prop} {l : Vector α n}
{H : ∀ a ∈ l, p a} :
(l.attachWith p H).unattach = l := by
cases l
@[simp] theorem unattach_attachWith {p : α → Prop} {xs : Vector α n}
{H : ∀ a ∈ xs, p a} :
(xs.attachWith p H).unattach = xs := by
cases xs
simp
@[simp] theorem getElem?_unattach {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) :
l.unattach[i]? = l[i]?.map Subtype.val := by
@[simp] theorem getElem?_unattach {p : α → Prop} {xs : Vector { x // p x } n} (i : Nat) :
xs.unattach[i]? = xs[i]?.map Subtype.val := by
simp [unattach]
@[simp] theorem getElem_unattach
{p : α → Prop} {l : Vector { x // p x } n} (i : Nat) (h : i < n) :
l.unattach[i] = (l[i]'(by simpa using h)).1 := by
{p : α → Prop} {xs : Vector { x // p x } n} (i : Nat) (h : i < n) :
xs.unattach[i] = (xs[i]'(by simpa using h)).1 := by
simp [unattach]
/-! ### Recognizing higher order functions using a function that only depends on the value. -/
@ -500,66 +510,66 @@ def unattach {α : Type _} {p : α → Prop} (l : Vector { x // p x } n) : Vecto
This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem foldl_subtype {p : α → Prop} {l : Vector { x // p x } n}
@[simp] theorem foldl_subtype {p : α → Prop} {xs : Vector { x // p x } n}
{f : β → { x // p x } → β} {g : β → α → β} {x : β}
(hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
l.foldl f x = l.unattach.foldl g x := by
rcases l with ⟨l, rfl⟩
xs.foldl f x = xs.unattach.foldl g x := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldl_subtype hf]
/--
This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem foldr_subtype {p : α → Prop} {l : Vector { x // p x } n}
@[simp] theorem foldr_subtype {p : α → Prop} {xs : Vector { x // p x } n}
{f : { x // p x } → β → β} {g : α → β → β} {x : β}
(hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
l.foldr f x = l.unattach.foldr g x := by
rcases l with ⟨l, rfl⟩
xs.foldr f x = xs.unattach.foldr g x := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldr_subtype hf]
/--
This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem map_subtype {p : α → Prop} {l : Vector { x // p x } n}
@[simp] theorem map_subtype {p : α → Prop} {xs : Vector { x // p x } n}
{f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
l.map f = l.unattach.map g := by
rcases l with ⟨l, rfl⟩
xs.map f = xs.unattach.map g := by
rcases xs with ⟨xs, rfl⟩
simp [Array.map_subtype hf]
@[simp] theorem findSome?_subtype {p : α → Prop} {l : Array { x // p x }}
@[simp] theorem findSome?_subtype {p : α → Prop} {xs : Vector { x // p x } n}
{f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
l.findSome? f = l.unattach.findSome? g := by
rcases l with ⟨l, rfl⟩
xs.findSome? f = xs.unattach.findSome? g := by
rcases xs with ⟨xs, rfl⟩
simp
rw [Array.findSome?_subtype hf]
@[simp] theorem find?_subtype {p : α → Prop} {l : Array { x // p x }}
@[simp] theorem find?_subtype {p : α → Prop} {xs : Array { x // p x }}
{f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
(l.find? f).map Subtype.val = l.unattach.find? g := by
rcases l with ⟨l, rfl⟩
(xs.find? f).map Subtype.val = xs.unattach.find? g := by
rcases xs with ⟨l, rfl⟩
simp
rw [Array.find?_subtype hf]
/-! ### Simp lemmas pushing `unattach` inwards. -/
@[simp] theorem unattach_reverse {p : α → Prop} {l : Vector { x // p x } n} :
l.reverse.unattach = l.unattach.reverse := by
rcases l with ⟨l, rfl⟩
@[simp] theorem unattach_reverse {p : α → Prop} {xs : Vector { x // p x } n} :
xs.reverse.unattach = xs.unattach.reverse := by
rcases xs with ⟨xs, rfl⟩
simp [Array.unattach_reverse]
@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : Vector { x // p x } n} :
(l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
rcases l₁
rcases l₂
@[simp] theorem unattach_append {p : α → Prop} {xs ys : Vector { x // p x } n} :
(xs ++ ys).unattach = xs.unattach ++ ys.unattach := by
rcases xs
rcases ys
simp
@[simp] theorem unattach_flatten {p : α → Prop} {l : Vector (Vector { x // p x } n) n} :
l.flatten.unattach = (l.map unattach).flatten := by
@[simp] theorem unattach_flatten {p : α → Prop} {xss : Vector (Vector { x // p x } n) n} :
xss.flatten.unattach = (xss.map unattach).flatten := by
unfold unattach
cases l using vector₂_induction
cases xss using vector₂_induction
simp only [flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype,
Array.unattach_attach, Array.map_id_fun', id_eq, map_mk, Array.map_flatten, map_subtype,
map_id_fun', unattach_mk, eq_mk]

View file

@ -17,6 +17,9 @@ import Init.Data.Stream
`Vector α n` is a thin wrapper around `Array α` for arrays of fixed size `n`.
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
/-- `Vector α n` is an `Array α` with size `n`. -/
structure Vector (α : Type u) (n : Nat) extends Array α where
/-- Array size. -/
@ -43,16 +46,16 @@ recommended_spelling "singleton" for "#v[x]" in [Vector.mk, «term#v[_,]»]
/-- Custom eliminator for `Vector α n` through `Array α` -/
@[elab_as_elim]
def elimAsArray {motive : Vector α n → Sort u}
(mk : ∀ (a : Array α) (ha : a.size = n), motive ⟨a, ha⟩) :
(v : Vector α n) → motive v
| ⟨a, ha⟩ => mk a ha
(mk : ∀ (xs : Array α) (ha : xs.size = n), motive ⟨xs, ha⟩) :
(xs : Vector α n) → motive xs
| ⟨xs, h⟩ => mk xs h
/-- Custom eliminator for `Vector α n` through `List α` -/
@[elab_as_elim]
def elimAsList {motive : Vector α n → Sort u}
(mk : ∀ (a : List α) (ha : a.length = n), motive ⟨⟨a⟩, ha⟩) :
(v : Vector α n) → motive v
| ⟨⟨a⟩, ha⟩ => mk a ha
(mk : ∀ (l : List α) (ha : l.length = n), motive ⟨⟨l⟩, ha⟩) :
(xs : Vector α n) → motive xs
| ⟨⟨xs⟩, ha⟩ => mk xs ha
/-- Make an empty vector with pre-allocated capacity. -/
@[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
@ -70,22 +73,22 @@ instance [Inhabited α] : Inhabited (Vector α n) where
default := mkVector n default
/-- Get an element of a vector using a `Fin` index. -/
@[inline] def get (v : Vector α n) (i : Fin n) : α :=
v.toArray[(i.cast v.size_toArray.symm).1]
@[inline] def get (xs : Vector α n) (i : Fin n) : α :=
xs.toArray[(i.cast xs.size_toArray.symm).1]
/-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/
@[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α :=
v.toArray.uget i (v.size_toArray.symm ▸ h)
@[inline] def uget (xs : Vector α n) (i : USize) (h : i.toNat < n) : α :=
xs.toArray.uget i (xs.size_toArray.symm ▸ h)
instance : GetElem (Vector α n) Nat α fun _ i => i < n where
getElem x i h := get x ⟨i, h⟩
getElem xs i h := get xs ⟨i, h⟩
/-- Check if there is an element which satisfies `a == ·`. -/
def contains [BEq α] (v : Vector α n) (a : α) : Bool := v.toArray.contains a
def contains [BEq α] (xs : Vector α n) (a : α) : Bool := xs.toArray.contains a
/-- `a ∈ v` is a predicate which asserts that `a` is in the vector `v`. -/
structure Mem (as : Vector α n) (a : α) : Prop where
val : a ∈ as.toArray
structure Mem (xs : Vector α n) (a : α) : Prop where
val : a ∈ xs.toArray
instance : Membership α (Vector α n) where
mem := Mem
@ -94,28 +97,28 @@ instance : Membership α (Vector α n) where
Get an element of a vector using a `Nat` index. Returns the given default value if the index is out
of bounds.
-/
@[inline] def getD (v : Vector α n) (i : Nat) (default : α) : α := v.toArray.getD i default
@[inline] def getD (xs : Vector α n) (i : Nat) (default : α) : α := xs.toArray.getD i default
/-- The last element of a vector. Panics if the vector is empty. -/
@[inline] def back! [Inhabited α] (v : Vector α n) : α := v.toArray.back!
@[inline] def back! [Inhabited α] (xs : Vector α n) : α := xs.toArray.back!
/-- The last element of a vector, or `none` if the vector is empty. -/
@[inline] def back? (v : Vector α n) : Option α := v.toArray.back?
@[inline] def back? (xs : Vector α n) : Option α := xs.toArray.back?
/-- The last element of a non-empty vector. -/
@[inline] def back [NeZero n] (v : Vector α n) : α :=
v[n - 1]'(Nat.sub_one_lt (NeZero.ne n))
@[inline] def back [NeZero n] (xs : Vector α n) : α :=
xs[n - 1]'(Nat.sub_one_lt (NeZero.ne n))
/-- The first element of a non-empty vector. -/
@[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
@[inline] def head [NeZero n] (xs : Vector α n) := xs[0]'(Nat.pos_of_neZero n)
/-- Push an element `x` to the end of a vector. -/
@[inline] def push (v : Vector α n) (x : α) : Vector α (n + 1) :=
v.toArray.push x, by simp⟩
@[inline] def push (xs : Vector α n) (x : α) : Vector α (n + 1) :=
xs.toArray.push x, by simp⟩
/-- Remove the last element of a vector. -/
@[inline] def pop (v : Vector α n) : Vector α (n - 1) :=
⟨Array.pop v.toArray, by simp⟩
@[inline] def pop (xs : Vector α n) : Vector α (n - 1) :=
⟨Array.pop xs.toArray, by simp⟩
/--
Set an element in a vector using a `Nat` index, with a tactic provided proof that the index is in
@ -123,8 +126,8 @@ bounds.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def set (v : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic): Vector α n :=
v.toArray.set i x (by simp [*]), by simp⟩
@[inline] def set (xs : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic): Vector α n :=
xs.toArray.set i x (by simp [*]), by simp⟩
/--
Set an element in a vector using a `Nat` index. Returns the vector unchanged if the index is out of
@ -132,153 +135,154 @@ bounds.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def setIfInBounds (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
v.toArray.setIfInBounds i x, by simp⟩
@[inline] def setIfInBounds (xs : Vector α n) (i : Nat) (x : α) : Vector α n :=
xs.toArray.setIfInBounds i x, by simp⟩
/--
Set an element in a vector using a `Nat` index. Panics if the index is out of bounds.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
v.toArray.set! i x, by simp⟩
@[inline] def set! (xs : Vector α n) (i : Nat) (x : α) : Vector α n :=
xs.toArray.set! i x, by simp⟩
@[inline] def foldlM [Monad m] (f : β → α → m β) (b : β) (v : Vector α n) : m β :=
v.toArray.foldlM f b
@[inline] def foldlM [Monad m] (f : β → α → m β) (b : β) (xs : Vector α n) : m β :=
xs.toArray.foldlM f b
@[inline] def foldrM [Monad m] (f : α → β → m β) (b : β) (v : Vector α n) : m β :=
v.toArray.foldrM f b
@[inline] def foldrM [Monad m] (f : α → β → m β) (b : β) (xs : Vector α n) : m β :=
xs.toArray.foldrM f b
@[inline] def foldl (f : β → α → β) (b : β) (v : Vector α n) : β :=
v.toArray.foldl f b
@[inline] def foldl (f : β → α → β) (b : β) (xs : Vector α n) : β :=
xs.toArray.foldl f b
@[inline] def foldr (f : α → β → β) (b : β) (v : Vector α n) : β :=
v.toArray.foldr f b
@[inline] def foldr (f : α → β → β) (b : β) (xs : Vector α n) : β :=
xs.toArray.foldr f b
/-- Append two vectors. -/
@[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) :=
v.toArray ++ w.toArray, by simp⟩
@[inline] def append (xs : Vector α n) (ys : Vector α m) : Vector α (n + m) :=
xs.toArray ++ ys.toArray, by simp⟩
instance : HAppend (Vector α n) (Vector α m) (Vector α (n + m)) where
hAppend := append
/-- Creates a vector from another with a provably equal length. -/
@[inline] protected def cast (h : n = m) (v : Vector α n) : Vector α m :=
v.toArray, by simp [*]⟩
@[inline] protected def cast (h : n = m) (xs : Vector α n) : Vector α m :=
xs.toArray, by simp [*]⟩
/--
Extracts the slice of a vector from indices `start` to `stop` (exclusive). If `start ≥ stop`, the
result is empty. If `stop` is greater than the size of the vector, the size is used instead.
-/
@[inline] def extract (v : Vector α n) (start : Nat := 0) (stop : Nat := n) : Vector α (min stop n - start) :=
v.toArray.extract start stop, by simp⟩
@[inline] def extract (xs : Vector α n) (start : Nat := 0) (stop : Nat := n) : Vector α (min stop n - start) :=
xs.toArray.extract start stop, by simp⟩
/--
Extract the first `m` elements of a vector. If `m` is greater than or equal to the size of the
Extract the first `i` elements of a vector. If `i` is greater than or equal to the size of the
vector then the vector is returned unchanged.
-/
@[inline] def take (v : Vector α n) (m : Nat) : Vector α (min m n) :=
v.toArray.take m, by simp⟩
@[inline] def take (xs : Vector α n) (i : Nat) : Vector α (min i n) :=
xs.toArray.take i, by simp⟩
@[simp] theorem take_eq_extract (v : Vector α n) (m : Nat) : v.take m = v.extract 0 m := rfl
@[simp] theorem take_eq_extract (xs : Vector α n) (i : Nat) : xs.take i = xs.extract 0 i := rfl
/--
Deletes the first `m` elements of a vector. If `m` is greater than or equal to the size of the
Deletes the first `i` elements of a vector. If `i` is greater than or equal to the size of the
vector then the empty vector is returned.
-/
@[inline] def drop (v : Vector α n) (m : Nat) : Vector α (n - m) :=
v.toArray.drop m, by simp⟩
@[inline] def drop (xs : Vector α n) (i : Nat) : Vector α (n - i) :=
xs.toArray.drop i, by simp⟩
@[simp] theorem drop_eq_cast_extract (v : Vector α n) (m : Nat) :
v.drop m = (v.extract m n).cast (by simp) := by
set_option linter.indexVariables false in
@[simp] theorem drop_eq_cast_extract (xs : Vector α n) (i : Nat) :
xs.drop i = (xs.extract i n).cast (by simp) := by
simp [drop, extract, Vector.cast]
/-- Shrinks a vector to the first `m` elements, by repeatedly popping the last element. -/
@[inline] def shrink (v : Vector α n) (m : Nat) : Vector α (min m n) :=
v.toArray.shrink m, by simp⟩
@[inline] def shrink (xs : Vector α n) (i : Nat) : Vector α (min i n) :=
xs.toArray.shrink i, by simp⟩
@[simp] theorem shrink_eq_take (v : Vector α n) (m : Nat) : v.shrink m = v.take m := by
@[simp] theorem shrink_eq_take (xs : Vector α n) (i : Nat) : xs.shrink i = xs.take i := by
simp [shrink, take]
/-- Maps elements of a vector using the function `f`. -/
@[inline] def map (f : α → β) (v : Vector α n) : Vector β n :=
v.toArray.map f, by simp⟩
@[inline] def map (f : α → β) (xs : Vector α n) : Vector β n :=
xs.toArray.map f, by simp⟩
/-- Maps elements of a vector using the function `f`, which also receives the index of the element. -/
@[inline] def mapIdx (f : Nat → α → β) (v : Vector α n) : Vector β n :=
v.toArray.mapIdx f, by simp⟩
@[inline] def mapIdx (f : Nat → α → β) (xs : Vector α n) : Vector β n :=
xs.toArray.mapIdx f, by simp⟩
/-- Maps elements of a vector using the function `f`,
which also receives the index of the element, and the fact that the index is less than the size of the vector. -/
@[inline] def mapFinIdx (v : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) : Vector β n :=
v.toArray.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h)), by simp⟩
@[inline] def mapFinIdx (xs : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) : Vector β n :=
xs.toArray.mapFinIdx (fun i a h => f i a (by simpa [xs.size_toArray] using h)), by simp⟩
/-- Map a monadic function over a vector. -/
@[inline] def mapM [Monad m] (f : α → m β) (v : Vector α n) : m (Vector β n) := do
@[inline] def mapM [Monad m] (f : α → m β) (xs : Vector α n) : m (Vector β n) := do
go 0 (Nat.zero_le n) #v[]
where
go (i : Nat) (h : i ≤ n) (r : Vector β i) : m (Vector β n) := do
if h' : i < n then
go (i+1) (by omega) (r.push (← f v[i]))
go (k : Nat) (h : k ≤ n) (acc : Vector β k) : m (Vector β n) := do
if h' : k < n then
go (k+1) (by omega) (acc.push (← f xs[k]))
else
return r.cast (by omega)
return acc.cast (by omega)
@[inline] protected def forM [Monad m] (v : Vector α n) (f : α → m PUnit) : m PUnit :=
v.toArray.forM f
@[inline] protected def forM [Monad m] (xs : Vector α n) (f : α → m PUnit) : m PUnit :=
xs.toArray.forM f
@[inline] def flatMapM [Monad m] (v : Vector α n) (f : α → m (Vector β k)) : m (Vector β (n * k)) := do
@[inline] def flatMapM [Monad m] (xs : Vector α n) (f : α → m (Vector β k)) : m (Vector β (n * k)) := do
go 0 (Nat.zero_le n) (#v[].cast (by omega))
where
go (i : Nat) (h : i ≤ n) (r : Vector β (i * k)) : m (Vector β (n * k)) := do
go (i : Nat) (h : i ≤ n) (acc : Vector β (i * k)) : m (Vector β (n * k)) := do
if h' : i < n then
go (i+1) (by omega) ((r ++ (← f v[i])).cast (Nat.succ_mul i k).symm)
go (i+1) (by omega) ((acc ++ (← f xs[i])).cast (Nat.succ_mul i k).symm)
else
return r.cast (by congr; omega)
return acc.cast (by congr; omega)
/-- Variant of `mapIdxM` which receives the index `i` along with the bound `i < n. -/
@[inline]
def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
(as : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) : m (Vector β n) :=
let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = n) (bs : Vector β (n - i)) : m (Vector β n) := do
(xs : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) : m (Vector β n) :=
let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = n) (ys : Vector β (n - i)) : m (Vector β n) := do
match i, inv with
| 0, _ => pure bs
| 0, _ => pure ys
| i+1, inv =>
have j_lt : j < n := by
rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
apply Nat.le_add_right
have : i + (j + 1) = n := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
map i (j+1) this ((bs.push (← f j as[j] j_lt)).cast (by omega))
map i (j+1) this ((ys.push (← f j xs[j] j_lt)).cast (by omega))
map n 0 rfl (#v[].cast (by simp))
@[inline]
def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Vector α n) : m (Vector β n) :=
as.mapFinIdxM fun i a _ => f i a
def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (xs : Vector α n) : m (Vector β n) :=
xs.mapFinIdxM fun i a _ => f i a
@[inline] def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Vector α n) : m β :=
as.toArray.firstM f
@[inline] def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (xs : Vector α n) : m β :=
xs.toArray.firstM f
@[inline] def flatten (v : Vector (Vector α n) m) : Vector α (m * n) :=
⟨(v.toArray.map Vector.toArray).flatten,
by rcases v; simp_all [Function.comp_def, Array.map_const']⟩
@[inline] def flatten (xs : Vector (Vector α n) m) : Vector α (m * n) :=
⟨(xs.toArray.map Vector.toArray).flatten,
by rcases xs; simp_all [Function.comp_def, Array.map_const']⟩
@[inline] def flatMap (v : Vector α n) (f : α → Vector β m) : Vector β (n * m) :=
v.toArray.flatMap fun a => (f a).toArray, by simp [Array.map_const']⟩
@[inline] def flatMap (xs : Vector α n) (f : α → Vector β m) : Vector β (n * m) :=
xs.toArray.flatMap fun a => (f a).toArray, by simp [Array.map_const']⟩
@[inline] def zipIdx (v : Vector α n) (k : Nat := 0) : Vector (α × Nat) n :=
v.toArray.zipIdx k, by simp⟩
@[inline] def zipIdx (xs : Vector α n) (k : Nat := 0) : Vector (α × Nat) n :=
xs.toArray.zipIdx k, by simp⟩
@[deprecated zipIdx (since := "2025-01-21")]
abbrev zipWithIndex := @zipIdx
@[inline] def zip (v : Vector α n) (w : Vector β n) : Vector (α × β) n :=
v.toArray.zip w.toArray, by simp⟩
@[inline] def zip (as : Vector α n) (bs : Vector β n) : Vector (α × β) n :=
as.toArray.zip bs.toArray, by simp⟩
/-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
@[inline] def zipWith (f : α → β → φ) (a : Vector α n) (b : Vector β n) : Vector φ n :=
⟨Array.zipWith f a.toArray b.toArray, by simp⟩
@[inline] def zipWith (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ n :=
as.toArray.zipWith f bs.toArray, by simp⟩
@[inline] def unzip (v : Vector (α × β) n) : Vector α n × Vector β n :=
⟨⟨v.toArray.unzip.1, by simp⟩, ⟨v.toArray.unzip.2, by simp⟩⟩
@[inline] def unzip (xs : Vector (α × β) n) : Vector α n × Vector β n :=
⟨⟨xs.toArray.unzip.1, by simp⟩, ⟨xs.toArray.unzip.2, by simp⟩⟩
/-- The vector of length `n` whose `i`-th element is `f i`. -/
@[inline] def ofFn (f : Fin n → α) : Vector α n :=
@ -289,17 +293,17 @@ Swap two elements of a vector using `Fin` indices.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def swap (v : Vector α n) (i j : Nat)
@[inline] def swap (xs : Vector α n) (i j : Nat)
(hi : i < n := by get_elem_tactic) (hj : j < n := by get_elem_tactic) : Vector α n :=
v.toArray.swap i j (by simpa using hi) (by simpa using hj), by simp⟩
xs.toArray.swap i j (by simpa using hi) (by simpa using hj), by simp⟩
/--
Swap two elements of a vector using `Nat` indices. Panics if either index is out of bounds.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def swapIfInBounds (v : Vector α n) (i j : Nat) : Vector α n :=
v.toArray.swapIfInBounds i j, by simp⟩
@[inline] def swapIfInBounds (xs : Vector α n) (i j : Nat) : Vector α n :=
xs.toArray.swapIfInBounds i j, by simp⟩
/--
Swaps an element of a vector with a given value using a `Fin` index. The original value is returned
@ -307,9 +311,9 @@ along with the updated vector.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def swapAt (v : Vector α n) (i : Nat) (x : α) (hi : i < n := by get_elem_tactic) :
@[inline] def swapAt (xs : Vector α n) (i : Nat) (x : α) (hi : i < n := by get_elem_tactic) :
α × Vector α n :=
let a := v.toArray.swapAt i x (by simpa using hi)
let a := xs.toArray.swapAt i x (by simpa using hi)
⟨a.fst, a.snd, by simp [a]⟩
/--
@ -318,8 +322,8 @@ bounds. The original value is returned along with the updated vector.
This will perform the update destructively provided that the vector has a reference count of 1.
-/
@[inline] def swapAt! (v : Vector α n) (i : Nat) (x : α) : α × Vector α n :=
let a := v.toArray.swapAt! i x
@[inline] def swapAt! (xs : Vector α n) (i : Nat) (x : α) : α × Vector α n :=
let a := xs.toArray.swapAt! i x
⟨a.fst, a.snd, by simp [a]⟩
/-- The vector `#v[0, 1, 2, ..., n-1]`. -/
@ -333,63 +337,63 @@ This will perform the update destructively provided that the vector has a refere
Compares two vectors of the same size using a given boolean relation `r`. `isEqv v w r` returns
`true` if and only if `r v[i] w[i]` is true for all indices `i`.
-/
@[inline] def isEqv (v w : Vector α n) (r : αα → Bool) : Bool :=
Array.isEqvAux v.toArray w.toArray (by simp) r n (by simp)
@[inline] def isEqv (xs ys : Vector α n) (r : αα → Bool) : Bool :=
Array.isEqvAux xs.toArray ys.toArray (by simp) r n (by simp)
instance [BEq α] : BEq (Vector α n) where
beq a b := isEqv a b (· == ·)
beq xs ys := isEqv xs ys (· == ·)
/-- Reverse the elements of a vector. -/
@[inline] def reverse (v : Vector α n) : Vector α n :=
v.toArray.reverse, by simp⟩
@[inline] def reverse (xs : Vector α n) : Vector α n :=
xs.toArray.reverse, by simp⟩
/-- Delete an element of a vector using a `Nat` index and a tactic provided proof. -/
@[inline] def eraseIdx (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
@[inline] def eraseIdx (xs : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
Vector α (n-1) :=
v.toArray.eraseIdx i (v.size_toArray.symm ▸ h), by simp [Array.size_eraseIdx]⟩
xs.toArray.eraseIdx i (xs.size_toArray.symm ▸ h), by simp [Array.size_eraseIdx]⟩
/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
@[inline] def eraseIdx! (xs : Vector α n) (i : Nat) : Vector α (n-1) :=
if _ : i < n then
v.eraseIdx i
xs.eraseIdx i
else
have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
have : Inhabited (Vector α (n-1)) := ⟨xs.pop⟩
panic! "index out of bounds"
/-- Insert an element into a vector using a `Nat` index and a tactic provided proof. -/
@[inline] def insertIdx (v : Vector α n) (i : Nat) (x : α) (h : i ≤ n := by get_elem_tactic) :
@[inline] def insertIdx (xs : Vector α n) (i : Nat) (x : α) (h : i ≤ n := by get_elem_tactic) :
Vector α (n+1) :=
v.toArray.insertIdx i x (v.size_toArray.symm ▸ h), by simp [Array.size_insertIdx]⟩
xs.toArray.insertIdx i x (xs.size_toArray.symm ▸ h), by simp [Array.size_insertIdx]⟩
/-- Insert an element into a vector using a `Nat` index. Panics if the index is out of bounds. -/
@[inline] def insertIdx! (v : Vector α n) (i : Nat) (x : α) : Vector α (n+1) :=
@[inline] def insertIdx! (xs : Vector α n) (i : Nat) (x : α) : Vector α (n+1) :=
if _ : i ≤ n then
v.insertIdx i x
xs.insertIdx i x
else
have : Inhabited (Vector α (n+1)) := ⟨v.push x⟩
have : Inhabited (Vector α (n+1)) := ⟨xs.push x⟩
panic! "index out of bounds"
/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
@[inline] def tail (v : Vector α n) : Vector α (n-1) :=
@[inline] def tail (xs : Vector α n) : Vector α (n-1) :=
if _ : 0 < n then
v.eraseIdx 0
xs.eraseIdx 0
else
v.cast (by omega)
xs.cast (by omega)
/--
Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
no element of the index matches the given value.
-/
@[inline] def finIdxOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
(v.toArray.finIdxOf? x).map (Fin.cast v.size_toArray)
@[inline] def finIdxOf? [BEq α] (xs : Vector α n) (x : α) : Option (Fin n) :=
(xs.toArray.finIdxOf? x).map (Fin.cast xs.size_toArray)
@[deprecated finIdxOf? (since := "2025-01-29")]
abbrev indexOf? := @finIdxOf?
/-- Finds the first index of a given value in a vector using a predicate. Returns `none` if the
no element of the index matches the given value. -/
@[inline] def findFinIdx? (p : α → Bool) (v : Vector α n) : Option (Fin n) :=
(v.toArray.findFinIdx? p).map (Fin.cast v.size_toArray)
@[inline] def findFinIdx? (p : α → Bool) (xs : Vector α n) : Option (Fin n) :=
(xs.toArray.findFinIdx? p).map (Fin.cast xs.size_toArray)
/--
Note that the universe level is contrained to `Type` here,
@ -423,41 +427,41 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
@[inline] def findSomeRev? (f : α → Option β) (as : Vector α n) : Option β :=
as.toArray.findSomeRev? f
/-- Returns `true` when `v` is a prefix of the vector `w`. -/
@[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
v.toArray.isPrefixOf w.toArray
/-- Returns `true` when `xs` is a prefix of the vector `ys`. -/
@[inline] def isPrefixOf [BEq α] (xs : Vector α m) (ys : Vector α n) : Bool :=
xs.toArray.isPrefixOf ys.toArray
/-- Returns `true` with the monad if `p` returns `true` for any element of the vector. -/
@[inline] def anyM [Monad m] (p : α → m Bool) (v : Vector α n) : m Bool :=
v.toArray.anyM p
@[inline] def anyM [Monad m] (p : α → m Bool) (xs : Vector α n) : m Bool :=
xs.toArray.anyM p
/-- Returns `true` with the monad if `p` returns `true` for all elements of the vector. -/
@[inline] def allM [Monad m] (p : α → m Bool) (v : Vector α n) : m Bool :=
v.toArray.allM p
@[inline] def allM [Monad m] (p : α → m Bool) (xs : Vector α n) : m Bool :=
xs.toArray.allM p
/-- Returns `true` if `p` returns `true` for any element of the vector. -/
@[inline] def any (v : Vector α n) (p : α → Bool) : Bool :=
v.toArray.any p
@[inline] def any (xs : Vector α n) (p : α → Bool) : Bool :=
xs.toArray.any p
/-- Returns `true` if `p` returns `true` for all elements of the vector. -/
@[inline] def all (v : Vector α n) (p : α → Bool) : Bool :=
v.toArray.all p
@[inline] def all (xs : Vector α n) (p : α → Bool) : Bool :=
xs.toArray.all p
/-- Count the number of elements of a vector that satisfy the predicate `p`. -/
@[inline] def countP (p : α → Bool) (v : Vector α n) : Nat :=
v.toArray.countP p
@[inline] def countP (p : α → Bool) (xs : Vector α n) : Nat :=
xs.toArray.countP p
/-- Count the number of elements of a vector that are equal to `a`. -/
@[inline] def count [BEq α] (a : α) (v : Vector α n) : Nat :=
v.toArray.count a
@[inline] def count [BEq α] (a : α) (xs : Vector α n) : Nat :=
xs.toArray.count a
/-! ### ForIn instance -/
@[simp] theorem mem_toArray_iff (a : α) (v : Vector α n) : a ∈ v.toArray ↔ a ∈ v :=
@[simp] theorem mem_toArray_iff (a : α) (xs : Vector α n) : a ∈ xs.toArray ↔ a ∈ xs :=
⟨fun h => ⟨h⟩, fun ⟨h⟩ => h⟩
instance : ForIn' m (Vector α n) α inferInstance where
forIn' v b f := Array.forIn' v.toArray b (fun a h b => f a (by simpa using h) b)
forIn' xs b f := Array.forIn' xs.toArray b (fun a h b => f a (by simpa using h) b)
/-! ### ForM instance -/
@ -471,12 +475,12 @@ instance : ForM m (Vector α n) α where
/-! ### ToStream instance -/
instance : ToStream (Vector α n) (Subarray α) where
toStream v := v.toArray[:n]
toStream xs := xs.toArray[:n]
/-! ### Lexicographic ordering -/
instance instLT [LT α] : LT (Vector α n) := ⟨fun v w => v.toArray < w.toArray⟩
instance instLE [LT α] : LE (Vector α n) := ⟨fun v w => v.toArray ≤ w.toArray⟩
instance instLT [LT α] : LT (Vector α n) := ⟨fun xs ys => xs.toArray < ys.toArray⟩
instance instLE [LT α] : LE (Vector α n) := ⟨fun xs ys => xs.toArray ≤ ys.toArray⟩
/--
Lexicographic comparator for vectors.
@ -485,10 +489,10 @@ Lexicographic comparator for vectors.
- `v` is pairwise equivalent via `==` to `w`, or
- there is an index `i` such that `lt v[i] w[i]`, and for all `j < i`, `v[j] == w[j]`.
-/
def lex [BEq α] (v w : Vector α n) (lt : αα → Bool := by exact (· < ·)) : Bool := Id.run do
def lex [BEq α] (xs ys : Vector α n) (lt : αα → Bool := by exact (· < ·)) : Bool := Id.run do
for h : i in [0 : n] do
if lt v[i] w[i] then
if lt xs[i] ys[i] then
return true
else if v[i] != w[i] then
else if xs[i] != ys[i] then
return false
return false

View file

@ -11,6 +11,9 @@ import Init.Data.Vector.Lemmas
# Lemmas about `Vector.countP` and `Vector.count`.
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
open Nat
@ -22,51 +25,51 @@ variable (p q : α → Bool)
@[simp] theorem countP_empty : countP p #v[] = 0 := rfl
@[simp] theorem countP_push_of_pos (l : Vector α n) (pa : p a) : countP p (l.push a) = countP p l + 1 := by
rcases l with ⟨l⟩
@[simp] theorem countP_push_of_pos (xs : Vector α n) (pa : p a) : countP p (xs.push a) = countP p xs + 1 := by
rcases xs with ⟨xs, rfl⟩
simp_all
@[simp] theorem countP_push_of_neg (l : Vector α n) (pa : ¬p a) : countP p (l.push a) = countP p l := by
rcases l with ⟨l, rfl⟩
@[simp] theorem countP_push_of_neg (xs : Vector α n) (pa : ¬p a) : countP p (xs.push a) = countP p xs := by
rcases xs with ⟨xs, rfl⟩
simp_all
theorem countP_push (a : α) (l : Vector α n) : countP p (l.push a) = countP p l + if p a then 1 else 0 := by
rcases l with ⟨l, rfl⟩
theorem countP_push (a : α) (xs : Vector α n) : countP p (xs.push a) = countP p xs + if p a then 1 else 0 := by
rcases xs with ⟨xs, rfl⟩
simp [Array.countP_push]
@[simp] theorem countP_singleton (a : α) : countP p #v[a] = if p a then 1 else 0 := by
simp [countP_push]
theorem size_eq_countP_add_countP (l : Vector α n) : n = countP p l + countP (fun a => ¬p a) l := by
rcases l with ⟨l, rfl⟩
theorem size_eq_countP_add_countP (xs : Vector α n) : n = countP p xs + countP (fun a => ¬p a) xs := by
rcases xs with ⟨xs, rfl⟩
simp [List.length_eq_countP_add_countP (p := p)]
theorem countP_le_size {l : Vector α n} : countP p l ≤ n := by
rcases l with ⟨l, rfl⟩
theorem countP_le_size {xs : Vector α n} : countP p xs ≤ n := by
rcases xs with ⟨xs, rfl⟩
simp [Array.countP_le_size (p := p)]
@[simp] theorem countP_append (l₁ : Vector α n) (l₂ : Vector α m) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
cases l₁
cases l₂
@[simp] theorem countP_append (xs : Vector α n) (ys : Vector α m) : countP p (xs ++ ys) = countP p xs + countP p ys := by
cases xs
cases ys
simp
@[simp] theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by
cases l
@[simp] theorem countP_pos_iff {p} : 0 < countP p xs ↔ ∃ a ∈ xs, p a := by
cases xs
simp
@[simp] theorem one_le_countP_iff {p} : 1 ≤ countP p l ↔ ∃ a ∈ l, p a :=
@[simp] theorem one_le_countP_iff {p} : 1 ≤ countP p xs ↔ ∃ a ∈ xs, p a :=
countP_pos_iff
@[simp] theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
cases l
@[simp] theorem countP_eq_zero {p} : countP p xs = 0 ↔ ∀ a ∈ xs, ¬p a := by
cases xs
simp
@[simp] theorem countP_eq_size {p} : countP p l = l.size ↔ ∀ a ∈ l, p a := by
cases l
@[simp] theorem countP_eq_size {p} : countP p xs = xs.size ↔ ∀ a ∈ xs, p a := by
cases xs
simp
@[simp] theorem countP_cast (p : α → Bool) (l : Vector α n) : countP p (l.cast h) = countP p l := by
rcases l with ⟨l, rfl⟩
@[simp] theorem countP_cast (p : α → Bool) (xs : Vector α n) : countP p (xs.cast h) = countP p xs := by
rcases xs with ⟨xs, rfl⟩
simp
theorem countP_mkVector (p : α → Bool) (a : α) (n : Nat) :
@ -74,51 +77,51 @@ theorem countP_mkVector (p : α → Bool) (a : α) (n : Nat) :
simp only [mkVector_eq_mk_mkArray, countP_cast, countP_mk]
simp [Array.countP_mkArray]
theorem boole_getElem_le_countP (p : α → Bool) (l : Vector α n) (i : Nat) (h : i < n) :
(if p l[i] then 1 else 0) ≤ l.countP p := by
rcases l with ⟨l, rfl⟩
theorem boole_getElem_le_countP (p : α → Bool) (xs : Vector α n) (i : Nat) (h : i < n) :
(if p xs[i] then 1 else 0) ≤ xs.countP p := by
rcases xs with ⟨xs, rfl⟩
simp [Array.boole_getElem_le_countP]
theorem countP_set (p : α → Bool) (l : Vector α n) (i : Nat) (a : α) (h : i < n) :
(l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0) := by
cases l
theorem countP_set (p : α → Bool) (xs : Vector α n) (i : Nat) (a : α) (h : i < n) :
(xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.countP_set, h]
@[simp] theorem countP_true : (countP fun (_ : α) => true) = (fun (_ : Vector α n) => n) := by
funext l
funext xs
rw [countP]
simp only [Array.countP_true, l.2]
simp only [Array.countP_true, xs.2]
@[simp] theorem countP_false : (countP fun (_ : α) => false) = (fun (_ : Vector α n) => 0) := by
funext l
funext xs
simp
@[simp] theorem countP_map (p : β → Bool) (f : α → β) (l : Vector α n) :
countP p (map f l) = countP (p ∘ f) l := by
rcases l with ⟨l, rfl⟩
@[simp] theorem countP_map (p : β → Bool) (f : α → β) (xs : Vector α n) :
countP p (map f xs) = countP (p ∘ f) xs := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem countP_flatten (l : Vector (Vector α m) n) :
countP p l.flatten = (l.map (countP p)).sum := by
rcases l with ⟨l, rfl⟩
@[simp] theorem countP_flatten (xss : Vector (Vector α m) n) :
countP p xss.flatten = (xss.map (countP p)).sum := by
rcases xss with ⟨xss, rfl⟩
simp [Function.comp_def]
theorem countP_flatMap (p : β → Bool) (l : Vector α n) (f : α → Vector β m) :
countP p (l.flatMap f) = (map (countP p ∘ f) l).sum := by
rcases l with ⟨l, rfl⟩
theorem countP_flatMap (p : β → Bool) (xs : Vector α n) (f : α → Vector β m) :
countP p (xs.flatMap f) = (map (countP p ∘ f) xs).sum := by
rcases xs with ⟨xs, rfl⟩
simp [Array.countP_flatMap, Function.comp_def]
@[simp] theorem countP_reverse (l : Vector α n) : countP p l.reverse = countP p l := by
cases l
@[simp] theorem countP_reverse (xs : Vector α n) : countP p xs.reverse = countP p xs := by
rcases xs with ⟨xs, rfl⟩
simp
variable {p q}
theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
cases l
theorem countP_mono_left (h : ∀ x ∈ xs, p x → q x) : countP p xs ≤ countP q xs := by
rcases xs with ⟨xs, rfl⟩
simpa using Array.countP_mono_left (by simpa using h)
theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l :=
theorem countP_congr (h : ∀ x ∈ xs, p x ↔ q x) : countP p xs = countP q xs :=
Nat.le_antisymm
(countP_mono_left fun x hx => (h x hx).1)
(countP_mono_left fun x hx => (h x hx).2)
@ -132,84 +135,84 @@ variable [BEq α]
@[simp] theorem count_empty (a : α) : count a #v[] = 0 := rfl
theorem count_push (a b : α) (l : Vector α n) :
count a (l.push b) = count a l + if b == a then 1 else 0 := by
rcases l with ⟨l, rfl⟩
theorem count_push (a b : α) (xs : Vector α n) :
count a (xs.push b) = count a xs + if b == a then 1 else 0 := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_push]
theorem count_eq_countP (a : α) (l : Vector α n) : count a l = countP (· == a) l := rfl
theorem count_eq_countP (a : α) (xs : Vector α n) : count a xs = countP (· == a) xs := rfl
theorem count_eq_countP' {a : α} : count (n := n) a = countP (· == a) := by
funext l
funext xs
apply count_eq_countP
theorem count_le_size (a : α) (l : Vector α n) : count a l ≤ n := countP_le_size _
theorem count_le_size (a : α) (xs : Vector α n) : count a xs ≤ n := countP_le_size _
theorem count_le_count_push (a b : α) (l : Vector α n) : count a l ≤ count a (l.push b) := by
rcases l with ⟨l, rfl⟩
theorem count_le_count_push (a b : α) (xs : Vector α n) : count a xs ≤ count a (xs.push b) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_push]
@[simp] theorem count_singleton (a b : α) : count a #v[b] = if b == a then 1 else 0 := by
simp [count_eq_countP]
@[simp] theorem count_append (a : α) (l₁ : Vector α n) (l₂ : Vector α m) :
count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
@[simp] theorem count_append (a : α) (xs : Vector α n) (ys : Vector α m) :
count a (xs ++ ys) = count a xs + count a ys :=
countP_append ..
@[simp] theorem count_flatten (a : α) (l : Vector (Vector α m) n) :
count a l.flatten = (l.map (count a)).sum := by
rcases l with ⟨l, rfl⟩
@[simp] theorem count_flatten (a : α) (xss : Vector (Vector α m) n) :
count a xss.flatten = (xss.map (count a)).sum := by
rcases xss with ⟨xss, rfl⟩
simp [Array.count_flatten, Function.comp_def]
@[simp] theorem count_reverse (a : α) (l : Vector α n) : count a l.reverse = count a l := by
rcases l with ⟨l, rfl⟩
@[simp] theorem count_reverse (a : α) (xs : Vector α n) : count a xs.reverse = count a xs := by
rcases xs with ⟨xs, rfl⟩
simp
theorem boole_getElem_le_count (a : α) (l : Vector α n) (i : Nat) (h : i < n) :
(if l[i] == a then 1 else 0) ≤ l.count a := by
rcases l with ⟨l, rfl⟩
theorem boole_getElem_le_count (a : α) (xs : Vector α n) (i : Nat) (h : i < n) :
(if xs[i] == a then 1 else 0) ≤ xs.count a := by
rcases xs with ⟨xs, rfl⟩
simp [Array.boole_getElem_le_count, h]
theorem count_set (a b : α) (l : Vector α n) (i : Nat) (h : i < n) :
(l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
rcases l with ⟨l, rfl⟩
theorem count_set (a b : α) (xs : Vector α n) (i : Nat) (h : i < n) :
(xs.set i a).count b = xs.count b - (if xs[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_set, h]
@[simp] theorem count_cast (l : Vector α n) : (l.cast h).count a = l.count a := by
rcases l with ⟨l, rfl⟩
@[simp] theorem count_cast (xs : Vector α n) : (xs.cast h).count a = xs.count a := by
rcases xs with ⟨xs, rfl⟩
simp
variable [LawfulBEq α]
@[simp] theorem count_push_self (a : α) (l : Vector α n) : count a (l.push a) = count a l + 1 := by
rcases l with ⟨l, rfl⟩
@[simp] theorem count_push_self (a : α) (xs : Vector α n) : count a (xs.push a) = count a xs + 1 := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_push_self]
@[simp] theorem count_push_of_ne (h : b ≠ a) (l : Vector α n) : count a (l.push b) = count a l := by
rcases l with ⟨l, rfl⟩
@[simp] theorem count_push_of_ne (h : b ≠ a) (xs : Vector α n) : count a (xs.push b) = count a xs := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_push_of_ne, h]
theorem count_singleton_self (a : α) : count a #v[a] = 1 := by simp
@[simp]
theorem count_pos_iff {a : α} {l : Vector α n} : 0 < count a l ↔ a ∈ l := by
rcases l with ⟨l, rfl⟩
theorem count_pos_iff {a : α} {xs : Vector α n} : 0 < count a xs ↔ a ∈ xs := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_pos_iff, beq_iff_eq, exists_eq_right]
@[simp] theorem one_le_count_iff {a : α} {l : Vector α n} : 1 ≤ count a l ↔ a ∈ l :=
@[simp] theorem one_le_count_iff {a : α} {xs : Vector α n} : 1 ≤ count a xs ↔ a ∈ xs :=
count_pos_iff
theorem count_eq_zero_of_not_mem {a : α} {l : Vector α n} (h : a ∉ l) : count a l = 0 :=
theorem count_eq_zero_of_not_mem {a : α} {xs : Vector α n} (h : a ∉ xs) : count a xs = 0 :=
Decidable.byContradiction fun h' => h <| count_pos_iff.1 (Nat.pos_of_ne_zero h')
theorem not_mem_of_count_eq_zero {a : α} {l : Vector α n} (h : count a l = 0) : a ∉ l :=
theorem not_mem_of_count_eq_zero {a : α} {xs : Vector α n} (h : count a xs = 0) : a ∉ xs :=
fun h' => Nat.ne_of_lt (count_pos_iff.2 h') h.symm
theorem count_eq_zero {l : Vector α n} : count a l = 0 ↔ a ∉ l :=
theorem count_eq_zero {xs : Vector α n} : count a xs = 0 ↔ a ∉ xs :=
⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩
theorem count_eq_size {l : Vector α n} : count a l = l.size ↔ ∀ b ∈ l, a = b := by
rcases l with ⟨l, rfl⟩
theorem count_eq_size {xs : Vector α n} : count a xs = xs.size ↔ ∀ b ∈ xs, a = b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_eq_size]
@[simp] theorem count_mkVector_self (a : α) (n : Nat) : count a (mkVector n a) = n := by
@ -220,14 +223,14 @@ theorem count_mkVector (a b : α) (n : Nat) : count a (mkVector n b) = if b == a
simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]
simp [Array.count_mkArray]
theorem count_le_count_map [DecidableEq β] (l : Vector α n) (f : α → β) (x : α) :
count x l ≤ count (f x) (map f l) := by
rcases l with ⟨l, rfl⟩
theorem count_le_count_map [DecidableEq β] (xs : Vector α n) (f : α → β) (x : α) :
count x xs ≤ count (f x) (map f xs) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_le_count_map]
theorem count_flatMap {α} [BEq β] (l : Vector α n) (f : α → Vector β m) (x : β) :
count x (l.flatMap f) = (map (count x ∘ f) l).sum := by
rcases l with ⟨l, rfl⟩
theorem count_flatMap {α} [BEq β] (xs : Vector α n) (f : α → Vector β m) (x : β) :
count x (xs.flatMap f) = (map (count x ∘ f) xs).sum := by
rcases xs with ⟨xs, rfl⟩
simp [Array.count_flatMap, Function.comp_def]
end count

View file

@ -7,62 +7,65 @@ prelude
import Init.Data.Array.DecidableEq
import Init.Data.Vector.Lemmas
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
theorem isEqv_iff_rel {a b : Vector α n} {r} :
Vector.isEqv a b r ↔ ∀ (i : Nat) (h' : i < n), r a[i] b[i] := by
rcases a with ⟨a, rfl⟩
rcases b with ⟨b, h⟩
theorem isEqv_iff_rel {xs ys : Vector α n} {r} :
Vector.isEqv xs ys r ↔ ∀ (i : Nat) (h' : i < n), r xs[i] ys[i] := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, h⟩
simp [Array.isEqv_iff_rel, h]
theorem isEqv_eq_decide (a b : Vector α n) (r) :
Vector.isEqv a b r = decide (∀ (i : Nat) (h' : i < n), r a[i] b[i]) := by
rcases a with ⟨a, rfl⟩
rcases b with ⟨b, h⟩
theorem isEqv_eq_decide (xs ys : Vector α n) (r) :
Vector.isEqv xs ys r = decide (∀ (i : Nat) (h' : i < n), r xs[i] ys[i]) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, h⟩
simp [Array.isEqv_eq_decide, h]
@[simp] theorem isEqv_toArray [BEq α] (a b : Vector α n) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
@[simp] theorem isEqv_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray.isEqv ys.toArray r) = (xs.isEqv ys r) := by
simp [isEqv_eq_decide, Array.isEqv_eq_decide]
theorem eq_of_isEqv [DecidableEq α] (a b : Vector α n) (h : Vector.isEqv a b (fun x y => x = y)) : a = b := by
rcases a with ⟨a, rfl⟩
rcases b with ⟨b, h⟩
theorem eq_of_isEqv [DecidableEq α] (xs ys : Vector α n) (h : Vector.isEqv xs ys (fun x y => x = y)) : xs = ys := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, h⟩
rw [← Vector.toArray_inj]
apply Array.eq_of_isEqv
simp_all
theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Vector α n) : Vector.isEqv a a (· == ·) = true := by
rcases a with ⟨a, rfl⟩
theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Vector α n) : Vector.isEqv xs xs (· == ·) = true := by
rcases xs with ⟨xs, rfl⟩
simp [Array.isEqv_self_beq]
theorem isEqv_self [DecidableEq α] (a : Vector α n) : Vector.isEqv a a (· = ·) = true := by
rcases a with ⟨a, rfl⟩
theorem isEqv_self [DecidableEq α] (xs : Vector α n) : Vector.isEqv xs xs (· = ·) = true := by
rcases xs with ⟨xs, rfl⟩
simp [Array.isEqv_self]
instance [DecidableEq α] : DecidableEq (Vector α n) :=
fun a b =>
match h:isEqv a b (fun a b => a = b) with
| true => isTrue (eq_of_isEqv a b h)
fun xs ys =>
match h:isEqv xs ys (fun x y => x = y) with
| true => isTrue (eq_of_isEqv xs ys h)
| false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
theorem beq_eq_decide [BEq α] (a b : Vector α n) :
(a == b) = decide (∀ (i : Nat) (h' : i < n), a[i] == b[i]) := by
theorem beq_eq_decide [BEq α] (xs ys : Vector α n) :
(xs == ys) = decide (∀ (i : Nat) (h' : i < n), xs[i] == ys[i]) := by
simp [BEq.beq, isEqv_eq_decide]
@[simp] theorem beq_mk [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
(mk a ha == mk b hb) = (a == b) := by
@[simp] theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) :
(mk xs ha == mk ys hb) = (xs == ys) := by
simp [BEq.beq]
@[simp] theorem beq_toArray [BEq α] (a b : Vector α n) : (a.toArray == b.toArray) = (a == b) := by
@[simp] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
simp [beq_eq_decide, Array.beq_eq_decide]
@[simp] theorem beq_toList [BEq α] (a b : Vector α n) : (a.toList == b.toList) = (a == b) := by
@[simp] theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by
simp [beq_eq_decide, List.beq_eq_decide]
instance [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n) where
rfl := by simp [BEq.beq, isEqv_self_beq]
eq_of_beq := by
rintro ⟨a, rfl⟩ ⟨b, h⟩ h'
rintro ⟨xs, rfl⟩ ⟨ys, h⟩ h'
simpa using h'
end Vector

View file

@ -11,59 +11,62 @@ import Init.Data.Array.Erase
# Lemmas about `Vector.eraseIdx`.
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
open Nat
/-! ### eraseIdx -/
theorem eraseIdx_eq_take_drop_succ (l : Vector α n) (i : Nat) (h) :
l.eraseIdx i = (l.take i ++ l.drop (i + 1)).cast (by omega) := by
rcases l with ⟨l, rfl⟩
theorem eraseIdx_eq_take_drop_succ (xs : Vector α n) (i : Nat) (h) :
xs.eraseIdx i = (xs.take i ++ xs.drop (i + 1)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.eraseIdx_eq_take_drop_succ, *]
theorem getElem?_eraseIdx (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) :
(l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]? := by
rcases l with ⟨l, rfl⟩
theorem getElem?_eraseIdx (xs : Vector α n) (i : Nat) (h : i < n) (j : Nat) :
(xs.eraseIdx i)[j]? = if j < i then xs[j]? else xs[j + 1]? := by
rcases xs with ⟨xs, rfl⟩
simp [Array.getElem?_eraseIdx]
theorem getElem?_eraseIdx_of_lt (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < i) :
(l.eraseIdx i)[j]? = l[j]? := by
theorem getElem?_eraseIdx_of_lt (xs : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < i) :
(xs.eraseIdx i)[j]? = xs[j]? := by
rw [getElem?_eraseIdx]
simp [h']
theorem getElem?_eraseIdx_of_ge (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : i ≤ j) :
(l.eraseIdx i)[j]? = l[j + 1]? := by
theorem getElem?_eraseIdx_of_ge (xs : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : i ≤ j) :
(xs.eraseIdx i)[j]? = xs[j + 1]? := by
rw [getElem?_eraseIdx]
simp only [dite_eq_ite, ite_eq_right_iff]
intro h'
omega
theorem getElem_eraseIdx (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < n - 1) :
(l.eraseIdx i)[j] = if h'' : j < i then l[j] else l[j + 1] := by
theorem getElem_eraseIdx (xs : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < n - 1) :
(xs.eraseIdx i)[j] = if h'' : j < i then xs[j] else xs[j + 1] := by
apply Option.some.inj
rw [← getElem?_eq_getElem, getElem?_eraseIdx]
split <;> simp
theorem mem_of_mem_eraseIdx {l : Vector α n} {i : Nat} {h} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l := by
rcases l with ⟨l, rfl⟩
theorem mem_of_mem_eraseIdx {xs : Vector α n} {i : Nat} {h} {a : α} (h : a ∈ xs.eraseIdx i) : a ∈ xs := by
rcases xs with ⟨xs, rfl⟩
simpa using Array.mem_of_mem_eraseIdx (by simpa using h)
theorem eraseIdx_append_of_lt_size {l : Vector α n} {k : Nat} (hk : k < n) (l' : Vector α n) (h) :
eraseIdx (l ++ l') k = (eraseIdx l k ++ l').cast (by omega) := by
rcases l with ⟨l
rcases l' with ⟨l'⟩
theorem eraseIdx_append_of_lt_size {xs : Vector α n} {k : Nat} (hk : k < n) (xs' : Vector α n) (h) :
eraseIdx (xs ++ xs') k = (eraseIdx xs k ++ xs').cast (by omega) := by
rcases xs with ⟨xs
rcases xs' with ⟨xs'⟩
simp [Array.eraseIdx_append_of_lt_size, *]
theorem eraseIdx_append_of_length_le {l : Vector α n} {k : Nat} (hk : n ≤ k) (l' : Vector α n) (h) :
eraseIdx (l ++ l') k = (l ++ eraseIdx l' (k - n)).cast (by omega) := by
rcases l with ⟨l
rcases l' with ⟨l'⟩
theorem eraseIdx_append_of_length_le {xs : Vector α n} {k : Nat} (hk : n ≤ k) (xs' : Vector α n) (h) :
eraseIdx (xs ++ xs') k = (xs ++ eraseIdx xs' (k - n)).cast (by omega) := by
rcases xs with ⟨xs
rcases xs' with ⟨xs'⟩
simp [Array.eraseIdx_append_of_length_le, *]
theorem eraseIdx_cast {l : Vector α n} {k : Nat} (h : k < m) :
eraseIdx (l.cast w) k h = (eraseIdx l k).cast (by omega) := by
rcases l with ⟨l, rfl
theorem eraseIdx_cast {xs : Vector α n} {k : Nat} (h : k < m) :
eraseIdx (xs.cast w) k h = (eraseIdx xs k).cast (by omega) := by
rcases xs with ⟨xs
simp
theorem eraseIdx_mkVector {n : Nat} {a : α} {k : Nat} {h} :
@ -71,43 +74,43 @@ theorem eraseIdx_mkVector {n : Nat} {a : α} {k : Nat} {h} :
rw [mkVector_eq_mk_mkArray, eraseIdx_mk]
simp [Array.eraseIdx_mkArray, *]
theorem mem_eraseIdx_iff_getElem {x : α} {l : Vector α n} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i w, i ≠ k ∧ l[i]'w = x := by
rcases l with ⟨l, rfl
theorem mem_eraseIdx_iff_getElem {x : α} {xs : Vector α n} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
rcases xs with ⟨xs
simp [Array.mem_eraseIdx_iff_getElem, *]
theorem mem_eraseIdx_iff_getElem? {x : α} {l : Vector α n} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i ≠ k, l[i]? = some x := by
rcases l with ⟨l, rfl
theorem mem_eraseIdx_iff_getElem? {x : α} {xs : Vector α n} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i ≠ k, xs[i]? = some x := by
rcases xs with ⟨xs
simp [Array.mem_eraseIdx_iff_getElem?, *]
theorem getElem_eraseIdx_of_lt (l : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : j < i) :
(l.eraseIdx i)[j] = l[j] := by
rcases l with ⟨l, rfl
theorem getElem_eraseIdx_of_lt (xs : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : j < i) :
(xs.eraseIdx i)[j] = xs[j] := by
rcases xs with ⟨xs
simp [Array.getElem_eraseIdx_of_lt, *]
theorem getElem_eraseIdx_of_ge (l : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : i ≤ j) :
(l.eraseIdx i)[j] = l[j + 1] := by
rcases l with ⟨l, rfl
theorem getElem_eraseIdx_of_ge (xs : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : i ≤ j) :
(xs.eraseIdx i)[j] = xs[j + 1] := by
rcases xs with ⟨xs
simp [Array.getElem_eraseIdx_of_ge, *]
theorem eraseIdx_set_eq {l : Vector α n} {i : Nat} {a : α} {h : i < n} :
(l.set i a).eraseIdx i = l.eraseIdx i := by
rcases l with ⟨l, rfl
theorem eraseIdx_set_eq {xs : Vector α n} {i : Nat} {a : α} {h : i < n} :
(xs.set i a).eraseIdx i = xs.eraseIdx i := by
rcases xs with ⟨xs
simp [Array.eraseIdx_set_eq, *]
theorem eraseIdx_set_lt {l : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) :
(l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
rcases l with ⟨l, rfl
theorem eraseIdx_set_lt {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) :
(xs.set i a).eraseIdx j = (xs.eraseIdx j).set (i - 1) a := by
rcases xs with ⟨xs
simp [Array.eraseIdx_set_lt, *]
theorem eraseIdx_set_gt {l : Vector α n} {i : Nat} {j : Nat} {a : α} (h : i < j) {w : j < n} :
(l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
rcases l with ⟨l, rfl
theorem eraseIdx_set_gt {xs : Vector α n} {i : Nat} {j : Nat} {a : α} (h : i < j) {w : j < n} :
(xs.set i a).eraseIdx j = (xs.eraseIdx j).set i a := by
rcases xs with ⟨xs
simp [Array.eraseIdx_set_gt, *]
@[simp] theorem set_getElem_succ_eraseIdx_succ
{l : Vector α n} {i : Nat} (h : i + 1 < n) :
(l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
rcases l with ⟨l, rfl
simp [List.set_getElem_succ_eraseIdx_succ, *]
{xs : Vector α n} {i : Nat} (h : i + 1 < n) :
(xs.eraseIdx (i + 1)).set i xs[i + 1] = xs.eraseIdx i := by
rcases xs with ⟨xs
simp [Array.set_getElem_succ_eraseIdx_succ, *]
end Vector

View file

@ -11,59 +11,64 @@ import Init.Data.Array.Extract
# Lemmas about `Vector.extract`
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
open Nat
namespace Vector
/-! ### extract -/
@[simp] theorem extract_of_size_lt {as : Vector α n} {i j : Nat} (h : n < j) :
as.extract i j = (as.extract i n).cast (by omega) := by
rcases as with ⟨as, rfl⟩
set_option linter.indexVariables false
@[simp] theorem extract_of_size_lt {xs : Vector α n} {i j : Nat} (h : n < j) :
xs.extract i j = (xs.extract i n).cast (by omega) := by
rcases xs with ⟨as, rfl⟩
simp [h]
@[simp]
theorem extract_push {as : Vector α n} {b : α} {start stop : Nat} (h : stop ≤ n) :
(as.push b).extract start stop = (as.extract start stop).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem extract_push {xs : Vector α n} {b : α} {start stop : Nat} (h : stop ≤ n) :
(xs.push b).extract start stop = (xs.extract start stop).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [h]
@[simp]
theorem extract_eq_pop {as : Vector α n} {stop : Nat} (h : stop = n - 1) :
as.extract 0 stop = as.pop.cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem extract_eq_pop {xs : Vector α n} {stop : Nat} (h : stop = n - 1) :
xs.extract 0 stop = xs.pop.cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [h]
@[simp]
theorem extract_append_extract {as : Vector α n} {i j k : Nat} :
as.extract i j ++ as.extract j k =
(as.extract (min i j) (max j k)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem extract_append_extract {xs : Vector α n} {i j k : Nat} :
xs.extract i j ++ xs.extract j k =
(xs.extract (min i j) (max j k)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp]
theorem push_extract_getElem {as : Vector α n} {i j : Nat} (h : j < n) :
(as.extract i j).push as[j] = (as.extract (min i j) (j + 1)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem push_extract_getElem {xs : Vector α n} {i j : Nat} (h : j < n) :
(xs.extract i j).push xs[j] = (xs.extract (min i j) (j + 1)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [h]
theorem extract_succ_right {as : Vector α n} {i j : Nat} (w : i < j + 1) (h : j < n) :
as.extract i (j + 1) = ((as.extract i j).push as[j]).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem extract_succ_right {xs : Vector α n} {i j : Nat} (w : i < j + 1) (h : j < n) :
xs.extract i (j + 1) = ((xs.extract i j).push xs[j]).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.extract_succ_right, w, h]
theorem extract_sub_one {as : Vector α n} {i j : Nat} (h : j < n) :
as.extract i (j - 1) = (as.extract i j).pop.cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem extract_sub_one {xs : Vector α n} {i j : Nat} (h : j < n) :
xs.extract i (j - 1) = (xs.extract i j).pop.cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.extract_sub_one, h]
@[simp]
theorem getElem?_extract_of_lt {as : Vector α n} {i j k : Nat} (h : k < min j n - i) :
(as.extract i j)[k]? = some (as[i + k]'(by omega)) := by
theorem getElem?_extract_of_lt {xs : Vector α n} {i j k : Nat} (h : k < min j n - i) :
(xs.extract i j)[k]? = some (xs[i + k]'(by omega)) := by
rcases xs with ⟨xs, rfl⟩
simp [getElem?_extract, h]
theorem getElem?_extract_of_succ {as : Vector α n} {j : Nat} :
(as.extract 0 (j + 1))[j]? = as[j]? := by
theorem getElem?_extract_of_succ {xs : Vector α n} {j : Nat} :
(xs.extract 0 (j + 1))[j]? = xs[j]? := by
simp only [Nat.sub_zero]
erw [getElem?_extract] -- Why does this not fire by `simp` or `rw`?
by_cases h : j < n
@ -72,39 +77,39 @@ theorem getElem?_extract_of_succ {as : Vector α n} {j : Nat} :
· rw [if_neg (by omega)]
simp_all
@[simp] theorem extract_extract {as : Vector α n} {i j k l : Nat} :
(as.extract i j).extract k l = (as.extract (i + k) (min (i + l) j)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
@[simp] theorem extract_extract {xs : Vector α n} {i j k l : Nat} :
(xs.extract i j).extract k l = (xs.extract (i + k) (min (i + l) j)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp
theorem extract_set {as : Vector α n} {i j k : Nat} (h : k < n) {a : α} :
(as.set k a).extract i j =
theorem extract_set {xs : Vector α n} {i j k : Nat} (h : k < n) {a : α} :
(xs.set k a).extract i j =
if _ : k < i then
as.extract i j
else if _ : k < min j as.size then
(as.extract i j).set (k - i) a (by omega)
else as.extract i j := by
rcases as with ⟨as, rfl⟩
xs.extract i j
else if _ : k < min j xs.size then
(xs.extract i j).set (k - i) a (by omega)
else xs.extract i j := by
rcases xs with ⟨xs, rfl⟩
simp only [set_mk, extract_mk, Array.extract_set]
split
· simp
· split <;> simp
theorem set_extract {as : Vector α n} {i j k : Nat} (h : k < min j n - i) {a : α} :
(as.extract i j).set k a = (as.set (i + k) a).extract i j := by
rcases as with ⟨as, rfl⟩
theorem set_extract {xs : Vector α n} {i j k : Nat} (h : k < min j n - i) {a : α} :
(xs.extract i j).set k a = (xs.set (i + k) a).extract i j := by
rcases xs with ⟨xs, rfl⟩
simp [Array.set_extract]
@[simp]
theorem extract_append {as : Vector α n} {bs : Vector α m} {i j : Nat} :
(as ++ bs).extract i j =
(as.extract i j ++ bs.extract (i - n) (j - n)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, rfl⟩
theorem extract_append {xs : Vector α n} {ys : Vector α m} {i j : Nat} :
(xs ++ ys).extract i j =
(xs.extract i j ++ ys.extract (i - n) (j - n)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, rfl⟩
simp
theorem extract_append_left {as : Vector α n} {bs : Vector α m} :
(as ++ bs).extract 0 n = (as.extract 0 n).cast (by omega) := by
theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
(xs ++ ys).extract 0 n = (xs.extract 0 n).cast (by omega) := by
ext i h
simp only [Nat.sub_zero, extract_append, extract_size, getElem_cast, getElem_append, Nat.min_self,
getElem_extract, Nat.zero_sub, Nat.zero_add, cast_cast]
@ -112,18 +117,18 @@ theorem extract_append_left {as : Vector α n} {bs : Vector α m} :
· rfl
· omega
@[simp] theorem extract_append_right {as : Vector α n} {bs : Vector α m} :
(as ++ bs).extract n (n + i) = (bs.extract 0 i).cast (by omega) := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, rfl⟩
@[simp] theorem extract_append_right {xs : Vector α n} {ys : Vector α m} :
(xs ++ ys).extract n (n + i) = (ys.extract 0 i).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, rfl⟩
simp only [mk_append_mk, extract_mk, Array.extract_append, Array.extract_size_left, Nat.sub_self,
Array.empty_append, Nat.sub_zero, cast_mk, eq_mk]
congr 1
omega
@[simp] theorem map_extract {as : Vector α n} {i j : Nat} :
(as.extract i j).map f = (as.map f).extract i j := by
ext k h
@[simp] theorem map_extract {xs : Vector α n} {i j : Nat} :
(xs.extract i j).map f = (xs.map f).extract i j := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem extract_mkVector {a : α} {n i j : Nat} :
@ -131,36 +136,36 @@ theorem extract_append_left {as : Vector α n} {bs : Vector α m} :
ext i h
simp
theorem extract_add_left {as : Vector α n} {i j k : Nat} :
as.extract (i + j) k = ((as.extract i k).extract j (k - i)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem extract_add_left {xs : Vector α n} {i j k : Nat} :
xs.extract (i + j) k = ((xs.extract i k).extract j (k - i)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp only [extract_mk, Array.extract_extract, cast_mk, eq_mk]
rw [Array.extract_add_left]
simp
theorem mem_extract_iff_getElem {as : Vector α n} {a : α} {i j : Nat} :
a ∈ as.extract i j ↔ ∃ (k : Nat) (hm : k < min j n - i), as[i + k] = a := by
rcases as with ⟨as⟩
theorem mem_extract_iff_getElem {xs : Vector α n} {a : α} {i j : Nat} :
a ∈ xs.extract i j ↔ ∃ (k : Nat) (hm : k < min j n - i), xs[i + k] = a := by
rcases xs with ⟨xs⟩
simp [Array.mem_extract_iff_getElem]
constructor <;>
· rintro ⟨k, h, rfl⟩
exact ⟨k, by omega, rfl⟩
theorem set_eq_push_extract_append_extract {as : Vector α n} {i : Nat} (h : i < n) {a : α} :
as.set i a = ((as.extract 0 i).push a ++ (as.extract (i + 1) n)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i < n) {a : α} :
xs.set i a = ((xs.extract 0 i).push a ++ (xs.extract (i + 1) n)).cast (by omega) := by
rcases xs with ⟨as, rfl⟩
simp [Array.set_eq_push_extract_append_extract, h]
theorem extract_reverse {as : Vector α n} {i j : Nat} :
as.reverse.extract i j = (as.extract (n - j) (n - i)).reverse.cast (by omega) := by
theorem extract_reverse {xs : Vector α n} {i j : Nat} :
xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by
ext i h
simp only [getElem_extract, getElem_reverse, getElem_cast]
congr 1
omega
theorem reverse_extract {as : Vector α n} {i j : Nat} :
(as.extract i j).reverse = (as.reverse.extract (n - j) (n - i)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
theorem reverse_extract {xs : Vector α n} {i j : Nat} :
(xs.extract i j).reverse = (xs.reverse.extract (n - j) (n - i)).cast (by omega) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.reverse_extract]
end Vector

View file

@ -7,6 +7,9 @@ prelude
import Init.Data.Array.FinRange
import Init.Data.Vector.OfFn
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
/-- `finRange n` is the vector of all elements of `Fin n` in order. -/

View file

@ -15,71 +15,77 @@ import Init.Data.Array.Find
We are still missing results about `idxOf?`, `findIdx`, and `findIdx?`.
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
open Nat
/-! ### findSome? -/
@[simp] theorem findSomeRev?_push_of_isSome (l : Vector α n) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a := by
rcases l with ⟨l, rfl⟩
@[simp] theorem findSomeRev?_push_of_isSome (xs : Vector α n) (h : (f a).isSome) : (xs.push a).findSomeRev? f = f a := by
rcases xs with ⟨xs, rfl⟩
simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isSome, h]
@[simp] theorem findSomeRev?_push_of_isNone (l : Vector α n) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f := by
rcases l with ⟨l, rfl⟩
@[simp] theorem findSomeRev?_push_of_isNone (xs : Vector α n) (h : (f a).isNone) : (xs.push a).findSomeRev? f = xs.findSomeRev? f := by
rcases xs with ⟨xs, rfl⟩
simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isNone, h]
theorem exists_of_findSome?_eq_some {f : α → Option β} {l : Vector α n} (w : l.findSome? f = some b) :
∃ a, a ∈ l ∧ f a = b := by
rcases l with ⟨l, rfl⟩
theorem exists_of_findSome?_eq_some {f : α → Option β} {xs : Vector α n} (w : xs.findSome? f = some b) :
∃ a, a ∈ xs ∧ f a = b := by
rcases xs with ⟨xs, rfl⟩
simpa using Array.exists_of_findSome?_eq_some (by simpa using w)
@[simp] theorem findSome?_eq_none_iff {f : α → Option β} {l : Vector α n} :
findSome? f l = none ↔ ∀ x ∈ l, f x = none := by
cases l; simp
@[simp] theorem findSome?_eq_none_iff {f : α → Option β} {xs : Vector α n} :
xs.findSome? f = none ↔ ∀ x ∈ xs, f x = none := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : Vector α n} :
(l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
cases l; simp
@[simp] theorem findSome?_isSome_iff {f : α → Option β} {xs : Vector α n} :
(xs.findSome? f).isSome ↔ ∃ x, x ∈ xs ∧ (f x).isSome := by
rcases xs with ⟨xs, rfl⟩
simp
theorem findSome?_eq_some_iff {f : α → Option β} {l : Vector α n} {b : β} :
l.findSome? f = some b ↔
∃ (k₁ k₂ : Nat) (w : n = k₁ + 1 + k₂) (l₁ : Vector α k₁) (a : α) (l₂ : Vector α k₂),
l = (l₁.push a ++ l₂).cast w.symm ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
rcases l with ⟨l, rfl⟩
theorem findSome?_eq_some_iff {f : α → Option β} {xs : Vector α n} {b : β} :
xs.findSome? f = some b ↔
∃ (k₁ k₂ : Nat) (w : n = k₁ + 1 + k₂) (ys : Vector α k₁) (a : α) (zs : Vector α k₂),
xs = (ys.push a ++ zs).cast w.symm ∧ f a = some b ∧ ∀ x ∈ ys, f x = none := by
rcases xs with ⟨xs, rfl⟩
simp only [findSome?_mk, mk_eq]
rw [Array.findSome?_eq_some_iff]
constructor
· rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
exact ⟨l₁.size, l₂.size, by simp, ⟨l₁, rfl⟩, a, ⟨l₂, rfl⟩, by simp, h₁, by simpa using h₂⟩
· rintro ⟨k₁, k₂, h, l₁, a, l₂, w, h₁, h₂⟩
exact ⟨l₁.toArray, a, l₂.toArray, by simp [w], h₁, by simpa using h₂⟩
· rintro ⟨ys, a, zs, rfl, h₁, h₂⟩
exact ⟨ys.size, zs.size, by simp, ⟨ys, rfl⟩, a, ⟨zs, rfl⟩, by simp, h₁, by simpa using h₂⟩
· rintro ⟨k₁, k₂, h, ys, a, zs, w, h₁, h₂⟩
exact ⟨ys.toArray, a, zs.toArray, by simp [w], h₁, by simpa using h₂⟩
@[simp] theorem findSome?_guard (l : Vector α n) : findSome? (Option.guard fun x => p x) l = find? p l := by
cases l; simp
@[simp] theorem findSome?_guard (xs : Vector α n) : findSome? (Option.guard fun x => p x) xs = find? p xs := by
rcases xs with ⟨xs, rfl⟩
simp
theorem find?_eq_findSome?_guard (l : Vector α n) : find? p l = findSome? (Option.guard fun x => p x) l :=
(findSome?_guard l).symm
theorem find?_eq_findSome?_guard (xs : Vector α n) : find? p xs = findSome? (Option.guard fun x => p x) xs :=
(findSome?_guard xs).symm
@[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : Vector α n) :
(l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
cases l; simp
@[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (xs : Vector α n) :
(xs.findSome? f).map g = xs.findSome? (Option.map g ∘ f) := by
cases xs; simp
theorem findSome?_map (f : β → γ) (l : Vector β n) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
rcases l with ⟨l, rfl⟩
theorem findSome?_map (f : β → γ) (xs : Vector β n) : findSome? p (xs.map f) = xs.findSome? (p ∘ f) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.findSome?_map]
theorem findSome?_append {l₁ : Vector α n₁} {l₂ : Vector α n₂} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
cases l₁; cases l₂; simp [Array.findSome?_append]
theorem findSome?_append {xs : Vector α n₁} {ys : Vector α n₂} : (xs ++ ys).findSome? f = (xs.findSome? f).or (ys.findSome? f) := by
cases xs; cases ys; simp [Array.findSome?_append]
theorem getElem?_zero_flatten (L : Vector (Vector α m) n) :
(flatten L)[0]? = L.findSome? fun l => l[0]? := by
cases L using vector₂_induction
theorem getElem?_zero_flatten (xss : Vector (Vector α m) n) :
(flatten xss)[0]? = xss.findSome? fun xs => xs[0]? := by
cases xss using vector₂_induction
simp [Array.getElem?_zero_flatten, Array.findSome?_map, Function.comp_def]
theorem getElem_zero_flatten.proof {L : Vector (Vector α m) n} (h : 0 < n * m) :
(L.findSome? fun l => l[0]?).isSome := by
cases L using vector₂_induction with
theorem getElem_zero_flatten.proof {xss : Vector (Vector α m) n} (h : 0 < n * m) :
(xss.findSome? fun xs => xs[0]?).isSome := by
cases xss using vector₂_induction with
| of xss h₁ h₂ =>
have hn : 0 < n := Nat.pos_of_mul_pos_right h
have hm : 0 < m := Nat.pos_of_mul_pos_left h
@ -88,9 +94,9 @@ theorem getElem_zero_flatten.proof {L : Vector (Vector α m) n} (h : 0 < n * m)
Option.isSome_some, and_true]
exact ⟨⟨xss[0], h₂ _ (by simp)⟩, by simp⟩
theorem getElem_zero_flatten {L : Vector (Vector α m) n} (h : 0 < n * m) :
(flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h) := by
have t := getElem?_zero_flatten L
theorem getElem_zero_flatten {xss : Vector (Vector α m) n} (h : 0 < n * m) :
(flatten xss)[0] = (xss.findSome? fun xs => xs[0]?).get (getElem_zero_flatten.proof h) := by
have t := getElem?_zero_flatten xss
simp [getElem?_eq_getElem, h] at t
simp [← t]
@ -116,13 +122,13 @@ theorem findSome?_mkVector : findSome? f (mkVector n a) = if n = 0 then none els
#v[a].find? p = if p a then some a else none := by
simp
@[simp] theorem findRev?_push_of_pos (l : Vector α n) (h : p a) :
findRev? p (l.push a) = some a := by
cases l; simp [h]
@[simp] theorem findRev?_push_of_pos (xs : Vector α n) (h : p a) :
findRev? p (xs.push a) = some a := by
cases xs; simp [h]
@[simp] theorem findRev?_cons_of_neg (l : Vector α n) (h : ¬p a) :
findRev? p (l.push a) = findRev? p l := by
cases l; simp [h]
@[simp] theorem findRev?_cons_of_neg (xs : Vector α n) (h : ¬p a) :
findRev? p (xs.push a) = findRev? p xs := by
cases xs; simp [h]
@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
cases l; simp
@ -166,24 +172,24 @@ theorem get_find?_mem {xs : Vector α n} (h) : (xs.find? p).get h ∈ xs := by
(xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
cases xs; simp
@[simp] theorem getElem?_zero_filter (p : α → Bool) (l : Vector α n) :
(l.filter p)[0]? = l.find? p := by
cases l; simp [← List.head?_eq_getElem?]
@[simp] theorem getElem?_zero_filter (p : α → Bool) (xs : Vector α n) :
(xs.filter p)[0]? = xs.find? p := by
cases xs; simp [← List.head?_eq_getElem?]
@[simp] theorem getElem_zero_filter (p : α → Bool) (l : Vector α n) (h) :
(l.filter p)[0] =
(l.find? p).get (by cases l; simpa [← Array.countP_eq_size_filter] using h) := by
cases l
@[simp] theorem getElem_zero_filter (p : α → Bool) (xs : Vector α n) (h) :
(xs.filter p)[0] =
(xs.find? p).get (by cases xs; simpa [← Array.countP_eq_size_filter] using h) := by
cases xs
simp [List.getElem_zero_eq_head]
@[simp] theorem find?_map (f : β → α) (xs : Vector β n) :
find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
cases xs; simp
@[simp] theorem find?_append {l₁ : Vector α n₁} {l₂ : Vector α n₂} :
(l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
cases l₁
cases l₂
@[simp] theorem find?_append {xs : Vector α n₁} {ys : Vector α n₂} :
(xs ++ ys).find? p = (xs.find? p).or (ys.find? p) := by
cases xs
cases ys
simp
@[simp] theorem find?_flatten (xs : Vector (Vector α m) n) (p : α → Bool) :
@ -250,15 +256,15 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := rfl
@[congr] theorem findFinIdx?_congr {p : α → Bool} {l₁ : Vector α n} {l₂ : Vector α n} (w : l₁ = l₂) :
findFinIdx? p l₁ = findFinIdx? p l₂ := by
@[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) :
findFinIdx? p xs = findFinIdx? p ys := by
subst w
simp
@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : Vector { x // p x } n}
@[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Vector { x // p x } n}
{f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
l.findFinIdx? f = l.unattach.findFinIdx? g := by
rcases l with ⟨l, rfl⟩
xs.findFinIdx? f = xs.unattach.findFinIdx? g := by
rcases xs with ⟨xs, rfl⟩
simp [hf, Function.comp_def]
end Vector

View file

@ -13,9 +13,10 @@ import Init.Data.Array.InsertIdx
Proves various lemmas about `Vector.insertIdx`.
-/
open Function
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
open Nat
open Function Nat
namespace Vector
@ -28,97 +29,98 @@ section InsertIdx
variable {a : α}
@[simp]
theorem insertIdx_zero (s : Vector α n) (x : α) : s.insertIdx 0 x = (#v[x] ++ s).cast (by omega) := by
cases s
theorem insertIdx_zero (xs : Vector α n) (x : α) : xs.insertIdx 0 x = (#v[x] ++ xs).cast (by omega) := by
cases xs
simp
theorem eraseIdx_insertIdx (i : Nat) (l : Vector α n) (h : i ≤ n) :
(l.insertIdx i a).eraseIdx i = l := by
rcases l with ⟨l, rfl⟩
theorem eraseIdx_insertIdx (i : Nat) (xs : Vector α n) (h : i ≤ n) :
(xs.insertIdx i a).eraseIdx i = xs := by
rcases xs with ⟨xs, rfl⟩
simp_all [Array.eraseIdx_insertIdx]
theorem insertIdx_eraseIdx_of_ge {as : Vector α n}
theorem insertIdx_eraseIdx_of_ge {xs : Vector α n}
(w₁ : i < n) (w₂ : j ≤ n - 1) (h : i ≤ j) :
(as.eraseIdx i).insertIdx j a =
((as.insertIdx (j + 1) a).eraseIdx i).cast (by omega) := by
rcases as with ⟨as, rfl⟩
(xs.eraseIdx i).insertIdx j a =
((xs.insertIdx (j + 1) a).eraseIdx i).cast (by omega) := by
rcases xs with ⟨as, rfl⟩
simpa using Array.insertIdx_eraseIdx_of_ge (by simpa) (by simpa) (by simpa)
theorem insertIdx_eraseIdx_of_le {as : Vector α n}
theorem insertIdx_eraseIdx_of_le {xs : Vector α n}
(w₁ : i < n) (w₂ : j ≤ n - 1) (h : j ≤ i) :
(as.eraseIdx i).insertIdx j a =
((as.insertIdx j a).eraseIdx (i + 1)).cast (by omega) := by
rcases as with ⟨as, rfl⟩
(xs.eraseIdx i).insertIdx j a =
((xs.insertIdx j a).eraseIdx (i + 1)).cast (by omega) := by
rcases xs with ⟨as, rfl⟩
simpa using Array.insertIdx_eraseIdx_of_le (by simpa) (by simpa) (by simpa)
theorem insertIdx_comm (a b : α) (i j : Nat) (l : Vector α n) (_ : i ≤ j) (_ : j ≤ n) :
(l.insertIdx i a).insertIdx (j + 1) b =
(l.insertIdx j b).insertIdx i a := by
rcases l with ⟨l, rfl⟩
theorem insertIdx_comm (a b : α) (i j : Nat) (xs : Vector α n) (_ : i ≤ j) (_ : j ≤ n) :
(xs.insertIdx i a).insertIdx (j + 1) b =
(xs.insertIdx j b).insertIdx i a := by
rcases xs with ⟨as, rfl⟩
simpa using Array.insertIdx_comm a b i j _ (by simpa) (by simpa)
theorem mem_insertIdx {l : Vector α n} {h : i ≤ n} : a ∈ l.insertIdx i b h ↔ a = b a ∈ l := by
rcases l with ⟨l, rfl⟩
theorem mem_insertIdx {xs : Vector α n} {h : i ≤ n} : a ∈ xs.insertIdx i b h ↔ a = b a ∈ xs := by
rcases xs with ⟨as, rfl⟩
simpa using Array.mem_insertIdx
set_option linter.indexVariables false in
@[simp]
theorem insertIdx_size_self (l : Vector α n) (x : α) : l.insertIdx n x = l.push x := by
rcases l with ⟨l, rfl⟩
theorem insertIdx_size_self (xs : Vector α n) (x : α) : xs.insertIdx n x = xs.push x := by
rcases xs with ⟨as, rfl⟩
simp
theorem getElem_insertIdx {as : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < n + 1) :
(as.insertIdx i x)[k] =
theorem getElem_insertIdx {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < n + 1) :
(xs.insertIdx i x)[k] =
if h₁ : k < i then
as[k]
xs[k]
else
if h₂ : k = i then
x
else
as[k-1] := by
rcases as with ⟨as, rfl⟩
xs[k-1] := by
rcases xs with ⟨xs, rfl⟩
simp [Array.getElem_insertIdx, w]
theorem getElem_insertIdx_of_lt {as : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
(as.insertIdx i x)[k] = as[k] := by
rcases as with ⟨as, rfl⟩
theorem getElem_insertIdx_of_lt {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
(xs.insertIdx i x)[k] = xs[k] := by
rcases xs with ⟨xs, rfl⟩
simp [Array.getElem_insertIdx, w, h]
theorem getElem_insertIdx_self {as : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
(as.insertIdx i x)[i] = x := by
rcases as with ⟨as, rfl⟩
theorem getElem_insertIdx_self {xs : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
(xs.insertIdx i x)[i] = x := by
rcases xs with ⟨xs, rfl⟩
simp [Array.getElem_insertIdx, w]
theorem getElem_insertIdx_of_gt {as : Vector α n} {x : α} {i k : Nat} (w : k ≤ n) (h : k > i) :
(as.insertIdx i x)[k] = as[k - 1] := by
rcases as with ⟨as, rfl⟩
theorem getElem_insertIdx_of_gt {xs : Vector α n} {x : α} {i k : Nat} (w : k ≤ n) (h : k > i) :
(xs.insertIdx i x)[k] = xs[k - 1] := by
rcases xs with ⟨xs, rfl⟩
simp [Array.getElem_insertIdx, w, h]
rw [dif_neg (by omega), dif_neg (by omega)]
theorem getElem?_insertIdx {l : Vector α n} {x : α} {i k : Nat} (h : i ≤ n) :
(l.insertIdx i x)[k]? =
theorem getElem?_insertIdx {xs : Vector α n} {x : α} {i k : Nat} (h : i ≤ n) :
(xs.insertIdx i x)[k]? =
if k < i then
l[k]?
xs[k]?
else
if k = i then
if k ≤ l.size then some x else none
if k ≤ xs.size then some x else none
else
l[k-1]? := by
rcases l with ⟨l, rfl⟩
xs[k-1]? := by
rcases xs with ⟨xs, rfl⟩
simp [Array.getElem?_insertIdx, h]
theorem getElem?_insertIdx_of_lt {l : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
(l.insertIdx i x)[k]? = l[k]? := by
rcases l with ⟨l, rfl⟩
theorem getElem?_insertIdx_of_lt {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
(xs.insertIdx i x)[k]? = xs[k]? := by
rcases xs with ⟨xs, rfl⟩
rw [getElem?_insertIdx, if_pos h]
theorem getElem?_insertIdx_self {l : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
(l.insertIdx i x)[i]? = some x := by
rcases l with ⟨l, rfl⟩
theorem getElem?_insertIdx_self {xs : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
(xs.insertIdx i x)[i]? = some x := by
rcases xs with ⟨xs, rfl⟩
rw [getElem?_insertIdx, if_neg (by omega), if_pos rfl, if_pos w]
theorem getElem?_insertIdx_of_ge {l : Vector α n} {x : α} {i k : Nat} (w : i < k) (h : k ≤ n) :
(l.insertIdx i x)[k]? = l[k - 1]? := by
rcases l with ⟨l, rfl⟩
theorem getElem?_insertIdx_of_ge {xs : Vector α n} {x : α} {i k : Nat} (w : i < k) (h : k ≤ n) :
(xs.insertIdx i x)[k]? = xs[k - 1]? := by
rcases xs with ⟨xs, rfl⟩
rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
end InsertIdx

File diff suppressed because it is too large Load diff

View file

@ -8,20 +8,23 @@ import Init.Data.Vector.Basic
import Init.Data.Vector.Lemmas
import Init.Data.Array.Lex.Lemmas
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
/-! ### Lexicographic ordering -/
@[simp] theorem lt_toArray [LT α] (l₁ l₂ : Vector α n) : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
@[simp] theorem le_toArray [LT α] (l₁ l₂ : Vector α n) : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
@[simp] theorem lt_toArray [LT α] (xs ys : Vector α n) : xs.toArray < ys.toArray ↔ xs < ys := Iff.rfl
@[simp] theorem le_toArray [LT α] (xs ys : Vector α n) : xs.toArray ≤ ys.toArray ↔ xs ≤ ys := Iff.rfl
@[simp] theorem lt_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList < l₂.toList ↔ l₁ < l₂ := Iff.rfl
@[simp] theorem le_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂ := Iff.rfl
@[simp] theorem lt_toList [LT α] (xs ys : Vector α n) : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
@[simp] theorem le_toList [LT α] (xs ys : Vector α n) : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : Vector α n) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : Vector α n) :
¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
protected theorem not_lt_iff_ge [LT α] (xs ys : Vector α n) : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (xs ys : Vector α n) :
¬ xs ≤ ys ↔ ys < xs :=
Decidable.not_not
@[simp] theorem mk_lt_mk [LT α] :
@ -30,54 +33,54 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁
@[simp] theorem mk_le_mk [LT α] :
Vector.mk (α := α) (n := n) data₁ size₁ ≤ Vector.mk data₂ size₂ ↔ data₁ ≤ data₂ := Iff.rfl
@[simp] theorem mk_lex_mk [BEq α] (lt : αα → Bool) {l₁ l₂ : Array α} {n₁ : l₁.size = n} {n₂ : l₂.size = n} :
(Vector.mk l₁ n₁).lex (Vector.mk l₂ n₂) lt = l₁.lex l₂ lt := by
@[simp] theorem mk_lex_mk [BEq α] (lt : αα → Bool) {xs ys : Array α} {n₁ : xs.size = n} {n₂ : ys.size = n} :
(Vector.mk xs n₁).lex (Vector.mk ys n₂) lt = xs.lex ys lt := by
simp [Vector.lex, Array.lex, n₁, n₂]
rfl
@[simp] theorem lex_toArray [BEq α] (lt : αα → Bool) (l₁ l₂ : Vector α n) :
l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
cases l₁
cases l₂
@[simp] theorem lex_toArray [BEq α] (lt : αα → Bool) (xs ys : Vector α n) :
xs.toArray.lex ys.toArray lt = xs.lex ys lt := by
cases xs
cases ys
simp
@[simp] theorem lex_toList [BEq α] (lt : αα → Bool) (l₁ l₂ : Vector α n) :
l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt := by
rcases l₁ with ⟨⟨l₁⟩, n₁⟩
rcases l₂ with ⟨⟨l₂⟩, n₂⟩
@[simp] theorem lex_toList [BEq α] (lt : αα → Bool) (xs ys : Vector α n) :
xs.toList.lex ys.toList lt = xs.lex ys lt := by
rcases xs with ⟨xs, n₁⟩
rcases ys with ⟨ys, n₂⟩
simp
@[simp] theorem lex_empty
[BEq α] {lt : αα → Bool} (l₁ : Vector α 0) : l₁.lex #v[] lt = false := by
cases l₁
[BEq α] {lt : αα → Bool} (xs : Vector α 0) : xs.lex #v[] lt = false := by
cases xs
simp_all
@[simp] theorem singleton_lex_singleton [BEq α] {lt : αα → Bool} : #v[a].lex #v[b] lt = lt a b := by
simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]
cases lt a b <;> cases a != b <;> simp [Id.run]
protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : αα → Prop)] (l : Vector α n) : ¬ l < l :=
Array.lt_irrefl l.toArray
protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : αα → Prop)] (xs : Vector α n) : ¬ xs < xs :=
Array.lt_irrefl xs.toArray
instance ltIrrefl [LT α] [Std.Irrefl (· < · : αα → Prop)] : Std.Irrefl (α := Vector α n) (· < ·) where
irrefl := Vector.lt_irrefl
@[simp] theorem not_lt_empty [LT α] (l : Vector α 0) : ¬ l < #v[] := Array.not_lt_empty l.toArray
@[simp] theorem empty_le [LT α] (l : Vector α 0) : #v[] ≤ l := Array.empty_le l.toArray
@[simp] theorem not_lt_empty [LT α] (xs : Vector α 0) : ¬ xs < #v[] := Array.not_lt_empty xs.toArray
@[simp] theorem empty_le [LT α] (xs : Vector α 0) : #v[] ≤ xs := Array.empty_le xs.toArray
@[simp] theorem le_empty [LT α] (l : Vector α 0) : l ≤ #v[] ↔ l = #v[] := by
cases l
@[simp] theorem le_empty [LT α] (xs : Vector α 0) : xs ≤ #v[] ↔ xs = #v[] := by
cases xs
simp
protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : αα → Prop)] (l : Vector α n) : l ≤ l :=
Array.le_refl l.toArray
protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : αα → Prop)] (xs : Vector α n) : xs ≤ xs :=
Array.le_refl xs.toArray
instance [LT α] [Std.Irrefl (· < · : αα → Prop)] : Std.Refl (· ≤ · : Vector α n → Vector α n → Prop) where
refl := Vector.le_refl
protected theorem lt_trans [LT α]
[i₁ : Trans (· < · : αα → Prop) (· < ·) (· < ·)]
{l₁ l₂ l₃ : Vector α n} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
{xs ys zs : Vector α n} (h₁ : xs < ys) (h₂ : ys < zs) : xs < zs :=
Array.lt_trans h₁ h₂
instance [LT α]
@ -90,7 +93,7 @@ protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
[i₁ : Std.Asymm (· < · : αα → Prop)]
[i₂ : Std.Antisymm (¬ · < · : αα → Prop)]
[i₃ : Trans (¬ · < · : αα → Prop) (¬ · < ·) (¬ · < ·)]
{l₁ l₂ l₃ : Vector α n} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
{xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
Array.lt_of_le_of_lt h₁ h₂
protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
@ -98,7 +101,7 @@ protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
[Std.Asymm (· < · : αα → Prop)]
[Std.Antisymm (¬ · < · : αα → Prop)]
[Trans (¬ · < · : αα → Prop) (¬ · < ·) (¬ · < ·)]
{l₁ l₂ l₃ : Vector α n} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
{xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
fun h₃ => h₁ (Vector.lt_of_le_of_lt h₂ h₃)
instance [DecidableEq α] [LT α] [DecidableLT α]
@ -111,7 +114,7 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
protected theorem lt_asymm [LT α]
[i : Std.Asymm (· < · : αα → Prop)]
{l₁ l₂ : Vector α n} (h : l₁ < l₂) : ¬ l₂ < l₁ := Array.lt_asymm h
{xs ys : Vector α n} (h : xs < ys) : ¬ ys < xs := Array.lt_asymm h
instance [DecidableEq α] [LT α] [DecidableLT α]
[Std.Asymm (· < · : αα → Prop)] :
@ -119,7 +122,7 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
asymm _ _ := Vector.lt_asymm
protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
[i : Std.Total (¬ · < · : αα → Prop)] (l₁ l₂ : Vector α n) : l₁ ≤ l₂ l₂ ≤ l₁ :=
[i : Std.Total (¬ · < · : αα → Prop)] (xs ys : Vector α n) : xs ≤ ys ys ≤ xs :=
Array.le_total _ _
instance [DecidableEq α] [LT α] [DecidableLT α]
@ -128,60 +131,58 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
total := Vector.le_total
@[simp] protected theorem not_lt [LT α]
{l₁ l₂ : Vector α n} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
{xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : Vector α n} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_not
{xs ys : Vector α n} : ¬ ys ≤ xs ↔ xs < ys := Decidable.not_not
protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
[i : Std.Total (¬ · < · : αα → Prop)]
{l₁ l₂ : Vector α n} (h : l₁ < l₂) : l₁ ≤ l₂ :=
{xs ys : Vector α n} (h : xs < ys) : xs ≤ ys :=
Array.le_of_lt h
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : αα → Prop)]
[Std.Antisymm (¬ · < · : αα → Prop)]
[Std.Total (¬ · < · : αα → Prop)]
{l₁ l₂ : Vector α n} : l₁ ≤ l₂ ↔ l₁ < l₂ l₁ = l₂ := by
simpa using Array.le_iff_lt_or_eq (xs := l₁.toArray) (ys := l₂.toArray)
{xs ys : Vector α n} : xs ≤ ys ↔ xs < ys xs = ys := by
simpa using Array.le_iff_lt_or_eq (xs := xs.toArray) (ys := ys.toArray)
@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : Vector α n} : lex l₁ l₂ = true ↔ l₁ < l₂ := by
cases l₁
cases l₂
{xs ys : Vector α n} : lex xs ys = true ↔ xs < ys := by
cases xs
cases ys
simp
@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : Vector α n} : lex l₁ l₂ = false ↔ l₂ ≤ l₁ := by
cases l₁
cases l₂
{xs ys : Vector α n} : lex xs ys = false ↔ ys ≤ xs := by
cases xs
cases ys
simp [Array.not_lt_iff_ge]
instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Vector α n) :=
fun l₁ l₂ => decidable_of_iff (lex l₁ l₂ = true) lex_eq_true_iff_lt
fun xs ys => decidable_of_iff (lex xs ys = true) lex_eq_true_iff_lt
instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Vector α n) :=
fun l₁ l₂ => decidable_of_iff (lex l₂ l₁ = false) lex_eq_false_iff_ge
fun xs ys => decidable_of_iff (lex ys xs = false) lex_eq_false_iff_ge
/--
`l₁` is lexicographically less than `l₂` if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.size`,
and `l₁` is shorter than `l₂` or
- there exists an index `i` such that
- for all `j < i`, `l₁[j] == l₂[j]` and
- `l₁[i] < l₂[i]`
`xs` is lexicographically less than `ys` if
there exists an index `i` such that
- for all `j < i`, `l₁[j] == l₂[j]` and
- `l₁[i] < l₂[i]`
-/
theorem lex_eq_true_iff_exists [BEq α] (lt : αα → Bool) {l₁ l₂ : Vector α n} :
lex l₁ l₂ lt = true ↔
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] == l₂[j]) ∧ lt l₁[i] l₂[i]) := by
rcases l₁ with ⟨l₁, n₁⟩
rcases l₂ with ⟨l₂, n₂⟩
theorem lex_eq_true_iff_exists [BEq α] (lt : αα → Bool) {xs ys : Vector α n} :
lex xs ys lt = true ↔
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → xs[j] == ys[j]) ∧ lt xs[i] ys[i]) := by
rcases xs with ⟨xs, n₁⟩
rcases ys with ⟨ys, n₂⟩
simp [Array.lex_eq_true_iff_exists, n₁, n₂]
/--
`l₁` is *not* lexicographically less than `l₂`
(which you might think of as "`l₂` is lexicographically greater than or equal to `l₁`"") if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length` or
- `l₁` is pairwise equivalent under `· == ·` to `l₂` or
- there exists an index `i` such that
- for all `j < i`, `l₁[j] == l₂[j]` and
- `l₂[i] < l₁[i]`
@ -197,47 +198,47 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : αα
(lt_irrefl : ∀ x y, x == y → lt x y = false)
(lt_asymm : ∀ x y, lt x y = true → lt y x = false)
(lt_antisymm : ∀ x y, lt x y = false → lt y x = false → x == y)
{l₁ l₂ : Vector α n} :
lex l₁ l₂ lt = false ↔
(l₂.isEqv l₁ (· == ·))
(∃ (i : Nat) (h : i < n),(∀ j, (hj : j < i) → l₁[j] == l₂[j]) ∧ lt l₂[i] l₁[i]) := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, n₂⟩
{xs ys : Vector α n} :
lex xs ys lt = false ↔
(ys.isEqv xs (· == ·))
(∃ (i : Nat) (h : i < n),(∀ j, (hj : j < i) → xs[j] == ys[j]) ∧ lt ys[i] xs[i]) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, n₂⟩
simp_all [Array.lex_eq_false_iff_exists, n₂]
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
l₁ < l₂
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) := by
cases l₁
cases l₂
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} :
xs < ys
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → xs[j] = ys[j]) ∧ xs[i] < ys[i]) := by
cases xs
cases ys
simp_all [Array.lt_iff_exists]
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : αα → Prop)]
[Std.Asymm (· < · : αα → Prop)]
[Std.Antisymm (¬ · < · : αα → Prop)] {l₁ l₂ : Vector α n} :
l₁ ≤ l₂
(l₁ = l₂)
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, n₂⟩
[Std.Antisymm (¬ · < · : αα → Prop)] {xs ys : Vector α n} :
xs ≤ ys
(xs = ys)
(∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → xs[j] = ys[j]) ∧ xs[i] < ys[i]) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, n₂⟩
simp [Array.le_iff_exists, ← n₂]
theorem append_left_lt [LT α] {l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ < l₃) :
l₁ ++ l₂ < l₁ ++ l₃ := by
theorem append_left_lt [LT α] {xs : Vector α n} {ys ys' : Vector α m} (h : ys < ys') :
xs ++ ys < xs ++ ys' := by
simpa using Array.append_left_lt h
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : αα → Prop)]
[Std.Asymm (· < · : αα → Prop)]
[Std.Antisymm (¬ · < · : αα → Prop)]
{l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ ≤ l₃) :
l₁ ++ l₂ ≤ l₁ ++ l₃ := by
{xs : Vector α n} {ys ys' : Vector α m} (h : ys ≤ ys') :
xs ++ ys ≤ xs ++ ys' := by
simpa using Array.append_left_le h
protected theorem map_lt [LT α] [LT β]
{l₁ l₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
map f l₁ < map f l₂ := by
{xs ys : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs < ys) :
map f xs < map f ys := by
simpa using Array.map_lt w h
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
@ -247,8 +248,8 @@ protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq
[Std.Irrefl (· < · : β → β → Prop)]
[Std.Asymm (· < · : β → β → Prop)]
[Std.Antisymm (¬ · < · : β → β → Prop)]
{l₁ l₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
map f l₁ ≤ map f l₂ := by
{xs ys : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs ≤ ys) :
map f xs ≤ map f ys := by
simpa using Array.map_le w h
end Vector

View file

@ -5,46 +5,50 @@ Authors: Kim Morrison
-/
prelude
import Init.Data.Array.MapIdx
import Init.Data.Vector.Attach
import Init.Data.Vector.Lemmas
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
/-! ### mapFinIdx -/
@[simp] theorem getElem_mapFinIdx (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat)
@[simp] theorem getElem_mapFinIdx (xs : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat)
(h : i < n) :
(a.mapFinIdx f)[i] = f i a[i] h := by
rcases a with ⟨a, rfl⟩
(xs.mapFinIdx f)[i] = f i xs[i] h := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem getElem?_mapFinIdx (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat) :
(a.mapFinIdx f)[i]? =
a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
@[simp] theorem getElem?_mapFinIdx (xs : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat) :
(xs.mapFinIdx f)[i]? =
xs[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
simp only [getElem?_def, getElem_mapFinIdx]
split <;> simp_all
/-! ### mapIdx -/
@[simp] theorem getElem_mapIdx (f : Nat → α → β) (a : Vector α n) (i : Nat) (h : i < n) :
(a.mapIdx f)[i] = f i (a[i]'(by simp_all)) := by
rcases a with ⟨a, rfl⟩
@[simp] theorem getElem_mapIdx (f : Nat → α → β) (xs : Vector α n) (i : Nat) (h : i < n) :
(xs.mapIdx f)[i] = f i (xs[i]'(by simp_all)) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem getElem?_mapIdx (f : Nat → α → β) (a : Vector α n) (i : Nat) :
(a.mapIdx f)[i]? = a[i]?.map (f i) := by
rcases a with ⟨a, rfl⟩
@[simp] theorem getElem?_mapIdx (f : Nat → α → β) (xs : Vector α n) (i : Nat) :
(xs.mapIdx f)[i]? = xs[i]?.map (f i) := by
rcases xs with ⟨xs, rfl⟩
simp
end Vector
namespace Array
@[simp] theorem mapFinIdx_toVector (l : Array α) (f : (i : Nat) → α → (h : i < l.size) → β) :
l.toVector.mapFinIdx f = (l.mapFinIdx f).toVector.cast (by simp) := by
@[simp] theorem mapFinIdx_toVector (xs : Array α) (f : (i : Nat) → α → (h : i < xs.size) → β) :
xs.toVector.mapFinIdx f = (xs.mapFinIdx f).toVector.cast (by simp) := by
ext <;> simp
@[simp] theorem mapIdx_toVector (f : Nat → α → β) (l : Array α) :
l.toVector.mapIdx f = (l.mapIdx f).toVector.cast (by simp) := by
@[simp] theorem mapIdx_toVector (f : Nat → α → β) (xs : Array α) :
xs.toVector.mapIdx f = (xs.mapIdx f).toVector.cast (by simp) := by
ext <;> simp
end Array
@ -53,50 +57,44 @@ namespace Vector
/-! ### zipIdx -/
@[simp] theorem toList_zipIdx (a : Vector α n) (k : Nat := 0) :
(a.zipIdx k).toList = a.toList.zipIdx k := by
rcases a with ⟨a, rfl⟩
@[simp] theorem toList_zipIdx (xs : Vector α n) (k : Nat := 0) :
(xs.zipIdx k).toList = xs.toList.zipIdx k := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem getElem_zipIdx (a : Vector α n) (i : Nat) (h : i < n) :
(a.zipIdx k)[i] = (a[i]'(by simp_all), k + i) := by
rcases a with ⟨a, rfl⟩
@[simp] theorem getElem_zipIdx (xs : Vector α n) (i : Nat) (h : i < n) :
(xs.zipIdx k)[i] = (xs[i]'(by simp_all), k + i) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem zipIdx_toVector {l : Array α} {k : Nat} :
l.toVector.zipIdx k = (l.zipIdx k).toVector.cast (by simp) := by
ext <;> simp
theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {x : α} {i : Nat} {l : Vector α n} {k : Nat} :
(x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = x := by
rcases l with ⟨l, rfl⟩
theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {x : α} {i : Nat} {xs : Vector α n} {k : Nat} :
(x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = x := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mk_mem_zipIdx_iff_le_and_getElem?_sub]
/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction. -/
theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {l : Vector α n} :
(x, i) ∈ l.zipIdx ↔ l[i]? = x := by
rcases l with ⟨l, rfl⟩
theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {xs : Vector α n} :
(x, i) ∈ xs.zipIdx ↔ xs[i]? = x := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mk_mem_zipIdx_iff_le_and_getElem?_sub]
theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : Vector α n} {k : Nat} :
x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
cases x
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {xs : Vector α n} {k : Nat} :
x ∈ xs.zipIdx k ↔ k ≤ x.2 ∧ xs[x.2 - k]? = some x.1 := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mem_zipIdx_iff_le_and_getElem?_sub]
/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction. -/
theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : Vector α n} :
x ∈ l.zipIdx ↔ l[x.2]? = some x.1 := by
rcases l with ⟨l, rfl⟩
theorem mem_zipIdx_iff_getElem? {x : α × Nat} {xs : Vector α n} :
x ∈ xs.zipIdx ↔ xs[x.2]? = some x.1 := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mem_zipIdx_iff_getElem?]
@[deprecated toList_zipIdx (since := "2025-01-27")]
abbrev toList_zipWithIndex := @toList_zipIdx
@[deprecated getElem_zipIdx (since := "2025-01-27")]
abbrev getElem_zipWithIndex := @getElem_zipIdx
@[deprecated zipIdx_toVector (since := "2025-01-27")]
abbrev zipWithIndex_toVector := @zipIdx_toVector
@[deprecated mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]
abbrev mk_mem_zipWithIndex_iff_le_and_getElem?_sub := @mk_mem_zipIdx_iff_le_and_getElem?_sub
@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-27")]
@ -123,50 +121,49 @@ theorem mapFinIdx_eq_ofFn {as : Vector α n} {f : (i : Nat) → α → (h : i <
rcases as with ⟨as, rfl⟩
simp [Array.mapFinIdx_eq_ofFn]
theorem mapFinIdx_append {K : Vector α n} {L : Vector α m} {f : (i : Nat) → α → (h : i < n + m) → β} :
(K ++ L).mapFinIdx f =
K.mapFinIdx (fun i a h => f i a (by omega)) ++
L.mapFinIdx (fun i a h => f (i + n) a (by omega)) := by
rcases K with ⟨K, rfl⟩
rcases L with ⟨L, rfl⟩
theorem mapFinIdx_append {xs : Vector α n} {ys : Vector α m} {f : (i : Nat) → α → (h : i < n + m) → β} :
(xs ++ ys).mapFinIdx f =
xs.mapFinIdx (fun i a h => f i a (by omega)) ++
ys.mapFinIdx (fun i a h => f (i + n) a (by omega)) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, rfl⟩
simp [Array.mapFinIdx_append]
@[simp]
theorem mapFinIdx_push {l : Vector α n} {a : α} {f : (i : Nat) → α → (h : i < n + 1) → β} :
mapFinIdx (l.push a) f =
(mapFinIdx l (fun i a h => f i a (by omega))).push (f l.size a (by simp)) := by
theorem mapFinIdx_push {xs : Vector α n} {a : α} {f : (i : Nat) → α → (h : i < n + 1) → β} :
mapFinIdx (xs.push a) f =
(mapFinIdx xs (fun i a h => f i a (by omega))).push (f xs.size a (by simp)) := by
simp [← append_singleton, mapFinIdx_append]
theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
#v[a].mapFinIdx f = #v[f 0 a (by simp)] := by
simp
-- FIXME this lemma can't be stated until we've aligned `List/Array/Vector.attach`:
-- theorem mapFinIdx_eq_zipWithIndex_map {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
-- l.mapFinIdx f = l.zipWithIndex.attach.map
-- fun ⟨⟨x, i⟩, m⟩ =>
-- f i x (by simp [mk_mem_zipWithIndex_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
-- ext <;> simp
theorem mapFinIdx_eq_zipIdx_map {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
xs.mapFinIdx f = xs.zipIdx.attach.map
fun ⟨⟨x, i⟩, m⟩ =>
f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
ext <;> simp
theorem exists_of_mem_mapFinIdx {b : β} {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β}
(h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < n), f i l[i] h = b := by
rcases l with ⟨l, rfl⟩
theorem exists_of_mem_mapFinIdx {b : β} {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β}
(h : b ∈ xs.mapFinIdx f) : ∃ (i : Nat) (h : i < n), f i xs[i] h = b := by
rcases xs with ⟨xs, rfl⟩
exact List.exists_of_mem_mapFinIdx (by simpa using h)
@[simp] theorem mem_mapFinIdx {b : β} {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < n), f i l[i] h = b := by
rcases l with ⟨l, rfl⟩
@[simp] theorem mem_mapFinIdx {b : β} {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
b ∈ xs.mapFinIdx f ↔ ∃ (i : Nat) (h : i < n), f i xs[i] h = b := by
rcases xs with ⟨xs, rfl⟩
simp
theorem mapFinIdx_eq_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
l.mapFinIdx f = l' ↔ ∀ (i : Nat) (h : i < n), l'[i] = f i l[i] h := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem mapFinIdx_eq_iff {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
xs.mapFinIdx f = xs' ↔ ∀ (i : Nat) (h : i < n), xs'[i] = f i xs[i] h := by
rcases xs with ⟨xs, rfl⟩
rcases xs' with ⟨xs', h⟩
simp [mapFinIdx_mk, eq_mk, getElem_mk, Array.mapFinIdx_eq_iff, h]
@[simp] theorem mapFinIdx_eq_singleton_iff {l : Vector α 1} {f : (i : Nat) → α → (h : i < 1) → β} {b : β} :
l.mapFinIdx f = #v[b] ↔ ∃ (a : α), l = #v[a] ∧ f 0 a (by omega) = b := by
rcases l with ⟨l, h⟩
@[simp] theorem mapFinIdx_eq_singleton_iff {xs : Vector α 1} {f : (i : Nat) → α → (h : i < 1) → β} {b : β} :
xs.mapFinIdx f = #v[b] ↔ ∃ (a : α), xs = #v[a] ∧ f 0 a (by omega) = b := by
rcases xs with ⟨xs, h⟩
simp only [mapFinIdx_mk, eq_mk, Array.mapFinIdx_eq_singleton_iff]
constructor
· rintro ⟨a, rfl, rfl⟩
@ -174,60 +171,60 @@ theorem mapFinIdx_eq_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n)
· rintro ⟨a, rfl, rfl⟩
exact ⟨a, by simp⟩
theorem mapFinIdx_eq_append_iff {l : Vector α (n + m)} {f : (i : Nat) → α → (h : i < n + m) → β}
{l₁ : Vector β n} {l₂ : Vector β m} :
l.mapFinIdx f = l₁ ++ l₂
∃ (l₁' : Vector α n) (l₂' : Vector α m), l = l₁' ++ l₂' ∧
l₁'.mapFinIdx (fun i a h => f i a (by omega)) = l₁
l₂'.mapFinIdx (fun i a h => f (i + n) a (by omega)) = l₂ := by
rcases l with ⟨l, h⟩
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, rfl⟩
theorem mapFinIdx_eq_append_iff {xs : Vector α (n + m)} {f : (i : Nat) → α → (h : i < n + m) → β}
{ys : Vector β n} {zs : Vector β m} :
xs.mapFinIdx f = ys ++ zs
∃ (ys' : Vector α n) (zs' : Vector α m), xs = ys' ++ zs' ∧
ys'.mapFinIdx (fun i a h => f i a (by omega)) = ys
zs'.mapFinIdx (fun i a h => f (i + n) a (by omega)) = zs := by
rcases xs with ⟨xs, h⟩
rcases ys with ⟨ys, rfl⟩
rcases zs with ⟨zs, rfl⟩
simp only [mapFinIdx_mk, mk_append_mk, eq_mk, Array.mapFinIdx_eq_append_iff, toArray_mapFinIdx,
mk_eq, toArray_append, exists_and_left, exists_prop]
constructor
· rintro ⟨l₁', l₂', rfl, h₁, h₂⟩
· rintro ⟨ys', zs', rfl, h₁, h₂⟩
have h₁' := congrArg Array.size h₁
have h₂' := congrArg Array.size h₂
simp only [Array.size_mapFinIdx] at h₁' h₂'
exact ⟨⟨l₁', h₁'⟩, ⟨l₂', h₂'⟩, by simp_all⟩
· rintro ⟨⟨l₁, s₁⟩, ⟨l₂, s₂⟩, rfl, h₁, h₂⟩
refine ⟨l₁, l₂, by simp_all⟩
exact ⟨⟨ys', h₁'⟩, ⟨zs', h₂'⟩, by simp_all⟩
· rintro ⟨⟨ys', s₁⟩, ⟨zs', s₂⟩, rfl, h₁, h₂⟩
refine ⟨ys', zs', by simp_all⟩
theorem mapFinIdx_eq_push_iff {l : Vector α (n + 1)} {b : β} {f : (i : Nat) → α → (h : i < n + 1) → β} {l₂ : Vector β n} :
l.mapFinIdx f = l₂.push b ↔
∃ (l₁ : Vector α n) (a : α), l = l₁.push a ∧
l₁.mapFinIdx (fun i a h => f i a (by omega)) = l₂ ∧ b = f n a (by omega) := by
rcases l with ⟨l, h⟩
rcases l₂ with ⟨l₂, rfl⟩
theorem mapFinIdx_eq_push_iff {xs : Vector α (n + 1)} {b : β} {f : (i : Nat) → α → (h : i < n + 1) → β} {ys : Vector β n} :
xs.mapFinIdx f = ys.push b ↔
∃ (zs : Vector α n) (a : α), xs = zs.push a ∧
zs.mapFinIdx (fun i a h => f i a (by omega)) = ys ∧ b = f n a (by omega) := by
rcases xs with ⟨xs, h⟩
rcases ys with ⟨ys, rfl⟩
simp only [mapFinIdx_mk, push_mk, eq_mk, Array.mapFinIdx_eq_push_iff, mk_eq, toArray_push,
toArray_mapFinIdx]
constructor
· rintro ⟨l₁, a, rfl, h₁, rfl⟩
· rintro ⟨zs, a, rfl, h₁, rfl⟩
simp only [Array.size_push, Nat.add_right_cancel_iff] at h
exact ⟨⟨l₁, h⟩, a, by simp_all⟩
· rintro ⟨⟨l₁, h⟩, a, rfl, h₁, rfl⟩
exact ⟨l₁, a, by simp_all⟩
exact ⟨⟨zs, h⟩, a, by simp_all⟩
· rintro ⟨⟨zs, h⟩, a, rfl, h₁, rfl⟩
exact ⟨zs, a, by simp_all⟩
theorem mapFinIdx_eq_mapFinIdx_iff {l : Vector α n} {f g : (i : Nat) → α → (h : i < n) → β} :
l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i] h := by
theorem mapFinIdx_eq_mapFinIdx_iff {xs : Vector α n} {f g : (i : Nat) → α → (h : i < n) → β} :
xs.mapFinIdx f = xs.mapFinIdx g ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = g i xs[i] h := by
rw [eq_comm, mapFinIdx_eq_iff]
simp
@[simp] theorem mapFinIdx_mapFinIdx {l : Vector α n}
@[simp] theorem mapFinIdx_mapFinIdx {xs : Vector α n}
{f : (i : Nat) → α → (h : i < n) → β}
{g : (i : Nat) → β → (h : i < n) → γ} :
(l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) h) := by
(xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx (fun i a h => g i (f i a h) h) := by
simp [mapFinIdx_eq_iff]
theorem mapFinIdx_eq_mkVector_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
l.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = b := by
rcases l with ⟨l, rfl⟩
theorem mapFinIdx_eq_mkVector_iff {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
xs.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] h = b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mapFinIdx_eq_mkArray_iff]
@[simp] theorem mapFinIdx_reverse {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
l.reverse.mapFinIdx f = (l.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse := by
rcases l with ⟨l, rfl⟩
@[simp] theorem mapFinIdx_reverse {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse := by
rcases xs with ⟨xs, rfl⟩
simp
/-! ### mapIdx -/
@ -236,43 +233,43 @@ theorem mapFinIdx_eq_mkVector_iff {l : Vector α n} {f : (i : Nat) → α → (h
theorem mapIdx_empty {f : Nat → α → β} : mapIdx f #v[] = #v[] :=
rfl
@[simp] theorem mapFinIdx_eq_mapIdx {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {g : Nat → α → β}
(h : ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i]) :
l.mapFinIdx f = l.mapIdx g := by
@[simp] theorem mapFinIdx_eq_mapIdx {xs : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {g : Nat → α → β}
(h : ∀ (i : Nat) (h : i < n), f i xs[i] h = g i xs[i]) :
xs.mapFinIdx f = xs.mapIdx g := by
simp_all [mapFinIdx_eq_iff]
theorem mapIdx_eq_mapFinIdx {l : Vector α n} {f : Nat → α → β} :
l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
theorem mapIdx_eq_mapFinIdx {xs : Vector α n} {f : Nat → α → β} :
xs.mapIdx f = xs.mapFinIdx (fun i a _ => f i a) := by
simp [mapFinIdx_eq_mapIdx]
theorem mapIdx_eq_zipIdx_map {l : Vector α n} {f : Nat → α → β} :
l.mapIdx f = l.zipIdx.map fun ⟨a, i⟩ => f i a := by
theorem mapIdx_eq_zipIdx_map {xs : Vector α n} {f : Nat → α → β} :
xs.mapIdx f = xs.zipIdx.map fun ⟨a, i⟩ => f i a := by
ext <;> simp
@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-27")]
abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
theorem mapIdx_append {K : Vector α n} {L : Vector α m} :
(K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size) := by
rcases K with ⟨K, rfl⟩
rcases L with ⟨L, rfl⟩
theorem mapIdx_append {xs : Vector α n} {ys : Vector α m} :
(xs ++ ys).mapIdx f = xs.mapIdx f ++ ys.mapIdx fun i => f (i + xs.size) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, rfl⟩
simp [Array.mapIdx_append]
@[simp]
theorem mapIdx_push {l : Vector α n} {a : α} :
mapIdx f (l.push a) = (mapIdx f l).push (f l.size a) := by
theorem mapIdx_push {xs : Vector α n} {a : α} :
mapIdx f (xs.push a) = (mapIdx f xs).push (f xs.size a) := by
simp [← append_singleton, mapIdx_append]
theorem mapIdx_singleton {a : α} : mapIdx f #v[a] = #v[f 0 a] := by
simp
theorem exists_of_mem_mapIdx {b : β} {l : Vector α n}
(h : b ∈ l.mapIdx f) : ∃ (i : Nat) (h : i < n), f i l[i] = b := by
theorem exists_of_mem_mapIdx {b : β} {xs : Vector α n}
(h : b ∈ xs.mapIdx f) : ∃ (i : Nat) (h : i < n), f i xs[i] = b := by
rw [mapIdx_eq_mapFinIdx] at h
simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h
@[simp] theorem mem_mapIdx {b : β} {l : Vector α n} :
b ∈ l.mapIdx f ↔ ∃ (i : Nat) (h : i < n), f i l[i] = b := by
@[simp] theorem mem_mapIdx {b : β} {xs : Vector α n} :
b ∈ xs.mapIdx f ↔ ∃ (i : Nat) (h : i < n), f i xs[i] = b := by
constructor
· intro h
exact exists_of_mem_mapIdx h
@ -280,37 +277,37 @@ theorem exists_of_mem_mapIdx {b : β} {l : Vector α n}
rw [mem_iff_getElem]
exact ⟨i, by simpa using h, by simp⟩
theorem mapIdx_eq_push_iff {l : Vector α (n + 1)} {b : β} :
mapIdx f l = l₂.push b ↔
∃ (a : α) (l₁ : Vector α n), l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b := by
theorem mapIdx_eq_push_iff {xs : Vector α (n + 1)} {b : β} :
mapIdx f xs = ys.push b ↔
∃ (a : α) (zs : Vector α n), xs = zs.push a ∧ mapIdx f zs = ys ∧ f zs.size a = b := by
rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_push_iff]
simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
constructor
· rintro ⟨l₁, a, rfl, rfl, rfl⟩
exact ⟨a, l₁, by simp⟩
· rintro ⟨a, l₁, rfl, rfl, rfl⟩
exact ⟨l₁, a, rfl, by simp⟩
· rintro ⟨zs, a, rfl, rfl, rfl⟩
exact ⟨a, zs, by simp⟩
· rintro ⟨a, zs, rfl, rfl, rfl⟩
exact ⟨zs, a, rfl, by simp⟩
@[simp] theorem mapIdx_eq_singleton_iff {l : Vector α 1} {f : Nat → α → β} {b : β} :
mapIdx f l = #v[b] ↔ ∃ (a : α), l = #v[a] ∧ f 0 a = b := by
rcases l with ⟨l
@[simp] theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat → α → β} {b : β} :
mapIdx f xs = #v[b] ↔ ∃ (a : α), xs = #v[a] ∧ f 0 a = b := by
rcases xs with ⟨xs
simp
theorem mapIdx_eq_append_iff {l : Vector α (n + m)} {f : Nat → α → β} {l₁ : Vector β n} {l₂ : Vector β m} :
mapIdx f l = l₁ ++ l₂
∃ (l₁' : Vector α n) (l₂' : Vector α m), l = l₁' ++ l₂' ∧
l₁'.mapIdx f = l₁
l₂'.mapIdx (fun i => f (i + l₁'.size)) = l₂ := by
rcases l with ⟨l, h⟩
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, rfl⟩
theorem mapIdx_eq_append_iff {xs : Vector α (n + m)} {f : Nat → α → β} {ys : Vector β n} {zs : Vector β m} :
mapIdx f xs = ys ++ zs
∃ (ys' : Vector α n) (zs' : Vector α m), xs = ys' ++ zs' ∧
ys'.mapIdx f = ys
zs'.mapIdx (fun i => f (i + ys'.size)) = zs := by
rcases xs with ⟨xs, h⟩
rcases ys with ⟨ys, rfl⟩
rcases zs with ⟨zs, rfl⟩
rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]
simp
theorem mapIdx_eq_iff {l : Vector α n} :
mapIdx f l = l' ↔ ∀ (i : Nat) (h : i < n), f i l[i] = l'[i] := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem mapIdx_eq_iff {xs : Vector α n} {f : Nat → α → β} {ys : Vector β n} :
mapIdx f xs = ys ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = ys[i] := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, h⟩
simp only [mapIdx_mk, eq_mk, Array.mapIdx_eq_iff, getElem_mk]
constructor
· rintro h' i h
@ -318,58 +315,58 @@ theorem mapIdx_eq_iff {l : Vector α n} :
simp_all
· intro h' i
specialize h' i
by_cases w : i < l.size
by_cases w : i < xs.size
· specialize h' w
simp_all
· simp only [Nat.not_lt] at w
simp_all [Array.getElem?_eq_none_iff.mpr w]
theorem mapIdx_eq_mapIdx_iff {l : Vector α n} :
mapIdx f l = mapIdx g l ↔ ∀ (i : Nat) (h : i < n), f i l[i] = g i l[i] := by
rcases l with ⟨l, rfl⟩
theorem mapIdx_eq_mapIdx_iff {xs : Vector α n} :
mapIdx f xs = mapIdx g xs ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = g i xs[i] := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mapIdx_eq_mapIdx_iff]
@[simp] theorem mapIdx_set {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
(l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) (by simpa) := by
rcases l with ⟨l, rfl⟩
@[simp] theorem mapIdx_set {xs : Vector α n} {i : Nat} {h : i < n} {a : α} :
(xs.set i a).mapIdx f = (xs.mapIdx f).set i (f i a) (by simpa) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem mapIdx_setIfInBounds {l : Vector α n} {i : Nat} {a : α} :
(l.setIfInBounds i a).mapIdx f = (l.mapIdx f).setIfInBounds i (f i a) := by
rcases l with ⟨l, rfl⟩
@[simp] theorem mapIdx_setIfInBounds {xs : Vector α n} {i : Nat} {a : α} :
(xs.setIfInBounds i a).mapIdx f = (xs.mapIdx f).setIfInBounds i (f i a) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem back?_mapIdx {l : Vector α n} {f : Nat → α → β} :
(mapIdx f l).back? = (l.back?).map (f (l.size - 1)) := by
rcases l with ⟨l, rfl⟩
@[simp] theorem back?_mapIdx {xs : Vector α n} {f : Nat → α → β} :
(mapIdx f xs).back? = (xs.back?).map (f (xs.size - 1)) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem back_mapIdx [NeZero n] {l : Vector α n} {f : Nat → α → β} :
(mapIdx f l).back = f (l.size - 1) (l.back) := by
rcases l with ⟨l, rfl⟩
@[simp] theorem back_mapIdx [NeZero n] {xs : Vector α n} {f : Nat → α → β} :
(mapIdx f xs).back = f (xs.size - 1) (xs.back) := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem mapIdx_mapIdx {l : Vector α n} {f : Nat → α → β} {g : Nat → β → γ} :
(l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i) := by
@[simp] theorem mapIdx_mapIdx {xs : Vector α n} {f : Nat → α → β} {g : Nat → β → γ} :
(xs.mapIdx f).mapIdx g = xs.mapIdx (fun i => g i ∘ f i) := by
simp [mapIdx_eq_iff]
theorem mapIdx_eq_mkVector_iff {l : Vector α n} {f : Nat → α → β} {b : β} :
mapIdx f l = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] = b := by
rcases l with ⟨l, rfl⟩
theorem mapIdx_eq_mkVector_iff {xs : Vector α n} {f : Nat → α → β} {b : β} :
mapIdx f xs = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i xs[i] = b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mapIdx_eq_mkArray_iff]
@[simp] theorem mapIdx_reverse {l : Vector α n} {f : Nat → α → β} :
l.reverse.mapIdx f = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse := by
rcases l with ⟨l, rfl⟩
@[simp] theorem mapIdx_reverse {xs : Vector α n} {f : Nat → α → β} :
xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by
rcases xs with ⟨xs, rfl⟩
simp [Array.mapIdx_reverse]
theorem toArray_mapFinIdxM [Monad m] [LawfulMonad m]
(a : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) :
toArray <$> a.mapFinIdxM f = a.toArray.mapFinIdxM
(fun i x h => f i x (size_toArray a ▸ h)) := by
(xs : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) :
toArray <$> xs.mapFinIdxM f = xs.toArray.mapFinIdxM
(fun i x h => f i x (size_toArray xs ▸ h)) := by
let rec go (i j : Nat) (inv : i + j = n) (bs : Vector β (n - i)) :
toArray <$> mapFinIdxM.map a f i j inv bs
= Array.mapFinIdxM.map a.toArray (fun i x h => f i x (size_toArray a ▸ h))
toArray <$> mapFinIdxM.map xs f i j inv bs
= Array.mapFinIdxM.map xs.toArray (fun i x h => f i x (size_toArray xs ▸ h))
i j (size_toArray _ ▸ inv) bs.toArray := by
match i with
| 0 => simp only [mapFinIdxM.map, map_pure, Array.mapFinIdxM.map, Nat.sub_zero]
@ -380,8 +377,8 @@ theorem toArray_mapFinIdxM [Monad m] [LawfulMonad m]
simp only [mapFinIdxM, Array.mapFinIdxM, size_toArray]
exact go _ _ _ _
theorem toArray_mapIdxM [Monad m] [LawfulMonad m] (a : Vector α n) (f : Nat → α → m β) :
toArray <$> a.mapIdxM f = a.toArray.mapIdxM f := by
theorem toArray_mapIdxM [Monad m] [LawfulMonad m] (xs : Vector α n) (f : Nat → α → m β) :
toArray <$> xs.mapIdxM f = xs.toArray.mapIdxM f := by
exact toArray_mapFinIdxM _ _
end Vector

View file

@ -13,6 +13,9 @@ import Init.Control.Lawful.Lemmas
# Lemmas about `Vector.forIn'` and `Vector.forIn`.
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
open Nat
@ -20,15 +23,15 @@ open Nat
/-! ## Monadic operations -/
@[simp] theorem map_toArray_inj [Monad m] [LawfulMonad m]
{v₁ : m (Vector α n)} {v₂ : m (Vector α n)} :
toArray <$> v₁ = toArray <$> v₂ ↔ v₁ = v₂ :=
{xs : m (Vector α n)} {ys : m (Vector α n)} :
toArray <$> xs = toArray <$> ys ↔ xs = ys :=
_root_.map_inj_right (by simp)
/-! ### mapM -/
@[congr] theorem mapM_congr [Monad m] {as bs : Vector α n} (w : as = bs)
@[congr] theorem mapM_congr [Monad m] {xs ys : Vector α n} (w : xs = ys)
{f : α → m β} :
as.mapM f = bs.mapM f := by
xs.mapM f = ys.mapM f := by
subst w
simp
@ -39,62 +42,62 @@ open Nat
simp
@[simp] theorem mapM_append [Monad m] [LawfulMonad m]
(f : α → m β) {l₁ : Vector α n} {l₂ : Vector α n'} :
(l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by
(f : α → m β) {xs : Vector α n} {ys : Vector α n'} :
(xs ++ ys).mapM f = (return (← xs.mapM f) ++ (← ys.mapM f)) := by
apply map_toArray_inj.mp
suffices toArray <$> (l₁ ++ l₂).mapM f = (return (← toArray <$> l₁.mapM f) ++ (← toArray <$> l₂.mapM f)) by
suffices toArray <$> (xs ++ ys).mapM f = (return (← toArray <$> xs.mapM f) ++ (← toArray <$> ys.mapM f)) by
rw [this]
simp only [bind_pure_comp, Functor.map_map, bind_map_left, map_bind, toArray_append]
simp
/-! ### foldlM and foldrM -/
theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Vector β₁ n) (init : α) :
(l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
rcases l with ⟨l, rfl⟩
theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (xs : Vector β₁ n) (init : α) :
(xs.map f).foldlM g init = xs.foldlM (fun x y => g x (f y)) init := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldlM_map]
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Vector β₁ n)
(init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
rcases l with ⟨l, rfl⟩
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (xs : Vector β₁ n)
(init : α) : (xs.map f).foldrM g init = xs.foldrM (fun x y => g (f x) y) init := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldrM_map]
theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Vector α n) (init : γ) :
(l.filterMap f).foldlM g init =
l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
rcases l with ⟨l, rfl⟩
theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (xs : Vector α n) (init : γ) :
(xs.filterMap f).foldlM g init =
xs.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldlM_filterMap]
rfl
theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Vector α n) (init : γ) :
(l.filterMap f).foldrM g init =
l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
rcases l with ⟨l, rfl⟩
theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (xs : Vector α n) (init : γ) :
(xs.filterMap f).foldrM g init =
xs.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldrM_filterMap]
rfl
theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Vector α n) (init : β) :
(l.filter p).foldlM g init =
l.foldlM (fun x y => if p y then g x y else pure x) init := by
rcases l with ⟨l, rfl⟩
theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (xs : Vector α n) (init : β) :
(xs.filter p).foldlM g init =
xs.foldlM (fun x y => if p y then g x y else pure x) init := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldlM_filter]
theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Vector α n) (init : β) :
(l.filter p).foldrM g init =
l.foldrM (fun x y => if p x then g x y else pure y) init := by
rcases l with ⟨l, rfl⟩
theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (xs : Vector α n) (init : β) :
(xs.filter p).foldrM g init =
xs.foldrM (fun x y => if p x then g x y else pure y) init := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldrM_filter]
@[simp] theorem foldlM_attachWith [Monad m]
(l : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} :
(l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
rcases l with ⟨l, rfl⟩
(xs : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ xs → q a) {f : β → { x // q x} → m β} {b} :
(xs.attachWith q H).foldlM f b = xs.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldlM_map]
@[simp] theorem foldrM_attachWith [Monad m] [LawfulMonad m]
(l : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} :
(l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
rcases l with ⟨l, rfl⟩
(xs : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ xs → q a) {f : { x // q x} → β → m β} {b} :
(xs.attachWith q H).foldrM f b = xs.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
rcases xs with ⟨xs, rfl⟩
simp [Array.foldrM_map]
/-! ### forM -/
@ -105,26 +108,26 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β
cases as <;> cases bs
simp_all
@[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ : Vector α n) (l₂ : Vector α n') (f : α → m PUnit) :
forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f) := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, rfl⟩
@[simp] theorem forM_append [Monad m] [LawfulMonad m] (xs : Vector α n) (ys : Vector α n') (f : α → m PUnit) :
forM (xs ++ ys) f = (do forM xs f; forM ys f) := by
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, rfl⟩
simp
@[simp] theorem forM_map [Monad m] [LawfulMonad m] (l : Vector α n) (g : α → β) (f : β → m PUnit) :
forM (l.map g) f = forM l (fun a => f (g a)) := by
cases l
@[simp] theorem forM_map [Monad m] [LawfulMonad m] (xs : Vector α n) (g : α → β) (f : β → m PUnit) :
forM (xs.map g) f = forM xs (fun a => f (g a)) := by
rcases xs with ⟨xs, rfl⟩
simp
/-! ### forIn' -/
@[congr] theorem forIn'_congr [Monad m] {as bs : Vector α n} (w : as = bs)
@[congr] theorem forIn'_congr [Monad m] {xs ys : Vector α n} (w : xs = ys)
{b b' : β} (hb : b = b')
{f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
{g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
{f : (a' : α) → a' ∈ xs → β → m (ForInStep β)}
{g : (a' : α) → a' ∈ ys → β → m (ForInStep β)}
(h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
forIn' as b f = forIn' bs b' g := by
cases as <;> cases bs
forIn' xs b f = forIn' ys b' g := by
cases xs <;> cases ys
simp only [eq_mk, mem_mk, forIn'_mk] at w h ⊢
exact Array.forIn'_congr w hb h
@ -133,41 +136,41 @@ We can express a for loop over a vector as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
(l : Vector α n) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
forIn' l init f = ForInStep.value <$>
l.attach.foldlM (fun b ⟨a, m⟩ => match b with
(xs : Vector α n) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (init : β) :
forIn' xs init f = ForInStep.value <$>
xs.attach.foldlM (fun b ⟨a, m⟩ => match b with
| .yield b => f a m b
| .done b => pure (.done b)) (ForInStep.yield init) := by
rcases l with ⟨l, rfl⟩
rcases xs with ⟨xs, rfl⟩
simp [Array.forIn'_eq_foldlM]
rfl
/-- We can express a for loop over a vector which always yields as a fold. -/
@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
(l : Vector α n) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
rcases l with ⟨l, rfl⟩
(xs : Vector α n) (f : (a : α) → a ∈ xs → β → m γ) (g : (a : α) → a ∈ xs → β → γ → β) (init : β) :
forIn' xs init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
xs.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
rcases xs with ⟨xs, rfl⟩
simp
theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
(l : Vector α n) (f : (a : α) → a ∈ l → β → β) (init : β) :
forIn' l init (fun a m b => pure (.yield (f a m b))) =
pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
rcases l with ⟨l, rfl⟩
(xs : Vector α n) (f : (a : α) → a ∈ xs → β → β) (init : β) :
forIn' xs init (fun a m b => pure (.yield (f a m b))) =
pure (f := m) (xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]
@[simp] theorem forIn'_yield_eq_foldl
(l : Vector α n) (f : (a : α) → a ∈ l → β → β) (init : β) :
forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
cases l
(xs : Vector α n) (f : (a : α) → a ∈ xs → β → β) (init : β) :
forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
rcases xs with ⟨xs, rfl⟩
simp [List.foldl_map]
@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
(l : Vector α n) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y := by
cases l
(xs : Vector α n) (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
forIn' (xs.map g) init f = forIn' xs init fun a h y => f (g a) (mem_map_of_mem g h) y := by
rcases xs with ⟨xs, rfl⟩
simp
/--
@ -175,41 +178,41 @@ We can express a for loop over a vector as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
(f : α → β → m (ForInStep β)) (init : β) (l : Vector α n) :
forIn l init f = ForInStep.value <$>
l.foldlM (fun b a => match b with
(f : α → β → m (ForInStep β)) (init : β) (xs : Vector α n) :
forIn xs init f = ForInStep.value <$>
xs.foldlM (fun b a => match b with
| .yield b => f a b
| .done b => pure (.done b)) (ForInStep.yield init) := by
rcases l with ⟨l, rfl⟩
rcases xs with ⟨xs, rfl⟩
simp [Array.forIn_eq_foldlM]
rfl
/-- We can express a for loop over a vector which always yields as a fold. -/
@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
(l : Vector α n) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
l.foldlM (fun b a => g a b <$> f a b) init := by
cases l
(xs : Vector α n) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
forIn xs init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
xs.foldlM (fun b a => g a b <$> f a b) init := by
rcases xs with ⟨xs, rfl⟩
simp
theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
(l : Vector α n) (f : α → β → β) (init : β) :
forIn l init (fun a b => pure (.yield (f a b))) =
pure (f := m) (l.foldl (fun b a => f a b) init) := by
rcases l with ⟨l, rfl⟩
(xs : Vector α n) (f : α → β → β) (init : β) :
forIn xs init (fun a b => pure (.yield (f a b))) =
pure (f := m) (xs.foldl (fun b a => f a b) init) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]
@[simp] theorem forIn_yield_eq_foldl
(l : Vector α n) (f : α → β → β) (init : β) :
forIn (m := Id) l init (fun a b => .yield (f a b)) =
l.foldl (fun b a => f a b) init := by
cases l
(xs : Vector α n) (f : α → β → β) (init : β) :
forIn (m := Id) xs init (fun a b => .yield (f a b)) =
xs.foldl (fun b a => f a b) init := by
rcases xs with ⟨xs, rfl⟩
simp
@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
(l : Vector α n) (g : α → β) (f : β → γ → m (ForInStep γ)) :
forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
cases l
(xs : Vector α n) (g : α → β) (f : β → γ → m (ForInStep γ)) :
forIn (xs.map g) init f = forIn xs init fun a y => f (g a) y := by
rcases xs with ⟨xs, rfl⟩
simp
end Vector

View file

@ -11,6 +11,9 @@ import Init.Data.Array.OfFn
# Theorems about `Vector.ofFn`
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :

View file

@ -14,6 +14,9 @@ import Init.Data.Array.Range
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
open Nat
@ -127,9 +130,9 @@ theorem range_succ (n : Nat) : range (succ n) = range n ++ #v[n] := by
rw [← toArray_inj]
simp [Array.range_succ]
theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
rw [← range'_eq_map_range]
simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
simp [← toList_inj, List.reverse_range']
@ -142,7 +145,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
@[simp] theorem take_range (m n : Nat) : take (range n) m = range (min m n) := by
@[simp] theorem take_range (n i : Nat) : take (range n) i = range (min i n) := by
ext <;> simp
erw [getElem_extract] -- Why is an `erw` needed here? This should be by simp!
simp
@ -158,43 +161,43 @@ theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
/-! ### zipIdx -/
@[simp]
theorem getElem?_zipIdx (l : Vector α n) (n m) : (zipIdx l n)[m]? = l[m]?.map fun a => (a, n + m) := by
theorem getElem?_zipIdx (xs : Vector α n) (i j) : (zipIdx xs i)[j]? = xs[j]?.map fun a => (a, i + j) := by
simp [getElem?_def]
theorem map_snd_add_zipIdx_eq_zipIdx (l : Vector α n) (m k : Nat) :
map (Prod.map id (· + m)) (zipIdx l k) = zipIdx l (m + k) := by
theorem map_snd_add_zipIdx_eq_zipIdx (xs : Vector α n) (m k : Nat) :
map (Prod.map id (· + m)) (zipIdx xs k) = zipIdx xs (m + k) := by
ext <;> simp <;> omega
@[simp]
theorem zipIdx_map_snd (m) (l : Vector α n) : map Prod.snd (zipIdx l m) = range' m n := by
rcases l with ⟨l, rfl⟩
theorem zipIdx_map_snd (i) (xs : Vector α n) : map Prod.snd (zipIdx xs i) = range' i n := by
rcases xs with ⟨xs, rfl⟩
simp [Array.zipIdx_map_snd]
@[simp]
theorem zipIdx_map_fst (m) (l : Vector α n) : map Prod.fst (zipIdx l m) = l := by
rcases l with ⟨l, rfl⟩
theorem zipIdx_map_fst (i) (xs : Vector α n) : map Prod.fst (zipIdx xs i) = xs := by
rcases xs with ⟨xs, rfl⟩
simp [Array.zipIdx_map_fst]
theorem zipIdx_eq_zip_range' (l : Vector α n) : l.zipIdx m = l.zip (range' m n) := by
theorem zipIdx_eq_zip_range' (xs : Vector α n) : xs.zipIdx i = xs.zip (range' i n) := by
simp [zip_of_prod (zipIdx_map_fst _ _) (zipIdx_map_snd _ _)]
@[simp]
theorem unzip_zipIdx_eq_prod (l : Vector α n) {m : Nat} :
(l.zipIdx m).unzip = (l, range' m n) := by
theorem unzip_zipIdx_eq_prod (xs : Vector α n) {i : Nat} :
(xs.zipIdx i).unzip = (xs, range' i n) := by
simp only [zipIdx_eq_zip_range', unzip_zip]
/-- Replace `zipIdx` with a starting index `m+1` with `zipIdx` starting from `m`,
/-- Replace `zipIdx` with a starting index `i+1` with `zipIdx` starting from `i`,
followed by a `map` increasing the indices by one. -/
theorem zipIdx_succ (l : Vector α n) (m : Nat) :
l.zipIdx (m + 1) = (l.zipIdx m).map (fun ⟨a, i⟩ => (a, i + 1)) := by
rcases l with ⟨l, rfl⟩
theorem zipIdx_succ (xs : Vector α n) (i : Nat) :
xs.zipIdx (i + 1) = (xs.zipIdx i).map (fun ⟨a, i⟩ => (a, i + 1)) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.zipIdx_succ]
/-- Replace `zipIdx` with a starting index with `zipIdx` starting from 0,
followed by a `map` increasing the indices. -/
theorem zipIdx_eq_map_add (l : Vector α n) (m : Nat) :
l.zipIdx m = l.zipIdx.map (fun ⟨a, i⟩ => (a, m + i)) := by
rcases l with ⟨l, rfl⟩
theorem zipIdx_eq_map_add (xs : Vector α n) (i : Nat) :
xs.zipIdx i = xs.zipIdx.map (fun ⟨a, j⟩ => (a, i + j)) := by
rcases xs with ⟨xs, rfl⟩
simp only [zipIdx_mk, map_mk, eq_mk]
rw [Array.zipIdx_eq_map_add]
@ -202,34 +205,34 @@ theorem zipIdx_eq_map_add (l : Vector α n) (m : Nat) :
theorem zipIdx_singleton (x : α) (k : Nat) : zipIdx #v[x] k = #v[(x, k)] :=
rfl
theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : Vector α n} :
(x, k + i) ∈ zipIdx l k ↔ l[i]? = some x := by
theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {xs : Vector α n} :
(x, k + i) ∈ zipIdx xs k ↔ xs[i]? = some x := by
simp [mem_iff_getElem?, and_left_comm]
theorem le_snd_of_mem_zipIdx {x : α × Nat} {k : Nat} {l : Vector α n} (h : x ∈ zipIdx l k) :
theorem le_snd_of_mem_zipIdx {x : α × Nat} {k : Nat} {xs : Vector α n} (h : x ∈ zipIdx xs k) :
k ≤ x.2 :=
(mk_mem_zipIdx_iff_le_and_getElem?_sub.1 h).1
theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ zipIdx l k) :
theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {k : Nat} {xs : Vector α n} (h : x ∈ zipIdx xs k) :
x.2 < k + n := by
rcases mem_iff_getElem.1 h with ⟨i, h', rfl⟩
simpa using h'
theorem snd_lt_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ l.zipIdx k) :
theorem snd_lt_of_mem_zipIdx {x : α × Nat} {k : Nat} {xs : Vector α n} (h : x ∈ zipIdx xs k) :
x.2 < n + k := by
simpa [Nat.add_comm] using snd_lt_add_of_mem_zipIdx h
theorem map_zipIdx (f : α → β) (l : Vector α n) (k : Nat) :
map (Prod.map f id) (zipIdx l k) = zipIdx (l.map f) k := by
cases l
theorem map_zipIdx (f : α → β) (xs : Vector α n) (k : Nat) :
map (Prod.map f id) (zipIdx xs k) = zipIdx (xs.map f) k := by
rcases xs with ⟨xs, rfl⟩
simp [Array.map_zipIdx]
theorem fst_mem_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ zipIdx l k) : x.1 ∈ l :=
zipIdx_map_fst k l ▸ mem_map_of_mem _ h
theorem fst_mem_of_mem_zipIdx {x : α × Nat} {xs : Vector α n} {k : Nat} (h : x ∈ zipIdx xs k) : x.1 ∈ xs :=
zipIdx_map_fst k xs ▸ mem_map_of_mem _ h
theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ zipIdx l k) :
x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) := by
cases l
theorem fst_eq_of_mem_zipIdx {x : α × Nat} {xs : Vector α n} {k : Nat} (h : x ∈ zipIdx xs k) :
x.1 = xs[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) := by
cases xs
exact Array.fst_eq_of_mem_zipIdx (by simpa using h)
theorem mem_zipIdx {x : α} {i : Nat} {xs : Vector α n} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
@ -242,9 +245,9 @@ theorem mem_zipIdx' {x : α} {i : Nat} {xs : Vector α n} (h : (x, i) ∈ xs.zip
i < n ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
⟨by simpa using snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩
theorem zipIdx_map (l : Vector α n) (k : Nat) (f : α → β) :
zipIdx (l.map f) k = (zipIdx l k).map (Prod.map f id) := by
cases l
theorem zipIdx_map (xs : Vector α n) (k : Nat) (f : α → β) :
zipIdx (xs.map f) k = (zipIdx xs k).map (Prod.map f id) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.zipIdx_map]
theorem zipIdx_append (xs : Vector α n) (ys : Vector α m) (k : Nat) :
@ -253,19 +256,19 @@ theorem zipIdx_append (xs : Vector α n) (ys : Vector α m) (k : Nat) :
rcases ys with ⟨ys, rfl⟩
simp [Array.zipIdx_append]
theorem zipIdx_eq_append_iff {l : Vector α (n + m)} {k : Nat} :
zipIdx l k = l₁ ++ l₂
∃ (l₁' : Vector α n) (l₂' : Vector α m),
l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + n) := by
rcases l with ⟨l, h⟩
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, rfl⟩
theorem zipIdx_eq_append_iff {xs : Vector α (n + m)} {k : Nat} :
zipIdx xs k = ys ++ zs
∃ (ys' : Vector α n) (zs' : Vector α m),
xs = ys' ++ zs' ∧ ys = zipIdx ys' k ∧ zs = zipIdx zs' (k + n) := by
rcases xs with ⟨xs, h⟩
rcases ys with ⟨ys, rfl⟩
rcases zs with ⟨zs, rfl⟩
simp only [zipIdx_mk, mk_append_mk, eq_mk, Array.zipIdx_eq_append_iff, mk_eq, toArray_append,
toArray_zipIdx]
constructor
· rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
exact ⟨⟨l₁', by simp⟩, ⟨l₂', by simp⟩, by simp⟩
· rintro ⟨⟨l₁', h₁⟩, ⟨l₂', h₂⟩, rfl, w₁, w₂⟩
exact ⟨l₁', l₂', by simp, w₁, by simp [h₁, w₂]⟩
· rintro ⟨ys', zs', rfl, rfl, rfl⟩
exact ⟨⟨ys', by simp⟩, ⟨zs', by simp⟩, by simp⟩
· rintro ⟨⟨ys', h₁⟩, ⟨zs', h₂⟩, rfl, w₁, w₂⟩
exact ⟨ys', zs', by simp, w₁, by simp [h₁, w₂]⟩
end Vector

View file

@ -11,6 +11,9 @@ import Init.Data.Vector.Lemmas
# Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`.
-/
-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Vector
open Nat
@ -19,20 +22,20 @@ open Nat
/-! ### zipWith -/
theorem zipWith_comm (f : α → β → γ) (la : Vector α n) (lb : Vector β n) :
zipWith f la lb = zipWith (fun b a => f a b) lb la := by
rcases la with ⟨la, rfl⟩
rcases lb with ⟨lb, h⟩
theorem zipWith_comm (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
zipWith f as bs = zipWith (fun b a => f a b) bs as := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simpa using Array.zipWith_comm _ _ _
theorem zipWith_comm_of_comm (f : αα → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Vector α n) :
zipWith f l l' = zipWith f l' l := by
theorem zipWith_comm_of_comm (f : αα → β) (comm : ∀ x y : α, f x y = f y x) (xs ys : Vector α n) :
zipWith f xs ys = zipWith f ys xs := by
rw [zipWith_comm]
simp only [comm]
@[simp]
theorem zipWith_self (f : αα → δ) (l : Vector α n) : zipWith f l l = l.map fun a => f a a := by
cases l
theorem zipWith_self (f : αα → δ) (xs : Vector α n) : zipWith f xs xs = xs.map fun a => f a a := by
cases xs
simp
/--
@ -49,192 +52,192 @@ theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/
theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
(zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by
cases l₁
cases l₂
(zipWith f as bs)[i]? = (as[i]?.map f).bind fun g => bs[i]?.map g := by
cases as
cases bs
simp [Array.getElem?_zipWith']
theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Vector α n} {l₂ : Vector β n} {z : γ} {i : Nat} :
(zipWith f l₁ l₂)[i]? = some z ↔
∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by
cases l₁
cases l₂
theorem getElem?_zipWith_eq_some {f : α → β → γ} {as : Vector α n} {bs : Vector β n} {z : γ} {i : Nat} :
(zipWith f as bs)[i]? = some z ↔
∃ x y, as[i]? = some x ∧ bs[i]? = some y ∧ f x y = z := by
cases as
cases bs
simp [Array.getElem?_zipWith_eq_some]
theorem getElem?_zip_eq_some {l₁ : Vector α n} {l₂ : Vector β n} {z : α × β} {i : Nat} :
(zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem getElem?_zip_eq_some {as : Vector α n} {bs : Vector β n} {z : α × β} {i : Nat} :
(zip as bs)[i]? = some z ↔ as[i]? = some z.1 ∧ bs[i]? = some z.2 := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.getElem?_zip_eq_some]
@[simp]
theorem zipWith_map {μ} (f : γ → δ → μ) (g : αγ) (h : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) :
zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem zipWith_map {μ} (f : γ → δ → μ) (g : αγ) (h : β → δ) (as : Vector α n) (bs : Vector β n) :
zipWith f (as.map g) (bs.map h) = zipWith (fun a b => f (g a) (h b)) as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.zipWith_map]
theorem zipWith_map_left (l₁ : Vector α n) (l₂ : Vector β n) (f : αα') (g : α' → β → γ) :
zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem zipWith_map_left (as : Vector α n) (bs : Vector β n) (f : αα') (g : α' → β → γ) :
zipWith g (as.map f) bs = zipWith (fun a b => g (f a) b) as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.zipWith_map_left]
theorem zipWith_map_right (l₁ : Vector α n) (l₂ : Vector β n) (f : β → β') (g : α → β' → γ) :
zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem zipWith_map_right (as : Vector α n) (bs : Vector β n) (f : β → β') (g : α → β' → γ) :
zipWith g as (bs.map f) = zipWith (fun a b => g a (f b)) as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.zipWith_map_right]
theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
(zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
(zipWith f as bs).foldr g i = (zip as bs).foldr (fun p r => g (f p.1 p.2) r) i := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simpa using Array.zipWith_foldr_eq_zip_foldr _
theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
(zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
(zipWith f as bs).foldl g i = (zip as bs).foldl (fun r p => g r (f p.1 p.2)) i := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simpa using Array.zipWith_foldl_eq_zip_foldl _
theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Vector γ n) (l' : Vector δ n) :
map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (as : Vector γ n) (bs : Vector δ n) :
map f (zipWith g as bs) = zipWith (fun x y => f (g x y)) as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.map_zipWith]
theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem take_zipWith : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i) := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.take_zipWith]
theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n) := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem extract_zipWith : (zipWith f as bs).extract i j = zipWith f (as.extract i j) (bs.extract i j) := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.extract_zipWith]
theorem zipWith_append (f : α → β → γ)
(l : Vector α n) (la : Vector α m) (l' : Vector β n) (lb : Vector β m) :
zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
rcases la with ⟨la, rfl⟩
rcases lb with ⟨lb, h'⟩
(as : Vector α n) (as' : Vector α m) (bs : Vector β n) (bs' : Vector β m) :
zipWith f (as ++ as') (bs ++ bs') = zipWith f as bs ++ zipWith f as' bs' := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
rcases as' with ⟨as', rfl⟩
rcases bs' with ⟨bs', h'⟩
simp [Array.zipWith_append, *]
theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} :
zipWith f l₁ l₂ = l₁' ++ l₂'
w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by
rcases l₁ with ⟨l₁, h₁⟩
rcases l₂ with ⟨l₂, h₂⟩
rcases l₁' with ⟨l₁', rfl⟩
rcases l₂' with ⟨l₂', rfl⟩
theorem zipWith_eq_append_iff {f : α → β → γ} {as : Vector α (n + m)} {bs : Vector β (n + m)} :
zipWith f as bs = xs ++ ys
as₁ as₂ bs₁ bs₂, as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zipWith f as₁ bs₁ ∧ ys = zipWith f as₂ bs₂ := by
rcases as with ⟨as, h₁⟩
rcases bs with ⟨bs, h₂⟩
rcases xs with ⟨xs, rfl⟩
rcases ys with ⟨ys, rfl⟩
simp only [mk_zipWith_mk, mk_append_mk, eq_mk, Array.zipWith_eq_append_iff,
mk_eq, toArray_append, toArray_zipWith]
constructor
· rintro ⟨w, x, y, z, h, rfl, rfl, rfl, rfl⟩
· rintro ⟨as₁, as₂, bs₁, bs₂, h, rfl, rfl, rfl, rfl⟩
simp only [Array.size_append, Array.size_zipWith] at h₁ h₂
exact ⟨mk w (by simp; omega), mk x (by simp; omega), mk y (by simp; omega), mk z (by simp; omega), by simp⟩
· rintro ⟨⟨w, hw⟩, ⟨x, hx⟩, ⟨y, hy⟩, ⟨z, hz⟩, rfl, rfl, w₁, w₂⟩
exact ⟨mk as₁ (by simp; omega), mk as₂ (by simp; omega), mk bs₁ (by simp; omega), mk bs₂ (by simp; omega), by simp⟩
· rintro ⟨⟨as₁, hw⟩, ⟨as₂, hx⟩, ⟨bs₁, hy⟩, ⟨bs₂, hz⟩, rfl, rfl, w₁, w₂⟩
simp only at w₁ w₂
exact ⟨w, x, y, z, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩
exact ⟨as₁, as₂, bs₁, bs₂, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩
@[simp] theorem zipWith_mkVector {a : α} {b : β} {n : Nat} :
zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b) := by
ext
simp
theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Vector α n) (l' : Vector β n) :
map (Function.uncurry f) (l.zip l') = zipWith f l l' := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.map_uncurry_zip_eq_zipWith]
theorem map_zip_eq_zipWith (f : α × β → γ) (l : Vector α n) (l' : Vector β n) :
map f (l.zip l') = zipWith (Function.curry f) l l' := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem map_zip_eq_zipWith (f : α × β → γ) (as : Vector α n) (bs : Vector β n) :
map f (as.zip bs) = zipWith (Function.curry f) as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.map_zip_eq_zipWith]
theorem reverse_zipWith :
(zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by
rcases l with ⟨l, rfl⟩
rcases l' with ⟨l', h⟩
theorem reverse_zipWith (f : α → β → γ) (as : Vector α n) (bs : Vector β n) :
(zipWith f as bs).reverse = zipWith f as.reverse bs.reverse := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.reverse_zipWith, h]
/-! ### zip -/
@[simp]
theorem getElem_zip {l : Vector α n} {l' : Vector β n} {i : Nat} {h : i < n} :
(zip l l')[i] = (l[i], l'[i]) :=
theorem getElem_zip {as : Vector α n} {bs : Vector β n} {i : Nat} {h : i < n} :
(zip as bs)[i] = (as[i], bs[i]) :=
getElem_zipWith ..
theorem zip_eq_zipWith (l₁ : Vector α n) (l₂ : Vector β n) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem zip_eq_zipWith (as : Vector α n) (bs : Vector β n) : zip as bs = zipWith Prod.mk as bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.zip_eq_zipWith, h]
theorem zip_map (f : αγ) (g : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) :
zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g) := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem zip_map (f : αγ) (g : β → δ) (as : Vector α n) (bs : Vector β n) :
zip (as.map f) (bs.map g) = (zip as bs).map (Prod.map f g) := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.zip_map, h]
theorem zip_map_left (f : αγ) (l₁ : Vector α n) (l₂ : Vector β n) :
zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
theorem zip_map_left (f : αγ) (as : Vector α n) (bs : Vector β n) :
zip (as.map f) bs = (zip as bs).map (Prod.map f id) := by rw [← zip_map, map_id]
theorem zip_map_right (f : β → γ) (l₁ : Vector α n) (l₂ : Vector β n) :
zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
theorem zip_map_right (f : β → γ) (as : Vector α n) (bs : Vector β n) :
zip as (bs.map f) = (zip as bs).map (Prod.map id f) := by rw [← zip_map, map_id]
theorem zip_append {l₁ : Vector α n} {l₂ : Vector β n} {r₁ : Vector α m} {r₂ : Vector β m} :
zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
rcases r₁ with ⟨r₁, rfl⟩
rcases r₂ with ⟨r₂, h'⟩
theorem zip_append {as : Vector α n} {bs : Vector β n} {as' : Vector α m} {bs' : Vector β m} :
zip (as ++ as') (bs ++ bs') = zip as bs ++ zip as' bs' := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
rcases as' with ⟨as', rfl⟩
rcases bs' with ⟨bs', h'⟩
simp [Array.zip_append, h, h']
theorem zip_map' (f : α → β) (g : αγ) (l : Vector α n) :
zip (l.map f) (l.map g) = l.map fun a => (f a, g a) := by
rcases l with ⟨l, rfl⟩
theorem zip_map' (f : α → β) (g : αγ) (xs : Vector α n) :
zip (xs.map f) (xs.map g) = xs.map fun a => (f a, g a) := by
rcases xs with ⟨xs, rfl⟩
simp [Array.zip_map']
theorem of_mem_zip {a b} {l₁ : Vector α n} {l₂ : Vector β n} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem of_mem_zip {a b} {as : Vector α n} {bs : Vector β n} : (a, b) ∈ zip as bs → a ∈ as ∧ b ∈ bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simpa using Array.of_mem_zip
theorem map_fst_zip (l₁ : Vector α n) (l₂ : Vector β n) :
map Prod.fst (zip l₁ l₂) = l₁ := by
cases l₁
cases l₂
simp_all [Array.map_fst_zip]
theorem map_fst_zip (as : Vector α n) (bs : Vector β n) :
map Prod.fst (zip as bs) = as := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.map_fst_zip, h]
theorem map_snd_zip (l₁ : Vector α n) (l₂ : Vector β n) :
map Prod.snd (zip l₁ l₂) = l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem map_snd_zip (as : Vector α n) (bs : Vector β n) :
map Prod.snd (zip as bs) = bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.map_snd_zip, h]
theorem map_prod_left_eq_zip {l : Vector α n} (f : α → β) :
(l.map fun x => (x, f x)) = l.zip (l.map f) := by
rcases l with ⟨l, rfl⟩
theorem map_prod_left_eq_zip {xs : Vector α n} (f : α → β) :
(xs.map fun x => (x, f x)) = xs.zip (xs.map f) := by
rcases xs with ⟨xs, rfl⟩
rw [← zip_map']
congr
simp
theorem map_prod_right_eq_zip {l : Vector α n} (f : α → β) :
(l.map fun x => (f x, x)) = (l.map f).zip l := by
rcases l with ⟨l, rfl⟩
theorem map_prod_right_eq_zip {xs : Vector α n} (f : α → β) :
(xs.map fun x => (f x, x)) = (xs.map f).zip xs := by
rcases xs with ⟨xs, rfl⟩
rw [← zip_map']
congr
simp
theorem zip_eq_append_iff {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} {l₁' : Vector (α × β) n} {l₂' : Vector (α × β) m} :
zip l₁ l₂ = l₁' ++ l₂'
w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by
theorem zip_eq_append_iff {as : Vector α (n + m)} {bs : Vector β (n + m)} {xs : Vector (α × β) n} {ys : Vector (α × β) m} :
zip as bs = xs ++ ys
as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
simp [zip_eq_zipWith, zipWith_eq_append_iff]
@[simp] theorem zip_mkVector {a : α} {b : β} {n : Nat} :
@ -244,41 +247,43 @@ theorem zip_eq_append_iff {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)}
/-! ### unzip -/
@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
induction l <;> simp_all
@[simp] theorem unzip_fst : (unzip xs).fst = xs.map Prod.fst := by
cases xs
simp_all
@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
induction l <;> simp_all
@[simp] theorem unzip_snd : (unzip xs).snd = xs.map Prod.snd := by
cases xs
simp_all
theorem unzip_eq_map (l : Vector (α × β) n) : unzip l = (l.map Prod.fst, l.map Prod.snd) := by
cases l
theorem unzip_eq_map (xs : Vector (α × β) n) : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by
cases xs
simp [List.unzip_eq_map]
theorem zip_unzip (l : Vector (α × β) n) : zip (unzip l).1 (unzip l).2 = l := by
rcases l with ⟨l, rfl⟩
theorem zip_unzip (xs : Vector (α × β) n) : zip (unzip xs).1 (unzip xs).2 = xs := by
cases xs
simp only [unzip_mk, mk_zip_mk, Array.zip_unzip]
theorem unzip_zip_left {l₁ : Vector α n} {l₂ : Vector β n} :
(unzip (zip l₁ l₂)).1 = l₁ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem unzip_zip_left {as : Vector α n} {bs : Vector β n} :
(unzip (zip as bs)).1 = as := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.unzip_zip_left, h, Array.map_fst_zip]
theorem unzip_zip_right {l₁ : Vector α n} {l₂ : Vector β n} :
(unzip (zip l₁ l₂)).2 = l₂ := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem unzip_zip_right {as : Vector α n} {bs : Vector β n} :
(unzip (zip as bs)).2 = bs := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.unzip_zip_right, h, Array.map_snd_zip]
theorem unzip_zip {l₁ : Vector α n} {l₂ : Vector β n} :
unzip (zip l₁ l₂) = (l₁, l₂) := by
rcases l₁ with ⟨l₁, rfl⟩
rcases l₂ with ⟨l₂, h⟩
theorem unzip_zip {as : Vector α n} {bs : Vector β n} :
unzip (zip as bs) = (as, bs) := by
rcases as with ⟨as, rfl⟩
rcases bs with ⟨bs, h⟩
simp [Array.unzip_zip, h, Array.map_fst_zip, Array.map_snd_zip]
theorem zip_of_prod {l : Vector α n} {l' : Vector β n} {lp : Vector (α × β) n} (hl : lp.map Prod.fst = l)
(hr : lp.map Prod.snd = l') : lp = l.zip l' := by
rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
theorem zip_of_prod {as : Vector α n} {bs : Vector β n} {xs : Vector (α × β) n} (hl : xs.map Prod.fst = as)
(hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
@[simp] theorem unzip_mkVector {n : Nat} {a : α} {b : β} :
unzip (mkVector n (a, b)) = (mkVector n a, mkVector n b) := by

View file

@ -65,8 +65,10 @@ def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
| Array.setIfInBounds _ _ i _ => [i]
| Array.insertIdx _ _ i _ _ => [i]
| Array.insertIdxIfInBounds _ _ i _ => [i]
| Array.insertIdx! _ _ i _ => [i]
| Array.eraseIdx _ _ i _ => [i]
| Array.eraseIdxIfInBounds _ _ i _ => [i]
| Array.eraseIdx! _ _ i => [i]
| Array.modify _ _ i _ => [i]
| Array.zipIdx _ _ i => [i]
| Array.swap _ _ i j _ => [i, j]
@ -78,6 +80,8 @@ def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
| Vector.setIfInBounds _ _ _ i _ => [i]
| Vector.insertIdx _ _ _ i _ _ => [i]
| Vector.eraseIdx _ _ _ i _ => [i]
| Vector.insertIdx! _ _ _ i _ => [i]
| Vector.eraseIdx! _ _ _ i => [i]
| Vector.zipIdx _ _ _ i => [i]
| Vector.swap _ _ _ i j _ => [i, j]
| _ => []
@ -151,10 +155,10 @@ def stripBinderName (s : String) : String :=
s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂" |>.stripSuffix "₃" |>.stripSuffix "₄"
/-- Allowed names for index variables. -/
def allowedIndices : List String := ["i", "j", "k", "start", "stop"]
def allowedIndices : List String := ["i", "j", "k", "start", "stop", "step"]
/-- Allowed names for width variables. -/
def allowedWidths : List String := ["n", "m"]
def allowedWidths : List String := ["n", "m", "k", "l", "size"]
/-- Allowed names for BitVec width variables. -/
def allowedBitVecWidths : List String := ["w"]
@ -176,16 +180,16 @@ def indexLinter : Linter
if !allowedIndices.contains (stripBinderName n) then
Linter.logLint linter.indexVariables idxStx
m!"Forbidden variable appearing as an index: use `i`, `j`, or `k`: {n}"
-- for (idxStx, n) in numericalWidths t do
-- if let .str _ n := n then
-- if !allowedWidths.contains (stripBinderName n) then
-- Linter.logLint linter.indexVariables idxStx
-- m!"Forbidden variable appearing as a width: use `n` or `m`: {n}"
-- for (idxStx, n) in bitVecWidths t do
-- if let .str _ n := n then
-- if !allowedBitVecWidths.contains (stripBinderName n) then
-- Linter.logLint linter.indexVariables idxStx
-- m!"Forbidden variable appearing as a BitVec width: use `w`: {n}"
for (idxStx, n) in numericalWidths t do
if let .str _ n := n then
if !allowedWidths.contains (stripBinderName n) then
Linter.logLint linter.indexVariables idxStx
m!"Forbidden variable appearing as a width: use `n` or `m`: {n}"
for (idxStx, n) in bitVecWidths t do
if let .str _ n := n then
if !allowedBitVecWidths.contains (stripBinderName n) then
Linter.logLint linter.indexVariables idxStx
m!"Forbidden variable appearing as a BitVec width: use `w`: {n}"
builtin_initialize addLinter indexLinter
@ -196,7 +200,7 @@ def allowedListNames : List String := ["l", "r", "s", "t", "tl", "ws", "xs", "ys
def allowedArrayNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]
/-- Allowed names for `Vector` variables. -/
def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds"]
def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]
/-- Find all binders appearing in the given info tree. -/
def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Syntax × Name × Expr)) :=
@ -243,12 +247,13 @@ def listVariablesLinter : Linter
unless (ty.getArg! 0).isAppOf `Array && n == "xss" do
Linter.logLint linter.listVariables stx
m!"Forbidden variable appearing as a `Array` name: {n}"
for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
if let .str _ n := n then
let n := stripBinderName n
if !allowedVectorNames.contains n then
Linter.logLint linter.listVariables stx
m!"Forbidden variable appearing as a `Vector` name: {n}"
unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
Linter.logLint linter.listVariables stx
m!"Forbidden variable appearing as a `Vector` name: {n}"
builtin_initialize addLinter listVariablesLinter

View file

@ -1,16 +1,16 @@
import Lean
/--
info: Vector.extract.hcongr_5.{u_1} (α α' : Type u_1) (e_1 : α = α') (n n' : Nat) (e_2 : n = n') (v : Vector α n)
(v' : Vector α' n') (e_3 : HEq v v') (start start' : Nat) (e_4 : start = start') (stop stop' : Nat)
(e_5 : stop = stop') : HEq (v.extract start stop) (v'.extract start' stop')
info: Vector.extract.hcongr_5.{u_1} (α α' : Type u_1) (e_1 : α = α') (n n' : Nat) (e_2 : n = n') (xs : Vector α n)
(xs' : Vector α' n') (e_3 : HEq xs xs') (start start' : Nat) (e_4 : start = start') (stop stop' : Nat)
(e_5 : stop = stop') : HEq (xs.extract start stop) (xs'.extract start' stop')
-/
#guard_msgs in
#check Vector.extract.hcongr_5
/--
info: Vector.extract.congr_simp.{u_1} {α : Type u_1} {n : Nat} (v v✝ : Vector α n) (e_v : v = v✝) (start stop : Nat) :
v.extract start stop = v✝.extract start stop
info: Vector.extract.congr_simp.{u_1} {α : Type u_1} {n : Nat} (xs xs✝ : Vector α n) (e_xs : xs = xs✝) (start stop : Nat) :
xs.extract start stop = xs✝.extract start stop
-/
#guard_msgs in
#check Vector.extract.congr_simp