Documentation

Mathlib.Data.List.AList

Association Lists #

This file defines association lists. An association list is a list where every element consists of a key and a value, and no two entries have the same key. The type of the value is allowed to be dependent on the type of the key.

This type dependence is implemented using Sigma: The elements of the list are of type Sigma β, for some type index β.

Main definitions #

Association lists are represented by the AList structure. This file defines this structure and provides ways to access, modify, and combine ALists.

References #

structure AList {α : Type u} (β : αType v) :
Type (max u v)

AList β is a key-value map stored as a List (i.e. a linked list). It is a wrapper around certain List functions with the added constraint that the list have unique keys.

Instances For
    def List.toAList {α : Type u} [DecidableEq α] {β : αType v} (l : List (Sigma β)) :

    Given l : List (Sigma β), create a term of type AList β by removing entries with duplicate keys.

    Instances For
      theorem AList.ext {α : Type u} {β : αType v} {s : AList β} {t : AList β} :
      s.entries = t.entriess = t
      theorem AList.ext_iff {α : Type u} {β : αType v} {s : AList β} {t : AList β} :
      s = t s.entries = t.entries
      instance AList.instDecidableEqAList {α : Type u} {β : αType v} [DecidableEq α] [(a : α) → DecidableEq (β a)] :

      keys #

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

      The list of keys of an association list.

      Instances For
        theorem AList.keys_nodup {α : Type u} {β : αType v} (s : AList β) :

        mem #

        instance AList.instMembershipAList {α : Type u} {β : αType v} :

        The predicate a ∈ s means that s has a value associated to the key a.

        theorem AList.mem_keys {α : Type u} {β : αType v} {a : α} {s : AList β} :
        theorem AList.mem_of_perm {α : Type u} {β : αType v} {a : α} {s₁ : AList β} {s₂ : AList β} (p : s₁.entries ~ s₂.entries) :
        a s₁ a s₂

        empty #

        instance AList.instEmptyCollectionAList {α : Type u} {β : αType v} :

        The empty association list.

        instance AList.instInhabitedAList {α : Type u} {β : αType v} :
        @[simp]
        theorem AList.not_mem_empty {α : Type u} {β : αType v} (a : α) :
        @[simp]
        theorem AList.empty_entries {α : Type u} {β : αType v} :
        .entries = []
        @[simp]
        theorem AList.keys_empty {α : Type u} {β : αType v} :

        singleton #

        def AList.singleton {α : Type u} {β : αType v} (a : α) (b : β a) :

        The singleton association list.

        Instances For
          @[simp]
          theorem AList.singleton_entries {α : Type u} {β : αType v} (a : α) (b : β a) :
          (AList.singleton a b).entries = [{ fst := a, snd := b }]
          @[simp]
          theorem AList.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :

          lookup #

          def AList.lookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
          Option (β a)

          Look up the value associated to a key in an association list.

          Instances For
            @[simp]
            theorem AList.lookup_empty {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
            theorem AList.lookup_isSome {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : AList β} :
            theorem AList.lookup_eq_none {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : AList β} :
            AList.lookup a s = none ¬a s
            theorem AList.mem_lookup_iff {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : AList β} :
            b AList.lookup a s { fst := a, snd := b } s.entries
            theorem AList.perm_lookup {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} (p : s₁.entries ~ s₂.entries) :
            instance AList.instDecidableMemAListInstMembershipAList {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
            theorem AList.keys_subset_keys_of_entries_subset_entries {α : Type u} {β : αType v} {s₁ : AList β} {s₂ : AList β} (h : s₁.entries s₂.entries) :

            replace #

            def AList.replace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :

            Replace a key with a given value in an association list. If the key is not present it does nothing.

            Instances For
              @[simp]
              theorem AList.keys_replace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :
              @[simp]
              theorem AList.mem_replace {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b : β a} {s : AList β} :
              a' AList.replace a b s a' s
              theorem AList.perm_replace {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} :
              s₁.entries ~ s₂.entries(AList.replace a b s₁).entries ~ (AList.replace a b s₂).entries
              def AList.foldl {α : Type u} {β : αType v} {δ : Type w} (f : δ(a : α) → β aδ) (d : δ) (m : AList β) :
              δ

              Fold a function over the key-value pairs in the map.

              Instances For

                erase #

                def AList.erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :

                Erase a key from the map. If the key is not present, do nothing.

                Instances For
                  @[simp]
                  theorem AList.keys_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
                  @[simp]
                  theorem AList.mem_erase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {s : AList β} :
                  a' AList.erase a s a' a a' s
                  theorem AList.perm_erase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} :
                  s₁.entries ~ s₂.entries(AList.erase a s₁).entries ~ (AList.erase a s₂).entries
                  @[simp]
                  theorem AList.lookup_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
                  @[simp]
                  theorem AList.lookup_erase_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {s : AList β} (h : a a') :
                  theorem AList.erase_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (a' : α) (s : AList β) :

                  insert #

                  def AList.insert {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :

                  Insert a key-value pair into an association list and erase any existing pair with the same key.

                  Instances For
                    @[simp]
                    theorem AList.insert_entries {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : AList β} :
                    (AList.insert a b s).entries = { fst := a, snd := b } :: List.kerase a s.entries
                    theorem AList.insert_entries_of_neg {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : AList β} (h : ¬a s) :
                    (AList.insert a b s).entries = { fst := a, snd := b } :: s.entries
                    theorem AList.insert_of_neg {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : AList β} (h : ¬a s) :
                    AList.insert a b s = { entries := { fst := a, snd := b } :: s.entries, nodupKeys := (_ : List.NodupKeys ({ fst := a, snd := b } :: s.entries)) }
                    @[simp]
                    theorem AList.insert_empty {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) :
                    @[simp]
                    theorem AList.mem_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b' : β a'} (s : AList β) :
                    a AList.insert a' b' s a = a' a s
                    @[simp]
                    theorem AList.keys_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} (s : AList β) :
                    theorem AList.perm_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} (p : s₁.entries ~ s₂.entries) :
                    (AList.insert a b s₁).entries ~ (AList.insert a b s₂).entries
                    @[simp]
                    theorem AList.lookup_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} (s : AList β) :
                    @[simp]
                    theorem AList.lookup_insert_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b' : β a'} {s : AList β} (h : a a') :
                    @[simp]
                    theorem AList.lookup_to_alist {α : Type u} {β : αType v} [DecidableEq α] {a : α} (s : List (Sigma β)) :
                    @[simp]
                    theorem AList.insert_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {b' : β a} (s : AList β) :
                    theorem AList.insert_insert_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b : β a} {b' : β a'} (s : AList β) (h : a a') :
                    (AList.insert a' b' (AList.insert a b s)).entries ~ (AList.insert a b (AList.insert a' b' s)).entries
                    @[simp]
                    theorem AList.insert_singleton_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {b' : β a} :
                    @[simp]
                    theorem AList.entries_toAList {α : Type u} {β : αType v} [DecidableEq α] (xs : List (Sigma β)) :
                    (List.toAList xs).entries = List.dedupKeys xs
                    theorem AList.toAList_cons {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)) :
                    List.toAList ({ fst := a, snd := b } :: xs) = AList.insert a b (List.toAList xs)
                    theorem AList.mk_cons_eq_insert {α : Type u} {β : αType v} [DecidableEq α] (c : Sigma β) (l : List (Sigma β)) (h : List.NodupKeys (c :: l)) :
                    { entries := c :: l, nodupKeys := h } = AList.insert c.fst c.snd { entries := l, nodupKeys := (_ : List.NodupKeys l) }
                    def AList.insertRec {α : Type u} {β : αType v} [DecidableEq α] {C : AList βSort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : AList β) → ¬a lC lC (AList.insert a b l)) (l : AList β) :
                    C l

                    Recursion on an AList, using insert. Use as induction l using AList.insertRec.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    • AList.insertRec H0 IH { entries := [], nodupKeys := nodupKeys } = H0
                    Instances For
                      @[simp]
                      theorem AList.insertRec_empty {α : Type u} {β : αType v} [DecidableEq α] {C : AList βSort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : AList β) → ¬a lC lC (AList.insert a b l)) :
                      theorem AList.insertRec_insert {α : Type u} {β : αType v} [DecidableEq α] {C : AList βSort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : AList β) → ¬a lC lC (AList.insert a b l)) {c : Sigma β} {l : AList β} (h : ¬c.fst l) :
                      AList.insertRec H0 IH (AList.insert c.fst c.snd l) = IH c.fst c.snd l h (AList.insertRec H0 IH l)
                      theorem AList.insertRec_insert_mk {α : Type u} {β : αType v} [DecidableEq α] {C : AList βSort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : AList β) → ¬a lC lC (AList.insert a b l)) {a : α} (b : β a) {l : AList β} (h : ¬a l) :
                      AList.insertRec H0 IH (AList.insert a b l) = IH a b l h (AList.insertRec H0 IH l)

                      extract #

                      def AList.extract {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
                      Option (β a) × AList β

                      Erase a key from the map, and return the corresponding value, if found.

                      Instances For
                        @[simp]
                        theorem AList.extract_eq_lookup_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :

                        union #

                        def AList.union {α : Type u} {β : αType v} [DecidableEq α] (s₁ : AList β) (s₂ : AList β) :

                        s₁ ∪ s₂ is the key-based union of two association lists. It is left-biased: if there exists an a ∈ s₁, lookup a (s₁ ∪ s₂) = lookup a s₁.

                        Instances For
                          instance AList.instUnionAList {α : Type u} {β : αType v} [DecidableEq α] :
                          @[simp]
                          theorem AList.union_entries {α : Type u} {β : αType v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} :
                          (s₁ s₂).entries = List.kunion s₁.entries s₂.entries
                          @[simp]
                          theorem AList.empty_union {α : Type u} {β : αType v} [DecidableEq α] {s : AList β} :
                          s = s
                          @[simp]
                          theorem AList.union_empty {α : Type u} {β : αType v} [DecidableEq α] {s : AList β} :
                          s = s
                          @[simp]
                          theorem AList.mem_union {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} :
                          a s₁ s₂ a s₁ a s₂
                          theorem AList.perm_union {α : Type u} {β : αType v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} {s₃ : AList β} {s₄ : AList β} (p₁₂ : s₁.entries ~ s₂.entries) (p₃₄ : s₃.entries ~ s₄.entries) :
                          (s₁ s₃).entries ~ (s₂ s₄).entries
                          theorem AList.union_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s₁ : AList β) (s₂ : AList β) :
                          AList.erase a (s₁ s₂) = AList.erase a s₁ AList.erase a s₂
                          @[simp]
                          theorem AList.lookup_union_left {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} :
                          a s₁AList.lookup a (s₁ s₂) = AList.lookup a s₁
                          @[simp]
                          theorem AList.lookup_union_right {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} :
                          ¬a s₁AList.lookup a (s₁ s₂) = AList.lookup a s₂
                          theorem AList.mem_lookup_union {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} :
                          b AList.lookup a (s₁ s₂) b AList.lookup a s₁ ¬a s₁ b AList.lookup a s₂
                          @[simp]
                          theorem AList.lookup_union_eq_some {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} :
                          AList.lookup a (s₁ s₂) = some b AList.lookup a s₁ = some b ¬a s₁ AList.lookup a s₂ = some b
                          theorem AList.mem_lookup_union_middle {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} {s₃ : AList β} :
                          b AList.lookup a (s₁ s₃)¬a s₂b AList.lookup a (s₁ s₂ s₃)
                          theorem AList.insert_union {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} :
                          AList.insert a b (s₁ s₂) = AList.insert a b s₁ s₂
                          theorem AList.union_assoc {α : Type u} {β : αType v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} {s₃ : AList β} :
                          (s₁ s₂ s₃).entries ~ (s₁ (s₂ s₃)).entries

                          disjoint #

                          def AList.Disjoint {α : Type u} {β : αType v} (s₁ : AList β) (s₂ : AList β) :

                          Two associative lists are disjoint if they have no common keys.

                          Instances For
                            theorem AList.union_comm_of_disjoint {α : Type u} {β : αType v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} (h : AList.Disjoint s₁ s₂) :
                            (s₁ s₂).entries ~ (s₂ s₁).entries