Documentation

Mathlib.Data.List.Sigma

Utilities for lists of sigmas #

This file includes several ways of interacting with List (Sigma β), treated as a key-value store.

If α : Type* and β : α → Type*, then we regard s : Sigma β as having key s.1 : α and value s.2 : β s.1. Hence, List (Sigma β) behaves like a key-value store.

Main Definitions #

keys #

def List.keys {α : Type u} {β : αType v} :
List (Sigma β)List α

List of keys from a list of key-value pairs

Equations
Instances For
    @[simp]
    theorem List.keys_nil {α : Type u} {β : αType v} :
    [].keys = []
    @[simp]
    theorem List.keys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
    (s :: l).keys = s.fst :: l.keys
    theorem List.mem_keys_of_mem {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
    s ls.fst l.keys
    theorem List.exists_of_mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} (h : a l.keys) :
    ∃ (b : β a), a, b l
    theorem List.mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
    a l.keys ∃ (b : β a), a, b l
    theorem List.not_mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
    al.keys ∀ (b : β a), a, bl
    theorem List.not_eq_key {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
    al.keys sl, a s.fst

    NodupKeys #

    def List.NodupKeys {α : Type u} {β : αType v} (l : List (Sigma β)) :

    Determines whether the store uses a key several times.

    Equations
    • l.NodupKeys = l.keys.Nodup
    Instances For
      theorem List.nodupKeys_iff_pairwise {α : Type u} {β : αType v} {l : List (Sigma β)} :
      l.NodupKeys List.Pairwise (fun (s s' : Sigma β) => s.fst s'.fst) l
      theorem List.NodupKeys.pairwise_ne {α : Type u} {β : αType v} {l : List (Sigma β)} (h : l.NodupKeys) :
      List.Pairwise (fun (s s' : Sigma β) => s.fst s'.fst) l
      @[simp]
      theorem List.nodupKeys_nil {α : Type u} {β : αType v} :
      [].NodupKeys
      @[simp]
      theorem List.nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
      (s :: l).NodupKeys s.fstl.keys l.NodupKeys
      theorem List.not_mem_keys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) :
      s.fstl.keys
      theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) :
      l.NodupKeys
      theorem List.NodupKeys.eq_of_fst_eq {α : Type u} {β : αType v} {l : List (Sigma β)} (nd : l.NodupKeys) {s : Sigma β} {s' : Sigma β} (h : s l) (h' : s' l) :
      s.fst = s'.fsts = s'
      theorem List.NodupKeys.eq_of_mk_mem {α : Type u} {β : αType v} {a : α} {b : β a} {b' : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : a, b l) (h' : a, b' l) :
      b = b'
      theorem List.nodupKeys_singleton {α : Type u} {β : αType v} (s : Sigma β) :
      [s].NodupKeys
      theorem List.NodupKeys.sublist {α : Type u} {β : αType v} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : l₁.Sublist l₂) :
      l₂.NodupKeysl₁.NodupKeys
      theorem List.NodupKeys.nodup {α : Type u} {β : αType v} {l : List (Sigma β)} :
      l.NodupKeysl.Nodup
      theorem List.perm_nodupKeys {α : Type u} {β : αType v} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : l₁.Perm l₂) :
      l₁.NodupKeys l₂.NodupKeys
      theorem List.nodupKeys_join {α : Type u} {β : αType v} {L : List (List (Sigma β))} :
      L.join.NodupKeys (lL, l.NodupKeys) List.Pairwise List.Disjoint (List.map List.keys L)
      theorem List.nodup_enum_map_fst {α : Type u} (l : List α) :
      (List.map Prod.fst l.enum).Nodup
      theorem List.mem_ext {α : Type u} {β : αType v} {l₀ : List (Sigma β)} {l₁ : List (Sigma β)} (nd₀ : l₀.Nodup) (nd₁ : l₁.Nodup) (h : ∀ (x : Sigma β), x l₀ x l₁) :
      l₀.Perm l₁

      dlookup #

      def List.dlookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
      List (Sigma β)Option (β a)

      dlookup a l is the first value in l corresponding to the key a, or none if no such element exists.

      Equations
      Instances For
        @[simp]
        theorem List.dlookup_nil {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
        List.dlookup a [] = none
        @[simp]
        theorem List.dlookup_cons_eq {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) :
        List.dlookup a (a, b :: l) = some b
        @[simp]
        theorem List.dlookup_cons_ne {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) :
        a s.fstList.dlookup a (s :: l) = List.dlookup a l
        theorem List.dlookup_isSome {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
        (List.dlookup a l).isSome = true a l.keys
        theorem List.dlookup_eq_none {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
        List.dlookup a l = none al.keys
        theorem List.of_mem_dlookup {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
        b List.dlookup a la, b l
        theorem List.mem_dlookup {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : a, b l) :
        theorem List.map_dlookup_eq_find {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
        Option.map (Sigma.mk a) (List.dlookup a l) = List.find? (fun (s : Sigma β) => decide (a = s.fst)) l
        theorem List.mem_dlookup_iff {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) :
        b List.dlookup a l a, b l
        theorem List.perm_dlookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) :
        theorem List.lookup_ext {α : Type u} {β : αType v} [DecidableEq α] {l₀ : List (Sigma β)} {l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys) (h : ∀ (x : α) (y : β x), y List.dlookup x l₀ y List.dlookup x l₁) :
        l₀.Perm l₁

        lookupAll #

        def List.lookupAll {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
        List (Sigma β)List (β a)

        lookup_all a l is the list of all values in l corresponding to the key a.

        Equations
        Instances For
          @[simp]
          theorem List.lookupAll_nil {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
          @[simp]
          theorem List.lookupAll_cons_eq {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) :
          List.lookupAll a (a, b :: l) = b :: List.lookupAll a l
          @[simp]
          theorem List.lookupAll_cons_ne {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) :
          a s.fstList.lookupAll a (s :: l) = List.lookupAll a l
          theorem List.lookupAll_eq_nil {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
          List.lookupAll a l = [] ∀ (b : β a), a, bl
          theorem List.head?_lookupAll {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
          (List.lookupAll a l).head? = List.dlookup a l
          theorem List.mem_lookupAll {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
          b List.lookupAll a l a, b l
          theorem List.lookupAll_sublist {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
          (List.map (Sigma.mk a) (List.lookupAll a l)).Sublist l
          theorem List.lookupAll_length_le_one {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
          (List.lookupAll a l).length 1
          theorem List.lookupAll_eq_dlookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
          List.lookupAll a l = (List.dlookup a l).toList
          theorem List.lookupAll_nodup {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
          (List.lookupAll a l).Nodup
          theorem List.perm_lookupAll {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) :

          kreplace #

          def List.kreplace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) :
          List (Sigma β)List (Sigma β)

          Replaces the first value with key a by b.

          Equations
          Instances For
            theorem List.kreplace_of_forall_not {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (H : ∀ (b : β a), a, bl) :
            theorem List.kreplace_self {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : a, b l) :
            theorem List.keys_kreplace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) :
            (List.kreplace a b l).keys = l.keys
            theorem List.kreplace_nodupKeys {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} :
            (List.kreplace a b l).NodupKeys l.NodupKeys
            theorem List.Perm.kreplace {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd : l₁.NodupKeys) :
            l₁.Perm l₂(List.kreplace a b l₁).Perm (List.kreplace a b l₂)

            kerase #

            def List.kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
            List (Sigma β)List (Sigma β)

            Remove the first pair with the key a.

            Equations
            Instances For
              theorem List.kerase_nil {α : Type u} {β : αType v} [DecidableEq α] {a : α} :
              List.kerase a [] = []
              @[simp]
              theorem List.kerase_cons_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a = s.fst) :
              List.kerase a (s :: l) = l
              @[simp]
              theorem List.kerase_cons_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a s.fst) :
              List.kerase a (s :: l) = s :: List.kerase a l
              @[simp]
              theorem List.kerase_of_not_mem_keys {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : al.keys) :
              theorem List.kerase_sublist {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
              (List.kerase a l).Sublist l
              theorem List.kerase_keys_subset {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
              (List.kerase a l).keys l.keys
              theorem List.mem_keys_of_mem_keys_kerase {α : Type u} {β : αType v} [DecidableEq α] {a₁ : α} {a₂ : α} {l : List (Sigma β)} :
              a₁ (List.kerase a₂ l).keysa₁ l.keys
              theorem List.exists_of_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : a l.keys) :
              ∃ (b : β a) (l₁ : List (Sigma β)) (l₂ : List (Sigma β)), al₁.keys l = l₁ ++ a, b :: l₂ List.kerase a l = l₁ ++ l₂
              @[simp]
              theorem List.mem_keys_kerase_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a₁ : α} {a₂ : α} {l : List (Sigma β)} (h : a₁ a₂) :
              a₁ (List.kerase a₂ l).keys a₁ l.keys
              theorem List.keys_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
              (List.kerase a l).keys = l.keys.erase a
              theorem List.kerase_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {l : List (Sigma β)} :
              theorem List.NodupKeys.kerase {α : Type u} {β : αType v} {l : List (Sigma β)} [DecidableEq α] (a : α) :
              l.NodupKeys(List.kerase a l).NodupKeys
              theorem List.Perm.kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd : l₁.NodupKeys) :
              l₁.Perm l₂(List.kerase a l₁).Perm (List.kerase a l₂)
              @[simp]
              theorem List.not_mem_keys_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) :
              a(List.kerase a l).keys
              @[simp]
              theorem List.dlookup_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) :
              @[simp]
              theorem List.dlookup_kerase_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {l : List (Sigma β)} (h : a a') :
              theorem List.kerase_append_left {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
              a l₁.keysList.kerase a (l₁ ++ l₂) = List.kerase a l₁ ++ l₂
              theorem List.kerase_append_right {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
              al₁.keysList.kerase a (l₁ ++ l₂) = l₁ ++ List.kerase a l₂
              theorem List.kerase_comm {α : Type u} {β : αType v} [DecidableEq α] (a₁ : α) (a₂ : α) (l : List (Sigma β)) :
              List.kerase a₂ (List.kerase a₁ l) = List.kerase a₁ (List.kerase a₂ l)
              theorem List.sizeOf_kerase {α : Type u_2} {β : αType u_1} [DecidableEq α] [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) :

              kinsert #

              def List.kinsert {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) :
              List (Sigma β)

              Insert the pair ⟨a, b⟩ and erase the first pair with the key a.

              Equations
              Instances For
                @[simp]
                theorem List.kinsert_def {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
                List.kinsert a b l = a, b :: List.kerase a l
                theorem List.mem_keys_kinsert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b' : β a'} {l : List (Sigma β)} :
                a (List.kinsert a' b' l).keys a = a' a l.keys
                theorem List.kinsert_nodupKeys {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (nd : l.NodupKeys) :
                (List.kinsert a b l).NodupKeys
                theorem List.Perm.kinsert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁.Perm l₂) :
                (List.kinsert a b l₁).Perm (List.kinsert a b l₂)
                theorem List.dlookup_kinsert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} (l : List (Sigma β)) :
                theorem List.dlookup_kinsert_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b' : β a'} {l : List (Sigma β)} (h : a a') :

                kextract #

                def List.kextract {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
                List (Sigma β)Option (β a) × List (Sigma β)

                Finds the first entry with a given key a and returns its value (as an Option because there might be no entry with key a) alongside with the rest of the entries.

                Equations
                Instances For
                  @[simp]
                  theorem List.kextract_eq_dlookup_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :

                  dedupKeys #

                  def List.dedupKeys {α : Type u} {β : αType v} [DecidableEq α] :
                  List (Sigma β)List (Sigma β)

                  Remove entries with duplicate keys from l : List (Sigma β).

                  Equations
                  Instances For
                    theorem List.dedupKeys_cons {α : Type u} {β : αType v} [DecidableEq α] {x : Sigma β} (l : List (Sigma β)) :
                    (x :: l).dedupKeys = List.kinsert x.fst x.snd l.dedupKeys
                    theorem List.nodupKeys_dedupKeys {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) :
                    l.dedupKeys.NodupKeys
                    theorem List.dlookup_dedupKeys {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
                    List.dlookup a l.dedupKeys = List.dlookup a l
                    theorem List.sizeOf_dedupKeys {α : Type u_2} {β : αType u_1} [DecidableEq α] [SizeOf (Sigma β)] (xs : List (Sigma β)) :
                    sizeOf xs.dedupKeys sizeOf xs

                    kunion #

                    def List.kunion {α : Type u} {β : αType v} [DecidableEq α] :
                    List (Sigma β)List (Sigma β)List (Sigma β)

                    kunion l₁ l₂ is the append to l₁ of l₂ after, for each key in l₁, the first matching pair in l₂ is erased.

                    Equations
                    Instances For
                      @[simp]
                      theorem List.nil_kunion {α : Type u} {β : αType v} [DecidableEq α] {l : List (Sigma β)} :
                      [].kunion l = l
                      @[simp]
                      theorem List.kunion_nil {α : Type u} {β : αType v} [DecidableEq α] {l : List (Sigma β)} :
                      l.kunion [] = l
                      @[simp]
                      theorem List.kunion_cons {α : Type u} {β : αType v} [DecidableEq α] {s : Sigma β} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
                      (s :: l₁).kunion l₂ = s :: l₁.kunion (List.kerase s.fst l₂)
                      @[simp]
                      theorem List.mem_keys_kunion {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
                      a (l₁.kunion l₂).keys a l₁.keys a l₂.keys
                      @[simp]
                      theorem List.kunion_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
                      (List.kerase a l₁).kunion (List.kerase a l₂) = List.kerase a (l₁.kunion l₂)
                      theorem List.NodupKeys.kunion {α : Type u} {β : αType v} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} [DecidableEq α] (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) :
                      (l₁.kunion l₂).NodupKeys
                      theorem List.Perm.kunion_right {α : Type u} {β : αType v} [DecidableEq α] {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (p : l₁.Perm l₂) (l : List (Sigma β)) :
                      (l₁.kunion l).Perm (l₂.kunion l)
                      theorem List.Perm.kunion_left {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
                      l₁.NodupKeysl₁.Perm l₂(l.kunion l₁).Perm (l.kunion l₂)
                      theorem List.Perm.kunion {α : Type u} {β : αType v} [DecidableEq α] {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} {l₃ : List (Sigma β)} {l₄ : List (Sigma β)} (nd₃ : l₃.NodupKeys) (p₁₂ : l₁.Perm l₂) (p₃₄ : l₃.Perm l₄) :
                      (l₁.kunion l₃).Perm (l₂.kunion l₄)
                      @[simp]
                      theorem List.dlookup_kunion_left {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : a l₁.keys) :
                      List.dlookup a (l₁.kunion l₂) = List.dlookup a l₁
                      @[simp]
                      theorem List.dlookup_kunion_right {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : al₁.keys) :
                      List.dlookup a (l₁.kunion l₂) = List.dlookup a l₂
                      theorem List.mem_dlookup_kunion {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
                      b List.dlookup a (l₁.kunion l₂) b List.dlookup a l₁ al₁.keys b List.dlookup a l₂
                      @[simp]
                      theorem List.dlookup_kunion_eq_some {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
                      List.dlookup a (l₁.kunion l₂) = some b List.dlookup a l₁ = some b al₁.keys List.dlookup a l₂ = some b
                      theorem List.mem_dlookup_kunion_middle {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} {l₃ : List (Sigma β)} (h₁ : b List.dlookup a (l₁.kunion l₃)) (h₂ : al₂.keys) :
                      b List.dlookup a ((l₁.kunion l₂).kunion l₃)