doc-next-gen

Mathlib.Data.W.Basic

Module docstring

{"# 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. "}

WType inductive
{α : Type*} (β : α → Type*)
Full source 
/--
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`.
-/
inductive WType {α : Type*} (β : α → Type*)
  | mk (a : α) (f : β a → WType β) : WType β
W-type (well-founded tree type)
Informal description
Given a type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}$, the W-type $\text{WType} \beta$ is the inductively defined type of finitely branching trees where each node is labeled by an element $a \in \alpha$ and the children of a node labeled $a$ are indexed by elements of $\beta a$.
instInhabitedWTypeUnitEmpty instance
: Inhabited (WType fun _ : Unit => Empty)
Full source 
instance : Inhabited (WType fun _ : Unit => Empty) :=
  ⟨WType.mk Unit.unit Empty.elim⟩
Inhabited W-type with Unit Labels and No Children
Informal description
The W-type $\text{WType} (\lambda \_ : \text{Unit} \Rightarrow \text{Empty})$ is inhabited, meaning there exists at least one element in this type of well-founded trees where nodes are labeled by the unit type and have no children (since $\text{Empty}$ has no elements).
WType.toSigma definition
: WType β → Σ a : α, β a → WType β
Full source 
/-- 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 β`. -/
def toSigma : WType β → Σa : α, β a → WType β
  | ⟨a, f⟩ => ⟨a, f⟩
Decomposition of a W-type tree into root label and children
Informal description
The function maps a well-founded tree $w$ of type $\text{WType} \beta$ to a pair $(a, f)$ where $a$ is the label of the root node of $w$ and $f$ is a function that maps each element of $\beta a$ to the corresponding child tree of $w$.
WType.ofSigma definition
: (Σ a : α, β a → WType β) → WType β
Full source 
/-- 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. -/
def ofSigma : (Σa : α, β a → WType β) → WType β
  | ⟨a, f⟩ => WType.mk a f
Construction of W-type tree from root label and children
Informal description
Given a pair $(a, f)$ where $a$ is an element of $\alpha$ and $f$ is a function from $\beta a$ to $\text{WType} \beta$, the function constructs a well-founded tree in $\text{WType} \beta$ with root labeled by $a$ and children given by $f$.
WType.ofSigma_toSigma theorem
: ∀ w : WType β, ofSigma (toSigma w) = w
Full source 
@[simp]
theorem ofSigma_toSigma : ∀ w : WType β, ofSigma (toSigma w) = w
  | ⟨_, _⟩ => rfl
Identity Property of W-type Tree Decomposition and Reconstruction
Informal description
For any well-founded tree $w$ of type $\text{WType} \beta$, the construction of a tree from its decomposition (root label and children) via `ofSigma` applied to `toSigma w` yields the original tree $w$. In other words, the composition `ofSigma ∘ toSigma` is the identity function on $\text{WType} \beta$.
WType.toSigma_ofSigma theorem
: ∀ s : Σ a : α, β a → WType β, toSigma (ofSigma s) = s
Full source 
@[simp]
theorem toSigma_ofSigma : ∀ s : Σa : α, β a → WType β, toSigma (ofSigma s) = s
  | ⟨_, _⟩ => rfl
Identity Property of W-type Tree Construction and Decomposition
Informal description
For any pair $(a, f)$ where $a$ is an element of $\alpha$ and $f$ is a function from $\beta a$ to $\text{WType} \beta$, the decomposition of the constructed tree $\text{ofSigma}(a, f)$ via $\text{toSigma}$ yields the original pair $(a, f)$. In other words, the composition $\text{toSigma} \circ \text{ofSigma}$ is the identity function on $\Sigma a : \alpha, \beta a \to \text{WType} \beta$.
WType.equivSigma definition
: WType β ≃ Σ a : α, β a → WType β
Full source 
/-- The canonical bijection with the sigma type, showing that `WType` is a fixed point of
  the polynomial functor `X ↦ Σ a : α, β a → X`. -/
@[simps]
def equivSigma : WTypeWType β ≃ Σa : α, β a → WType β where
  toFun := toSigma
  invFun := ofSigma
  left_inv := ofSigma_toSigma
  right_inv := toSigma_ofSigma
Bijection between W-type and its polynomial functor representation
Informal description
The bijection $\text{WType} \beta \simeq \Sigma a : \alpha, \beta a \to \text{WType} \beta$ shows that $\text{WType} \beta$ is a fixed point of the polynomial functor $X \mapsto \Sigma a : \alpha, \beta a \to X$. The bijection is given by the functions $\text{toSigma}$ (decomposing a tree into its root label and children) and $\text{ofSigma}$ (constructing a tree from a root label and children), which are mutual inverses.
WType.elim definition
(γ : Type*) (fγ : (Σ a : α, β a → γ) → γ) : WType β → γ
Full source 
/-- The canonical map from `WType β` into any type `γ` given a map `(Σ a : α, β a → γ) → γ`. -/
def elim (γ : Type*) (fγ : (Σ a : α, β a → γ) → γ) : WType β → γ
  | ⟨a, f⟩ => fγ ⟨a, fun b => elim γ fγ (f b)⟩
