data.W

# W types

Given α : Type and β : α → Type, the W type determined by this data, W β, 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 β 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.

inductive W {α : Type u_1} :
(α → Type u_2)Type (max u_1 u_2)
• mk : Π {α : Type u_1} (β : α → Type u_2) (a : α), (β aW β)W β

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

@[instance]
def W.inhabited  :
inhabited (W (λ (_x : unit), empty))

Equations
def W.depth {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] :
W β

The depth of a finitely branching tree.

Equations
theorem W.depth_pos {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] (t : W β) :
0 < t.depth

theorem W.depth_lt_depth_mk {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] (a : α) (f : β aW β) (i : β a) :
(f i).depth < (W.mk a f).depth

@[instance]
def encodable.encodable {α : Type u_1} {β : α → Type u_2} [Π (a : α), fintype (β a)] [Π (a : α), encodable (β a)] [encodable α] :

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

Equations