Documentation

Init.Data.Array.Bootstrap

Bootstrapping theorems about arrays #

This file contains some theorems about Array and List needed for Init.Data.List.Impl.

@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
def Array.get {α : Type u} (a : Array α) (i : Nat) (h : i < a.size) :
α

Use the indexing notation a[i] instead.

Access an element from an array without needing a runtime bounds checks, using a Nat index and a proof that it is in bounds.

This function does not use get_elem_tactic to automatically find the proof that the index is in bounds. This is because the tactic itself needs to look up values in arrays.

Equations
    Instances For
      @[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17")]
      def Array.get! {α : Type u} [Inhabited α] (a : Array α) (i : Nat) :
      α

      Use the indexing notation a[i]! instead.

      Access an element from an array, or panic if the index is out of bounds.

      Equations
        Instances For
          @[irreducible]
          theorem Array.foldlM_toList.aux {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : βαm β} {xs : Array α} {i j : Nat} (H : xs.size i + j) {b : β} :
          foldlM.loop f xs xs.size i j b = List.foldlM f b (List.drop j xs.toList)
          @[simp]
          theorem Array.foldlM_toList {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : βαm β} {init : β} {xs : Array α} :
          List.foldlM f init xs.toList = foldlM f init xs
          @[simp]
          theorem Array.foldl_toList {β : Type u_1} {α : Type u_2} (f : βαβ) {init : β} {xs : Array α} :
          List.foldl f init xs.toList = foldl f init xs
          theorem Array.foldrM_eq_reverse_foldlM_toList.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : αβm β} {xs : Array α} {init : β} {i : Nat} (h : i xs.size) :
          List.foldlM (fun (x : β) (y : α) => f y x) init (List.take i xs.toList).reverse = foldrM.fold f xs 0 i h init
          theorem Array.foldrM_eq_reverse_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : αβm β} {init : β} {xs : Array α} :
          foldrM f init xs = List.foldlM (fun (x : β) (y : α) => f y x) init xs.toList.reverse
          @[simp]
          theorem Array.foldrM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : αβm β} {init : β} {xs : Array α} :
          List.foldrM f init xs.toList = foldrM f init xs
          @[simp]
          theorem Array.foldr_toList {α : Type u_1} {β : Type u_2} (f : αββ) {init : β} {xs : Array α} :
          List.foldr f init xs.toList = foldr f init xs
          @[simp]
          theorem Array.toList_push {α : Type u_1} {xs : Array α} {x : α} :
          (xs.push x).toList = xs.toList ++ [x]
          @[reducible, inline, deprecated Array.toList_push (since := "2025-05-26")]
          abbrev Array.push_toList {α : Type u_1} {xs : Array α} {x : α} :
          (xs.push x).toList = xs.toList ++ [x]
          Equations
            Instances For
              @[simp]
              theorem Array.toListAppend_eq {α : Type u_1} {xs : Array α} {l : List α} :
              @[simp]
              theorem Array.toListImpl_eq {α : Type u_1} {xs : Array α} :
              @[simp]
              theorem Array.toList_pop {α : Type u_1} {xs : Array α} :
              @[reducible, inline, deprecated Array.toList_pop (since := "2025-02-17")]
              abbrev Array.pop_toList {α : Type u_1} {xs : Array α} :
              Equations
                Instances For
                  @[simp]
                  theorem Array.append_eq_append {α : Type u_1} {xs ys : Array α} :
                  xs.append ys = xs ++ ys
                  @[simp]
                  theorem Array.toList_append {α : Type u_1} {xs ys : Array α} :
                  (xs ++ ys).toList = xs.toList ++ ys.toList
                  @[simp]
                  theorem Array.toList_empty {α : Type u_1} :
                  @[simp]
                  theorem Array.append_empty {α : Type u_1} {xs : Array α} :
                  xs ++ #[] = xs
                  @[reducible, inline, deprecated Array.append_empty (since := "2025-01-13")]
                  abbrev Array.append_nil {α : Type u_1} {xs : Array α} :
                  xs ++ #[] = xs
                  Equations
                    Instances For
                      @[simp]
                      theorem Array.empty_append {α : Type u_1} {xs : Array α} :
                      #[] ++ xs = xs
                      @[reducible, inline, deprecated Array.empty_append (since := "2025-01-13")]
                      abbrev Array.nil_append {α : Type u_1} {xs : Array α} :
                      #[] ++ xs = xs
                      Equations
                        Instances For
                          @[simp]
                          theorem Array.append_assoc {α : Type u_1} {xs ys zs : Array α} :
                          xs ++ ys ++ zs = xs ++ (ys ++ zs)
                          @[simp]
                          theorem Array.appendList_eq_append {α : Type u_1} {xs : Array α} {l : List α} :
                          xs.appendList l = xs ++ l
                          @[simp]
                          theorem Array.toList_appendList {α : Type u_1} {xs : Array α} {l : List α} :
                          (xs ++ l).toList = xs.toList ++ l
                          @[reducible, inline, deprecated Array.toList_appendList (since := "2024-12-11")]
                          abbrev Array.appendList_toList {α : Type u_1} {xs : Array α} {l : List α} :
                          (xs ++ l).toList = xs.toList ++ l
                          Equations
                            Instances For