Recursor for W-types
Informal description
Given a type $\gamma$ and a function $f_\gamma : (\Sigma a : \alpha, \beta a \to \gamma) \to \gamma$, the function $\text{WType.elim} \gamma f_\gamma$ maps each well-founded tree in $\text{WType} \beta$ to an element of $\gamma$ by recursively applying $f_\gamma$ to the root label and the results of eliminating the children.
WType.elim_injective theorem
(γ : Type*) (fγ : (Σ a : α, β a → γ) → γ) (fγ_injective : Function.Injective fγ) : Function.Injective (elim γ fγ)
Full source 
theorem elim_injective (γ : Type*) (fγ : (Σ a : α, β a → γ) → γ)
    (fγ_injective : Function.Injective fγ) : Function.Injective (elim γ fγ)
  | ⟨a₁, f₁⟩, ⟨a₂, f₂⟩, h => by
    obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
    congr with x
    exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x :)
Injectivity of W-type Recursor
Informal description
For any type $\gamma$ and function $f_\gamma : (\Sigma a : \alpha, \beta a \to \gamma) \to \gamma$, if $f_\gamma$ is injective, then the recursor $\text{WType.elim} \gamma f_\gamma$ is also injective as a function from $\text{WType} \beta$ to $\gamma$.
WType.infinite_of_nonempty_of_isEmpty theorem
(a b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] : Infinite (WType β)
Full source 
theorem infinite_of_nonempty_of_isEmpty (a b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] :
    Infinite (WType β) :=
  ⟨by
    intro hf
    have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
    refine
      not_injective_infinite_finite
        (fun n : ℕ =>
          show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩)
        ?_
    intro n m h
    induction' n with n ih generalizing m
    · rcases m with - | m <;> simp_all
    · rcases m with - | m
      · simp_all
      · refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]⟩
Infinite W-type from Nonempty and Empty Fibers
Informal description
For any elements $a$ and $b$ of type $\alpha$, if $\beta a$ is nonempty and $\beta b$ is empty, then the W-type $\text{WType} \beta$ is infinite.
WType.depth definition
: WType β → ℕ
Full source 
/-- The depth of a finitely branching tree. -/
def depth : WType β → ℕ
  | ⟨_, f⟩ => (Finset.sup Finset.univ fun n => depth (f n)) + 1
Depth of a W-type tree
Informal description
The depth of a finitely branching tree in the W-type $\text{WType} \beta$ is defined recursively as follows: for a tree $\langle a, f \rangle$ where $a \in \alpha$ and $f : \beta a \to \text{WType} \beta$, the depth is the supremum of the depths of its children (indexed by $\beta a$) plus one.
WType.depth_pos theorem
(t : WType β) : 0 < t.depth
Full source 
theorem depth_pos (t : WType β) : 0 < t.depth := by
  cases t
  apply Nat.succ_pos
Positivity of Depth in W-types
Informal description
For any finitely branching tree $t$ in the W-type $\text{WType} \beta$, the depth of $t$ is strictly positive, i.e., $0 < \text{depth}(t)$.
WType.depth_lt_depth_mk theorem
(a : α) (f : β a → WType β) (i : β a) : depth (f i) < depth ⟨a, f⟩
Full source 
theorem depth_lt_depth_mk (a : α) (f : β a → WType β) (i : β a) : depth (f i) < depth ⟨a, f⟩ :=
  Nat.lt_succ_of_le (Finset.le_sup (f := (depth <| f ·)) (Finset.mem_univ i))
Depth Inequality for W-type Trees: $\text{depth}(f(i)) < \text{depth}(\langle a, f \rangle)$
Informal description
For any element $a \in \alpha$, any function $f : \beta a \to \text{WType} \beta$, and any index $i \in \beta a$, the depth of the child tree $f(i)$ is strictly less than the depth of the parent tree $\langle a, f \rangle$.
WType.instEncodable instance
: Encodable (WType β)
Full source 
/-- `WType` is encodable when `α` is an encodable fintype and for every `a : α`, `β a` is
encodable. -/
instance : Encodable (WType β) := by
  haveI h' : ∀ n, Encodable (WType' β n) := fun n => Nat.rec encodable_zero encodable_succ n
  let f : WType β → Σn, WType' β n := fun t => ⟨t.depth, ⟨t, le_rfl⟩⟩
  let finv : (Σn, WType' β n) → WType β := fun p => p.2.1
  have : ∀ t, finv (f t) = t := fun t => rfl
  exact Encodable.ofLeftInverse f finv this
Encodability of W-types with Encodable Parameters
Informal description
For any encodable finite type $\alpha$ and a family of encodable types $\beta : \alpha \to \text{Type}$, the W-type $\text{WType} \beta$ is also encodable. This means there exists an encoding function $\text{encode} : \text{WType} \beta \to \mathbb{N}$ and a decoding function $\text{decode} : \mathbb{N} \to \text{Option } (\text{WType} \beta)$ that are partial inverses of each other.