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 α 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.{u} (n + 1)) : PFunctor.W (MvPFunctor.last P) → Fin2 n → Type u

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

• root: {n : ℕ} → {P : MvPFunctor.{u} (n + 1)} → (a : P.A) → (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) → (i : Fin2 n) → (MvPFunctor.drop P).B a i → MvPFunctor.WPath P (WType.mk a f) i
• child: {n : ℕ} → {P : MvPFunctor.{u} (n + 1)} → (a : P.A) → (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) → (i : Fin2 n) → (j : (MvPFunctor.last P).B a) → MvPFunctor.WPath P (f j) i → MvPFunctor.WPath P (WType.mk a f) i

instance MvPFunctor.WPath.inhabited {n : ℕ} (P : MvPFunctor.{u} (n + 1)) (x : PFunctor.W (MvPFunctor.last P)) {i : Fin2 n} [I : Inhabited ((MvPFunctor.drop P).B (PFunctor.W.head x) i)] : Inhabited (MvPFunctor.WPath P x i)

Equations

• MvPFunctor.WPath.inhabited P x = { default := match x, I with | WType.mk a f, I => MvPFunctor.WPath.root a f i default }

def MvPFunctor.wPathCasesOn {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (g' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (g : (j : (MvPFunctor.last P).B a) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α

Specialized destructor on WPath

Equations

• MvPFunctor.wPathCasesOn P g' g i x = match i, x with | i, MvPFunctor.WPath.root .(a) .(f) .(i) c => g' i c | i, MvPFunctor.WPath.child .(a) .(f) .(i) j c => g j i c

def MvPFunctor.wPathDestLeft {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (h : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) : TypeVec.Arrow ((MvPFunctor.drop P).B a) α

Specialized destructor on WPath

Equations

• MvPFunctor.wPathDestLeft P h i c = h i (MvPFunctor.WPath.root a f i c)

def MvPFunctor.wPathDestRight {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (h : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) (j : (MvPFunctor.last P).B a) : TypeVec.Arrow (MvPFunctor.WPath P (f j)) α

Specialized destructor on WPath

Equations

• MvPFunctor.wPathDestRight P h j i c = h i (MvPFunctor.WPath.child a f i j c)

theorem MvPFunctor.wPathDestLeft_wPathCasesOn {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (g' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (g : (j : (MvPFunctor.last P).B a) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) : MvPFunctor.wPathDestLeft P (MvPFunctor.wPathCasesOn P g' g) = g'

theorem MvPFunctor.wPathDestRight_wPathCasesOn {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (g' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (g : (j : (MvPFunctor.last P).B a) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) : MvPFunctor.wPathDestRight P (MvPFunctor.wPathCasesOn P g' g) = g

theorem MvPFunctor.wPathCasesOn_eta {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (h : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) : MvPFunctor.wPathCasesOn P (MvPFunctor.wPathDestLeft P h) (MvPFunctor.wPathDestRight P h) = h

theorem MvPFunctor.comp_wPathCasesOn {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (h : TypeVec.Arrow α β) {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)} (g' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (g : (j : (MvPFunctor.last P).B a) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) : TypeVec.comp h (MvPFunctor.wPathCasesOn P g' g) = MvPFunctor.wPathCasesOn P (TypeVec.comp h g') fun (i : (MvPFunctor.last P).B a) => TypeVec.comp h (g i)

def MvPFunctor.wp {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : MvPFunctor.{u} 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

• MvPFunctor.wp P = { A := PFunctor.W (MvPFunctor.last P), B := MvPFunctor.WPath P }

def MvPFunctor.W {n : ℕ} (P : MvPFunctor.{u} (n + 1)) (α : TypeVec.{u} n) : Type u

W-type of P

Equations

• MvPFunctor.W P α = ↑(MvPFunctor.wp P) α

instance MvPFunctor.mvfunctorW {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : MvFunctor (MvPFunctor.W P)

Equations

• MvPFunctor.mvfunctorW P = id inferInstance

First, describe operations on W as a polynomial functor.

def MvPFunctor.wpMk {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) : MvPFunctor.W P α

Constructor for wp

Equations

• MvPFunctor.wpMk P a f f' = { fst := WType.mk a f, snd := f' }

def MvPFunctor.wpRec {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_2} n} {C : Type u_1} (g : (a : P.A) → (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) → TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α → ((MvPFunctor.last P).B a → C) → C) (x : PFunctor.W (MvPFunctor.last P)) : TypeVec.Arrow (MvPFunctor.WPath P x) α → C

Equations

• MvPFunctor.wpRec P g (WType.mk a f) f' = g a f f' fun (i : (MvPFunctor.last P).B a) => MvPFunctor.wpRec P g (f i) (MvPFunctor.wPathDestRight P f' i)

theorem MvPFunctor.wpRec_eq {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_2} n} {C : Type u_1} (g : (a : P.A) → (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) → TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α → ((MvPFunctor.last P).B a → C) → C) (a : P.A) (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) (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.last P).B a) => MvPFunctor.wpRec P g (f i) (MvPFunctor.wPathDestRight P f' i)

theorem MvPFunctor.wp_ind {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {C : (x : PFunctor.W (MvPFunctor.last P)) → TypeVec.Arrow (MvPFunctor.WPath P x) α → Prop} (ih : ∀ (a : P.A) (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α), (∀ (i : (MvPFunctor.last P).B a), C (f i) (MvPFunctor.wPathDestRight P f' i)) → C (WType.mk a f) f') (x : PFunctor.W (MvPFunctor.last P)) (f' : TypeVec.Arrow (MvPFunctor.WPath P x) α) : 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.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α) : MvPFunctor.W P α

Constructor for W

Equations

• One or more equations did not get rendered due to their size.

def MvPFunctor.wRec {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : Type u_1} (g : (a : P.A) → TypeVec.Arrow ((MvPFunctor.drop P).B a) α → ((MvPFunctor.last P).B a → MvPFunctor.W P α) → ((MvPFunctor.last P).B a → C) → C) : MvPFunctor.W P α → C

Recursor for W

Equations

• One or more equations did not get rendered due to their size.

theorem MvPFunctor.wRec_eq {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : Type u_1} (g : (a : P.A) → TypeVec.Arrow ((MvPFunctor.drop P).B a) α → ((MvPFunctor.last P).B a → MvPFunctor.W P α) → ((MvPFunctor.last P).B a → C) → C) (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α) : MvPFunctor.wRec P g (MvPFunctor.wMk P a f' f) = g a f' f fun (i : (MvPFunctor.last P).B a) => MvPFunctor.wRec P g (f i)

Defining equation for the recursor of W

theorem MvPFunctor.w_ind {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : MvPFunctor.W P α → Prop} (ih : ∀ (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α), (∀ (i : (MvPFunctor.last P).B a), C (f i)) → C (MvPFunctor.wMk P a f' f)) (x : MvPFunctor.W P α) : C x

Induction principle for W

theorem MvPFunctor.w_cases {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : MvPFunctor.W P α → Prop} (ih : ∀ (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α), C (MvPFunctor.wMk P a f' f)) (x : MvPFunctor.W P α) : C x

def MvPFunctor.wMap {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) : MvPFunctor.W P α → MvPFunctor.W P β

W-types are functorial

Equations

• MvPFunctor.wMap P g x = MvFunctor.map g x

theorem MvPFunctor.wMk_eq {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f : (MvPFunctor.last P).B a → PFunctor.W (MvPFunctor.last P)) (g' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (g : (j : (MvPFunctor.last P).B a) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) : (MvPFunctor.wMk P a g' fun (i : (MvPFunctor.last P).B a) => { fst := f i, snd := g i }) = { fst := WType.mk a f, snd := MvPFunctor.wPathCasesOn P g' g }

theorem MvPFunctor.w_map_wMk {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α) : MvFunctor.map g (MvPFunctor.wMk P a f' f) = MvPFunctor.wMk P a (TypeVec.comp g f') fun (i : (MvPFunctor.last P).B a) => MvFunctor.map g (f i)

@[reducible]

def MvPFunctor.objAppend1 {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → β) : ↑P (α ::: β)

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

Equations

• MvPFunctor.objAppend1 P a f' f = { fst := a, snd := TypeVec.splitFun f' f }

theorem MvPFunctor.map_objAppend1 {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {γ : TypeVec.{u} n} (g : TypeVec.Arrow α γ) (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α) : MvFunctor.map (g ::: MvPFunctor.wMap P g) (MvPFunctor.objAppend1 P a f' f) = MvPFunctor.objAppend1 P a (TypeVec.comp g f') fun (x : (MvPFunctor.last P).B a) => MvPFunctor.wMap P 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.wMk' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} : ↑P (α ::: MvPFunctor.W P α) → MvPFunctor.W P α

Constructor for the W-type of P

Equations

• MvPFunctor.wMk' P x = match x with | { fst := a, snd := f } => MvPFunctor.wMk P a (TypeVec.dropFun f) (TypeVec.lastFun f)

def MvPFunctor.wDest' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} : MvPFunctor.W P α → ↑P (α ::: MvPFunctor.W P α)

Destructor for the W-type of P

Equations

• One or more equations did not get rendered due to their size.

theorem MvPFunctor.wDest'_wMk {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f' : TypeVec.Arrow ((MvPFunctor.drop P).B a) α) (f : (MvPFunctor.last P).B a → MvPFunctor.W P α) : MvPFunctor.wDest' P (MvPFunctor.wMk P a f' f) = { fst := a, snd := TypeVec.splitFun f' f }

theorem MvPFunctor.wDest'_wMk' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (x : ↑P (α ::: MvPFunctor.W P α)) : MvPFunctor.wDest' P (MvPFunctor.wMk' P x) = x