mathlibdocumentation

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 #

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

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
• = {default := mvpfunctor.W_path.inhabited._match_1 P x I}
• mvpfunctor.W_path.inhabited._match_1 P f) I =
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 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 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 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)) α) :
(P.W_path_cases_on g' g) = P.W_path_cases_on g') (λ (i : P.last.B a), (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) :
Type u

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 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 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 f)) α(P.last.B a → C) → C) (a : P.A) (f : P.last.B a → P.last.W) (f' : typevec.arrow (P.W_path f)) α) :
P.Wp_rec g 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 f)) α), (∀ (i : P.last.B a), C (f i) (P.W_path_dest_right f' i))C 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

• 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.W_mk {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f' : (P.drop.B a).arrow α) (f : 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} (g : Π (a : P.A), (P.drop.B a).arrow α(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).arrow α(P.last.B aP.W α)(P.last.B a → C) → C) (a : P.A) (f' : (P.drop.B a).arrow α) (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).arrow α) (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).arrow α) (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} (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⟩) = 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 aP.W α) :
(P.W_mk a f' f) = P.W_mk a f') (λ (i : P.last.B a), (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 aP.W α) :
mvfunctor.map (g ::: P.W_map g) (P.obj_append1 a f' f) = P.obj_append1 a 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 aP.W α) :
P.W_dest' (P.W_mk a f' f) = a,
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