Documentation

Init.Data.Option.Attach

source
@[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
Instances For
    source
    @[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
    Instances For
      source
      @[simp]
      theorem Option.attach_none {α : Type u_1} :
      none.attach = none
      source
      @[simp]
      theorem Option.attachWith_none {α : Type u_1} {P : α → Prop} {H : ∀ (x : α), x ∈ none → P x} :
      none.attachWith P H = none
      source
      @[simp]
      theorem Option.attach_some {α : Type u_1} {x : α} :
      (some x).attach = some ⟨x, ⋯⟩
      source
      @[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, ⋯⟩
      source
      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
      source
      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 ⋯
      source
      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
      source
      @[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
      Instances For
        source
        theorem Option.attach_map_subtype_val {α : Type u_1} (o : Option α) :
        Option.map Subtype.val o.attach = o
        source
        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
        source
        @[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
        Instances For
          source
          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
          source
          theorem Option.mem_attach {α : Type u_1} (o : Option α) (x : { x : α // x ∈ o }) :
          x ∈ o.attach
          source
          @[simp]
          theorem Option.isNone_attach {α : Type u_1} (o : Option α) :
          o.attach.isNone = o.isNone
          source
          @[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
          source
          @[simp]
          theorem Option.isSome_attach {α : Type u_1} (o : Option α) :
          o.attach.isSome = o.isSome
          source
          @[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
          source
          @[simp]
          theorem Option.attach_eq_none_iff {α : Type u_1} {o : Option α} :
          o.attach = none ↔ o = none
          source
          @[simp]
          theorem Option.attach_eq_some_iff {α : Type u_1} {o : Option α} {x : { x : α // x ∈ o }} :
          o.attach = some x ↔ o = some x.val
          source
          @[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
          source
          @[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
          source
          @[simp]
          theorem Option.get_attach {α : Type u_1} {o : Option α} (h : o.attach.isSome = true) :
          o.attach.get h = ⟨o.get ⋯, ⋯⟩
          source
          @[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 ⋯, ⋯⟩
          source
          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
          source
          @[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
          source
          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
          source
          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) ⋯)
          source
          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 ⋯
          source
          @[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
          Instances For
            source
            @[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
            source
            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 ⋯
            source
            @[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
            source
            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
            source
            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⟩
            source
            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
            source
            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
            source
            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.

            source
            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
            Instances For
              source
              @[simp]
              theorem Option.unattach_none {α : Type u_1} {p : α → Prop} :
              none.unattach = none
              source
              @[simp]
              theorem Option.unattach_some {α : Type u_1} {p : α → Prop} {a : { x : α // p x }} :
              (some a).unattach = some a.val
              source
              @[simp]
              theorem Option.isSome_unattach {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} :
              o.unattach.isSome = o.isSome
              source
              @[simp]
              theorem Option.isNone_unattach {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} :
              o.unattach.isNone = o.isNone
              source
              @[simp]
              theorem Option.unattach_attach {α : Type u_1} (o : Option α) :
              o.attach.unattach = o
              source
              @[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. #

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

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