mathlib documentation

data.pfunctor.multivariate.W

The W construction as a multivariate polynomial functor.

W types are well-founded tree-like structures. They are defined as the least fixpoint of a polynomial functor.

Main definitions

Implementation notes

Three views of M-types:

Specifically, we define the polynomial functor Wp as:

As a result Wp.obj α is made of a dataless tree and a function from its valid paths to values of α

Reference

inductive mvpfunctor.W_path {n : } (P : mvpfunctor (n + 1)) :
P.last.Wfin2 nType u

A path from the root of a tree to one of its node

@[instance]
def mvpfunctor.W_path.inhabited {n : } (P : mvpfunctor (n + 1)) (x : P.last.W) {i : fin2 n} [I : inhabited (P.drop.B x.head i)] :

Equations
def mvpfunctor.W_path_cases_on {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} :
P.drop.B a α(Π (j : P.last.B a), P.W_path (f j) α)P.W_path (W.mk a f) α

Specialized destructor on W_path

Equations
def mvpfunctor.W_path_dest_left {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} :
P.W_path (W.mk a f) αP.drop.B a α

Specialized destructor on W_path

Equations
def mvpfunctor.W_path_dest_right {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (h : P.W_path (W.mk a f) α) (j : P.last.B a) :
P.W_path (f j) α

Specialized destructor on W_path

Equations
theorem mvpfunctor.W_path_dest_left_W_path_cases_on {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a α) (g : Π (j : P.last.B a), P.W_path (f j) α) :

theorem mvpfunctor.W_path_dest_right_W_path_cases_on {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a α) (g : Π (j : P.last.B a), P.W_path (f j) α) :

theorem mvpfunctor.W_path_cases_on_eta {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (h : P.W_path (W.mk a f) α) :

theorem mvpfunctor.comp_W_path_cases_on {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : typevec n} (h : α β) {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a α) (g : Π (j : P.last.B a), P.W_path (f j) α) :
h P.W_path_cases_on g' g = P.W_path_cases_on (h g') (λ (i : P.last.B a), h g i)

def mvpfunctor.Wp {n : } :
mvpfunctor (n + 1)mvpfunctor n

Polynomial functor for the W-type of P. A is a data-less well-founded tree whereas, for a given a : A, B a is a valid path in tree a so that Wp.obj α is made of a tree and a function from its valid paths to the values it contains

Equations
@[nolint]
def mvpfunctor.W {n : } :
mvpfunctor (n + 1)typevec nType u

W-type of P

Equations
@[instance]
def mvpfunctor.mvfunctor_W {n : } (P : mvpfunctor (n + 1)) :

Equations

First, describe operations on W as a polynomial functor.

def mvpfunctor.Wp_mk {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f : P.last.B a → P.last.W) :
P.W_path (W.mk a f) αP.W α

Constructor for Wp

Equations
def mvpfunctor.Wp_rec {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_2} (g : Π (a : P.A) (f : P.last.B a → P.last.W), P.W_path (W.mk a f) α(P.last.B a → C) → C) (x : P.last.W) :
P.W_path x α → C

Recursor for Wp

Equations
theorem mvpfunctor.Wp_rec_eq {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_2} (g : Π (a : P.A) (f : P.last.B a → P.last.W), P.W_path (W.mk a f) α(P.last.B a → C) → C) (a : P.A) (f : P.last.B a → P.last.W) (f' : P.W_path (W.mk a f) α) :
P.Wp_rec g (W.mk a f) f' = g a f f' (λ (i : P.last.B a), P.Wp_rec g (f i) (P.W_path_dest_right f' i))

theorem mvpfunctor.Wp_ind {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : Π (x : P.last.W), P.W_path x α → Prop} (ih : ∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : P.W_path (W.mk a f) α), (∀ (i : P.last.B a), C (f i) (P.W_path_dest_right f' i))C (W.mk a f) f') (x : P.last.W) (f' : P.W_path x α) :
C x f'

Now think of W as defined inductively by the data ⟨a, f', f⟩ where

def mvpfunctor.W_mk {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) :
P.drop.B a α(P.last.B aP.W α)P.W α

Constructor for W

Equations
def mvpfunctor.W_rec {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_1} :
(Π (a : P.A), P.drop.B a α(P.last.B aP.W α)(P.last.B a → C) → C)P.W α → C

Recursor for W

Equations
theorem mvpfunctor.W_rec_eq {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_1} (g : Π (a : P.A), P.drop.B a α(P.last.B aP.W α)(P.last.B a → C) → C) (a : P.A) (f' : P.drop.B a α) (f : P.last.B aP.W α) :
P.W_rec g (P.W_mk a f' f) = g a f' f (λ (i : P.last.B a), P.W_rec g (f i))

Defining equation for the recursor of W

theorem mvpfunctor.W_ind {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : P.W α → Prop} (ih : ∀ (a : P.A) (f' : P.drop.B a α) (f : P.last.B aP.W α), (∀ (i : P.last.B a), C (f i))C (P.W_mk a f' f)) (x : P.W α) :
C x

Induction principle for W

theorem mvpfunctor.W_cases {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : P.W α → Prop} (ih : ∀ (a : P.A) (f' : P.drop.B a α) (f : P.last.B aP.W α), C (P.W_mk a f' f)) (x : P.W α) :
C x

def mvpfunctor.W_map {n : } (P : mvpfunctor (n + 1)) {α β : typevec n} :
α βP.W αP.W β

W-types are functorial

Equations
theorem mvpfunctor.W_mk_eq {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f : P.last.B a → P.last.W) (g' : P.drop.B a α) (g : Π (j : P.last.B a), P.W_path (f j) α) :
P.W_mk a g' (λ (i : P.last.B a), f i, g i⟩) = W.mk a f, P.W_path_cases_on g' g

theorem mvpfunctor.W_map_W_mk {n : } (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α β) (a : P.A) (f' : P.drop.B a α) (f : P.last.B aP.W α) :
g <$$> P.W_mk a f' f = P.W_mk a (g f') (λ (i : P.last.B a), g <$$> f i)

def mvpfunctor.obj_append1 {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (a : P.A) :
P.drop.B a α(P.last.B a → β)P.obj ::: β)

Constructor of a value of P.obj (α ::: β) from components. Useful to avoid complicated type annotation

Equations
theorem mvpfunctor.map_obj_append1 {n : } (P : mvpfunctor (n + 1)) {α γ : typevec n} (g : α γ) (a : P.A) (f' : P.drop.B a α) (f : P.last.B aP.W α) :
(g ::: P.W_map g) <$$> P.obj_append1 a f' f = P.obj_append1 a (g f') (λ (x : P.last.B a), P.W_map g (f x))

Yet another view of the W type: as a fixed point for a multivariate polynomial functor. These are needed to use the W-construction to construct a fixed point of a qpf, since the qpf axioms are expressed in terms of map on P.

def mvpfunctor.W_mk' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} :
P.obj ::: P.W α)P.W α

Constructor for the W-type of P

Equations
def mvpfunctor.W_dest' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} :
P.W αP.obj ::: P.W α)

Destructor for the W-type of P

Equations
theorem mvpfunctor.W_dest'_W_mk {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f' : P.drop.B a α) (f : P.last.B aP.W α) :
P.W_dest' (P.W_mk a f' f) = a, typevec.split_fun f' f

theorem mvpfunctor.W_dest'_W_mk' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (x : P.obj ::: P.W α)) :
P.W_dest' (P.W_mk' x) = x