Documentation

Mathlib.Data.W.Basic

W types #

Given α : Type and β : α → Type, the W type determined by this data, WType β, is the inductively defined type of trees where the nodes are labeled by elements of α and the children of a node labeled a are indexed by elements of β a.

This file is currently a stub, awaiting a full development of the theory. Currently, the main result is that if α is an encodable fintype and β a is encodable for every a : α, then WType β is encodable. This can be used to show the encodability of other inductive types, such as those that are commonly used to formalize syntax, e.g. terms and expressions in a given language. The strategy is illustrated in the example found in the file prop_encodable in the archive/examples folder of mathlib.

Implementation details #

While the name WType is somewhat verbose, it is preferable to putting a single character identifier W in the root namespace.

inductive WType {α : Type u_1} (β : αType u_2) :
Type (max u_1 u_2)

Given β : α → Type*, WType β is the type of finitely branching trees where nodes are labeled by elements of α and the children of a node labeled a are indexed by elements of β a.

  • mk: {α : Type u_1} → {β : αType u_2} → (a : α) → (β aWType β)WType β
Instances For
    Equations
    def WType.toSigma {α : Type u_1} {β : αType u_2} :
    WType β(a : α) × (β aWType β)

    The canonical map to the corresponding sigma type, returning the label of a node as an element a of α, and the children of the node as a function β a → WType β.

    Equations
    Instances For
      def WType.ofSigma {α : Type u_1} {β : αType u_2} :
      (a : α) × (β aWType β)WType β

      The canonical map from the sigma type into a WType. Given a node a : α, and its children as a function β a → WType β, return the corresponding tree.

      Equations
      Instances For
        @[simp]
        theorem WType.ofSigma_toSigma {α : Type u_1} {β : αType u_2} (w : WType β) :
        WType.ofSigma w.toSigma = w
        @[simp]
        theorem WType.toSigma_ofSigma {α : Type u_1} {β : αType u_2} (s : (a : α) × (β aWType β)) :
        (WType.ofSigma s).toSigma = s
        @[simp]
        theorem WType.equivSigma_symm_apply {α : Type u_1} (β : αType u_2) :
        ∀ (a : (a : α) × (β aWType β)), (WType.equivSigma β).symm a = WType.ofSigma a
        @[simp]
        theorem WType.equivSigma_apply {α : Type u_1} (β : αType u_2) :
        ∀ (a : WType β), (WType.equivSigma β) a = a.toSigma
        def WType.equivSigma {α : Type u_1} (β : αType u_2) :
        WType β (a : α) × (β aWType β)

        The canonical bijection with the sigma type, showing that WType is a fixed point of the polynomial functor X ↦ Σ a : α, β a → X.

        Equations
        • WType.equivSigma β = { toFun := WType.toSigma, invFun := WType.ofSigma, left_inv := , right_inv := }
        Instances For
          def WType.elim {α : Type u_1} {β : αType u_2} (γ : Type u_3) (fγ : (a : α) × (β aγ)γ) :
          WType βγ

          The canonical map from WType β into any type γ given a map (Σ a : α, β a → γ) → γ.

          Equations
          Instances For
            theorem WType.elim_injective {α : Type u_1} {β : αType u_2} (γ : Type u_3) (fγ : (a : α) × (β aγ)γ) (fγ_injective : Function.Injective ) :
            instance WType.instIsEmpty {α : Type u_1} {β : αType u_2} [hα : IsEmpty α] :
            Equations
            • =
            theorem WType.infinite_of_nonempty_of_isEmpty {α : Type u_1} {β : αType u_2} (a : α) (b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] :
            def WType.depth {α : Type u_1} {β : αType u_2} [(a : α) → Fintype (β a)] :
            WType β

            The depth of a finitely branching tree.

            Equations
            • (WType.mk a f).depth = (Finset.univ.sup fun (n : β a) => (f n).depth) + 1
            Instances For
              theorem WType.depth_pos {α : Type u_1} {β : αType u_2} [(a : α) → Fintype (β a)] (t : WType β) :
              0 < t.depth
              theorem WType.depth_lt_depth_mk {α : Type u_1} {β : αType u_2} [(a : α) → Fintype (β a)] (a : α) (f : β aWType β) (i : β a) :
              (f i).depth < (WType.mk a f).depth
              instance WType.instEncodable {α : Type u_1} {β : αType u_2} [(a : α) → Fintype (β a)] [(a : α) → Encodable (β a)] [Encodable α] :

              WType is encodable when α is an encodable fintype and for every a : α, β a is encodable.

              Equations