mathlib3 documentation

data.pfunctor.multivariate.W

The W construction as a multivariate polynomial functor. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)) :

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

Instances for mvpfunctor.W_path
@[protected, 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} (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :

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} (h : typevec.arrow (P.W_path (W_type.mk a f)) α) :
(P.drop.B a).arrow α

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 : typevec.arrow (P.W_path (W_type.mk a f)) α) (j : P.last.B a) :
typevec.arrow (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).arrow α) (g : Π (j : P.last.B a), typevec.arrow (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).arrow α) (g : Π (j : P.last.B a), typevec.arrow (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 : typevec.arrow (P.W_path (W_type.mk a f)) α) :
theorem mvpfunctor.comp_W_path_cases_on {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : typevec n} (h : α.arrow β) {a : P.A} {f : P.last.B a P.last.W} (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :
typevec.comp h (P.W_path_cases_on g' g) = P.W_path_cases_on (typevec.comp h g') (λ (i : P.last.B a), typevec.comp h (g i))
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

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

W-type of P

Equations
Instances for mvpfunctor.W
@[protected, 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) (f' : typevec.arrow (P.W_path (W_type.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), typevec.arrow (P.W_path (W_type.mk a f)) α (P.last.B a C) C) (x : P.last.W) (f' : typevec.arrow (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), typevec.arrow (P.W_path (W_type.mk a f)) α (P.last.B a C) C) (a : P.A) (f : P.last.B a P.last.W) (f' : typevec.arrow (P.W_path (W_type.mk a f)) α) :
P.Wp_rec g (W_type.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), typevec.arrow (P.W_path x) α Prop} (ih : (a : P.A) (f : P.last.B a P.last.W) (f' : typevec.arrow (P.W_path (W_type.mk a f)) α), ( (i : P.last.B a), C (f i) (P.W_path_dest_right f' i)) C (W_type.mk a f) f') (x : P.last.W) (f' : typevec.arrow (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) (f' : (P.drop.B a).arrow α) (f : P.last.B a P.W α) :
P.W α

Constructor for W

Equations
def mvpfunctor.W_rec {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_1} (g : Π (a : P.A), (P.drop.B a).arrow α (P.last.B a P.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).arrow α (P.last.B a P.W α) (P.last.B a C) C) (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a P.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).arrow α) (f : P.last.B a P.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).arrow α) (f : P.last.B a P.W α), C (P.W_mk a f' f)) (x : P.W α) :
C x
def mvpfunctor.W_map {n : } (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α.arrow β) :
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).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :
P.W_mk a g' (λ (i : P.last.B a), f i, g i⟩) = W_type.mk a f, P.W_path_cases_on g' g
theorem mvpfunctor.W_map_W_mk {n : } (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α.arrow β) (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a P.W α) :
mvfunctor.map g (P.W_mk a f' f) = P.W_mk a (typevec.comp g f') (λ (i : P.last.B a), mvfunctor.map g (f i))
@[reducible]
def mvpfunctor.obj_append1 {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (a : P.A) (f' : (P.drop.B a).arrow α) (f : 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 : α.arrow γ) (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a P.W α) :
mvfunctor.map (g ::: P.W_map g) (P.obj_append1 a f' f) = P.obj_append1 a (typevec.comp 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).arrow α) (f : P.last.B a P.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