mathlib3 documentation

data.W.basic

W types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given α : Type and β : α → Type, the W type determined by this data, W_type β, 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 W_type β 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 W_type is somewhat verbose, it is preferable to putting a single character identifier W in the root namespace.

source
inductive W_type {α : Type u_1} (β : α → Type u_2) :
Type (max u_1 u_2)

Given β : α → Type*, W_type β 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.

Instances for W_type
source
@[protected, instance]
def W_type.inhabited  :
inhabited (W_type (λ (_x : unit), empty))
Equations
source
def W_type.to_sigma {α : Type u_1} {β : α → Type u_2} :
W_type β → (Σ (a : α), β a → W_type β)

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

Equations
source
def W_type.of_sigma {α : Type u_1} {β : α → Type u_2} :
(Σ (a : α), β a → W_type β) → W_type β

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

Equations
source
@[simp]
theorem W_type.of_sigma_to_sigma {α : Type u_1} {β : α → Type u_2} (w : W_type β) :
W_type.of_sigma w.to_sigma = w
source
@[simp]
theorem W_type.to_sigma_of_sigma {α : Type u_1} {β : α → Type u_2} (s : Σ (a : α), β a → W_type β) :
(W_type.of_sigma s).to_sigma = s
source
def W_type.equiv_sigma {α : Type u_1} (β : α → Type u_2) :
W_type β ≃ Σ (a : α), β a → W_type β

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

Equations
source
@[simp]
theorem W_type.equiv_sigma_apply {α : Type u_1} (β : α → Type u_2) (ᾰ : W_type β) :
⇑(W_type.equiv_sigma β) ᾰ = ᾰ.to_sigma
source
@[simp]
theorem W_type.equiv_sigma_symm_apply {α : Type u_1} (β : α → Type u_2) (ᾰ : Σ (a : α), (λ (a : α), β a) a → W_type (λ (a : α), β a)) :
⇑((W_type.equiv_sigma β).symm) ᾰ = W_type.of_sigma ᾰ
source
def W_type.elim {α : Type u_1} {β : α → Type u_2} (γ : Type u_3) (fγ : (Σ (a : α), β a → γ) → γ) :
W_type β → γ

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

Equations
source
theorem W_type.elim_injective {α : Type u_1} {β : α → Type u_2} (γ : Type u_3) (fγ : (Σ (a : α), β a → γ) → γ) (fγ_injective : function.injective fγ) :
function.injective (W_type.elim γ fγ)
source
@[protected, instance]
def W_type.is_empty {α : Type u_1} {β : α → Type u_2} [hα : is_empty α] :
is_empty (W_type β)
source
theorem W_type.infinite_of_nonempty_of_is_empty {α : Type u_1} {β : α → Type u_2} (a b : α) [ha : nonempty (β a)] [he : is_empty (β b)] :
infinite (W_type β)
source
def W_type.depth {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] :
W_type β → ℕ

The depth of a finitely branching tree.

Equations
source
theorem W_type.depth_pos {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] (t : W_type β) :
0 < t.depth
source
theorem W_type.depth_lt_depth_mk {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] (a : α) (f : β a → W_type β) (i : β a) :
(f i).depth < (W_type.mk a f).depth
source
@[protected, instance]
def W_type.encodable {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] [Π (a : α), encodable (β a)] [encodable α] :
encodable (W_type β)

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

Equations