def Vector.pmap {α : Type u_1} {β : Type u_2} {n : Nat} {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n) (H : ∀ (a : α), a ∈ xs → P a) : Vector β n

O(n). Partial map. If f : Π a, P a → β is a partial function defined on a : α satisfying P, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy P, using the proof to apply f.

We replace this at runtime with a more efficient version via the csimp lemma pmap_eq_pmapImpl.

Equations

• Vector.pmap f xs H = { toArray := Array.pmap f xs.toArray ⋯, size_toArray := ⋯ }

@[implemented_by _private.Init.Data.Vector.Attach.0.Vector.attachWithImpl]

def Vector.attachWith {α : Type u_1} {n : Nat} (xs : Vector α n) (P : α → Prop) (H : ∀ (x : α), x ∈ xs → P x) : Vector { x : α // P x } n

O(1). "Attach" a proof P x that holds for all the elements of xs to produce a new array with the same elements but in the type {x // P x}.

Equations

• xs.attachWith P H = { toArray := xs.toArray.attachWith P ⋯, size_toArray := ⋯ }

@[inline]

def Vector.attach {α : Type u_1} {n : Nat} (xs : Vector α n) : Vector { x : α // x ∈ xs } n

O(1). "Attach" the proof that the elements of xs are in xs to produce a new vector with the same elements but in the type {x // x ∈ xs}.

Equations

• xs.attach = xs.attachWith (Membership.mem xs) ⋯

@[simp]

theorem Vector.attachWith_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {P : α → Prop} {H : ∀ (x : α), x ∈ { toArray := xs, size_toArray := h } → P x} : { toArray := xs, size_toArray := h }.attachWith P H = { toArray := xs.attachWith P ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.attach_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} : { toArray := xs, size_toArray := h }.attach = { toArray := xs.attachWith (fun (x : α) => x ∈ { toArray := xs, size_toArray := h }) ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.pmap_mk {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Array α} {h : xs.size = n} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ (a : α), a ∈ { toArray := xs, size_toArray := h } → P a} : pmap f { toArray := xs, size_toArray := h } H = { toArray := Array.pmap f xs ⋯, size_toArray := ⋯ }

@[simp]

theorem Vector.toArray_attachWith {α : Type u_1} {n : Nat} {xs : Vector α n} {P : α → Prop} {H : ∀ (x : α), x ∈ xs → P x} : (xs.attachWith P H).toArray = xs.toArray.attachWith P ⋯

@[simp]

theorem Vector.toArray_attach {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.attach.toArray = xs.toArray.attachWith (fun (x : α) => x ∈ xs) ⋯

@[simp]

theorem Vector.toArray_pmap {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ (a : α), a ∈ xs → P a} : (pmap f xs H).toArray = Array.pmap f xs.toArray ⋯

@[simp]

theorem Vector.toList_attachWith {α : Type u_1} {n : Nat} {xs : Vector α n} {P : α → Prop} {H : ∀ (x : α), x ∈ xs → P x} : (xs.attachWith P H).toList = xs.toList.attachWith P ⋯

@[simp]

theorem Vector.toList_attach {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.attach.toList = xs.toList.attachWith (fun (x : α) => x ∈ xs) ⋯

@[simp]

theorem Vector.toList_pmap {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ (a : α), a ∈ xs → P a} : (pmap f xs H).toList = List.pmap f xs.toList ⋯

@[simp]

theorem Vector.pmap_empty {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} : pmap f { toArray := #[], size_toArray := ⋯ } ⋯ = { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.pmap_push {α : Type u_1} {β : Type u_2} {n : Nat} {P : α → Prop} {f : (a : α) → P a → β} {a : α} {xs : Vector α n} {h : ∀ (b : α), b ∈ xs.push a → P b} : pmap f (xs.push a) h = (pmap f xs ⋯).push (f a ⋯)

@[simp]

theorem Vector.attach_empty {α : Type u_1} : { toArray := #[], size_toArray := ⋯ }.attach = { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.attachWith_empty {α : Type u_1} {P : α → Prop} (H : ∀ (x : α), x ∈ { toArray := #[], size_toArray := ⋯ } → P x) : { toArray := #[], size_toArray := ⋯ }.attachWith P H = { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.pmap_eq_map {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : pmap (fun (a : α) (x : p a) => f a) xs H = map f xs

theorem Vector.pmap_congr_left {α : Type u_1} {β : Type u_2} {n : Nat} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (xs : Vector α n) {H₁ : ∀ (a : α), a ∈ xs → p a} {H₂ : ∀ (a : α), a ∈ xs → q a} (h : ∀ (a : α), a ∈ xs → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) : pmap f xs H₁ = pmap g xs H₂

theorem Vector.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : map g (pmap f xs H) = pmap (fun (a : α) (h : p a) => g (f a h)) xs H

theorem Vector.pmap_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : Nat} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {xs : Vector α n} (H : ∀ (a : β), a ∈ map f xs → p a) : pmap g (map f xs) H = pmap (fun (a : α) (h : p (f a)) => g (f a) h) xs ⋯

theorem Vector.attach_congr {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : xs = ys) : xs.attach = map (fun (x : { x : α // x ∈ ys }) => ⟨x.val, ⋯⟩) ys.attach

theorem Vector.attachWith_congr {α : Type u_1} {n : Nat} {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {H : ∀ (x : α), x ∈ xs → P x} : xs.attachWith P H = ys.attachWith P ⋯

@[simp]

theorem Vector.attach_push {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} : (xs.push a).attach = (map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach).push ⟨a, ⋯⟩

@[simp]

theorem Vector.attachWith_push {α : Type u_1} {n : Nat} {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ (x : α), x ∈ xs.push a → P x} : (xs.push a).attachWith P H = (xs.attachWith P ⋯).push ⟨a, ⋯⟩

theorem Vector.pmap_eq_map_attach {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : pmap f xs H = map (fun (x : { x : α // x ∈ xs }) => f x.val ⋯) xs.attach

@[simp]

theorem Vector.pmap_eq_attachWith {α : Type u_1} {n : Nat} {p q : α → Prop} {f : ∀ (a : α), p a → q a} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : pmap (fun (a : α) (h : p a) => ⟨a, ⋯⟩) xs H = xs.attachWith q ⋯

theorem Vector.attach_map_val {α : Type u_1} {n : Nat} {β : Type u_2} (xs : Vector α n) (f : α → β) : map (fun (i : { i : α // i ∈ xs }) => f i.val) xs.attach = map f xs

@[reducible, inline, deprecated Vector.attach_map_val (since := "2025-02-17")]

abbrev Vector.attach_map_coe {α : Type u_1} {n : Nat} {β : Type u_2} (xs : Vector α n) (f : α → β) : map (fun (i : { i : α // i ∈ xs }) => f i.val) xs.attach = map f xs

Equations

• @Vector.attach_map_coe = @Vector.attach_map_val

theorem Vector.attach_map_subtype_val {α : Type u_1} {n : Nat} (xs : Vector α n) : map Subtype.val xs.attach = xs

theorem Vector.attachWith_map_val {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : map (fun (i : { i : α // p i }) => f i.val) (xs.attachWith p H) = map f xs

@[reducible, inline, deprecated Vector.attachWith_map_val (since := "2025-02-17")]

abbrev Vector.attachWith_map_coe {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : map (fun (i : { i : α // p i }) => f i.val) (xs.attachWith p H) = map f xs

Equations

• @Vector.attachWith_map_coe = @Vector.attachWith_map_val

theorem Vector.attachWith_map_subtype_val {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) : map Subtype.val (xs.attachWith p H) = xs

@[simp]

theorem Vector.mem_attach {α : Type u_1} {n : Nat} (xs : Vector α n) (x : { x : α // x ∈ xs }) : x ∈ xs.attach

@[simp]

theorem Vector.mem_attachWith {α : Type u_1} {n : Nat} {xs : Vector α n} {q : α → Prop} (H : ∀ (x : α), x ∈ xs → q x) (x : { x : α // q x }) : x ∈ xs.attachWith q H ↔ x.val ∈ xs

@[simp]

theorem Vector.mem_pmap {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs → p a} {b : β} : b ∈ pmap f xs H ↔ ∃ (a : α), ∃ (h : a ∈ xs), f a ⋯ = b

theorem Vector.mem_pmap_of_mem {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs → p a} {a : α} (h : a ∈ xs) : f a ⋯ ∈ pmap f xs H

theorem Vector.pmap_eq_self {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Prop} {hp : ∀ (a : α), a ∈ xs → p a} {f : (a : α) → p a → α} : pmap f xs hp = xs ↔ ∀ (a : α) (h : a ∈ xs), f a ⋯ = a

@[simp]

theorem Vector.getElem?_pmap {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} (h : ∀ (a : α), a ∈ xs → p a) (i : Nat) : (pmap f xs h)[i]? = Option.pmap f xs[i]? ⋯

@[simp]

theorem Vector.getElem_pmap {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} (f : (a : α) → p a → β) {xs : Vector α n} (h : ∀ (a : α), a ∈ xs → p a) {i : Nat} (hn : i < n) : (pmap f xs h)[i] = f xs[i] ⋯

@[simp]

theorem Vector.getElem?_attachWith {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} : (xs.attachWith P H)[i]? = Option.pmap Subtype.mk xs[i]? ⋯

@[simp]

theorem Vector.getElem?_attach {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} : xs.attach[i]? = Option.pmap Subtype.mk xs[i]? ⋯

@[simp]

theorem Vector.getElem_attachWith {α : Type u_1} {n : Nat} {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} {i : Nat} (h : i < n) : (xs.attachWith P H)[i] = ⟨xs[i], ⋯⟩

@[simp]

theorem Vector.getElem_attach {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs.attach[i] = ⟨xs[i], ⋯⟩

@[simp]

theorem Vector.pmap_attach {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {p : { x : α // x ∈ xs } → Prop} {f : (a : { x : α // x ∈ xs }) → p a → β} (H : ∀ (a : { x : α // x ∈ xs }), a ∈ xs.attach → p a) : pmap f xs.attach H = pmap (fun (a : α) (h : (fun (a : α) => ∃ (h : a ∈ xs), p ⟨a, h⟩) a) => f ⟨a, ⋯⟩ ⋯) xs ⋯

@[simp]

theorem Vector.pmap_attachWith {α : Type u_1} {n : Nat} {q : α → Prop} {β : Type u_2} {xs : Vector α n} {p : { x : α // q x } → Prop} {f : (a : { x : α // q x }) → p a → β} (H₁ : ∀ (x : α), x ∈ xs → q x) (H₂ : ∀ (a : { x : α // q x }), a ∈ xs.attachWith q H₁ → p a) : pmap f (xs.attachWith q H₁) H₂ = pmap (fun (a : α) (h : (fun (a : α) => ∃ (h : q a), p ⟨a, h⟩) a) => f ⟨a, ⋯⟩ ⋯) xs ⋯

theorem Vector.foldl_pmap {α : Type u_1} {n : Nat} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β} (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) : foldl g x (pmap f xs H) = foldl (fun (acc : γ) (a : { x : α // x ∈ xs }) => g acc (f a.val ⋯)) x xs.attach

theorem Vector.foldr_pmap {α : Type u_1} {n : Nat} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β} (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) : foldr g x (pmap f xs H) = foldr (fun (a : { x : α // x ∈ xs }) (acc : γ) => g (f a.val ⋯) acc) x xs.attach

theorem Vector.foldl_attach {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : β → α → β} {b : β} : foldl (fun (acc : β) (t : { x : α // x ∈ xs }) => f acc t.val) b xs.attach = foldl f b xs

If we fold over l.attach with a function that ignores the membership predicate, we get the same results as folding over l directly.

This is useful when we need to use attach to show termination.

Unfortunately this can't be applied by simp because of the higher order unification problem, and even when rewriting we need to specify the function explicitly. See however foldl_subtype below.

theorem Vector.foldr_attach {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → β → β} {b : β} : foldr (fun (t : { x : α // x ∈ xs }) (acc : β) => f t.val acc) b xs.attach = foldr f b xs

If we fold over l.attach with a function that ignores the membership predicate, we get the same results as folding over l directly.

This is useful when we need to use attach to show termination.

Unfortunately this can't be applied by simp because of the higher order unification problem, and even when rewriting we need to specify the function explicitly. See however foldr_subtype below.

theorem Vector.attach_map {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → β} : (map f xs).attach = map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) xs.attach

theorem Vector.attachWith_map {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ map f xs → P b) : (map f xs).attachWith P H = map (fun (x : { x : α // (P ∘ f) x }) => match x with | ⟨x, h⟩ => ⟨f x, h⟩) (xs.attachWith (P ∘ f) ⋯)

@[simp]

theorem Vector.map_attachWith {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} {f : { x : α // P x } → β} : map f (xs.attachWith P H) = map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => f ⟨x, ⋯⟩) xs.attach

theorem Vector.map_attachWith_eq_pmap {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} {f : { x : α // P x } → β} : map f (xs.attachWith P H) = pmap (fun (a : α) (h : a ∈ xs ∧ P a) => f ⟨a, ⋯⟩) xs ⋯

theorem Vector.map_attach_eq_pmap {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : { x : α // x ∈ xs } → β} : map f xs.attach = pmap (fun (a : α) (h : a ∈ xs) => f ⟨a, h⟩) xs ⋯

See also pmap_eq_map_attach for writing pmap in terms of map and attach.

@[reducible, inline, deprecated Vector.map_attach_eq_pmap (since := "2025-02-09")]

abbrev Vector.map_attach {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : { x : α // x ∈ xs } → β} : map f xs.attach = pmap (fun (a : α) (h : a ∈ xs) => f ⟨a, h⟩) xs ⋯

Equations

• @Vector.map_attach = @Vector.map_attach_eq_pmap

theorem Vector.pmap_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {p : α → Prop} {q : β → Prop} {g : (a : α) → p a → β} {f : (b : β) → q b → γ} {xs : Vector α n} (H₁ : ∀ (a : α), a ∈ xs → p a) (H₂ : ∀ (a : β), a ∈ pmap g xs H₁ → q a) : pmap f (pmap g xs H₁) H₂ = pmap (fun (a : { x : α // x ∈ xs }) (h : p a.val) => f (g a.val h) ⋯) xs.attach ⋯

@[simp]

theorem Vector.pmap_append {ι : Type u_1} {α : Type u_2} {n m : Nat} {p : ι → Prop} {f : (a : ι) → p a → α} {xs : Vector ι n} {ys : Vector ι m} (h : ∀ (a : ι), a ∈ xs ++ ys → p a) : pmap f (xs ++ ys) h = pmap f xs ⋯ ++ pmap f ys ⋯

theorem Vector.pmap_append' {α : Type u_1} {β : Type u_2} {n m : Nat} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} {ys : Vector α m} (h₁ : ∀ (a : α), a ∈ xs → p a) (h₂ : ∀ (a : α), a ∈ ys → p a) : pmap f (xs ++ ys) ⋯ = pmap f xs h₁ ++ pmap f ys h₂

@[simp]

theorem Vector.attach_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).attach = map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach ++ map (fun (x : { x : α // x ∈ ys }) => match x with | ⟨y, h⟩ => ⟨y, ⋯⟩) ys.attach

@[simp]

theorem Vector.attachWith_append {α : Type u_1} {n m : Nat} {P : α → Prop} {xs : Vector α n} {ys : Vector α m} {H : ∀ (a : α), a ∈ xs ++ ys → P a} : (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯

@[simp]

theorem Vector.pmap_reverse {α : Type u_1} {β : Type u_2} {n : Nat} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs.reverse → P a) : pmap f xs.reverse H = (pmap f xs ⋯).reverse

theorem Vector.reverse_pmap {α : Type u_1} {β : Type u_2} {n : Nat} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → P a) : (pmap f xs H).reverse = pmap f xs.reverse ⋯

@[simp]

theorem Vector.attachWith_reverse {α : Type u_1} {n : Nat} {P : α → Prop} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs.reverse → P a} : xs.reverse.attachWith P H = (xs.attachWith P ⋯).reverse

theorem Vector.reverse_attachWith {α : Type u_1} {n : Nat} {P : α → Prop} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs → P a} : (xs.attachWith P H).reverse = xs.reverse.attachWith P ⋯

@[simp]

theorem Vector.attach_reverse {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.reverse.attach = map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach.reverse

theorem Vector.reverse_attach {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.attach.reverse = map (fun (x : { x : α // x ∈ xs.reverse }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.reverse.attach

@[simp]

theorem Vector.back?_pmap {α : Type u_1} {β : Type u_2} {n : Nat} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → P a) : (pmap f xs H).back? = Option.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.back?

@[simp]

theorem Vector.back?_attachWith {α : Type u_1} {n : Nat} {P : α → Prop} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs → P a} : (xs.attachWith P H).back? = xs.back?.pbind fun (a : α) (h : xs.back? = some a) => some ⟨a, ⋯⟩

@[simp]

theorem Vector.back?_attach {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.attach.back? = xs.back?.pbind fun (a : α) (h : xs.back? = some a) => some ⟨a, ⋯⟩

@[simp]

theorem Vector.countP_attach {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : countP (fun (a : { x : α // x ∈ xs }) => p a.val) xs.attach = countP p xs

@[simp]

theorem Vector.countP_attachWith {α : Type u_1} {n : Nat} {p : α → Prop} {q : α → Bool} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs → p a} : countP (fun (a : { x : α // p x }) => q a.val) (xs.attachWith p H) = countP q xs

@[simp]

theorem Vector.count_attach {α : Type u_1} {n : Nat} [BEq α] {xs : Vector α n} {a : { x : α // x ∈ xs }} : count a xs.attach = count a.val xs

@[simp]

theorem Vector.count_attachWith {α : Type u_1} {n : Nat} [BEq α] {p : α → Prop} {xs : Vector α n} (H : ∀ (a : α), a ∈ xs → p a) {a : { x : α // p x }} : count a (xs.attachWith p H) = count a.val xs

@[simp]

theorem Vector.countP_pmap {α : Type u_1} {β : Type u_2} {n : Nat} {p : α → Prop} {g : (a : α) → p a → β} {f : β → Bool} {xs : Vector α n} (H₁ : ∀ (a : α), a ∈ xs → p a) : countP f (pmap g xs H₁) = countP (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => f (g a ⋯)) xs.attach

unattach

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 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.

def Vector.unattach {n : Nat} {α : Type u_1} {p : α → Prop} (xs : Vector { x : α // p x } n) : Vector α n

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.

Equations

• xs.unattach = Vector.map (fun (x : { x : α // p x }) => x.val) xs

theorem Vector.unattach_empty {α : Type u_1} {p : α → Prop} : { toArray := #[], size_toArray := ⋯ }.unattach = { toArray := #[], size_toArray := ⋯ }

@[reducible, inline, deprecated Vector.unattach_empty (since := "2025-05-26")]

abbrev Vector.unattach_nil {α : Type u_1} {p : α → Prop} : { toArray := #[], size_toArray := ⋯ }.unattach = { toArray := #[], size_toArray := ⋯ }

Equations

• @Vector.unattach_nil = @Vector.unattach_empty

@[simp]

theorem Vector.unattach_push {α : Type u_1} {n : Nat} {p : α → Prop} {a : { x : α // p x }} {xs : Vector { x : α // p x } n} : (xs.push a).unattach = xs.unattach.push a.val

@[simp]

theorem Vector.mem_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} {a : α} : a ∈ xs.unattach ↔ ∃ (h : p a), ⟨a, h⟩ ∈ xs

@[simp]

theorem Vector.unattach_mk {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Array { x : α // p x }} {h : xs.size = n} : { toArray := xs, size_toArray := h }.unattach = { toArray := xs.unattach, size_toArray := ⋯ }

@[simp]

theorem Vector.toArray_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} : xs.unattach.toArray = xs.toArray.unattach

@[simp]

theorem Vector.toList_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} : xs.unattach.toList = xs.toList.unattach

@[simp]

theorem Vector.unattach_attach {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.attach.unattach = xs

@[simp]

theorem Vector.unattach_attachWith {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector α n} {H : ∀ (a : α), a ∈ xs → p a} : (xs.attachWith p H).unattach = xs

@[simp]

theorem Vector.getElem?_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} (i : Nat) : xs.unattach[i]? = Option.map Subtype.val xs[i]?

@[simp]

theorem Vector.getElem_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} (i : Nat) (h : i < n) : xs.unattach[i] = xs[i].val

Recognizing higher order functions using a function that only depends on the value.

@[simp]

theorem Vector.foldl_subtype {α : Type u_1} {n : Nat} {β : Type u_2} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : β → { x : α // p x } → β} {g : β → α → β} {x : β} (hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) : foldl f x xs = foldl g x xs.unattach

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 Vector.foldr_subtype {α : Type u_1} {n : Nat} {β : Type u_2} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → β → β} {g : α → β → β} {x : β} (hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) : foldr f x xs = foldr g x xs.unattach

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 Vector.map_subtype {α : Type u_1} {n : Nat} {β : Type u_2} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → β} {g : α → β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : map f xs = map g xs.unattach

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 Vector.findSome?_subtype {α : Type u_1} {n : Nat} {β : Type u_2} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → Option β} {g : α → Option β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findSome? f xs = findSome? g xs.unattach

@[simp]

theorem Vector.find?_subtype {α : Type u_1} {p : α → Prop} {xs : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Option.map Subtype.val (Array.find? f xs) = Array.find? g xs.unattach

@[simp]

theorem Vector.all_subtype {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : xs.all f = xs.unattach.all g

@[simp]

theorem Vector.any_subtype {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : xs.any f = xs.unattach.any g

Simp lemmas pushing unattach inwards.

@[simp]

theorem Vector.unattach_reverse {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} : xs.reverse.unattach = xs.unattach.reverse

@[simp]

theorem Vector.unattach_append {α : Type u_1} {n : Nat} {p : α → Prop} {xs ys : Vector { x : α // p x } n} : (xs ++ ys).unattach = xs.unattach ++ ys.unattach

@[simp]

theorem Vector.unattach_flatten {α : Type u_1} {n : Nat} {p : α → Prop} {xss : Vector (Vector { x : α // p x } n) n} : xss.flatten.unattach = (map unattach xss).flatten

@[simp]

theorem Vector.unattach_replicate {α : Type u_1} {p : α → Prop} {n : Nat} {x : { x : α // p x }} : (replicate n x).unattach = replicate n x.val

@[reducible, inline, deprecated Vector.unattach_replicate (since := "2025-03-18")]

abbrev Vector.unattach_mkVector {α : Type u_1} {p : α → Prop} {n : Nat} {x : { x : α // p x }} : (replicate n x).unattach = replicate n x.val

Equations

• @Vector.unattach_mkVector = @Vector.unattach_replicate