source
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 = Vector.mk (Array.pmap f xs.toArray ⋯) ⋯

Instances For

source
@[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 = Vector.mk (xs.toArray.attachWith P ⋯) ⋯

Instances For

source
@[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) ⋯

Instances For

source
@[simp]
theorem Vector.attachWith_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} {P : α → Prop} {H : ∀ (x : α), x ∈ mk xs h → P x} :
(mk xs h).attachWith P H = mk (xs.attachWith P ⋯) ⋯
source
@[simp]
theorem Vector.attach_mk {α : Type u_1} {n : Nat} {xs : Array α} {h : xs.size = n} :
(mk xs h).attach = mk (xs.attachWith (fun (x : α) => x ∈ mk xs h) ⋯) ⋯
source
@[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 ∈ mk xs h → P a} :
pmap f (mk xs h) H = mk (Array.pmap f xs ⋯) ⋯
source
@[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 ⋯
source
@[simp]
theorem Vector.toArray_attach {α : Type u_1} {n : Nat} {xs : Vector α n} :
xs.attach.toArray = xs.toArray.attachWith (fun (x : α) => x ∈ xs) ⋯
source
@[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 ⋯
source
@[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 ⋯
source
@[simp]
theorem Vector.toList_attach {α : Type u_1} {n : Nat} {xs : Vector α n} :
xs.attach.toList = xs.toList.attachWith (fun (x : α) => x ∈ xs) ⋯
source
@[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 ⋯
source
@[inline]
def Vector.pmapImpl {α : 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

Implementation of `pmap` using the zero-copy version of `attach`.

Equations

- Vector.pmapImpl f xs H = Vector.map (fun (x : { x : α // P x }) => match x with | ⟨x, h'⟩ => f x h') (xs.attachWith P H)

Instances For

source
@[csimp]
theorem Vector.pmap_eq_pmapImpl :
@pmap = @pmapImpl
source
@[simp]
theorem Vector.pmap_empty {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} :
pmap f #v[] ⋯ = #v[]
source
@[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 ⋯)
source
@[simp]
theorem Vector.attach_empty {α : Type u_1} :
#v[].attach = #v[]
source
@[simp]
theorem Vector.attachWith_empty {α : Type u_1} {P : α → Prop} (H : ∀ (x : α), x ∈ #v[] → P x) :
#v[].attachWith P H = #v[]
source
@[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
source
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₂
source
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
source
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 ⋯
source
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
source
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 ⋯
source
@[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, ⋯⟩
source
@[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, ⋯⟩
source
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
source
@[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 ⋯
source
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
source
theorem Vector.attach_map_subtype_val {α : Type u_1} {n : Nat} (xs : Vector α n) :
map Subtype.val xs.attach = xs
source
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
source
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
source
@[simp]
theorem Vector.mem_attach {α : Type u_1} {n : Nat} (xs : Vector α n) (x : { x : α // x ∈ xs }) :
x ∈ xs.attach
source
@[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
source
@[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
source
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
source
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
source
@[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]? ⋯
source
@[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] ⋯
source
@[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]? ⋯
source
@[simp]
theorem Vector.getElem?_attach {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} :
xs.attach[i]? = Option.pmap Subtype.mk xs[i]? ⋯
source
@[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], ⋯⟩
source
@[simp]
theorem Vector.getElem_attach {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) :
xs.attach[i] = ⟨xs[i], ⋯⟩
source
@[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 ⋯
source
@[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 ⋯
source
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
source
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
source
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.

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

source
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
source
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) ⋯)
source
@[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
source
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 ⋯
source
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`.

source
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 ⋯
source
@[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 ⋯
source
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₂
source
@[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
source
@[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 ⋯
source
@[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
source
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 ⋯
source
@[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
source
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 ⋯
source
@[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
source
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
source
@[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?
source
@[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, ⋯⟩
source
@[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, ⋯⟩
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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.

source
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

Instances For

source
theorem Vector.unattach_empty {α : Type u_1} {p : α → Prop} :
#v[].unattach = #v[]
source
@[reducible, inline, deprecated Vector.unattach_empty (since := "2025-05-26")]
abbrev Vector.unattach_nil {α : Type u_1} {p : α → Prop} :
#v[].unattach = #v[]
Equations

- @Vector.unattach_nil = @Vector.unattach_empty

Instances For

source
@[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
source
@[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
source
@[simp]
theorem Vector.unattach_mk {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Array { x : α // p x }} {h : xs.size = n} :
(mk xs h).unattach = mk xs.unattach ⋯
source
@[simp]
theorem Vector.toArray_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} :
xs.unattach.toArray = xs.toArray.unattach
source
@[simp]
theorem Vector.toList_unattach {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} :
xs.unattach.toList = xs.toList.unattach
source
@[simp]
theorem Vector.unattach_attach {α : Type u_1} {n : Nat} {xs : Vector α n} :
xs.attach.unattach = xs
source
@[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
source
@[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]?
source
@[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. #

source
@[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.

source
@[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.

source
@[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.

source
@[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
source
@[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
source
@[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
source
@[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. #

source
@[simp]
theorem Vector.unattach_reverse {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} :
xs.reverse.unattach = xs.unattach.reverse
source
@[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
source
@[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
source
@[simp]
theorem Vector.unattach_replicate {α : Type u_1} {p : α → Prop} {n : Nat} {x : { x : α // p x }} :
(replicate n x).unattach = replicate n x.val
source
@[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

Instances For