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

Maps a partially defined function (defined on those terms of α that satisfy a predicate P) over an array xs : Array α, given a proof that every element of xs in fact satisfies P.

Array.pmap, named for “partial map,” is the equivalent of Array.map for such partial functions.

Equations

• Array.pmap f xs H = (List.pmap f xs.toList ⋯).toArray

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

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

“Attaches” individual proofs to an array of values that satisfy a predicate P, returning an array of elements in the corresponding subtype { x // P x }.

O(1).

Equations

• xs.attachWith P H = { toList := xs.toList.attachWith P ⋯ }

@[inline]

def Array.attach {α : Type u_1} (xs : Array α) : Array { x : α // x ∈ xs }

“Attaches” the proof that the elements of xs are in fact elements of xs, producing a new array with the same elements but in the subtype { x // x ∈ xs }.

O(1).

This function is primarily used to allow definitions by well-founded recursion that use higher-order functions (such as Array.map) to prove that an value taken from a list is smaller than the list. This allows the well-founded recursion mechanism to prove that the function terminates.

Equations

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

@[simp]

theorem List.attachWith_toArray {α : Type u_1} {l : List α} {P : α → Prop} {H : ∀ (x : α), x ∈ l.toArray → P x} : l.toArray.attachWith P H = (l.attachWith P ⋯).toArray

@[simp]

theorem List.attach_toArray {α : Type u_1} {l : List α} : l.toArray.attach = (l.attachWith (fun (x : α) => x ∈ l.toArray) ⋯).toArray

@[simp]

theorem List.pmap_toArray {α : Type u_1} {β : Type u_2} {l : List α} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ (a : α), a ∈ l.toArray → P a} : Array.pmap f l.toArray H = (pmap f l ⋯).toArray

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Array.attach_empty {α : Type u_1} : #[].attach = #[]

@[simp]

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

@[simp]

theorem List.attachWith_mem_toArray {α : Type u_1} {l : List α} : l.attachWith (fun (x : α) => x ∈ l.toArray) ⋯ = map (fun (x : { x : α // x ∈ l }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) l.attach

@[simp]

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

theorem Array.pmap_congr_left {α : Type u_1} {β : Type u_2} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (xs : Array α) {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 Array.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {xs : Array α} (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 Array.pmap_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {xs : Array α} (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 Array.attach_congr {α : Type u_1} {xs ys : Array α} (h : xs = ys) : xs.attach = map (fun (x : { x : α // x ∈ ys }) => ⟨x.val, ⋯⟩) ys.attach

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

Equations

• @Array.attach_map_coe = @Array.attach_map_val

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

theorem Array.attachWith_map_val {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {xs : Array α} (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 Array.attachWith_map_val (since := "2025-02-17")]

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

Equations

• @Array.attachWith_map_coe = @Array.attachWith_map_val

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Array.size_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} {H : ∀ (a : α), a ∈ xs → p a} : (pmap f xs H).size = xs.size

@[simp]

theorem Array.size_attach {α : Type u_1} {xs : Array α} : xs.attach.size = xs.size

@[simp]

theorem Array.size_attachWith {α : Type u_1} {p : α → Prop} {xs : Array α} {H : ∀ (x : α), x ∈ xs → p x} : (xs.attachWith p H).size = xs.size

@[simp]

theorem Array.pmap_eq_empty_iff {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} {H : ∀ (a : α), a ∈ xs → p a} : pmap f xs H = #[] ↔ xs = #[]

theorem Array.pmap_ne_empty_iff {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) {xs : Array α} (H : ∀ (a : α), a ∈ xs → P a) : pmap f xs H ≠ #[] ↔ xs ≠ #[]

theorem Array.pmap_eq_self {α : Type u_1} {xs : Array α} {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 Array.attach_eq_empty_iff {α : Type u_1} {xs : Array α} : xs.attach = #[] ↔ xs = #[]

theorem Array.attach_ne_empty_iff {α : Type u_1} {xs : Array α} : xs.attach ≠ #[] ↔ xs ≠ #[]

@[simp]

theorem Array.attachWith_eq_empty_iff {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} : xs.attachWith P H = #[] ↔ xs = #[]

theorem Array.attachWith_ne_empty_iff {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} : xs.attachWith P H ≠ #[] ↔ xs ≠ #[]

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Array.pmap_attach {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.pmap_attachWith {α : Type u_1} {q : α → Prop} {β : Type u_2} {xs : Array α} {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 Array.foldl_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {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 Array.foldr_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {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

@[simp]

theorem Array.foldl_attachWith {α : Type u_1} {β : Type u_2} {stop : Nat} {xs : Array α} {q : α → Prop} (H : ∀ (a : α), a ∈ xs → q a) {f : β → { x : α // q x } → β} {b : β} (w : stop = xs.size) : foldl f b (xs.attachWith q H) 0 stop = foldl (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, h⟩ => f b ⟨a, ⋯⟩) b xs.attach

@[simp]

theorem Array.foldr_attachWith {α : Type u_1} {β : Type u_2} {start : Nat} {xs : Array α} {q : α → Prop} (H : ∀ (a : α), a ∈ xs → q a) {f : { x : α // q x } → β → β} {b : β} (w : start = xs.size) : foldr f b (xs.attachWith q H) start = foldr (fun (a : { x : α // x ∈ xs }) (acc : β) => f ⟨a.val, ⋯⟩ acc) b xs.attach

theorem Array.foldl_attach {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.foldr_attach {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.attach_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : (map f xs).attach = map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) xs.attach

theorem Array.attachWith_map {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.map_attachWith {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.map_attachWith_eq_pmap {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.map_attach_eq_pmap {α : Type u_1} {β : Type u_2} {xs : Array α} {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 Array.map_attach_eq_pmap (since := "2025-02-09")]

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

Equations

• @Array.map_attach = @Array.map_attach_eq_pmap

theorem Array.attach_filterMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} : (filterMap f xs).attach = filterMap (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => (f x).pbind fun (b : β) (m : f x = some b) => some ⟨b, ⋯⟩) xs.attach

theorem Array.attach_filter {α : Type u_1} {xs : Array α} (p : α → Bool) : (filter p xs).attach = filterMap (fun (x : { x : α // x ∈ xs }) => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) xs.attach

@[simp]

theorem Array.filterMap_attachWith {α : Type u_1} {β : Type u_2} {stop : Nat} {q : α → Prop} {xs : Array α} {f : { x : α // q x } → Option β} (H : ∀ (x : α), x ∈ xs → q x) (w : stop = (xs.attachWith q H).size) : filterMap f (xs.attachWith q H) 0 stop = filterMap (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => f ⟨x, ⋯⟩) xs.attach

@[simp]

theorem Array.filter_attachWith {α : Type u_1} {stop : Nat} {q : α → Prop} {xs : Array α} {p : { x : α // q x } → Bool} (H : ∀ (x : α), x ∈ xs → q x) (w : stop = (xs.attachWith q H).size) : filter p (xs.attachWith q H) 0 stop = map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) (filter (fun (x : { x : α // x ∈ xs }) => match x with | ⟨x, h⟩ => p ⟨x, ⋯⟩) xs.attach)

theorem Array.pmap_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {q : β → Prop} {g : (a : α) → p a → β} {f : (b : β) → q b → γ} {xs : Array α} (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 Array.pmap_append {ι : Type u_1} {α : Type u_2} {p : ι → Prop} {f : (a : ι) → p a → α} {xs ys : Array ι} (h : ∀ (a : ι), a ∈ xs ++ ys → p a) : pmap f (xs ++ ys) h = pmap f xs ⋯ ++ pmap f ys ⋯

theorem Array.pmap_append' {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs ys : Array α} (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 Array.attach_append {α : Type u_1} {xs ys : Array α} : (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 | ⟨x, h⟩ => ⟨x, ⋯⟩) ys.attach

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem Array.back?_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (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 Array.back?_attachWith {α : Type u_1} {P : α → Prop} {xs : Array α} {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 Array.back?_attach {α : Type u_1} {xs : Array α} : xs.attach.back? = xs.back?.pbind fun (a : α) (h : xs.back? = some a) => some ⟨a, ⋯⟩

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Array.countP_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {g : (a : α) → p a → β} {f : β → Bool} {xs : Array α} (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

Array.unattach is the (one-sided) inverse of Array.attach. It is a synonym for Array.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 : Array { 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.

Further, we provide simp lemmas that push unattach inwards.

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

Maps an array of terms in a subtype to the corresponding terms in the type by forgetting that they satisfy the predicate.

This is the inverse of Array.attachWith and a synonym for xs.map (·.val).

Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such as map_subtype, and is ideally subsequently simplified away by unattach_attach.

This function is usually inserted automatically by Lean as an intermediate step while proving termination. It is rarely used explicitly in code. It is introduced as an intermediate step during the elaboration of definitions by well-founded recursion. If this function is encountered in a proof state, the right approach is usually the tactic simp [Array.unattach, -Array.map_subtype].

Equations

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

@[simp]

theorem Array.unattach_empty {α : Type u_1} {p : α → Prop} : #[].unattach = #[]

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

abbrev Array.unattach_nil {α : Type u_1} {p : α → Prop} : #[].unattach = #[]

Equations

• @Array.unattach_nil = @Array.unattach_empty

@[simp]

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

@[simp]

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

@[simp]

theorem Array.size_unattach {α : Type u_1} {p : α → Prop} {xs : Array { x : α // p x }} : xs.unattach.size = xs.size

@[simp]

theorem List.unattach_toArray {α : Type u_1} {p : α → Prop} {xs : List { x : α // p x }} : xs.toArray.unattach = xs.unattach.toArray

@[simp]

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

@[simp]

theorem Array.unattach_attach {α : Type u_1} {xs : Array α} : xs.attach.unattach = xs

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Array.foldl_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x : α // p x }} {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 Array.foldl_subtype' {α : Type u_1} {β : Type u_2} {stop : Nat} {p : α → Prop} {xs : Array { x : α // p x }} {f : β → { x : α // p x } → β} {g : β → α → β} {x : β} (hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) (h : stop = xs.size) : foldl f x xs 0 stop = foldl g x xs.unattach

Variant of foldl_subtype with side condition to check stop = l.size.

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

Variant of foldr_subtype with side condition to check stop = l.size.

@[simp]

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

@[simp]

theorem Array.flatMap_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x : α // p x }} {f : { x : α // p x } → Array β} {g : α → Array β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : flatMap f xs = flatMap g xs.unattach

@[simp]

theorem Array.findSome?_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x : α // p x }} {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 Array.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 (find? f xs) = find? g xs.unattach

@[simp]

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

@[simp]

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

Simp lemmas pushing unattach inwards.

@[simp]

theorem Array.unattach_filter {α : 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) : (filter f xs).unattach = filter g xs.unattach

@[simp]

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

@[simp]

theorem Array.unattach_append {α : Type u_1} {p : α → Prop} {xs₁ xs₂ : Array { x : α // p x }} : (xs₁ ++ xs₂).unattach = xs₁.unattach ++ xs₂.unattach

@[simp]

theorem Array.unattach_flatten {α : Type u_1} {p : α → Prop} {xs : Array (Array { x : α // p x })} : xs.flatten.unattach = (map unattach xs).flatten

@[simp]

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

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

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

Equations

• @Array.unattach_mkArray = @Array.unattach_replicate

Well-founded recursion preprocessing setup

theorem Array.map_wfParam {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : map f (wfParam xs) = map f xs.attach.unattach

theorem Array.map_unattach {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → β} : map f xs.unattach = map (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs

theorem Array.foldl_wfParam {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → α → β} {x : β} : foldl f x (wfParam xs) = foldl f x xs.attach.unattach

theorem Array.foldl_unattach {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : β → α → β} {x : β} : foldl f x xs.unattach = foldl (fun (s : β) (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint s f (binderNameHint x (f s) (binderNameHint h () (f s (wfParam x))))) x xs

theorem Array.foldr_wfParam {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β → β} {x : β} : foldr f x (wfParam xs) = foldr f x xs.attach.unattach

theorem Array.foldr_unattach {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → β → β} {x : β} : foldr f x xs.unattach = foldr (fun (x : Subtype P) (s : β) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint s (f x) (binderNameHint h () (f (wfParam x) s)))) x xs

theorem Array.filter_wfParam {α : Type u_1} {xs : Array α} {f : α → Bool} : filter f (wfParam xs) = filter f xs.attach.unattach

theorem Array.filter_unattach {α : Type u_1} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Bool} : filter f xs.unattach = (filter (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs).unattach

theorem Array.reverse_wfParam {α : Type u_1} {xs : Array α} : (wfParam xs).reverse = xs.attach.unattach.reverse

theorem Array.reverse_unattach {α : Type u_1} {P : α → Prop} {xs : Array (Subtype P)} : xs.unattach.reverse = xs.reverse.unattach

theorem Array.filterMap_wfParam {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} : filterMap f (wfParam xs) = filterMap f xs.attach.unattach

theorem Array.filterMap_unattach {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Option β} : filterMap f xs.unattach = filterMap (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs

theorem Array.flatMap_wfParam {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} : flatMap f (wfParam xs) = flatMap f xs.attach.unattach

theorem Array.flatMap_unattach {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Array β} : flatMap f xs.unattach = flatMap (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs