W types

Given α : Type and β : α → Type→ 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.

ink

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

• mk: {α : Type u_1} → {β : α → Type u_2} → (a : α) → (β a → WType β) → WType β

Given β : α → Type _→ 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.

ink

instance instInhabitedWTypeUnitEmpty : Inhabited (WType fun x => Empty)

Equations

• instInhabitedWTypeUnitEmpty = { default := WType.mk () Empty.elim }

ink

def WType.toSigma {α : Type u_1} {β : α → Type u_2} : WType β → (a : α) × (β a → WType β)

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 β→ WType β.

Equations

• WType.toSigma x = match x with | WType.mk a f => { fst := a, snd := f }

ink

def WType.ofSigma {α : Type u_1} {β : α → Type u_2} : (a : α) × (β a → WType β) → WType β

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

Equations

• WType.ofSigma x = match x with | { fst := a, snd := f } => WType.mk a f

ink

@[simp]

theorem WType.ofSigma_toSigma {α : Type u_1} {β : α → Type u_2} (w : WType β) : WType.ofSigma (WType.toSigma w) = w

ink

@[simp]

theorem WType.toSigma_ofSigma {α : Type u_1} {β : α → Type u_2} (s : (a : α) × (β a → WType β)) : WType.toSigma (WType.ofSigma s) = s

ink

@[simp]

theorem WType.equivSigma_symm_apply {α : Type u_1} (β : α → Type u_2) : ∀ (a : (a : α) × (β a → WType fun a => β a)), ↑(Equiv.symm (WType.equivSigma β)) a = WType.ofSigma a

ink

@[simp]

theorem WType.equivSigma_apply {α : Type u_1} (β : α → Type u_2) : ∀ (a : WType β), ↑(WType.equivSigma β) a = WType.toSigma a

ink

def WType.equivSigma {α : Type u_1} (β : α → Type u_2) : WType β ≃ (a : α) × (β a → WType β)

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

Equations

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

ink

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

• WType.elim γ fγ (WType.mk a f) = fγ { fst := a, snd := fun b => WType.elim γ fγ (f b) }

ink

theorem WType.elim_injective {α : Type u_2} {β : α → Type u_3} (γ : Type u_1) (fγ : (a : α) × (β a → γ) → γ) (fγ_injective : Function.Injective fγ) : Function.Injective (WType.elim γ fγ)

ink

instance WType.instIsEmptyWType {α : Type u_1} {β : α → Type u_2} [hα : IsEmpty α] : IsEmpty (WType β)

Equations

• @WType.instIsEmptyWType = @WType.instIsEmptyWType.proof_1

ink

theorem WType.infinite_of_nonempty_of_isEmpty {α : Type u_2} {β : α → Type u_1} (a : α) (b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] : Infinite (WType β)

ink

def WType.depth {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Fintype (β a)] : WType β → ℕ

The depth of a finitely branching tree.

Equations

• WType.depth (WType.mk a f) = (Finset.sup Finset.univ fun n => WType.depth (f n)) + 1

ink

theorem WType.depth_pos {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Fintype (β a)] (t : WType β) : 0 < WType.depth t

ink

theorem WType.depth_lt_depth_mk {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Fintype (β a)] (a : α) (f : β a → WType β) (i : β a) : WType.depth (f i) < WType.depth (WType.mk a f)

ink

instance WType.instEncodableWType {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → Fintype (β a)] [inst : (a : α) → Encodable (β a)] [inst : Encodable α] : Encodable (WType β)

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

Equations

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