# Documentation

Mathlib.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 #

• W_mk - constructor
• W_dest - destructor
• W_rec - recursor: basis for defining functions by structural recursion on P.W α
• W_rec_eq - defining equation for W_rec
• W_ind - induction principle for P.W α

## Implementation notes #

Three views of M-types:

• wp: polynomial functor
• W: data type inductively defined by a triple: shape of the root, data in the root and children of the root
• W: least fixed point of a polynomial functor

Specifically, we define the polynomial functor wp as:

• A := a tree-like structure without information in the nodes
• B := given the tree-like structure t, B t is a valid path (specified inductively by W_path) from the root of t to any given node.

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

## Reference #

• Jeremy Avigad, Mario M. Carneiro and Simon Hudon. [Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
inductive MvPFunctor.WPath {n : } (P : MvPFunctor (n + 1)) :
Fin2 nType u

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

Instances For
instance MvPFunctor.WPath.inhabited {n : } (P : MvPFunctor (n + 1)) (x : ) {i : Fin2 n} [I : Inhabited ()] :
def MvPFunctor.wPathCasesOn {n : } (P : MvPFunctor (n + 1)) {α : } {a : P.A} {f : } (g' : TypeVec.Arrow () α) (g : (j : ) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) :

Specialized destructor on WPath

Instances For
def MvPFunctor.wPathDestLeft {n : } (P : MvPFunctor (n + 1)) {α : } {a : P.A} {f : } (h : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) :

Specialized destructor on WPath

Instances For
def MvPFunctor.wPathDestRight {n : } (P : MvPFunctor (n + 1)) {α : } {a : P.A} {f : } (h : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) (j : ) :

Specialized destructor on WPath

Instances For
theorem MvPFunctor.wPathDestLeft_wPathCasesOn {n : } (P : MvPFunctor (n + 1)) {α : } {a : P.A} {f : } (g' : TypeVec.Arrow () α) (g : (j : ) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) :
= g'
theorem MvPFunctor.wPathDestRight_wPathCasesOn {n : } (P : MvPFunctor (n + 1)) {α : } {a : P.A} {f : } (g' : TypeVec.Arrow () α) (g : (j : ) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) :
= g
theorem MvPFunctor.wPathCasesOn_eta {n : } (P : MvPFunctor (n + 1)) {α : } {a : P.A} {f : } (h : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) :
theorem MvPFunctor.comp_wPathCasesOn {n : } (P : MvPFunctor (n + 1)) {α : } {β : } (h : ) {a : P.A} {f : } (g' : TypeVec.Arrow () α) (g : (j : ) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) :
def MvPFunctor.wp {n : } (P : MvPFunctor (n + 1)) :

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

Instances For
def MvPFunctor.W {n : } (P : MvPFunctor (n + 1)) (α : ) :

W-type of P

Instances For
instance MvPFunctor.mvfunctorW {n : } (P : MvPFunctor (n + 1)) :

First, describe operations on W as a polynomial functor.

def MvPFunctor.wpMk {n : } (P : MvPFunctor (n + 1)) {α : } (a : P.A) (f : ) (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) :

Constructor for wp

Instances For
def MvPFunctor.wpRec {n : } (P : MvPFunctor (n + 1)) {α : } {C : Type u_1} (g : (a : P.A) → (f : ) → TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α(C) → C) (x : ) :
C
Equations
Instances For
theorem MvPFunctor.wpRec_eq {n : } (P : MvPFunctor (n + 1)) {α : } {C : Type u_1} (g : (a : P.A) → (f : ) → TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α(C) → C) (a : P.A) (f : ) (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) :
MvPFunctor.wpRec P g (WType.mk a f) f' = g a f f' fun i => MvPFunctor.wpRec P g (f i) ()
theorem MvPFunctor.wp_ind {n : } (P : MvPFunctor (n + 1)) {α : } {C : (x : ) → Prop} (ih : (a : P.A) → (f : ) → (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) → ((i : ) → C (f i) ()) → C (WType.mk a f) f') (x : ) (f' : ) :
C x f'

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

• a : P.A is the shape of the top node
• f' : P.drop.B a ⟹ α is the contents of the top node
• f : P.last.B a → P.last.W are the subtrees
def MvPFunctor.wMk {n : } (P : MvPFunctor (n + 1)) {α : } (a : P.A) (f' : TypeVec.Arrow () α) (f : ) :

Constructor for W

Instances For
def MvPFunctor.wRec {n : } (P : MvPFunctor (n + 1)) {α : } {C : Type u_1} (g : (a : P.A) → TypeVec.Arrow () α() → (C) → C) :
C

Recursor for W

Instances For
theorem MvPFunctor.wRec_eq {n : } (P : MvPFunctor (n + 1)) {α : } {C : Type u_1} (g : (a : P.A) → TypeVec.Arrow () α() → (C) → C) (a : P.A) (f' : TypeVec.Arrow () α) (f : ) :
MvPFunctor.wRec P g (MvPFunctor.wMk P a f' f) = g a f' f fun i => MvPFunctor.wRec P g (f i)

Defining equation for the recursor of W

theorem MvPFunctor.w_ind {n : } (P : MvPFunctor (n + 1)) {α : } {C : Prop} (ih : (a : P.A) → (f' : TypeVec.Arrow () α) → (f : ) → ((i : ) → C (f i)) → C (MvPFunctor.wMk P a f' f)) (x : ) :
C x

Induction principle for W

theorem MvPFunctor.w_cases {n : } (P : MvPFunctor (n + 1)) {α : } {C : Prop} (ih : (a : P.A) → (f' : TypeVec.Arrow () α) → (f : ) → C (MvPFunctor.wMk P a f' f)) (x : ) :
C x
def MvPFunctor.wMap {n : } (P : MvPFunctor (n + 1)) {α : } {β : } (g : ) :

W-types are functorial

Instances For
theorem MvPFunctor.wMk_eq {n : } (P : MvPFunctor (n + 1)) {α : } (a : P.A) (f : ) (g' : TypeVec.Arrow () α) (g : (j : ) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) :
(MvPFunctor.wMk P a g' fun i => { fst := f i, snd := g i }) = { fst := WType.mk a f, snd := }
theorem MvPFunctor.w_map_wMk {n : } (P : MvPFunctor (n + 1)) {α : } {β : } (g : ) (a : P.A) (f' : TypeVec.Arrow () α) (f : ) :
MvFunctor.map g (MvPFunctor.wMk P a f' f) = MvPFunctor.wMk P a (TypeVec.comp g f') fun i => MvFunctor.map g (f i)
@[reducible]
def MvPFunctor.objAppend1 {n : } (P : MvPFunctor (n + 1)) {α : } {β : Type u} (a : P.A) (f' : TypeVec.Arrow () α) (f : β) :

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

Instances For
theorem MvPFunctor.map_objAppend1 {n : } (P : MvPFunctor (n + 1)) {α : } {γ : } (g : ) (a : P.A) (f' : TypeVec.Arrow () α) (f : ) :

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.wMk' {n : } (P : MvPFunctor (n + 1)) {α : } :
MvPFunctor.Obj P (α ::: )

Constructor for the W-type of P

Instances For
def MvPFunctor.wDest' {n : } (P : MvPFunctor (n + 1)) {α : } :
MvPFunctor.Obj P (α ::: )

Destructor for the W-type of P`

Instances For
theorem MvPFunctor.wDest'_wMk {n : } (P : MvPFunctor (n + 1)) {α : } (a : P.A) (f' : TypeVec.Arrow () α) (f : ) :
MvPFunctor.wDest' P (MvPFunctor.wMk P a f' f) = { fst := a, snd := }
theorem MvPFunctor.wDest'_wMk' {n : } (P : MvPFunctor (n + 1)) {α : } (x : MvPFunctor.Obj P (α ::: )) :
= x