HepLean Documentation

Init.Data.Array.Attach

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

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 = { toList := xs.toList.attachWith P ⋯ }
Instances For
    source
    @[inline]
    def Array.attach {α : Type u_1} (xs : Array α) :
    Array { x : α // x ∈ xs }

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

    Equations
    Instances For
      source
      @[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
      source
      @[simp]
      theorem List.attach_toArray {α : Type u_1} {l : List α} :
      l.toArray.attach = (l.attachWith (fun (x : α) => x ∈ l.toArray) ⋯).toArray
      source
      @[simp]
      theorem Array.toList_attachWith {α : Type u_1} {l : Array α} {P : α → Prop} {H : ∀ (x : α), x ∈ l → P x} :
      (l.attachWith P H).toList = l.toList.attachWith P ⋯
      source
      @[simp]
      theorem Array.toList_attach {α : Type u_1} {l : Array α} :
      l.attach.toList = l.toList.attachWith (fun (x : α) => x ∈ l) ⋯

      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.

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

      A synonym for l.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 [Array.unattach, -Array.map_subtype] to unfold.

      Equations
      • l.unattach = Array.map (fun (x : { x : α // p x }) => x.val) l
      Instances For
        source
        @[simp]
        theorem Array.unattach_nil {α : Type u_1} {p : α → Prop} :
        #[].unattach = #[]
        source
        @[simp]
        theorem Array.unattach_push {α : Type u_1} {p : α → Prop} {a : { x : α // p x }} {l : Array { x : α // p x }} :
        (l.push a).unattach = l.unattach.push a.val
        source
        @[simp]
        theorem Array.size_unattach {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} :
        l.unattach.size = l.size
        source
        @[simp]
        theorem List.unattach_toArray {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} :
        l.toArray.unattach = l.unattach.toArray
        source
        @[simp]
        theorem Array.toList_unattach {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} :
        l.unattach.toList = l.toList.unattach
        source
        @[simp]
        theorem Array.unattach_attach {α : Type u_1} {l : Array α} :
        l.attach.unattach = l
        source
        @[simp]
        theorem Array.unattach_attachWith {α : Type u_1} {p : α → Prop} {l : Array α} {H : ∀ (a : α), a ∈ l → p a} :
        (l.attachWith p H).unattach = l

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

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

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

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

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

        source
        @[simp]
        theorem Array.map_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x} :
        Array.map f l = Array.map g l.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 Array.filterMap_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → Option β} {g : α → Option β} {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x} :
        Array.filterMap f l = Array.filterMap g l.unattach
        source
        @[simp]
        theorem Array.unattach_filter {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x} :
        (Array.filter f l).unattach = Array.filter g l.unattach

        Simp lemmas pushing unattach inwards. #

        source
        @[simp]
        theorem Array.unattach_reverse {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} :
        l.reverse.unattach = l.unattach.reverse
        source
        @[simp]
        theorem Array.unattach_append {α : Type u_1} {p : α → Prop} {l₁ l₂ : Array { x : α // p x }} :
        (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach