Documentation

Mathlib.Logic.Encodable.Basic

Encodable types #

This file defines encodable (constructively countable) types as a typeclass. This is used to provide explicit encode/decode functions from and to , with the information that those functions are inverses of each other. The difference with Denumerable is that finite types are encodable. For infinite types, Encodable and Denumerable agree.

Main declarations #

Implementation notes #

The point of asking for an explicit partial inverse decode : ℕ → Option α to encode : α → ℕ is to make the range of encode decidable even when the finiteness of α is not.

class Encodable (α : Type u_1) :
Type u_1

Constructively countable type. Made from an explicit injection encode : α → ℕ and a partial inverse decode : ℕ → Option α. Note that finite types are countable. See Denumerable if you wish to enforce infiniteness.

Instances
    @[simp]
    theorem Encodable.encodek {α : Type u_1} [self : Encodable α] (a : α) :

    Invariant relationship between encoding and decoding

    theorem Encodable.encode_injective {α : Type u_1} [Encodable α] :
    Function.Injective Encodable.encode
    @[simp]
    theorem Encodable.encode_inj {α : Type u_1} [Encodable α] {a : α} {b : α} :
    @[instance 400]
    instance Encodable.countable {α : Type u_1} [Encodable α] :
    Equations
    • =

    An encodable type has decidable equality. Not set as an instance because this is usually not the best way to infer decidability.

    Equations
    Instances For
      def Encodable.ofLeftInjection {α : Type u_1} {β : Type u_2} [Encodable α] (f : βα) (finv : αOption β) (linv : ∀ (b : β), finv (f b) = some b) :

      If α is encodable and there is an injection f : β → α, then β is encodable as well.

      Equations
      Instances For
        def Encodable.ofLeftInverse {α : Type u_1} {β : Type u_2} [Encodable α] (f : βα) (finv : αβ) (linv : ∀ (b : β), finv (f b) = b) :

        If α is encodable and f : β → α is invertible, then β is encodable as well.

        Equations
        Instances For
          def Encodable.ofEquiv {β : Type u_2} (α : Type u_3) [Encodable α] (e : β α) :

          Encodability is preserved by equivalence.

          Equations
          Instances For
            theorem Encodable.encode_ofEquiv {α : Type u_3} {β : Type u_4} [Encodable α] (e : β α) (b : β) :
            theorem Encodable.decode_ofEquiv {α : Type u_3} {β : Type u_4} [Encodable α] (e : β α) (n : ) :
            Equations
            @[instance 100]
            instance IsEmpty.toEncodable {α : Type u_1} [IsEmpty α] :
            Equations
            • IsEmpty.toEncodable = { encode := fun (a : α) => isEmptyElim a, decode := fun (x : ) => none, encodek := }
            Equations
            @[simp]
            instance Option.encodable {α : Type u_3} [h : Encodable α] :

            If α is encodable, then so is Option α.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Encodable.encode_none {α : Type u_1} [Encodable α] :
            @[simp]
            theorem Encodable.encode_some {α : Type u_1} [Encodable α] (a : α) :
            @[simp]
            def Encodable.decode₂ (α : Type u_3) [Encodable α] (n : ) :

            Failsafe variant of decode. decode₂ α n returns the preimage of n under encode if it exists, and returns none if it doesn't. This requirement could be imposed directly on decode but is not to help make the definition easier to use.

            Equations
            Instances For
              theorem Encodable.mem_decode₂ {α : Type u_1} [Encodable α] {n : } {a : α} :
              @[simp]
              theorem Encodable.decode₂_ne_none_iff {α : Type u_1} [Encodable α] {n : } :
              Encodable.decode₂ α n none n Set.range Encodable.encode
              theorem Encodable.decode₂_inj {α : Type u_1} [Encodable α] {n : } {a₁ : α} {a₂ : α} (h₁ : a₁ Encodable.decode₂ α n) (h₂ : a₂ Encodable.decode₂ α n) :
              a₁ = a₂
              def Encodable.decidableRangeEncode (α : Type u_3) [Encodable α] :
              DecidablePred fun (x : ) => x Set.range Encodable.encode

              The encoding function has decidable range.

              Equations
              Instances For
                def Encodable.equivRangeEncode (α : Type u_3) [Encodable α] :
                α (Set.range Encodable.encode)

                An encodable type is equivalent to the range of its encoding function.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Unique.encodable {α : Type u_1} [Unique α] :

                  A type with unique element is encodable. This is not an instance to avoid diamonds.

                  Equations
                  • Unique.encodable = { encode := fun (x : α) => 0, decode := fun (x : ) => some default, encodek := }
                  Instances For
                    def Encodable.encodeSum {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] :
                    α β

                    Explicit encoding function for the sum of two encodable types.

                    Equations
                    Instances For
                      def Encodable.decodeSum {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] (n : ) :
                      Option (α β)

                      Explicit decoding function for the sum of two encodable types.

                      Equations
                      Instances For
                        instance Sum.encodable {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] :
                        Encodable (α β)

                        If α and β are encodable, then so is their sum.

                        Equations
                        • Sum.encodable = { encode := Encodable.encodeSum, decode := Encodable.decodeSum, encodek := }
                        @[simp]
                        theorem Encodable.encode_inl {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] (a : α) :
                        @[simp]
                        theorem Encodable.encode_inr {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] (b : β) :
                        @[simp]
                        theorem Encodable.decode_ge_two (n : ) (h : 2 n) :
                        def Encodable.encodeSigma {α : Type u_1} {γ : αType u_3} [Encodable α] [(a : α) → Encodable (γ a)] :
                        Sigma γ

                        Explicit encoding function for Sigma γ

                        Equations
                        Instances For
                          def Encodable.decodeSigma {α : Type u_1} {γ : αType u_3} [Encodable α] [(a : α) → Encodable (γ a)] (n : ) :

                          Explicit decoding function for Sigma γ

                          Equations
                          Instances For
                            instance Sigma.encodable {α : Type u_1} {γ : αType u_3} [Encodable α] [(a : α) → Encodable (γ a)] :
                            Equations
                            • Sigma.encodable = { encode := Encodable.encodeSigma, decode := Encodable.decodeSigma, encodek := }
                            @[simp]
                            theorem Encodable.decode_sigma_val {α : Type u_1} {γ : αType u_3} [Encodable α] [(a : α) → Encodable (γ a)] (n : ) :
                            Encodable.decode n = (Encodable.decode n.unpair.1).bind fun (a : α) => Option.map (Sigma.mk a) (Encodable.decode n.unpair.2)
                            @[simp]
                            theorem Encodable.encode_sigma_val {α : Type u_1} {γ : αType u_3} [Encodable α] [(a : α) → Encodable (γ a)] (a : α) (b : γ a) :
                            instance Encodable.Prod.encodable {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] :
                            Encodable (α × β)

                            If α and β are encodable, then so is their product.

                            Equations
                            @[simp]
                            theorem Encodable.decode_prod_val {α : Type u_1} {β : Type u_2} [Encodable β] [i : Encodable α] (n : ) :
                            Encodable.decode n = (Encodable.decode n.unpair.1).bind fun (a : α) => Option.map (Prod.mk a) (Encodable.decode n.unpair.2)
                            @[simp]
                            theorem Encodable.encode_prod_val {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] (a : α) (b : β) :
                            def Encodable.encodeSubtype {α : Type u_1} {P : αProp} [encA : Encodable α] :
                            { a : α // P a }

                            Explicit encoding function for a decidable subtype of an encodable type

                            Equations
                            Instances For
                              def Encodable.decodeSubtype {α : Type u_1} {P : αProp} [encA : Encodable α] [decP : DecidablePred P] (v : ) :
                              Option { a : α // P a }

                              Explicit decoding function for a decidable subtype of an encodable type

                              Equations
                              Instances For
                                instance Subtype.encodable {α : Type u_1} {P : αProp} [encA : Encodable α] [decP : DecidablePred P] :
                                Encodable { a : α // P a }

                                A decidable subtype of an encodable type is encodable.

                                Equations
                                • Subtype.encodable = { encode := Encodable.encodeSubtype, decode := Encodable.decodeSubtype, encodek := }
                                theorem Encodable.Subtype.encode_eq {α : Type u_1} {P : αProp} [encA : Encodable α] [decP : DecidablePred P] (a : Subtype P) :
                                instance Fin.encodable (n : ) :
                                Equations

                                The lift of an encodable type is encodable

                                Equations
                                instance PLift.encodable {α : Type u_1} [Encodable α] :

                                The lift of an encodable type is encodable.

                                Equations
                                noncomputable def Encodable.ofInj {α : Type u_1} {β : Type u_2} [Encodable β] (f : αβ) (hf : Function.Injective f) :

                                If β is encodable and there is an injection f : α → β, then α is encodable as well.

                                Equations
                                Instances For
                                  noncomputable def Encodable.ofCountable (α : Type u_3) [Countable α] :

                                  If α is countable, then it has a (non-canonical) Encodable structure.

                                  Equations
                                  Instances For
                                    theorem nonempty_encodable (α : Type u_1) [Countable α] :

                                    See also nonempty_fintype, nonempty_denumerable.

                                    def ULower (α : Type u_1) [Encodable α] :

                                    ULower α : Type is an equivalent type in the lowest universe, given Encodable α.

                                    Equations
                                    Instances For
                                      instance instDecidableEqULower {α : Type u_1} [Encodable α] :
                                      Equations
                                      instance instEncodableULower {α : Type u_1} [Encodable α] :
                                      Equations
                                      • instEncodableULower = id inferInstance
                                      def ULower.equiv (α : Type u_1) [Encodable α] :
                                      α ULower α

                                      The equivalence between the encodable type α and ULower α : Type.

                                      Equations
                                      Instances For
                                        def ULower.down {α : Type u_1} [Encodable α] (a : α) :

                                        Lowers an a : α into ULower α.

                                        Equations
                                        Instances For
                                          instance ULower.instInhabited {α : Type u_1} [Encodable α] [Inhabited α] :
                                          Equations
                                          def ULower.up {α : Type u_1} [Encodable α] (a : ULower α) :
                                          α

                                          Lifts an a : ULower α into α.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem ULower.down_up {α : Type u_1} [Encodable α] {a : ULower α} :
                                            ULower.down a.up = a
                                            @[simp]
                                            theorem ULower.up_down {α : Type u_1} [Encodable α] {a : α} :
                                            (ULower.down a).up = a
                                            @[simp]
                                            theorem ULower.up_eq_up {α : Type u_1} [Encodable α] {a : ULower α} {b : ULower α} :
                                            a.up = b.up a = b
                                            @[simp]
                                            theorem ULower.down_eq_down {α : Type u_1} [Encodable α] {a : α} {b : α} :
                                            theorem ULower.ext {α : Type u_1} [Encodable α] {a : ULower α} {b : ULower α} :
                                            a.up = b.upa = b
                                            def Encodable.chooseX {α : Type u_1} {p : αProp} [Encodable α] [DecidablePred p] (h : ∃ (x : α), p x) :
                                            { a : α // p a }

                                            Constructive choice function for a decidable subtype of an encodable type.

                                            Equations
                                            Instances For
                                              def Encodable.choose {α : Type u_1} {p : αProp} [Encodable α] [DecidablePred p] (h : ∃ (x : α), p x) :
                                              α

                                              Constructive choice function for a decidable predicate over an encodable type.

                                              Equations
                                              Instances For
                                                theorem Encodable.choose_spec {α : Type u_1} {p : αProp} [Encodable α] [DecidablePred p] (h : ∃ (x : α), p x) :
                                                theorem Encodable.axiom_of_choice {α : Type u_1} {β : αType u_2} {R : (x : α) → β xProp} [(a : α) → Encodable (β a)] [(x : α) → (y : β x) → Decidable (R x y)] (H : ∀ (x : α), ∃ (y : β x), R x y) :
                                                ∃ (f : (a : α) → β a), ∀ (x : α), R x (f x)

                                                A constructive version of Classical.axiom_of_choice for Encodable types.

                                                theorem Encodable.skolem {α : Type u_1} {β : αType u_2} {P : (x : α) → β xProp} [(a : α) → Encodable (β a)] [(x : α) → (y : β x) → Decidable (P x y)] :
                                                (∀ (x : α), ∃ (y : β x), P x y) ∃ (f : (a : α) → β a), ∀ (x : α), P x (f x)

                                                A constructive version of Classical.skolem for Encodable types.

                                                def Encodable.encode' (α : Type u_1) [Encodable α] :
                                                α

                                                The encode function, viewed as an embedding.

                                                Equations
                                                Instances For
                                                  Equations
                                                  • =
                                                  instance Encodable.instIsTotalPreimageNatCoeEmbeddingEncode'Le {α : Type u_1} [Encodable α] :
                                                  IsTotal α ((Encodable.encode' α) ⁻¹'o fun (x x_1 : ) => x x_1)
                                                  Equations
                                                  • =
                                                  noncomputable def Directed.sequence {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] {r : ββProp} (f : αβ) (hf : Directed r f) :
                                                  α

                                                  Given a Directed r function f : α → β defined on an encodable inhabited type, construct a noncomputable sequence such that r (f (x n)) (f (x (n + 1))) and r (f a) (f (x (encode a + 1)).

                                                  Equations
                                                  Instances For
                                                    theorem Directed.sequence_mono_nat {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] {r : ββProp} {f : αβ} (hf : Directed r f) (n : ) :
                                                    r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))
                                                    theorem Directed.rel_sequence {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] {r : ββProp} {f : αβ} (hf : Directed r f) (a : α) :
                                                    r (f a) (f (Directed.sequence f hf (Encodable.encode a + 1)))
                                                    theorem Directed.sequence_mono {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] [Preorder β] {f : αβ} (hf : Directed (fun (x x_1 : β) => x x_1) f) :
                                                    theorem Directed.le_sequence {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] [Preorder β] {f : αβ} (hf : Directed (fun (x x_1 : β) => x x_1) f) (a : α) :
                                                    theorem Directed.sequence_anti {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] [Preorder β] {f : αβ} (hf : Directed (fun (x x_1 : β) => x x_1) f) :
                                                    theorem Directed.sequence_le {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] [Preorder β] {f : αβ} (hf : Directed (fun (x x_1 : β) => x x_1) f) (a : α) :
                                                    def Quotient.rep {α : Type u_1} {s : Setoid α} [DecidableRel fun (x x_1 : α) => x x_1] [Encodable α] (q : Quotient s) :
                                                    α

                                                    Representative of an equivalence class. This is a computable version of Quot.out for a setoid on an encodable type.

                                                    Equations
                                                    Instances For
                                                      theorem Quotient.rep_spec {α : Type u_1} {s : Setoid α} [DecidableRel fun (x x_1 : α) => x x_1] [Encodable α] (q : Quotient s) :
                                                      q.rep = q
                                                      def encodableQuotient {α : Type u_1} {s : Setoid α} [DecidableRel fun (x x_1 : α) => x x_1] [Encodable α] :

                                                      The quotient of an encodable space by a decidable equivalence relation is encodable.

                                                      Equations
                                                      Instances For