Documentation

Mathlib.Logic.Equiv.List

Equivalences involving List-like types #

This file defines some additional constructive equivalences using Encodable and the pairing function on .

def Encodable.encodeList {α : Type u_1} [Encodable α] :
List α

Explicit encoding function for List α

Equations
Instances For
    @[irreducible]
    def Encodable.decodeList {α : Type u_1} [Encodable α] :
    Option (List α)

    Explicit decoding function for List α

    Equations
    Instances For
      instance List.encodable {α : Type u_1} [Encodable α] :

      If α is encodable, then so is List α. This uses the pair and unpair functions from Data.Nat.Pairing.

      Equations
      • List.encodable = { encode := Encodable.encodeList, decode := Encodable.decodeList, encodek := }
      instance List.countable {α : Type u_2} [Countable α] :
      Equations
      • =
      @[simp]
      @[simp]
      theorem Encodable.encode_list_cons {α : Type u_1} [Encodable α] (a : α) (l : List α) :
      @[simp]
      theorem Encodable.decode_list_succ {α : Type u_1} [Encodable α] (v : ) :
      Encodable.decode v.succ = Seq.seq ((fun (x1 : α) (x2 : List α) => x1 :: x2) <$> Encodable.decode (Nat.unpair v).1) fun (x : Unit) => Encodable.decode (Nat.unpair v).2
      theorem Encodable.length_le_encode {α : Type u_1} [Encodable α] (l : List α) :
      def Encodable.encodeMultiset {α : Type u_1} [Encodable α] (s : Multiset α) :

      Explicit encoding function for Multiset α

      Equations
      Instances For
        def Encodable.decodeMultiset {α : Type u_1} [Encodable α] (n : ) :

        Explicit decoding function for Multiset α

        Equations
        Instances For
          instance Multiset.encodable {α : Type u_1} [Encodable α] :

          If α is encodable, then so is Multiset α.

          Equations
          • Multiset.encodable = { encode := Encodable.encodeMultiset, decode := Encodable.decodeMultiset, encodek := }
          instance Multiset.countable {α : Type u_2} [Countable α] :

          If α is countable, then so is Multiset α.

          Equations
          • =
          def Encodable.encodableOfList {α : Type u_1} [DecidableEq α] (l : List α) (H : ∀ (x : α), x l) :

          A listable type with decidable equality is encodable.

          Equations
          Instances For

            A finite type is encodable. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def Fintype.toEncodable (α : Type u_2) [Fintype α] :

              A noncomputable way to arbitrarily choose an ordering on a finite type. It is not made into a global instance, since it involves an arbitrary choice. This can be locally made into an instance with attribute [local instance] Fintype.toEncodable.

              Equations
              Instances For
                instance Vector.encodable {α : Type u_1} [Encodable α] {n : } :

                If α is encodable, then so is Vector α n.

                Equations
                • Vector.encodable = Subtype.encodable
                instance Vector.countable {α : Type u_1} [Countable α] {n : } :

                If α is countable, then so is Vector α n.

                Equations
                • =
                instance Encodable.finArrow {α : Type u_1} [Encodable α] {n : } :
                Encodable (Fin nα)

                If α is encodable, then so is Fin n → α.

                Equations
                instance Encodable.finPi (n : ) (π : Fin nType u_2) [(i : Fin n) → Encodable (π i)] :
                Encodable ((i : Fin n) → π i)
                Equations
                instance Finset.encodable {α : Type u_1} [Encodable α] :

                If α is encodable, then so is Finset α.

                Equations
                • One or more equations did not get rendered due to their size.
                instance Finset.countable {α : Type u_1} [Countable α] :

                If α is countable, then so is Finset α.

                Equations
                • =
                def Encodable.fintypeArrow (α : Type u_2) (β : Type u_3) [DecidableEq α] [Fintype α] [Encodable β] :
                Trunc (Encodable (αβ))

                When α is finite and β is encodable, α → β is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

                Equations
                Instances For
                  def Encodable.fintypePi (α : Type u_2) (π : αType u_3) [DecidableEq α] [Fintype α] [(a : α) → Encodable (π a)] :
                  Trunc (Encodable ((a : α) → π a))

                  When α is finite and all π a are encodable, Π a, π a is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Encodable.sortedUniv (α : Type u_2) [Fintype α] [Encodable α] :
                    List α

                    The elements of a Fintype as a sorted list.

                    Equations
                    Instances For
                      @[simp]
                      theorem Encodable.mem_sortedUniv {α : Type u_2} [Fintype α] [Encodable α] (x : α) :
                      @[simp]
                      @[simp]
                      theorem Encodable.sortedUniv_nodup (α : Type u_2) [Fintype α] [Encodable α] :
                      @[simp]
                      theorem Encodable.sortedUniv_toFinset (α : Type u_2) [Fintype α] [Encodable α] [DecidableEq α] :
                      (Encodable.sortedUniv α).toFinset = Finset.univ

                      An encodable Fintype is equivalent to the same size Fin.

                      Equations
                      Instances For
                        instance Encodable.fintypeArrowOfEncodable {α : Type u_2} {β : Type u_3} [Encodable α] [Fintype α] [Encodable β] :
                        Encodable (αβ)

                        If α and β are encodable and α is a fintype, then α → β is encodable as well.

                        Equations
                        @[irreducible]

                        If α is denumerable, then so is List α.

                        Equations
                        @[simp]

                        Outputs the list of differences of the input list, that is lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]

                        Equations
                        Instances For

                          Outputs the list of partial sums of the input list, that is raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]

                          Equations
                          Instances For
                            theorem Denumerable.raise_lower {l : List } {n : } :
                            List.Sorted (fun (x1 x2 : ) => x1 x2) (n :: l)Denumerable.raise (Denumerable.lower l n) n = l
                            theorem Denumerable.raise_chain (l : List ) (n : ) :
                            List.Chain (fun (x1 x2 : ) => x1 x2) n (Denumerable.raise l n)
                            theorem Denumerable.raise_sorted (l : List ) (n : ) :
                            List.Sorted (fun (x1 x2 : ) => x1 x2) (Denumerable.raise l n)

                            raise l n is a non-decreasing sequence.

                            If α is denumerable, then so is Multiset α. Warning: this is not the same encoding as used in Multiset.encodable.

                            Equations
                            • One or more equations did not get rendered due to their size.

                            Outputs the list of differences minus one of the input list, that is lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...].

                            Equations
                            Instances For

                              Outputs the list of partial sums plus one of the input list, that is raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]. Adding one each time ensures the elements are distinct.

                              Equations
                              Instances For
                                theorem Denumerable.raise_lower' {l : List } {n : } :
                                (∀ ml, n m)List.Sorted (fun (x1 x2 : ) => x1 < x2) lDenumerable.raise' (Denumerable.lower' l n) n = l
                                theorem Denumerable.raise'_chain (l : List ) {m : } {n : } :
                                m < nList.Chain (fun (x1 x2 : ) => x1 < x2) m (Denumerable.raise' l n)
                                theorem Denumerable.raise'_sorted (l : List ) (n : ) :
                                List.Sorted (fun (x1 x2 : ) => x1 < x2) (Denumerable.raise' l n)

                                raise' l n is a strictly increasing sequence.

                                Makes raise' l n into a finset. Elements are distinct thanks to raise'_sorted.

                                Equations
                                Instances For
                                  instance Denumerable.finset {α : Type u_1} [Denumerable α] :

                                  If α is denumerable, then so is Finset α. Warning: this is not the same encoding as used in Finset.encodable.

                                  Equations
                                  • One or more equations did not get rendered due to their size.

                                  The type lists on unit is canonically equivalent to the natural numbers.

                                  Equations
                                  Instances For

                                    List is equivalent to .

                                    Equations
                                    Instances For
                                      def Equiv.listEquivSelfOfEquivNat {α : Type u_1} (e : α ) :
                                      List α α

                                      If α is equivalent to , then List α is equivalent to α.

                                      Equations
                                      Instances For