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

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

“Attaches” a proof that some predicate holds for an optional value, if present, returning a subtype that expresses this fact.

This function is primarily used to implement Option.attach, which allows definitions by well-founded recursion that use iteration operators (such as Option.map) to prove that an optional value drawn from a parameter is smaller than the parameter. This allows the well-founded recursion mechanism to prove that the function terminates.

Equations

• none.attachWith P H_2 = none
• (some x).attachWith P H_2 = some ⟨x, ⋯⟩

@[inline]

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

“Attaches” a proof that an optional value, if present, is indeed this value, returning a subtype that expresses this fact.

This function is primarily used to allow definitions by well-founded recursion that use iteration operators (such as Option.map) to prove that an optional value drawn from a parameter is smaller than the parameter. This allows the well-founded recursion mechanism to prove that the function terminates.

Equations

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

@[simp]

theorem Option.attach_none {α : Type u_1} : none.attach = none

@[simp]

theorem Option.attachWith_none {α : Type u_1} {P : α → Prop} {H : ∀ (x : α), x ∈ none → P x} : none.attachWith P H = none

@[simp]

theorem Option.attach_some {α : Type u_1} {x : α} : (some x).attach = some ⟨x, ⋯⟩

@[simp]

theorem Option.attachWith_some {α : Type u_1} {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) : (some x).attachWith P h = some ⟨x, ⋯⟩

theorem Option.attach_congr {α : Type u_1} {o₁ o₂ : Option α} (h : o₁ = o₂) : o₁.attach = Option.map (fun (x : { x : α // x ∈ o₂ }) => ⟨x.val, ⋯⟩) o₂.attach

theorem Option.attachWith_congr {α : Type u_1} {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ (x : α), x ∈ o₁ → P x} : o₁.attachWith P H = o₂.attachWith P ⋯

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

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

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

Equations

• @Option.attach_map_coe = @Option.attach_map_val

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

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

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

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

Equations

• @Option.attachWith_map_coe = @Option.attachWith_map_val

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

theorem Option.mem_attach {α : Type u_1} (o : Option α) (x : { x : α // x ∈ o }) : x ∈ o.attach

@[simp]

theorem Option.isNone_attach {α : Type u_1} (o : Option α) : o.attach.isNone = o.isNone

@[simp]

theorem Option.isNone_attachWith {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : (o.attachWith p H).isNone = o.isNone

@[simp]

theorem Option.isSome_attach {α : Type u_1} (o : Option α) : o.attach.isSome = o.isSome

@[simp]

theorem Option.isSome_attachWith {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : (o.attachWith p H).isSome = o.isSome

@[simp]

theorem Option.attach_eq_none_iff {α : Type u_1} {o : Option α} : o.attach = none ↔ o = none

@[simp]

theorem Option.attach_eq_some_iff {α : Type u_1} {o : Option α} {x : { x : α // x ∈ o }} : o.attach = some x ↔ o = some x.val

@[simp]

theorem Option.attachWith_eq_none_iff {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), a ∈ o → p a) : o.attachWith p H = none ↔ o = none

@[simp]

theorem Option.attachWith_eq_some_iff {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), a ∈ o → p a) {x : { x : α // p x }} : o.attachWith p H = some x ↔ o = some x.val

@[simp]

theorem Option.get_attach {α : Type u_1} {o : Option α} (h : o.attach.isSome = true) : o.attach.get h = ⟨o.get ⋯, ⋯⟩

@[simp]

theorem Option.get_attachWith {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), a ∈ o → p a) (h : (o.attachWith p H).isSome = true) : (o.attachWith p H).get h = ⟨o.get ⋯, ⋯⟩

theorem Option.toList_attach {α : Type u_1} (o : Option α) : o.attach.toList = List.map (fun (x : { x : α // x ∈ o.toList }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) o.toList.attach

@[simp]

theorem Option.attach_toList {α : Type u_1} (o : Option α) : o.toList.attach = (Option.map (fun (x : { x : α // x ∈ o }) => match x with | ⟨a, h⟩ => ⟨a, ⋯⟩) o.attach).toList

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

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

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

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

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

Equations

• @Option.map_attach = @Option.map_attach_eq_pmap

@[simp]

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

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

@[simp]

theorem Option.map_attach_eq_attachWith {α : Type u_1} {o : Option α} {p : α → Prop} (f : ∀ (a : α), a ∈ o → p a) : Option.map (fun (x : { x : α // x ∈ o }) => ⟨x.val, ⋯⟩) o.attach = o.attachWith p f

theorem Option.attach_bind {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : (o.bind f).attach = o.attach.bind fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => Option.map (fun (x_1 : { x_1 : β // x_1 ∈ f x }) => match x_1 with | ⟨y, h'⟩ => ⟨y, ⋯⟩) (f x).attach

theorem Option.bind_attach {α : Type u_1} {β : Type u_2} {o : Option α} {f : { x : α // x ∈ o } → Option β} : o.attach.bind f = o.pbind fun (a : α) (h : a ∈ o) => f ⟨a, h⟩

theorem Option.pbind_eq_bind_attach {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a ∈ o → Option β} : o.pbind f = o.attach.bind fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => f x h

theorem Option.attach_filter {α : Type u_1} {o : Option α} {p : α → Bool} : (Option.filter p o).attach = o.attach.bind fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => if h' : p x = true then some ⟨x, ⋯⟩ else none

theorem Option.filter_attach {α : Type u_1} {o : Option α} {p : { x : α // x ∈ o } → Bool} : Option.filter p o.attach = o.pbind fun (a : α) (h : a ∈ o) => if p ⟨a, h⟩ = true then some ⟨a, h⟩ else none

unattach

Option.unattach is the (one-sided) inverse of Option.attach. It is a synonym for Option.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 : Option { 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 Option.unattach {α : Type u_1} {p : α → Prop} (o : Option { x : α // p x }) : Option α

Remove an attached proof that the value in an Option is indeed that value.

This function is usually inserted automatically by Lean, rather than 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 [Option.unattach, -Option.map_subtype].

It is a synonym for Option.map Subtype.val.

Equations

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

@[simp]

theorem Option.unattach_none {α : Type u_1} {p : α → Prop} : none.unattach = none

@[simp]

theorem Option.unattach_some {α : Type u_1} {p : α → Prop} {a : { x : α // p x }} : (some a).unattach = some a.val

@[simp]

theorem Option.isSome_unattach {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} : o.unattach.isSome = o.isSome

@[simp]

theorem Option.isNone_unattach {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} : o.unattach.isNone = o.isNone

@[simp]

theorem Option.unattach_attach {α : Type u_1} (o : Option α) : o.attach.unattach = o

@[simp]

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

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

@[simp]

theorem Option.map_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Option.map f o = Option.map g o.unattach

This lemma identifies maps over lists 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 Option.bind_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x : α // p x }} {f : { x : α // p x } → Option β} {g : α → Option β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : o.bind f = o.unattach.bind g

@[simp]

theorem Option.unattach_filter {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : (Option.filter f o).unattach = Option.filter g o.unattach